author | wenzelm |
Thu, 19 Dec 2019 17:29:35 +0100 | |
changeset 71325 | 0131b7b44c32 |
parent 71324 | d0e14780b278 |
child 71578 | d59d557f4ee0 |
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 |
||
71322 | 152 |
section \<open>Mercurial repository setup \label{sec:hg-setup}\<close> |
153 |
||
154 |
text \<open> |
|
155 |
The @{tool_def hg_setup} tool simplifies the setup of Mercurial |
|
71325 | 156 |
repositories, with hosting via Phabricator (\chref{ch:phabricator}) or SSH |
157 |
file server access. |
|
71322 | 158 |
|
159 |
@{verbatim [display] |
|
160 |
\<open>Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR |
|
161 |
||
162 |
Options are: |
|
163 |
-n NAME remote repository name (default: base name of LOCAL_DIR) |
|
164 |
-p PATH Mercurial path name (default: "default") |
|
165 |
-r assume that remote repository already exists |
|
166 |
||
167 |
Setup a remote vs. local Mercurial repository: REMOTE either refers to a |
|
168 |
Phabricator server "user@host" or SSH file server "ssh://user@host/path".\<close>} |
|
169 |
||
170 |
The \<^verbatim>\<open>REMOTE\<close> repository specification \<^emph>\<open>excludes\<close> the actual repository |
|
171 |
name: that is given by the base name of \<^verbatim>\<open>LOCAL_DIR\<close>, or via option \<^verbatim>\<open>-n\<close>. |
|
172 |
||
173 |
By default, both sides of the repository are created on demand by default. |
|
174 |
In contrast, option \<^verbatim>\<open>-r\<close> assumes that the remote repository already exists: |
|
175 |
it avoids accidental creation of a persistent repository with unintended |
|
176 |
name. |
|
177 |
||
178 |
The local \<^verbatim>\<open>.hg/hgrc\<close> file is changed to refer to the remote repository, |
|
179 |
usually via the symbolic path name ``\<^verbatim>\<open>default\<close>''; option \<^verbatim>\<open>-p\<close> allows to |
|
180 |
provided a different name. |
|
181 |
\<close> |
|
182 |
||
71324 | 183 |
subsubsection \<open>Examples\<close> |
184 |
||
185 |
text \<open> |
|
186 |
Setup the current directory as a repository with Phabricator server hosting: |
|
187 |
@{verbatim [display] \<open> isabelle hg_setup vcs@vcs.example.org .\<close>} |
|
188 |
||
189 |
\<^medskip> |
|
190 |
Setup the current directory as a repository with plain SSH server hosting: |
|
191 |
@{verbatim [display] \<open> isabelle hg_setup ssh://files.example.org/data/repositories .\<close>} |
|
192 |
||
193 |
\<^medskip> |
|
194 |
Both variants require SSH access to the target server, via public key |
|
195 |
without password. |
|
196 |
\<close> |
|
197 |
||
71322 | 198 |
|
58618 | 199 |
section \<open>Installing standalone Isabelle executables \label{sec:tool-install}\<close> |
28224 | 200 |
|
61575 | 201 |
text \<open> |
202 |
By default, the main Isabelle binaries (@{executable "isabelle"} etc.) are |
|
203 |
just run from their location within the distribution directory, probably |
|
204 |
indirectly by the shell through its @{setting PATH}. Other schemes of |
|
205 |
installation are supported by the @{tool_def install} tool: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
206 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
207 |
\<open>Usage: isabelle install [OPTIONS] BINDIR |
28224 | 208 |
|
209 |
Options are: |
|
50132 | 210 |
-d DISTDIR refer to DISTDIR as Isabelle distribution |
28224 | 211 |
(default ISABELLE_HOME) |
212 |
||
50132 | 213 |
Install Isabelle executables with absolute references to the |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
214 |
distribution directory.\<close>} |
28224 | 215 |
|
61575 | 216 |
The \<^verbatim>\<open>-d\<close> option overrides the current Isabelle distribution directory as |
217 |
determined by @{setting ISABELLE_HOME}. |
|
28224 | 218 |
|
61575 | 219 |
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
|
220 |
@{executable "isabelle"} and @{executable isabelle_scala_script} should be |
61575 | 221 |
placed, which is typically a directory in the shell's @{setting PATH}, such |
222 |
as \<^verbatim>\<open>$HOME/bin\<close>. |
|
48815 | 223 |
|
61406 | 224 |
\<^medskip> |
61575 | 225 |
It is also possible to make symbolic links of the main Isabelle executables |
226 |
manually, but making separate copies outside the Isabelle distribution |
|
227 |
directory will not work! |
|
228 |
\<close> |
|
28224 | 229 |
|
230 |
||
58618 | 231 |
section \<open>Creating instances of the Isabelle logo\<close> |
28224 | 232 |
|
61575 | 233 |
text \<open> |
234 |
The @{tool_def logo} tool creates instances of the generic Isabelle logo as |
|
235 |
EPS and PDF, for inclusion in {\LaTeX} documents. |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
236 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
237 |
\<open>Usage: isabelle logo [OPTIONS] XYZ |
28224 | 238 |
|
49072
747835eb2782
"isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents:
48985
diff
changeset
|
239 |
Create instance XYZ of the Isabelle logo (as EPS and PDF). |
28224 | 240 |
|
241 |
Options are: |
|
49072
747835eb2782
"isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents:
48985
diff
changeset
|
242 |
-n NAME alternative output base name (default "isabelle_xyx") |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
243 |
-q quiet mode\<close>} |
48936 | 244 |
|
61575 | 245 |
Option \<^verbatim>\<open>-n\<close> specifies an alternative (base) name for the generated files. |
246 |
The default is \<^verbatim>\<open>isabelle_\<close>\<open>xyz\<close> in lower-case. |
|
48936 | 247 |
|
61503 | 248 |
Option \<^verbatim>\<open>-q\<close> omits printing of the result file name. |
48936 | 249 |
|
61406 | 250 |
\<^medskip> |
61575 | 251 |
Implementors of Isabelle tools and applications are encouraged to make |
252 |
derived Isabelle logos for their own projects using this template. |
|
253 |
\<close> |
|
28224 | 254 |
|
255 |
||
58618 | 256 |
section \<open>Output the version identifier of the Isabelle distribution\<close> |
28224 | 257 |
|
58618 | 258 |
text \<open> |
48602 | 259 |
The @{tool_def version} tool displays Isabelle version information: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
260 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
261 |
\<open>Usage: isabelle version [OPTIONS] |
41511 | 262 |
|
263 |
Options are: |
|
264 |
-i short identification (derived from Mercurial id) |
|
265 |
||
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
266 |
Display Isabelle version information.\<close>} |
41511 | 267 |
|
61406 | 268 |
\<^medskip> |
61575 | 269 |
The default is to output the full version string of the Isabelle |
68394 | 270 |
distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2018: August 2018\<close>. |
41511 | 271 |
|
61575 | 272 |
The \<^verbatim>\<open>-i\<close> option produces a short identification derived from the Mercurial |
273 |
id of the @{setting ISABELLE_HOME} directory. |
|
58618 | 274 |
\<close> |
28224 | 275 |
|
67399 | 276 |
end |