author | wenzelm |
Mon, 25 Mar 2019 17:21:26 +0100 | |
changeset 69981 | 3dced198b9ec |
parent 68394 | bc2fd0e2047e |
child 71322 | 0256ce61f405 |
permissions | -rw-r--r-- |
61656 | 1 |
(*:maxLineLen=78:*) |
61575 | 2 |
|
28224 | 3 |
theory Misc |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
41512
diff
changeset
|
4 |
imports Base |
28224 | 5 |
begin |
6 |
||
58618 | 7 |
chapter \<open>Miscellaneous tools \label{ch:tools}\<close> |
28224 | 8 |
|
58618 | 9 |
text \<open> |
61575 | 10 |
Subsequently we describe various Isabelle related utilities, given in |
11 |
alphabetical order. |
|
58618 | 12 |
\<close> |
28224 | 13 |
|
14 |
||
58618 | 15 |
section \<open>Resolving Isabelle components \label{sec:tool-components}\<close> |
48844 | 16 |
|
58618 | 17 |
text \<open> |
48844 | 18 |
The @{tool_def components} tool resolves Isabelle components: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
19 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
20 |
\<open>Usage: isabelle components [OPTIONS] [COMPONENTS ...] |
48844 | 21 |
|
22 |
Options are: |
|
50653
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
50132
diff
changeset
|
23 |
-I init user settings |
48844 | 24 |
-R URL component repository |
25 |
(default $ISABELLE_COMPONENT_REPOSITORY) |
|
53435 | 26 |
-a resolve all missing components |
48844 | 27 |
-l list status |
28 |
||
29 |
Resolve Isabelle components via download and installation. |
|
30 |
COMPONENTS are identified via base name. |
|
31 |
||
68224 | 32 |
ISABELLE_COMPONENT_REPOSITORY="https://isabelle.in.tum.de/components"\<close>} |
48844 | 33 |
|
61575 | 34 |
Components are initialized as described in \secref{sec:components} in a |
35 |
permissive manner, which can mark components as ``missing''. This state is |
|
36 |
amended by letting @{tool "components"} download and unpack components that |
|
63680 | 37 |
are published on the default component repository |
68224 | 38 |
\<^url>\<open>https://isabelle.in.tum.de/components\<close> in particular. |
48844 | 39 |
|
61575 | 40 |
Option \<^verbatim>\<open>-R\<close> specifies an alternative component repository. Note that |
41 |
\<^verbatim>\<open>file:///\<close> URLs can be used for local directories. |
|
48844 | 42 |
|
61575 | 43 |
Option \<^verbatim>\<open>-a\<close> selects all missing components to be resolved. Explicit |
44 |
components may be named as command line-arguments as well. Note that |
|
45 |
components are uniquely identified by their base name, while the |
|
46 |
installation takes place in the location that was specified in the attempt |
|
47 |
to initialize the component before. |
|
48844 | 48 |
|
61575 | 49 |
Option \<^verbatim>\<open>-l\<close> lists the current state of available and missing components |
50 |
with their location (full name) within the file-system. |
|
50653
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
50132
diff
changeset
|
51 |
|
61575 | 52 |
Option \<^verbatim>\<open>-I\<close> initializes the user settings file to subscribe to the standard |
53 |
components specified in the Isabelle repository clone --- this does not make |
|
54 |
any sense for regular Isabelle releases. If the file already exists, it |
|
55 |
needs to be edited manually according to the printed explanation. |
|
58618 | 56 |
\<close> |
48844 | 57 |
|
58 |
||
58618 | 59 |
section \<open>Displaying documents \label{sec:tool-display}\<close> |
28224 | 60 |
|
61575 | 61 |
text \<open> |
62 |
The @{tool_def display} tool displays documents in DVI or PDF format: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
63 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
64 |
\<open>Usage: isabelle display DOCUMENT |
28224 | 65 |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
66 |
Display DOCUMENT (in DVI or PDF format).\<close>} |
28224 | 67 |
|
61406 | 68 |
\<^medskip> |
61575 | 69 |
The settings @{setting DVI_VIEWER} and @{setting PDF_VIEWER} determine the |
70 |
programs for viewing the corresponding file formats. Normally this opens the |
|
71 |
document via the desktop environment, potentially in an asynchronous manner |
|
72 |
with re-use of previews views. |
|
58618 | 73 |
\<close> |
28224 | 74 |
|
75 |
||
58618 | 76 |
section \<open>Viewing documentation \label{sec:tool-doc}\<close> |
28224 | 77 |
|
58618 | 78 |
text \<open> |
52444
2cfe6656d6d6
slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents:
52052
diff
changeset
|
79 |
The @{tool_def doc} tool displays Isabelle documentation: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
80 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
81 |
\<open>Usage: isabelle doc [DOC ...] |
28224 | 82 |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
83 |
View Isabelle documentation.\<close>} |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
84 |
|
61575 | 85 |
If called without arguments, it lists all available documents. Each line |
86 |
starts with an identifier, followed by a short description. Any of these |
|
87 |
identifiers may be specified as arguments, in order to display the |
|
88 |
corresponding document (see also \secref{sec:tool-display}). |
|
28224 | 89 |
|
61406 | 90 |
\<^medskip> |
61575 | 91 |
The @{setting ISABELLE_DOCS} setting specifies the list of directories |
92 |
(separated by colons) to be scanned for documentations. |
|
58618 | 93 |
\<close> |
28224 | 94 |
|
95 |
||
58618 | 96 |
section \<open>Shell commands within the settings environment \label{sec:tool-env}\<close> |
47828 | 97 |
|
61575 | 98 |
text \<open> |
99 |
The @{tool_def env} tool is a direct wrapper for the standard |
|
100 |
\<^verbatim>\<open>/usr/bin/env\<close> command on POSIX systems, running within the Isabelle |
|
101 |
settings environment (\secref{sec:settings}). |
|
47828 | 102 |
|
61575 | 103 |
The command-line arguments are that of the underlying version of \<^verbatim>\<open>env\<close>. For |
104 |
example, the following invokes an instance of the GNU Bash shell within the |
|
105 |
Isabelle environment: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
106 |
@{verbatim [display] \<open>isabelle env bash\<close>} |
58618 | 107 |
\<close> |
47828 | 108 |
|
109 |
||
58618 | 110 |
section \<open>Inspecting the settings environment \label{sec:tool-getenv}\<close> |
28224 | 111 |
|
58618 | 112 |
text \<open>The Isabelle settings environment --- as provided by the |
28224 | 113 |
site-default and user-specific settings files --- can be inspected |
48602 | 114 |
with the @{tool_def getenv} tool: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
115 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
116 |
\<open>Usage: isabelle getenv [OPTIONS] [VARNAMES ...] |
28224 | 117 |
|
118 |
Options are: |
|
119 |
-a display complete environment |
|
120 |
-b print values only (doesn't work for -a) |
|
31497 | 121 |
-d FILE dump complete environment to FILE |
122 |
(null terminated entries) |
|
28224 | 123 |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
124 |
Get value of VARNAMES from the Isabelle settings.\<close>} |
28224 | 125 |
|
61575 | 126 |
With the \<^verbatim>\<open>-a\<close> option, one may inspect the full process environment that |
127 |
Isabelle related programs are run in. This usually contains much more |
|
128 |
variables than are actually Isabelle settings. Normally, output is a list of |
|
129 |
lines of the form \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close>. The \<^verbatim>\<open>-b\<close> option causes only the values |
|
130 |
to be printed. |
|
31497 | 131 |
|
61575 | 132 |
Option \<^verbatim>\<open>-d\<close> produces a dump of the complete environment to the specified |
133 |
file. Entries are terminated by the ASCII null character, i.e.\ the C string |
|
134 |
terminator. |
|
58618 | 135 |
\<close> |
28224 | 136 |
|
137 |
||
58618 | 138 |
subsubsection \<open>Examples\<close> |
28224 | 139 |
|
61575 | 140 |
text \<open> |
141 |
Get the location of @{setting ISABELLE_HOME_USER} where user-specific |
|
142 |
information is stored: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
143 |
@{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>} |
28224 | 144 |
|
61406 | 145 |
\<^medskip> |
61575 | 146 |
Get the value only of the same settings variable, which is particularly |
147 |
useful in shell scripts: |
|
68219 | 148 |
@{verbatim [display] \<open>isabelle getenv -b ISABELLE_HOME_USER\<close>} |
58618 | 149 |
\<close> |
28224 | 150 |
|
151 |
||
58618 | 152 |
section \<open>Installing standalone Isabelle executables \label{sec:tool-install}\<close> |
28224 | 153 |
|
61575 | 154 |
text \<open> |
155 |
By default, the main Isabelle binaries (@{executable "isabelle"} etc.) are |
|
156 |
just run from their location within the distribution directory, probably |
|
157 |
indirectly by the shell through its @{setting PATH}. Other schemes of |
|
158 |
installation are supported by the @{tool_def install} tool: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
159 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
160 |
\<open>Usage: isabelle install [OPTIONS] BINDIR |
28224 | 161 |
|
162 |
Options are: |
|
50132 | 163 |
-d DISTDIR refer to DISTDIR as Isabelle distribution |
28224 | 164 |
(default ISABELLE_HOME) |
165 |
||
50132 | 166 |
Install Isabelle executables with absolute references to the |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
167 |
distribution directory.\<close>} |
28224 | 168 |
|
61575 | 169 |
The \<^verbatim>\<open>-d\<close> option overrides the current Isabelle distribution directory as |
170 |
determined by @{setting ISABELLE_HOME}. |
|
28224 | 171 |
|
61575 | 172 |
The \<open>BINDIR\<close> argument tells where executable wrapper scripts for |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62562
diff
changeset
|
173 |
@{executable "isabelle"} and @{executable isabelle_scala_script} should be |
61575 | 174 |
placed, which is typically a directory in the shell's @{setting PATH}, such |
175 |
as \<^verbatim>\<open>$HOME/bin\<close>. |
|
48815 | 176 |
|
61406 | 177 |
\<^medskip> |
61575 | 178 |
It is also possible to make symbolic links of the main Isabelle executables |
179 |
manually, but making separate copies outside the Isabelle distribution |
|
180 |
directory will not work! |
|
181 |
\<close> |
|
28224 | 182 |
|
183 |
||
58618 | 184 |
section \<open>Creating instances of the Isabelle logo\<close> |
28224 | 185 |
|
61575 | 186 |
text \<open> |
187 |
The @{tool_def logo} tool creates instances of the generic Isabelle logo as |
|
188 |
EPS and PDF, for inclusion in {\LaTeX} documents. |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
189 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
190 |
\<open>Usage: isabelle logo [OPTIONS] XYZ |
28224 | 191 |
|
49072
747835eb2782
"isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents:
48985
diff
changeset
|
192 |
Create instance XYZ of the Isabelle logo (as EPS and PDF). |
28224 | 193 |
|
194 |
Options are: |
|
49072
747835eb2782
"isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents:
48985
diff
changeset
|
195 |
-n NAME alternative output base name (default "isabelle_xyx") |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
196 |
-q quiet mode\<close>} |
48936 | 197 |
|
61575 | 198 |
Option \<^verbatim>\<open>-n\<close> specifies an alternative (base) name for the generated files. |
199 |
The default is \<^verbatim>\<open>isabelle_\<close>\<open>xyz\<close> in lower-case. |
|
48936 | 200 |
|
61503 | 201 |
Option \<^verbatim>\<open>-q\<close> omits printing of the result file name. |
48936 | 202 |
|
61406 | 203 |
\<^medskip> |
61575 | 204 |
Implementors of Isabelle tools and applications are encouraged to make |
205 |
derived Isabelle logos for their own projects using this template. |
|
206 |
\<close> |
|
28224 | 207 |
|
208 |
||
58618 | 209 |
section \<open>Output the version identifier of the Isabelle distribution\<close> |
28224 | 210 |
|
58618 | 211 |
text \<open> |
48602 | 212 |
The @{tool_def version} tool displays Isabelle version information: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
213 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
214 |
\<open>Usage: isabelle version [OPTIONS] |
41511 | 215 |
|
216 |
Options are: |
|
217 |
-i short identification (derived from Mercurial id) |
|
218 |
||
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
219 |
Display Isabelle version information.\<close>} |
41511 | 220 |
|
61406 | 221 |
\<^medskip> |
61575 | 222 |
The default is to output the full version string of the Isabelle |
68394 | 223 |
distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2018: August 2018\<close>. |
41511 | 224 |
|
61575 | 225 |
The \<^verbatim>\<open>-i\<close> option produces a short identification derived from the Mercurial |
226 |
id of the @{setting ISABELLE_HOME} directory. |
|
58618 | 227 |
\<close> |
28224 | 228 |
|
67399 | 229 |
end |