author | wenzelm |
Fri, 03 Dec 2021 15:11:16 +0100 | |
changeset 74873 | 0ab2ed1489eb |
parent 73826 | 72900f34dbb3 |
child 75161 | 95612f330c93 |
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 |
73741 | 25 |
{\LaTeX} sources of a session (exports from its build database) into PDF. |
58618 | 26 |
\<close> |
28221 | 27 |
|
28 |
||
62013 | 29 |
section \<open>Generating HTML browser information \label{sec:info}\<close> |
28221 | 30 |
|
58618 | 31 |
text \<open> |
61575 | 32 |
As a side-effect of building sessions, Isabelle is able to generate theory |
33 |
browsing information, including HTML documents that show the theory sources |
|
34 |
and the relationship with its ancestors and descendants. Besides the HTML |
|
35 |
file that is generated for every theory, Isabelle stores links to all |
|
36 |
theories of a session in an index file. As a second hierarchy, groups of |
|
37 |
sessions are organized as \<^emph>\<open>chapters\<close>, with a separate index. Note that the |
|
38 |
implicit tree structure of the session build hierarchy is \<^emph>\<open>not\<close> relevant |
|
51417 | 39 |
for the presentation. |
28221 | 40 |
|
61406 | 41 |
\<^medskip> |
62013 | 42 |
To generate theory browsing information for an existing session, just invoke |
43 |
@{tool build} with suitable options: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
44 |
@{verbatim [display] \<open>isabelle build -o browser_info -v -c FOL\<close>} |
28221 | 45 |
|
61575 | 46 |
The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as |
47 |
reported by the above verbose invocation of the build process. |
|
28221 | 48 |
|
67219 | 49 |
Many Isabelle sessions (such as \<^session>\<open>HOL-Library\<close> in |
73826
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73741
diff
changeset
|
50 |
\<^dir>\<open>~~/src/HOL/Library\<close>) also provide theory documents in PDF. These are |
67219 | 51 |
prepared automatically as well if enabled like this: |
73826
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73741
diff
changeset
|
52 |
@{verbatim [display] \<open>isabelle build -o browser_info -o document -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
|
53 |
|
61575 | 54 |
Enabling both browser info and document preparation simultaneously causes an |
55 |
appropriate ``document'' link to be included in the HTML index. Documents |
|
56 |
may be generated independently of browser information as well, see |
|
57 |
\secref{sec:tool-document} for further details. |
|
28221 | 58 |
|
61406 | 59 |
\<^bigskip> |
61575 | 60 |
The theory browsing information is stored in a sub-directory directory |
61 |
determined by the @{setting_ref ISABELLE_BROWSER_INFO} setting plus a prefix |
|
62 |
corresponding to the session chapter and identifier. In order to present |
|
63 |
Isabelle applications on the web, the corresponding subdirectory from |
|
64 |
@{setting ISABELLE_BROWSER_INFO} can be put on a WWW server. |
|
65 |
\<close> |
|
28221 | 66 |
|
61406 | 67 |
|
58618 | 68 |
section \<open>Preparing session root directories \label{sec:tool-mkroot}\<close> |
28221 | 69 |
|
61575 | 70 |
text \<open> |
71 |
The @{tool_def mkroot} tool configures a given directory as session root, |
|
72 |
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
|
73 |
@{verbatim [display] |
67043 | 74 |
\<open>Usage: isabelle mkroot [OPTIONS] [DIRECTORY] |
28221 | 75 |
|
76 |
Options are: |
|
67043 | 77 |
-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
|
78 |
-I init Mercurial repository and add generated files |
67043 | 79 |
-T LATEX provide title in LaTeX notation (default: session name) |
80 |
-n NAME alternative session name (default: directory base name) |
|
28221 | 81 |
|
67043 | 82 |
Prepare session root directory (default: current directory). |
83 |
\<close>} |
|
28221 | 84 |
|
61575 | 85 |
The results are placed in the given directory \<open>dir\<close>, which refers to the |
86 |
current directory by default. The @{tool mkroot} tool is conservative in the |
|
87 |
sense that it does not overwrite existing files or directories. Earlier |
|
88 |
attempts to generate a session root need to be deleted manually. |
|
28221 | 89 |
|
67042
677cab7c2b85
adapted to changed ROOT syntax (see 13857f49d215);
wenzelm
parents:
63680
diff
changeset
|
90 |
The generated session template will be accompanied by a formal document, |
67043 | 91 |
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
|
92 |
\chref{ch:present}). |
28221 | 93 |
|
67043 | 94 |
Options \<^verbatim>\<open>-T\<close> and \<^verbatim>\<open>-A\<close> specify the document title and author explicitly, |
95 |
using {\LaTeX} source notation. |
|
96 |
||
67069
f11486d31586
init Mercurial repository for the generated session files;
wenzelm
parents:
67043
diff
changeset
|
97 |
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
|
98 |
adds all generated files (without commit). |
f11486d31586
init Mercurial repository for the generated session files;
wenzelm
parents:
67043
diff
changeset
|
99 |
|
67043 | 100 |
Option \<^verbatim>\<open>-n\<close> specifies an alternative session name; otherwise the base name |
101 |
of the given directory is used. |
|
28221 | 102 |
|
61406 | 103 |
\<^medskip> |
61575 | 104 |
The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} specifies |
67043 | 105 |
the parent session. |
61503 | 106 |
\<close> |
28221 | 107 |
|
108 |
||
58618 | 109 |
subsubsection \<open>Examples\<close> |
28221 | 110 |
|
61575 | 111 |
text \<open> |
67042
677cab7c2b85
adapted to changed ROOT syntax (see 13857f49d215);
wenzelm
parents:
63680
diff
changeset
|
112 |
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
|
113 |
@{verbatim [display] \<open>isabelle mkroot Test && isabelle build -D Test\<close>} |
28221 | 114 |
|
61406 | 115 |
\<^medskip> |
61575 | 116 |
Upgrade the current directory into a session ROOT with document preparation, |
117 |
and build it: |
|
67042
677cab7c2b85
adapted to changed ROOT syntax (see 13857f49d215);
wenzelm
parents:
63680
diff
changeset
|
118 |
@{verbatim [display] \<open>isabelle mkroot && isabelle build -D .\<close>} |
58618 | 119 |
\<close> |
28221 | 120 |
|
121 |
||
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
122 |
section \<open>Preparing Isabelle session documents \label{sec:tool-document}\<close> |
28221 | 123 |
|
61575 | 124 |
text \<open> |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
125 |
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
|
126 |
is: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
127 |
@{verbatim [display] |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
128 |
\<open>Usage: isabelle document [OPTIONS] SESSION |
28221 | 129 |
|
130 |
Options are: |
|
72675 | 131 |
-O DIR output directory for LaTeX sources and resulting PDF |
132 |
-P DIR output directory for resulting PDF |
|
133 |
-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
|
134 |
-V verbose latex |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
135 |
-d DIR include session directory |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
136 |
-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
|
137 |
-v verbose build |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
138 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
139 |
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
|
140 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
141 |
Generated {\LaTeX} sources are taken from the session build database: |
72650
787ba1d19d3a
more robust: ensure coherence wrt. build database;
wenzelm
parents:
72648
diff
changeset
|
142 |
@{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
|
143 |
Further files are generated on the spot, notably essential Isabelle style |
787ba1d19d3a
more robust: ensure coherence wrt. build database;
wenzelm
parents:
72648
diff
changeset
|
144 |
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
|
145 |
(excluding imports from other sessions). |
28221 | 146 |
|
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72650
diff
changeset
|
147 |
\<^medskip> Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-v\<close> have the same meaning as for @{tool |
72648 | 148 |
build}. |
28221 | 149 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
150 |
\<^medskip> Option \<^verbatim>\<open>-V\<close> prints full output of {\LaTeX} tools. |
28221 | 151 |
|
72675 | 152 |
\<^medskip> Option \<^verbatim>\<open>-O\<close>~\<open>dir\<close> specifies the output directory for generated {\LaTeX} |
153 |
sources and the result PDF file. Options \<^verbatim>\<open>-P\<close> and \<^verbatim>\<open>-S\<close> only refer to the |
|
154 |
PDF and sources, respectively. |
|
28221 | 155 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
156 |
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
|
157 |
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
|
158 |
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
|
159 |
\<^verbatim>\<open>output/document.pdf\<close>. |
28221 | 160 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
161 |
\<^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
|
162 |
\<^verbatim>\<open>root.tex\<close> and optional \<^verbatim>\<open>root.bib\<close> (bibliography) and \<^verbatim>\<open>root.idx\<close> (index) |
73741 | 163 |
using standard {\LaTeX} tools. Actual command-lines are given by settings |
74873 | 164 |
@{setting_ref ISABELLE_LUALATEX} (or @{setting_ref ISABELLE_PDFLATEX}), |
73741 | 165 |
@{setting_ref ISABELLE_BIBTEX}, @{setting_ref ISABELLE_MAKEINDEX}: these |
166 |
variables are used without quoting in shell scripts, and thus may contain |
|
167 |
additional options. |
|
168 |
||
74873 | 169 |
The system option @{system_option_def "document_build"} specifies an |
170 |
alternative build engine, e.g. within the session \<^verbatim>\<open>ROOT\<close> file as |
|
171 |
``\<^verbatim>\<open>options [document_build = pdflatex]\<close>''. The following standard engines |
|
172 |
are available: |
|
173 |
||
174 |
\<^item> \<^verbatim>\<open>lualatex\<close> (default) uses the shell command \<^verbatim>\<open>$ISABELLE_LUALATEX\<close> on |
|
175 |
the main \<^verbatim>\<open>root.tex\<close> file, with further runs of \<^verbatim>\<open>$ISABELLE_BIBTEX\<close> and |
|
176 |
\<^verbatim>\<open>$ISABELLE_MAKEINDEX\<close> as required. |
|
177 |
||
178 |
\<^item> \<^verbatim>\<open>pdflatex\<close> uses \<^verbatim>\<open>$ISABELLE_PDFLATEX\<close> instead of \<^verbatim>\<open>$ISABELLE_LUALATEX\<close>, |
|
179 |
and the other tools as above. |
|
180 |
||
181 |
\<^item> \<^verbatim>\<open>build\<close> invokes an executable script of the same name in a private |
|
182 |
directory containing all \isakeyword{document\_files} and other generated |
|
183 |
document sources. The script is invoked as ``\<^verbatim>\<open>./build pdf\<close>~\<open>name\<close>'' for |
|
184 |
the document variant name; it needs to produce a corresponding |
|
185 |
\<open>name\<close>\<^verbatim>\<open>.pdf\<close> file by arbitrary means on its own. |
|
186 |
||
187 |
Further engines can be defined by add-on components in Isabelle/Scala |
|
188 |
(\secref{sec:scala-build}), providing a service class derived from |
|
189 |
\<^scala_type>\<open>isabelle.Document_Build.Engine\<close>. Available classes are listed |
|
190 |
in \<^scala>\<open>isabelle.Document_Build.engines\<close>. |
|
73741 | 191 |
\<close> |
192 |
||
28221 | 193 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
194 |
subsubsection \<open>Examples\<close> |
28221 | 195 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
196 |
text \<open> |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
197 |
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
|
198 |
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
|
199 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
200 |
@{verbatim [display] \<open>isabelle document -v -V -O. FOL\<close>} |
58618 | 201 |
\<close> |
28221 | 202 |
|
67399 | 203 |
end |