author | wenzelm |
Tue, 18 May 2021 20:19:02 +0200 | |
changeset 73733 | b13b2c1d419e |
parent 73724 | 5a3a2a52648d |
child 73741 | 941915a3b811 |
permissions | -rw-r--r-- |
61656 | 1 |
(*:maxLineLen=78:*) |
61575 | 2 |
|
28221 | 3 |
theory Presentation |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42009
diff
changeset
|
4 |
imports Base |
28221 | 5 |
begin |
6 |
||
58618 | 7 |
chapter \<open>Presenting theories \label{ch:present}\<close> |
28221 | 8 |
|
61575 | 9 |
text \<open> |
10 |
Isabelle provides several ways to present the outcome of formal |
|
11 |
developments, including WWW-based browsable libraries or actual printable |
|
12 |
documents. Presentation is centered around the concept of \<^emph>\<open>sessions\<close> |
|
13 |
(\chref{ch:session}). The global session structure is that of a tree, with |
|
14 |
Isabelle Pure at its root, further object-logics derived (e.g.\ HOLCF from |
|
15 |
HOL, and HOL from Pure), and application sessions further on in the |
|
16 |
hierarchy. |
|
28221 | 17 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
18 |
The command-line tools @{tool_ref mkroot} and @{tool_ref build} provide the |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
19 |
primary means for managing Isabelle sessions, including options for |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
20 |
presentation: ``\<^verbatim>\<open>document=pdf\<close>'' generates PDF output from the theory |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
21 |
session, and ``\<^verbatim>\<open>document_output=dir\<close>'' emits a copy of the document sources |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
22 |
with the PDF into the given directory (relative to the session directory). |
28221 | 23 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
24 |
Alternatively, @{tool_ref document} may be used to turn the generated |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
25 |
{\LaTeX} sources of a session (exports from its build database) into PDF, |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
26 |
using suitable invocations of @{tool_ref latex}. |
58618 | 27 |
\<close> |
28221 | 28 |
|
29 |
||
62013 | 30 |
section \<open>Generating HTML browser information \label{sec:info}\<close> |
28221 | 31 |
|
58618 | 32 |
text \<open> |
61575 | 33 |
As a side-effect of building sessions, Isabelle is able to generate theory |
34 |
browsing information, including HTML documents that show the theory sources |
|
35 |
and the relationship with its ancestors and descendants. Besides the HTML |
|
36 |
file that is generated for every theory, Isabelle stores links to all |
|
37 |
theories of a session in an index file. As a second hierarchy, groups of |
|
38 |
sessions are organized as \<^emph>\<open>chapters\<close>, with a separate index. Note that the |
|
39 |
implicit tree structure of the session build hierarchy is \<^emph>\<open>not\<close> relevant |
|
51417 | 40 |
for the presentation. |
28221 | 41 |
|
61406 | 42 |
\<^medskip> |
62013 | 43 |
To generate theory browsing information for an existing session, just invoke |
44 |
@{tool build} with suitable options: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
45 |
@{verbatim [display] \<open>isabelle build -o browser_info -v -c FOL\<close>} |
28221 | 46 |
|
61575 | 47 |
The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as |
48 |
reported by the above verbose invocation of the build process. |
|
28221 | 49 |
|
67219 | 50 |
Many Isabelle sessions (such as \<^session>\<open>HOL-Library\<close> in |
51 |
\<^dir>\<open>~~/src/HOL/Library\<close>) also provide printable documents in PDF. These are |
|
52 |
prepared automatically as well if enabled like this: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
53 |
@{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>} |
48814
d488a5f25bf6
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents:
48722
diff
changeset
|
54 |
|
61575 | 55 |
Enabling both browser info and document preparation simultaneously causes an |
56 |
appropriate ``document'' link to be included in the HTML index. Documents |
|
57 |
may be generated independently of browser information as well, see |
|
58 |
\secref{sec:tool-document} for further details. |
|
28221 | 59 |
|
61406 | 60 |
\<^bigskip> |
61575 | 61 |
The theory browsing information is stored in a sub-directory directory |
62 |
determined by the @{setting_ref ISABELLE_BROWSER_INFO} setting plus a prefix |
|
63 |
corresponding to the session chapter and identifier. In order to present |
|
64 |
Isabelle applications on the web, the corresponding subdirectory from |
|
65 |
@{setting ISABELLE_BROWSER_INFO} can be put on a WWW server. |
|
66 |
\<close> |
|
28221 | 67 |
|
61406 | 68 |
|
58618 | 69 |
section \<open>Preparing session root directories \label{sec:tool-mkroot}\<close> |
28221 | 70 |
|
61575 | 71 |
text \<open> |
72 |
The @{tool_def mkroot} tool configures a given directory as session root, |
|
73 |
with some \<^verbatim>\<open>ROOT\<close> file and optional document source directory. Its usage is: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
74 |
@{verbatim [display] |
67043 | 75 |
\<open>Usage: isabelle mkroot [OPTIONS] [DIRECTORY] |
28221 | 76 |
|
77 |
Options are: |
|
67043 | 78 |
-A LATEX provide author in LaTeX notation (default: user name) |
67069
f11486d31586
init Mercurial repository for the generated session files;
wenzelm
parents:
67043
diff
changeset
|
79 |
-I init Mercurial repository and add generated files |
67043 | 80 |
-T LATEX provide title in LaTeX notation (default: session name) |
81 |
-n NAME alternative session name (default: directory base name) |
|
28221 | 82 |
|
67043 | 83 |
Prepare session root directory (default: current directory). |
84 |
\<close>} |
|
28221 | 85 |
|
61575 | 86 |
The results are placed in the given directory \<open>dir\<close>, which refers to the |
87 |
current directory by default. The @{tool mkroot} tool is conservative in the |
|
88 |
sense that it does not overwrite existing files or directories. Earlier |
|
89 |
attempts to generate a session root need to be deleted manually. |
|
28221 | 90 |
|
67042
677cab7c2b85
adapted to changed ROOT syntax (see 13857f49d215);
wenzelm
parents:
63680
diff
changeset
|
91 |
The generated session template will be accompanied by a formal document, |
67043 | 92 |
with \<open>DIRECTORY\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see also |
67042
677cab7c2b85
adapted to changed ROOT syntax (see 13857f49d215);
wenzelm
parents:
63680
diff
changeset
|
93 |
\chref{ch:present}). |
28221 | 94 |
|
67043 | 95 |
Options \<^verbatim>\<open>-T\<close> and \<^verbatim>\<open>-A\<close> specify the document title and author explicitly, |
96 |
using {\LaTeX} source notation. |
|
97 |
||
67069
f11486d31586
init Mercurial repository for the generated session files;
wenzelm
parents:
67043
diff
changeset
|
98 |
Option \<^verbatim>\<open>-I\<close> initializes a Mercurial repository in the target directory, and |
f11486d31586
init Mercurial repository for the generated session files;
wenzelm
parents:
67043
diff
changeset
|
99 |
adds all generated files (without commit). |
f11486d31586
init Mercurial repository for the generated session files;
wenzelm
parents:
67043
diff
changeset
|
100 |
|
67043 | 101 |
Option \<^verbatim>\<open>-n\<close> specifies an alternative session name; otherwise the base name |
102 |
of the given directory is used. |
|
28221 | 103 |
|
61406 | 104 |
\<^medskip> |
61575 | 105 |
The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} specifies |
67043 | 106 |
the parent session. |
61503 | 107 |
\<close> |
28221 | 108 |
|
109 |
||
58618 | 110 |
subsubsection \<open>Examples\<close> |
28221 | 111 |
|
61575 | 112 |
text \<open> |
67042
677cab7c2b85
adapted to changed ROOT syntax (see 13857f49d215);
wenzelm
parents:
63680
diff
changeset
|
113 |
Produce session \<^verbatim>\<open>Test\<close> within a separate directory of the same name: |
677cab7c2b85
adapted to changed ROOT syntax (see 13857f49d215);
wenzelm
parents:
63680
diff
changeset
|
114 |
@{verbatim [display] \<open>isabelle mkroot Test && isabelle build -D Test\<close>} |
28221 | 115 |
|
61406 | 116 |
\<^medskip> |
61575 | 117 |
Upgrade the current directory into a session ROOT with document preparation, |
118 |
and build it: |
|
67042
677cab7c2b85
adapted to changed ROOT syntax (see 13857f49d215);
wenzelm
parents:
63680
diff
changeset
|
119 |
@{verbatim [display] \<open>isabelle mkroot && isabelle build -D .\<close>} |
58618 | 120 |
\<close> |
28221 | 121 |
|
122 |
||
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
123 |
section \<open>Preparing Isabelle session documents \label{sec:tool-document}\<close> |
28221 | 124 |
|
61575 | 125 |
text \<open> |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
126 |
The @{tool_def document} tool prepares logic session documents. Its usage |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
127 |
is: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
128 |
@{verbatim [display] |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
129 |
\<open>Usage: isabelle document [OPTIONS] SESSION |
28221 | 130 |
|
131 |
Options are: |
|
72675 | 132 |
-O DIR output directory for LaTeX sources and resulting PDF |
133 |
-P DIR output directory for resulting PDF |
|
134 |
-S DIR output directory for LaTeX sources |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
135 |
-V verbose latex |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
136 |
-d DIR include session directory |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
137 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
138 |
-v verbose build |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
139 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
140 |
Prepare the theory document of a session.\<close>} |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67151
diff
changeset
|
141 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
142 |
Generated {\LaTeX} sources are taken from the session build database: |
72650
787ba1d19d3a
more robust: ensure coherence wrt. build database;
wenzelm
parents:
72648
diff
changeset
|
143 |
@{tool_ref build} is invoked beforehand to ensure that it is up-to-date. |
787ba1d19d3a
more robust: ensure coherence wrt. build database;
wenzelm
parents:
72648
diff
changeset
|
144 |
Further files are generated on the spot, notably essential Isabelle style |
787ba1d19d3a
more robust: ensure coherence wrt. build database;
wenzelm
parents:
72648
diff
changeset
|
145 |
files, and \<^verbatim>\<open>session.tex\<close> to input all theory sources from the session |
787ba1d19d3a
more robust: ensure coherence wrt. build database;
wenzelm
parents:
72648
diff
changeset
|
146 |
(excluding imports from other sessions). |
28221 | 147 |
|
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72650
diff
changeset
|
148 |
\<^medskip> Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-v\<close> have the same meaning as for @{tool |
72648 | 149 |
build}. |
28221 | 150 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
151 |
\<^medskip> Option \<^verbatim>\<open>-V\<close> prints full output of {\LaTeX} tools. |
28221 | 152 |
|
72675 | 153 |
\<^medskip> Option \<^verbatim>\<open>-O\<close>~\<open>dir\<close> specifies the output directory for generated {\LaTeX} |
154 |
sources and the result PDF file. Options \<^verbatim>\<open>-P\<close> and \<^verbatim>\<open>-S\<close> only refer to the |
|
155 |
PDF and sources, respectively. |
|
28221 | 156 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
157 |
For example, for output directory ``\<^verbatim>\<open>output\<close>'' and the default document |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
158 |
variant ``\<^verbatim>\<open>document\<close>'', the generated document sources are placed into the |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
159 |
subdirectory \<^verbatim>\<open>output/document/\<close> and the resulting PDF into |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
160 |
\<^verbatim>\<open>output/document.pdf\<close>. |
28221 | 161 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
162 |
\<^medskip> Isabelle is usually smart enough to create the PDF from the given |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
163 |
\<^verbatim>\<open>root.tex\<close> and optional \<^verbatim>\<open>root.bib\<close> (bibliography) and \<^verbatim>\<open>root.idx\<close> (index) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
164 |
using standard {\LaTeX} tools. Alternatively, \isakeyword{document\_files} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
165 |
in the session \<^verbatim>\<open>ROOT\<close> may include an executable \<^verbatim>\<open>build\<close> script to take |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
166 |
care of that. It is invoked with command-line arguments for the document |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
167 |
format (\<^verbatim>\<open>pdf\<close>) and the document variant name. The script needs to produce |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
168 |
corresponding output files, e.g.\ \<^verbatim>\<open>root.pdf\<close> for default document variants |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
169 |
(the main work can be delegated to @{tool latex}). \<close> |
28221 | 170 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
171 |
subsubsection \<open>Examples\<close> |
28221 | 172 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
173 |
text \<open> |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
174 |
Produce the document from session \<^verbatim>\<open>FOL\<close> with full verbosity, and a copy in |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
175 |
the current directory (subdirectory \<^verbatim>\<open>document\<close> and file \<^verbatim>\<open>document.pdf)\<close>: |
48814
d488a5f25bf6
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents:
48722
diff
changeset
|
176 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
177 |
@{verbatim [display] \<open>isabelle document -v -V -O. FOL\<close>} |
58618 | 178 |
\<close> |
28221 | 179 |
|
180 |
||
58618 | 181 |
section \<open>Running {\LaTeX} within the Isabelle environment |
182 |
\label{sec:tool-latex}\<close> |
|
28221 | 183 |
|
61575 | 184 |
text \<open> |
185 |
The @{tool_def latex} tool provides the basic interface for Isabelle |
|
186 |
document preparation. Its usage is: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
187 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
188 |
\<open>Usage: isabelle latex [OPTIONS] [FILE] |
28221 | 189 |
|
190 |
Options are: |
|
73724 | 191 |
-o FORMAT specify output format: pdf (default), bbl, idx |
28221 | 192 |
|
193 |
Run LaTeX (and related tools) on FILE (default root.tex), |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
194 |
producing the specified output format.\<close>} |
28221 | 195 |
|
61575 | 196 |
Appropriate {\LaTeX}-related programs are run on the input file, according |
72309
564012e31db1
discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents:
67399
diff
changeset
|
197 |
to the given output format: @{executable pdflatex}, @{executable bibtex} |
564012e31db1
discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents:
67399
diff
changeset
|
198 |
(for \<^verbatim>\<open>bbl\<close>), and @{executable makeindex} (for \<^verbatim>\<open>idx\<close>). The actual commands |
564012e31db1
discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents:
67399
diff
changeset
|
199 |
are determined from the settings environment (@{setting ISABELLE_PDFLATEX} |
564012e31db1
discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents:
67399
diff
changeset
|
200 |
etc.). |
58618 | 201 |
\<close> |
28221 | 202 |
|
203 |
||
58618 | 204 |
subsubsection \<open>Examples\<close> |
28221 | 205 |
|
61575 | 206 |
text \<open> |
207 |
Invoking @{tool latex} by hand may be occasionally useful when debugging |
|
208 |
failed attempts of the automatic document preparation stage of batch-mode |
|
209 |
Isabelle. The abortive process leaves the sources at a certain place within |
|
210 |
@{setting ISABELLE_BROWSER_INFO}, see the runtime error message for details. |
|
211 |
This enables users to inspect {\LaTeX} runs in further detail, e.g.\ like |
|
212 |
this: |
|
48602 | 213 |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
214 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
215 |
\<open>cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document" |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
216 |
isabelle latex -o pdf\<close>} |
58618 | 217 |
\<close> |
28221 | 218 |
|
67399 | 219 |
end |