author | wenzelm |
Wed, 13 Mar 2013 15:12:14 +0100 | |
changeset 51417 | d266f9329368 |
parent 51054 | d6de6e81574d |
child 52744 | 49825ba687ce |
permissions | -rw-r--r-- |
28221 | 1 |
theory Presentation |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42009
diff
changeset
|
2 |
imports Base |
28221 | 3 |
begin |
4 |
||
5 |
chapter {* Presenting theories \label{ch:present} *} |
|
6 |
||
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
|
7 |
text {* Isabelle provides several ways to present the outcome of |
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
|
8 |
formal developments, including WWW-based browsable libraries or |
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
|
9 |
actual printable documents. Presentation is centered around the |
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
|
10 |
concept of \emph{sessions} (\chref{ch:session}). The global session |
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
|
11 |
structure is that of a tree, with Isabelle Pure at its root, further |
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
|
12 |
object-logics derived (e.g.\ HOLCF from HOL, and HOL from Pure), and |
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
|
13 |
application sessions further on in the hierarchy. |
28221 | 14 |
|
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
|
15 |
The tools @{tool_ref mkroot} and @{tool_ref build} provide the |
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
|
16 |
primary means for managing Isabelle sessions, including proper setup |
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
|
17 |
for presentation; @{tool build} takes care to have @{executable_ref |
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
|
18 |
"isabelle-process"} run any additional stages required for document |
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
|
19 |
preparation, notably the @{tool_ref document} and @{tool_ref latex}. |
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
|
20 |
The complete tool chain for managing batch-mode Isabelle sessions is |
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
|
21 |
illustrated in \figref{fig:session-tools}. |
28221 | 22 |
|
23 |
\begin{figure}[htbp] |
|
24 |
\begin{center} |
|
25 |
\begin{tabular}{lp{0.6\textwidth}} |
|
26 |
||
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
|
27 |
@{tool_ref mkroot} & invoked once by the user to initialize the |
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
|
28 |
session @{verbatim ROOT} with optional @{verbatim document} |
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
|
29 |
directory; \\ |
28221 | 30 |
|
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
|
31 |
@{tool_ref build} & invoked repeatedly by the user to keep |
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
|
32 |
session output up-to-date (HTML, documents etc.); \\ |
28221 | 33 |
|
48602 | 34 |
@{executable "isabelle-process"} & run through @{tool_ref |
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
|
35 |
build}; \\ |
28221 | 36 |
|
48602 | 37 |
@{tool_ref document} & run by the Isabelle process if document |
38 |
preparation is enabled; \\ |
|
28221 | 39 |
|
48602 | 40 |
@{tool_ref latex} & universal {\LaTeX} tool wrapper invoked |
41 |
multiple times by @{tool_ref document}; also useful for manual |
|
42 |
experiments; \\ |
|
28221 | 43 |
|
44 |
\end{tabular} |
|
45 |
\caption{The tool chain of Isabelle session presentation} \label{fig:session-tools} |
|
46 |
\end{center} |
|
47 |
\end{figure} |
|
48 |
*} |
|
49 |
||
50 |
||
51 |
section {* Generating theory browser information \label{sec:info} *} |
|
52 |
||
53 |
text {* |
|
54 |
\index{theory browsing information|bold} |
|
55 |
||
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
|
56 |
As a side-effect of building sessions, Isabelle is able to generate |
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
|
57 |
theory browsing information, including HTML documents that show the |
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
|
58 |
theory sources and the relationship with its ancestors and |
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
|
59 |
descendants. Besides the HTML file that is generated for every |
51417 | 60 |
theory, Isabelle stores links to all theories of a session in an |
61 |
index file. As a second hierarchy, groups of sessions are organized |
|
62 |
as \emph{chapters}, with a separate index. Note that the implicit |
|
63 |
tree structure of the session build hierarchy is \emph{not} relevant |
|
64 |
for the presentation. |
|
28221 | 65 |
|
66 |
Isabelle also generates graph files that represent the theory |
|
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
|
67 |
dependencies within a session. There is a graph browser Java applet |
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
|
68 |
embedded in the generated HTML pages, and also a stand-alone |
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
|
69 |
application that allows browsing theory graphs without having to |
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
|
70 |
start a WWW client first. The latter version also includes features |
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
|
71 |
such as generating Postscript files, which are not available in the |
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
|
72 |
applet version. See \secref{sec:browse} for further information. |
28221 | 73 |
|
74 |
\medskip |
|
75 |
||
76 |
The easiest way to let Isabelle generate theory browsing information |
|
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
|
77 |
for existing sessions is to invoke @{tool build} with suitable |
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
|
78 |
options: |
28221 | 79 |
|
80 |
\begin{ttbox} |
|
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
|
81 |
isabelle build -o browser_info -v -c FOL |
28221 | 82 |
\end{ttbox} |
83 |
||
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
|
84 |
The presentation output will appear in @{verbatim |
51417 | 85 |
"$ISABELLE_BROWSER_INFO/FOL/FOL"} as reported by the above verbose |
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
|
86 |
invocation of the build process. |
28221 | 87 |
|
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
|
88 |
Many Isabelle sessions (such as @{verbatim "HOL-Library"} in @{file |
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
|
89 |
"~~/src/HOL/Library"}) also provide actual printable documents. |
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
|
90 |
These are prepared automatically as well if enabled like this: |
28221 | 91 |
\begin{ttbox} |
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
|
92 |
isabelle build -o browser_info -o document=pdf -v -c HOL-Library |
28221 | 93 |
\end{ttbox} |
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
|
94 |
|
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
|
95 |
Enabling both browser info and document preparation simultaneously |
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
|
96 |
causes an appropriate ``document'' link to be included in the HTML |
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
|
97 |
index. Documents may be generated independently of browser |
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
|
98 |
information as well, see \secref{sec:tool-document} for further |
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
|
99 |
details. |
28221 | 100 |
|
101 |
\bigskip The theory browsing information is stored in a |
|
102 |
sub-directory directory determined by the @{setting_ref |
|
103 |
ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the |
|
51417 | 104 |
session chapter and identifier. In order to present Isabelle |
105 |
applications on the web, the corresponding subdirectory from |
|
106 |
@{setting ISABELLE_BROWSER_INFO} can be put on a WWW server. *} |
|
28221 | 107 |
|
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
|
108 |
section {* Preparing session root directories \label{sec:tool-mkroot} *} |
28221 | 109 |
|
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
|
110 |
text {* The @{tool_def mkroot} tool configures a given directory as |
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
|
111 |
session root, with some @{verbatim ROOT} file and optional document |
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
|
112 |
source directory. Its usage is: |
28221 | 113 |
\begin{ttbox} |
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
|
114 |
Usage: isabelle mkroot [OPTIONS] [DIR] |
28221 | 115 |
|
116 |
Options are: |
|
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
|
117 |
-d enable document preparation |
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
|
118 |
-n NAME alternative session name (default: DIR base name) |
28221 | 119 |
|
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
|
120 |
Prepare session root DIR (default: current directory). |
28221 | 121 |
\end{ttbox} |
122 |
||
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
|
123 |
The results are placed in the given directory @{text dir}, which |
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
|
124 |
refers to the current directory by default. The @{tool mkroot} tool |
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
|
125 |
is conservative in the sense that it does not overwrite existing |
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
|
126 |
files or directories. Earlier attempts to generate a session root |
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
|
127 |
need to be deleted manually. |
28221 | 128 |
|
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
|
129 |
\medskip Option @{verbatim "-d"} indicates that the session shall be |
51054 | 130 |
accompanied by a formal document, with @{text DIR}@{verbatim |
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
|
131 |
"/document/root.tex"} as its {\LaTeX} entry point (see also |
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
|
132 |
\chref{ch:present}). |
28221 | 133 |
|
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
|
134 |
Option @{verbatim "-n"} allows to specify an alternative session |
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
|
135 |
name; otherwise the base name of the given directory is used. |
28221 | 136 |
|
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
|
137 |
\medskip The implicit Isabelle settings variable @{setting |
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
|
138 |
ISABELLE_LOGIC} specifies the parent session, and @{setting |
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
|
139 |
ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled |
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
|
140 |
into the generated @{verbatim ROOT} file. *} |
28221 | 141 |
|
142 |
||
143 |
subsubsection {* Examples *} |
|
144 |
||
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
|
145 |
text {* Produce session @{verbatim Test} (with document preparation) |
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
|
146 |
within a separate directory of the same name: |
28221 | 147 |
\begin{ttbox} |
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
|
148 |
isabelle mkroot -d Test && isabelle build -D Test |
28221 | 149 |
\end{ttbox} |
150 |
||
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
|
151 |
\medskip Upgrade the current directory into a session ROOT with |
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
|
152 |
document preparation, and build it: |
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
|
153 |
\begin{ttbox} |
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
|
154 |
isabelle mkroot -d && isabelle build -D . |
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
|
155 |
\end{ttbox} |
28221 | 156 |
*} |
157 |
||
158 |
||
159 |
section {* Preparing Isabelle session documents |
|
160 |
\label{sec:tool-document} *} |
|
161 |
||
48602 | 162 |
text {* The @{tool_def document} tool prepares logic session |
51054 | 163 |
documents, processing the sources as provided by the user and |
48602 | 164 |
generated by Isabelle. Its usage is: |
28221 | 165 |
\begin{ttbox} |
48602 | 166 |
Usage: isabelle document [OPTIONS] [DIR] |
28221 | 167 |
|
168 |
Options are: |
|
169 |
-c cleanup -- be aggressive in removing old stuff |
|
170 |
-n NAME specify document name (default 'document') |
|
171 |
-o FORMAT specify output format: dvi (default), dvi.gz, ps, |
|
172 |
ps.gz, pdf |
|
173 |
-t TAGS specify tagged region markup |
|
174 |
||
175 |
Prepare the theory session document in DIR (default 'document') |
|
176 |
producing the specified output format. |
|
177 |
\end{ttbox} |
|
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
|
178 |
This tool is usually run automatically as part of the Isabelle build |
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
|
179 |
process, provided document preparation has been enabled via suitable |
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
|
180 |
options. It may be manually invoked on the generated browser |
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
|
181 |
information document output as well, e.g.\ in case of errors |
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
|
182 |
encountered in the batch run. |
28221 | 183 |
|
48602 | 184 |
\medskip The @{verbatim "-c"} option tells @{tool document} to |
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
|
185 |
dispose the document sources after successful operation! This is |
28221 | 186 |
the right thing to do for sources generated by an Isabelle process, |
187 |
but take care of your files in manual document preparation! |
|
188 |
||
189 |
\medskip The @{verbatim "-n"} and @{verbatim "-o"} option specify |
|
190 |
the final output file name and format, the default is ``@{verbatim |
|
191 |
document.dvi}''. Note that the result will appear in the parent of |
|
192 |
the target @{verbatim DIR}. |
|
193 |
||
194 |
\medskip The @{verbatim "-t"} option tells {\LaTeX} how to interpret |
|
195 |
tagged Isabelle command regions. Tags are specified as a comma |
|
196 |
separated list of modifier/name pairs: ``@{verbatim "+"}@{text |
|
197 |
foo}'' (or just ``@{text foo}'') means to keep, ``@{verbatim |
|
198 |
"-"}@{text foo}'' to drop, and ``@{verbatim "/"}@{text foo}'' to |
|
199 |
fold text tagged as @{text foo}. The builtin default is equivalent |
|
200 |
to the tag specification ``@{verbatim |
|
30113
5ea17e90b08a
isabelle document: adapted (postulated) defaults for tags to actual isabelle.sty;
wenzelm
parents:
29435
diff
changeset
|
201 |
"+theory,+proof,+ML,+visible,-invisible"}''; see also the {\LaTeX} |
28221 | 202 |
macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and |
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40387
diff
changeset
|
203 |
@{verbatim "\\isafoldtag"}, in @{file |
28238 | 204 |
"~~/lib/texinputs/isabelle.sty"}. |
28221 | 205 |
|
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
|
206 |
\medskip Document preparation requires a @{verbatim document} |
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
|
207 |
directory within the session sources. This directory is supposed to |
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
|
208 |
contain all the files needed to produce the final document --- apart |
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
|
209 |
from the actual theories which are generated by Isabelle. |
28221 | 210 |
|
48602 | 211 |
\medskip For most practical purposes, @{tool document} is smart |
212 |
enough to create any of the specified output formats, taking |
|
28221 | 213 |
@{verbatim root.tex} supplied by the user as a starting point. This |
214 |
even includes multiple runs of {\LaTeX} to accommodate references |
|
215 |
and bibliographies (the latter assumes @{verbatim root.bib} within |
|
216 |
the same directory). |
|
217 |
||
48657
63ef2f0cf8bb
simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents:
48616
diff
changeset
|
218 |
In more complex situations, a separate @{verbatim build} script for |
63ef2f0cf8bb
simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents:
48616
diff
changeset
|
219 |
the document sources may be given. It is invoked with command-line |
63ef2f0cf8bb
simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents:
48616
diff
changeset
|
220 |
arguments for the document format and the document variant name. |
63ef2f0cf8bb
simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents:
48616
diff
changeset
|
221 |
The script needs to produce corresponding output files, e.g.\ |
63ef2f0cf8bb
simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents:
48616
diff
changeset
|
222 |
@{verbatim root.pdf} for target format @{verbatim pdf} (and default |
51054 | 223 |
variants). The main work can be again delegated to @{tool latex}, |
224 |
but it is also possible to harvest generated {\LaTeX} sources and |
|
225 |
copy them elsewhere. |
|
28221 | 226 |
|
42009
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
227 |
\medskip When running the session, Isabelle copies the content of |
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
228 |
the original @{verbatim document} directory into its proper place |
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
229 |
within @{setting ISABELLE_BROWSER_INFO}, according to the session |
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
230 |
path and document variant. Then, for any processed theory @{text A} |
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
231 |
some {\LaTeX} source is generated and put there as @{text |
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
232 |
A}@{verbatim ".tex"}. Furthermore, a list of all generated theory |
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
233 |
files is put into @{verbatim session.tex}. Typically, the root |
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
234 |
{\LaTeX} file provided by the user would include @{verbatim |
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
235 |
session.tex} to get a document containing all the theories. |
28221 | 236 |
|
237 |
The {\LaTeX} versions of the theories require some macros defined in |
|
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40387
diff
changeset
|
238 |
@{file "~~/lib/texinputs/isabelle.sty"}. Doing @{verbatim |
28238 | 239 |
"\\usepackage{isabelle}"} in @{verbatim root.tex} should be fine; |
48602 | 240 |
the underlying @{tool latex} already includes an appropriate path |
241 |
specification for {\TeX} inputs. |
|
28221 | 242 |
|
243 |
If the text contains any references to Isabelle symbols (such as |
|
244 |
@{verbatim "\\"}@{verbatim "<forall>"}) then @{verbatim |
|
28238 | 245 |
"isabellesym.sty"} should be included as well. This package |
246 |
contains a standard set of {\LaTeX} macro definitions @{verbatim |
|
28221 | 247 |
"\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28504
diff
changeset
|
248 |
"<"}@{text foo}@{verbatim ">"}, see \cite{isabelle-implementation} for a |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28504
diff
changeset
|
249 |
complete list of predefined Isabelle symbols. Users may invent |
28221 | 250 |
further symbols as well, just by providing {\LaTeX} macros in a |
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40387
diff
changeset
|
251 |
similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of |
51054 | 252 |
the Isabelle distribution. |
28221 | 253 |
|
254 |
For proper setup of DVI and PDF documents (with hyperlinks and |
|
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40387
diff
changeset
|
255 |
bookmarks), we recommend to include @{file |
28238 | 256 |
"~~/lib/texinputs/pdfsetup.sty"} as well. |
28221 | 257 |
|
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
|
258 |
\medskip As a final step of Isabelle document preparation, @{tool |
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
|
259 |
document}~@{verbatim "-c"} is run on the resulting copy of the |
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
|
260 |
@{verbatim document} directory. Thus the actual output document is |
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
|
261 |
built and installed in its proper place. The generated sources are |
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
|
262 |
deleted after successful run of {\LaTeX} and friends. |
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
|
263 |
|
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
|
264 |
Some care is needed if the document output location is configured |
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
|
265 |
differently, say within a directory whose content is still required |
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
|
266 |
afterwards! |
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
|
267 |
*} |
28221 | 268 |
|
269 |
||
270 |
section {* Running {\LaTeX} within the Isabelle environment |
|
271 |
\label{sec:tool-latex} *} |
|
272 |
||
48602 | 273 |
text {* The @{tool_def latex} tool provides the basic interface for |
28221 | 274 |
Isabelle document preparation. Its usage is: |
275 |
\begin{ttbox} |
|
48602 | 276 |
Usage: isabelle latex [OPTIONS] [FILE] |
28221 | 277 |
|
278 |
Options are: |
|
279 |
-o FORMAT specify output format: dvi (default), dvi.gz, ps, |
|
280 |
ps.gz, pdf, bbl, idx, sty, syms |
|
281 |
||
282 |
Run LaTeX (and related tools) on FILE (default root.tex), |
|
283 |
producing the specified output format. |
|
284 |
\end{ttbox} |
|
285 |
||
286 |
Appropriate {\LaTeX}-related programs are run on the input file, |
|
287 |
according to the given output format: @{executable latex}, |
|
288 |
@{executable pdflatex}, @{executable dvips}, @{executable bibtex} |
|
289 |
(for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim |
|
290 |
idx}). The actual commands are determined from the settings |
|
291 |
environment (@{setting ISABELLE_LATEX} etc.). |
|
292 |
||
293 |
The @{verbatim sty} output format causes the Isabelle style files to |
|
294 |
be updated from the distribution. This is useful in special |
|
295 |
situations where the document sources are to be processed another |
|
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
|
296 |
time by separate tools. |
28221 | 297 |
|
298 |
The @{verbatim syms} output is for internal use; it generates lists |
|
299 |
of symbols that are available without loading additional {\LaTeX} |
|
300 |
packages. |
|
301 |
*} |
|
302 |
||
303 |
||
304 |
subsubsection {* Examples *} |
|
305 |
||
48602 | 306 |
text {* Invoking @{tool latex} by hand may be occasionally useful when |
307 |
debugging failed attempts of the automatic document preparation |
|
308 |
stage of batch-mode Isabelle. The abortive process leaves the |
|
309 |
sources at a certain place within @{setting ISABELLE_BROWSER_INFO}, |
|
310 |
see the runtime error message for details. This enables users to |
|
311 |
inspect {\LaTeX} runs in further detail, e.g.\ like this: |
|
312 |
||
28221 | 313 |
\begin{ttbox} |
51417 | 314 |
cd ~/.isabelle/IsabelleXXXX/browser_info/Unsorted/Test/document |
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28238
diff
changeset
|
315 |
isabelle latex -o pdf |
28221 | 316 |
\end{ttbox} |
317 |
*} |
|
318 |
||
319 |
end |