author | wenzelm |
Sat, 11 Jun 2022 22:55:21 +0200 | |
changeset 75555 | 197a5b3a1ea2 |
parent 75511 | b32fdb67f851 |
child 75556 | 1f6fc2416a48 |
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 |
|
71579 | 14 |
section \<open>Building Isabelle docker images\<close> |
15 |
||
16 |
text \<open> |
|
17 |
Docker\<^footnote>\<open>\<^url>\<open>https://docs.docker.com\<close>\<close> provides a self-contained environment |
|
18 |
for complex applications called \<^emph>\<open>container\<close>, although it does not fully |
|
19 |
contain the program in a strict sense of the word. This includes basic |
|
20 |
operating system services (usually based on Linux), shared libraries and |
|
21 |
other required packages. Thus Docker is a light-weight alternative to |
|
22 |
regular virtual machines, or a heavy-weight alternative to conventional |
|
23 |
self-contained applications. |
|
24 |
||
25 |
Although Isabelle can be easily run on a variety of OS environments without |
|
26 |
extra containment, Docker images may occasionally be useful when a |
|
27 |
standardized Linux environment is required, even on |
|
28 |
Windows\<^footnote>\<open>\<^url>\<open>https://docs.docker.com/docker-for-windows\<close>\<close> and |
|
29 |
macOS\<^footnote>\<open>\<^url>\<open>https://docs.docker.com/docker-for-mac\<close>\<close>. Further uses are in |
|
30 |
common cloud computing environments, where applications need to be submitted |
|
31 |
as Docker images in the first place. |
|
32 |
||
33 |
\<^medskip> |
|
34 |
The @{tool_def build_docker} tool builds docker images from a standard |
|
35 |
Isabelle application archive for Linux: |
|
36 |
||
37 |
@{verbatim [display] |
|
38 |
\<open>Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE |
|
39 |
||
40 |
Options are: |
|
41 |
-B NAME base image (default "ubuntu") |
|
72525 | 42 |
-E set Isabelle/bin/isabelle as entrypoint |
71579 | 43 |
-P NAME additional Ubuntu package collection ("X11", "latex") |
44 |
-l NAME default logic (default ISABELLE_LOGIC="HOL") |
|
45 |
-n no docker build |
|
46 |
-o FILE output generated Dockerfile |
|
47 |
-p NAME additional Ubuntu package |
|
48 |
-t TAG docker build tag |
|
49 |
-v verbose |
|
50 |
||
51 |
Build Isabelle docker image with default logic image, using a standard |
|
52 |
Isabelle application archive for Linux (local file or remote URL).\<close>} |
|
53 |
||
54 |
Option \<^verbatim>\<open>-E\<close> sets \<^verbatim>\<open>bin/isabelle\<close> of the contained Isabelle distribution as |
|
55 |
the standard entry point of the Docker image. Thus \<^verbatim>\<open>docker run\<close> will |
|
56 |
imitate the \<^verbatim>\<open>isabelle\<close> command-line tool (\secref{sec:isabelle-tool}) of a |
|
57 |
regular local installation, but it lacks proper GUI support: \<^verbatim>\<open>isabelle jedit\<close> |
|
58 |
will not work without further provisions. Note that the default entrypoint |
|
59 |
may be changed later via \<^verbatim>\<open>docker run --entrypoint="..."\<close>. |
|
60 |
||
61 |
Option \<^verbatim>\<open>-t\<close> specifies the Docker image tag: this a symbolic name within the |
|
62 |
local Docker name space, but also relevant for Docker |
|
63 |
Hub\<^footnote>\<open>\<^url>\<open>https://hub.docker.com\<close>\<close>. |
|
64 |
||
65 |
Option \<^verbatim>\<open>-l\<close> specifies the default logic image of the Isabelle distribution |
|
66 |
contained in the Docker environment: it will be produced by \<^verbatim>\<open>isabelle build -b\<close> |
|
67 |
as usual (\secref{sec:tool-build}) and stored within the image. |
|
68 |
||
69 |
\<^medskip> |
|
70 |
Option \<^verbatim>\<open>-B\<close> specifies the Docker image taken as starting point for the |
|
71 |
Isabelle installation: it needs to be a suitable version of Ubuntu Linux. |
|
72 |
The default \<^verbatim>\<open>ubuntu\<close> refers to the latest LTS version provided by Canonical |
|
73 |
as the official Ubuntu vendor\<^footnote>\<open>\<^url>\<open>https://hub.docker.com/_/ubuntu\<close>\<close>. For |
|
74427 | 74 |
Isabelle2021-1 this should be Ubuntu 20.04 LTS. |
71579 | 75 |
|
76 |
Option \<^verbatim>\<open>-p\<close> includes additional Ubuntu packages, using the terminology |
|
77 |
of \<^verbatim>\<open>apt-get install\<close> within the underlying Linux distribution. |
|
78 |
||
79 |
Option \<^verbatim>\<open>-P\<close> refers to high-level package collections: \<^verbatim>\<open>X11\<close> or \<^verbatim>\<open>latex\<close> as |
|
73534
e7fb17bca374
discontinue old Ubuntu 18.04 LTS, e.g. it cannot build documentation "prog-prove";
wenzelm
parents:
73484
diff
changeset
|
80 |
provided by \<^verbatim>\<open>isabelle build_docker\<close> (assuming Ubuntu 20.04 LTS). This |
71579 | 81 |
imposes extra weight on the resulting Docker images. Note that \<^verbatim>\<open>X11\<close> will |
82 |
only provide remote X11 support according to the modest GUI quality |
|
83 |
standards of the late 1990-ies. |
|
84 |
||
85 |
\<^medskip> |
|
86 |
Option \<^verbatim>\<open>-n\<close> suppresses the actual \<^verbatim>\<open>docker build\<close> process. Option \<^verbatim>\<open>-o\<close> |
|
87 |
outputs the generated \<^verbatim>\<open>Dockerfile\<close>. Both options together produce a |
|
88 |
Dockerfile only, which might be useful for informative purposes or other |
|
89 |
tools. |
|
90 |
||
91 |
Option \<^verbatim>\<open>-v\<close> disables quiet-mode of the underlying \<^verbatim>\<open>docker build\<close> process. |
|
92 |
\<close> |
|
93 |
||
94 |
||
95 |
subsubsection \<open>Examples\<close> |
|
96 |
||
97 |
text \<open> |
|
98 |
Produce a Dockerfile (without image) from a remote Isabelle distribution: |
|
99 |
@{verbatim [display] |
|
100 |
\<open> isabelle build_docker -E -n -o Dockerfile |
|
74427 | 101 |
https://isabelle.in.tum.de/website-Isabelle2021-1/dist/Isabelle2021-1_linux.tar.gz\<close>} |
71579 | 102 |
|
103 |
Build a standard Isabelle Docker image from a local Isabelle distribution, |
|
104 |
with \<^verbatim>\<open>bin/isabelle\<close> as executable entry point: |
|
105 |
||
106 |
@{verbatim [display] |
|
74427 | 107 |
\<open> isabelle build_docker -E -t test/isabelle:Isabelle2021-1 Isabelle2021-1_linux.tar.gz\<close>} |
71579 | 108 |
|
109 |
Invoke the raw Isabelle/ML process within that image: |
|
110 |
@{verbatim [display] |
|
74427 | 111 |
\<open> docker run test/isabelle:Isabelle2021-1 process -e "Session.welcome ()"\<close>} |
71579 | 112 |
|
113 |
Invoke a Linux command-line tool within the contained Isabelle system |
|
114 |
environment: |
|
115 |
@{verbatim [display] |
|
74427 | 116 |
\<open> docker run test/isabelle:Isabelle2021-1 env uname -a\<close>} |
71579 | 117 |
The latter should always report a Linux operating system, even when running |
118 |
on Windows or macOS. |
|
119 |
\<close> |
|
120 |
||
28224 | 121 |
|
73172 | 122 |
section \<open>Managing Isabelle components \label{sec:tool-components}\<close> |
48844 | 123 |
|
58618 | 124 |
text \<open> |
73172 | 125 |
The @{tool_def components} tool manages Isabelle components: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
126 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
127 |
\<open>Usage: isabelle components [OPTIONS] [COMPONENTS ...] |
48844 | 128 |
|
129 |
Options are: |
|
50653
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
50132
diff
changeset
|
130 |
-I init user settings |
73172 | 131 |
-R URL component repository (default $ISABELLE_COMPONENT_REPOSITORY) |
53435 | 132 |
-a resolve all missing components |
48844 | 133 |
-l list status |
73172 | 134 |
-u DIR update $ISABELLE_HOME_USER/components: add directory |
135 |
-x DIR update $ISABELLE_HOME_USER/components: remove directory |
|
48844 | 136 |
|
73172 | 137 |
Resolve Isabelle components via download and installation: given COMPONENTS |
138 |
are identified via base name. Further operations manage etc/settings and |
|
139 |
etc/components in $ISABELLE_HOME_USER. |
|
48844 | 140 |
|
73172 | 141 |
ISABELLE_COMPONENT_REPOSITORY="..." |
142 |
ISABELLE_HOME_USER="..." |
|
143 |
\<close>} |
|
48844 | 144 |
|
61575 | 145 |
Components are initialized as described in \secref{sec:components} in a |
146 |
permissive manner, which can mark components as ``missing''. This state is |
|
147 |
amended by letting @{tool "components"} download and unpack components that |
|
63680 | 148 |
are published on the default component repository |
68224 | 149 |
\<^url>\<open>https://isabelle.in.tum.de/components\<close> in particular. |
48844 | 150 |
|
61575 | 151 |
Option \<^verbatim>\<open>-R\<close> specifies an alternative component repository. Note that |
152 |
\<^verbatim>\<open>file:///\<close> URLs can be used for local directories. |
|
48844 | 153 |
|
61575 | 154 |
Option \<^verbatim>\<open>-a\<close> selects all missing components to be resolved. Explicit |
155 |
components may be named as command line-arguments as well. Note that |
|
156 |
components are uniquely identified by their base name, while the |
|
157 |
installation takes place in the location that was specified in the attempt |
|
158 |
to initialize the component before. |
|
48844 | 159 |
|
73172 | 160 |
\<^medskip> |
61575 | 161 |
Option \<^verbatim>\<open>-l\<close> lists the current state of available and missing components |
162 |
with their location (full name) within the file-system. |
|
50653
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
50132
diff
changeset
|
163 |
|
73172 | 164 |
\<^medskip> |
61575 | 165 |
Option \<^verbatim>\<open>-I\<close> initializes the user settings file to subscribe to the standard |
166 |
components specified in the Isabelle repository clone --- this does not make |
|
73484 | 167 |
any sense for regular Isabelle releases. An existing file that does not |
168 |
contain a suitable line ``\<^verbatim>\<open>init_components\<close>\<open>\<dots>\<close>\<^verbatim>\<open>components/main\<close>'' needs |
|
169 |
to be edited according to the printed explanation. |
|
73172 | 170 |
|
171 |
\<^medskip> |
|
172 |
Options \<^verbatim>\<open>-u\<close> and \<^verbatim>\<open>-x\<close> operate on user components listed in |
|
75161
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
75116
diff
changeset
|
173 |
\<^path>\<open>$ISABELLE_HOME_USER/etc/components\<close>: this avoids manual editing of |
73172 | 174 |
Isabelle configuration files. |
58618 | 175 |
\<close> |
48844 | 176 |
|
177 |
||
58618 | 178 |
section \<open>Viewing documentation \label{sec:tool-doc}\<close> |
28224 | 179 |
|
58618 | 180 |
text \<open> |
52444
2cfe6656d6d6
slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents:
52052
diff
changeset
|
181 |
The @{tool_def doc} tool displays Isabelle documentation: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
182 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
183 |
\<open>Usage: isabelle doc [DOC ...] |
28224 | 184 |
|
75116 | 185 |
View Isabelle PDF documentation.\<close>} |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
186 |
|
61575 | 187 |
If called without arguments, it lists all available documents. Each line |
188 |
starts with an identifier, followed by a short description. Any of these |
|
189 |
identifiers may be specified as arguments, in order to display the |
|
72309
564012e31db1
discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents:
71579
diff
changeset
|
190 |
corresponding document. |
28224 | 191 |
|
61406 | 192 |
\<^medskip> |
61575 | 193 |
The @{setting ISABELLE_DOCS} setting specifies the list of directories |
194 |
(separated by colons) to be scanned for documentations. |
|
58618 | 195 |
\<close> |
28224 | 196 |
|
197 |
||
58618 | 198 |
section \<open>Shell commands within the settings environment \label{sec:tool-env}\<close> |
47828 | 199 |
|
61575 | 200 |
text \<open> |
201 |
The @{tool_def env} tool is a direct wrapper for the standard |
|
202 |
\<^verbatim>\<open>/usr/bin/env\<close> command on POSIX systems, running within the Isabelle |
|
203 |
settings environment (\secref{sec:settings}). |
|
47828 | 204 |
|
61575 | 205 |
The command-line arguments are that of the underlying version of \<^verbatim>\<open>env\<close>. For |
206 |
example, the following invokes an instance of the GNU Bash shell within the |
|
207 |
Isabelle environment: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
208 |
@{verbatim [display] \<open>isabelle env bash\<close>} |
58618 | 209 |
\<close> |
47828 | 210 |
|
211 |
||
58618 | 212 |
section \<open>Inspecting the settings environment \label{sec:tool-getenv}\<close> |
28224 | 213 |
|
58618 | 214 |
text \<open>The Isabelle settings environment --- as provided by the |
28224 | 215 |
site-default and user-specific settings files --- can be inspected |
48602 | 216 |
with the @{tool_def getenv} tool: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
217 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
218 |
\<open>Usage: isabelle getenv [OPTIONS] [VARNAMES ...] |
28224 | 219 |
|
220 |
Options are: |
|
221 |
-a display complete environment |
|
222 |
-b print values only (doesn't work for -a) |
|
73581 | 223 |
-d FILE dump complete environment to file (NUL terminated entries) |
28224 | 224 |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
225 |
Get value of VARNAMES from the Isabelle settings.\<close>} |
28224 | 226 |
|
61575 | 227 |
With the \<^verbatim>\<open>-a\<close> option, one may inspect the full process environment that |
228 |
Isabelle related programs are run in. This usually contains much more |
|
229 |
variables than are actually Isabelle settings. Normally, output is a list of |
|
230 |
lines of the form \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close>. The \<^verbatim>\<open>-b\<close> option causes only the values |
|
231 |
to be printed. |
|
31497 | 232 |
|
61575 | 233 |
Option \<^verbatim>\<open>-d\<close> produces a dump of the complete environment to the specified |
73581 | 234 |
file. Entries are terminated by the ASCII NUL character, i.e.\ the string |
235 |
terminator in C. Thus the Isabelle/Scala operation |
|
236 |
\<^scala_method>\<open>isabelle.Isabelle_System.init\<close> can import the settings |
|
237 |
environment robustly, and provide its own |
|
238 |
\<^scala_method>\<open>isabelle.Isabelle_System.getenv\<close> function. |
|
58618 | 239 |
\<close> |
28224 | 240 |
|
241 |
||
58618 | 242 |
subsubsection \<open>Examples\<close> |
28224 | 243 |
|
61575 | 244 |
text \<open> |
245 |
Get the location of @{setting ISABELLE_HOME_USER} where user-specific |
|
246 |
information is stored: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
247 |
@{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>} |
28224 | 248 |
|
61406 | 249 |
\<^medskip> |
61575 | 250 |
Get the value only of the same settings variable, which is particularly |
251 |
useful in shell scripts: |
|
68219 | 252 |
@{verbatim [display] \<open>isabelle getenv -b ISABELLE_HOME_USER\<close>} |
58618 | 253 |
\<close> |
28224 | 254 |
|
255 |
||
71322 | 256 |
section \<open>Mercurial repository setup \label{sec:hg-setup}\<close> |
257 |
||
258 |
text \<open> |
|
259 |
The @{tool_def hg_setup} tool simplifies the setup of Mercurial |
|
71325 | 260 |
repositories, with hosting via Phabricator (\chref{ch:phabricator}) or SSH |
261 |
file server access. |
|
71322 | 262 |
|
263 |
@{verbatim [display] |
|
264 |
\<open>Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR |
|
265 |
||
266 |
Options are: |
|
267 |
-n NAME remote repository name (default: base name of LOCAL_DIR) |
|
268 |
-p PATH Mercurial path name (default: "default") |
|
269 |
-r assume that remote repository already exists |
|
270 |
||
271 |
Setup a remote vs. local Mercurial repository: REMOTE either refers to a |
|
272 |
Phabricator server "user@host" or SSH file server "ssh://user@host/path".\<close>} |
|
273 |
||
274 |
The \<^verbatim>\<open>REMOTE\<close> repository specification \<^emph>\<open>excludes\<close> the actual repository |
|
275 |
name: that is given by the base name of \<^verbatim>\<open>LOCAL_DIR\<close>, or via option \<^verbatim>\<open>-n\<close>. |
|
276 |
||
277 |
By default, both sides of the repository are created on demand by default. |
|
278 |
In contrast, option \<^verbatim>\<open>-r\<close> assumes that the remote repository already exists: |
|
279 |
it avoids accidental creation of a persistent repository with unintended |
|
280 |
name. |
|
281 |
||
282 |
The local \<^verbatim>\<open>.hg/hgrc\<close> file is changed to refer to the remote repository, |
|
283 |
usually via the symbolic path name ``\<^verbatim>\<open>default\<close>''; option \<^verbatim>\<open>-p\<close> allows to |
|
75161
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
75116
diff
changeset
|
284 |
provide a different name. |
71322 | 285 |
\<close> |
286 |
||
71324 | 287 |
subsubsection \<open>Examples\<close> |
288 |
||
289 |
text \<open> |
|
290 |
Setup the current directory as a repository with Phabricator server hosting: |
|
291 |
@{verbatim [display] \<open> isabelle hg_setup vcs@vcs.example.org .\<close>} |
|
292 |
||
293 |
\<^medskip> |
|
294 |
Setup the current directory as a repository with plain SSH server hosting: |
|
295 |
@{verbatim [display] \<open> isabelle hg_setup ssh://files.example.org/data/repositories .\<close>} |
|
296 |
||
297 |
\<^medskip> |
|
298 |
Both variants require SSH access to the target server, via public key |
|
299 |
without password. |
|
300 |
\<close> |
|
301 |
||
71322 | 302 |
|
75555
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
303 |
section \<open>Mercurial repository synchronization \label{sec:tool-hg-sync}\<close> |
75476 | 304 |
|
305 |
text \<open> |
|
75479 | 306 |
The @{tool_def hg_sync} tool synchronizes a local Mercurial repository with |
75511 | 307 |
a target directory. |
75476 | 308 |
|
309 |
@{verbatim [display] |
|
310 |
\<open>Usage: isabelle hg_sync [OPTIONS] TARGET |
|
311 |
||
312 |
Options are: |
|
75511 | 313 |
-F RULE add rsync filter RULE |
314 |
(e.g. "protect /foo" to avoid deletion) |
|
75476 | 315 |
-R ROOT explicit repository root directory |
316 |
(default: implicit from current directory) |
|
75493 | 317 |
-T thorough treatment of file content and directory times |
75476 | 318 |
-n no changes: dry-run |
75479 | 319 |
-r REV explicit revision (default: state of working directory) |
75499 | 320 |
-p PORT explicit SSH port (default: 22) |
75476 | 321 |
-v verbose |
322 |
||
75479 | 323 |
Synchronize Mercurial repository with TARGET directory, |
75476 | 324 |
which can be local or remote (using notation of rsync).\<close>} |
325 |
||
326 |
The \<^verbatim>\<open>TARGET\<close> specification can be a local or remote directory (via ssh), |
|
75511 | 327 |
using \<^verbatim>\<open>rsync\<close>\<^footnote>\<open>\<^url>\<open>https://linux.die.net/man/1/rsync\<close>\<close> notation for |
328 |
destinations; see also examples below. The content is written directly into |
|
329 |
the target, \<^emph>\<open>without\<close> creating a separate sub-directory. The special |
|
330 |
sub-directory \<^verbatim>\<open>.hg_sync\<close> within the target contains meta data from the |
|
331 |
original Mercurial repository. Repeated synchronization is guarded by the |
|
332 |
presence of a \<^verbatim>\<open>.hg_sync\<close> sub-directory: this sanity check prevents |
|
333 |
accidental changes (or deletion!) of targets that were not created by @{tool |
|
334 |
hg_sync}. |
|
75476 | 335 |
|
75479 | 336 |
\<^medskip> Option \<^verbatim>\<open>-r\<close> specifies an explicit revision of the repository; the default |
337 |
is the current state of the working directory (which might be uncommitted). |
|
338 |
||
75476 | 339 |
\<^medskip> Option \<^verbatim>\<open>-v\<close> enables verbose mode. Option \<^verbatim>\<open>-n\<close> enables ``dry-run'' mode: |
75511 | 340 |
operations are only simulated; use it with option \<^verbatim>\<open>-v\<close> to actually see |
341 |
results. |
|
75476 | 342 |
|
75489 | 343 |
\<^medskip> Option \<^verbatim>\<open>-F\<close> adds a filter rule to the underlying \<^verbatim>\<open>rsync\<close> command; |
344 |
multiple \<^verbatim>\<open>-F\<close> options may be given to accumulate a list of rules. |
|
75476 | 345 |
|
346 |
\<^medskip> Option \<^verbatim>\<open>-R\<close> specifies an explicit repository root directory. The default |
|
75479 | 347 |
is to derive it from the current directory, searching upwards until a |
348 |
suitable \<^verbatim>\<open>.hg\<close> directory is found. |
|
75487 | 349 |
|
75493 | 350 |
\<^medskip> Option \<^verbatim>\<open>-T\<close> indicates thorough treatment of file content and directory |
351 |
times. The default is to consider files with equal time and size already as |
|
352 |
equal, and to ignore time stamps on directories. |
|
75499 | 353 |
|
354 |
\<^medskip> Option \<^verbatim>\<open>-p\<close> specifies an explicit port for the SSH connection underlying |
|
355 |
\<^verbatim>\<open>rsync\<close>. |
|
75476 | 356 |
\<close> |
357 |
||
358 |
subsubsection \<open>Examples\<close> |
|
359 |
||
360 |
text \<open> |
|
75490
5e37ea93759d
clarified documentation: $ISABELLE_HOME is not a repository for regular releases;
wenzelm
parents:
75489
diff
changeset
|
361 |
Synchronize the current repository onto a remote host, with accurate |
75493 | 362 |
treatment of all content: |
75511 | 363 |
@{verbatim [display] \<open> isabelle hg_sync -T remotename:test/repos\<close>} |
75476 | 364 |
\<close> |
365 |
||
366 |
||
58618 | 367 |
section \<open>Installing standalone Isabelle executables \label{sec:tool-install}\<close> |
28224 | 368 |
|
61575 | 369 |
text \<open> |
370 |
By default, the main Isabelle binaries (@{executable "isabelle"} etc.) are |
|
371 |
just run from their location within the distribution directory, probably |
|
372 |
indirectly by the shell through its @{setting PATH}. Other schemes of |
|
373 |
installation are supported by the @{tool_def install} tool: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
374 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
375 |
\<open>Usage: isabelle install [OPTIONS] BINDIR |
28224 | 376 |
|
377 |
Options are: |
|
50132 | 378 |
-d DISTDIR refer to DISTDIR as Isabelle distribution |
28224 | 379 |
(default ISABELLE_HOME) |
380 |
||
50132 | 381 |
Install Isabelle executables with absolute references to the |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
382 |
distribution directory.\<close>} |
28224 | 383 |
|
61575 | 384 |
The \<^verbatim>\<open>-d\<close> option overrides the current Isabelle distribution directory as |
385 |
determined by @{setting ISABELLE_HOME}. |
|
28224 | 386 |
|
61575 | 387 |
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
|
388 |
@{executable "isabelle"} and @{executable isabelle_scala_script} should be |
61575 | 389 |
placed, which is typically a directory in the shell's @{setting PATH}, such |
390 |
as \<^verbatim>\<open>$HOME/bin\<close>. |
|
48815 | 391 |
|
61406 | 392 |
\<^medskip> |
61575 | 393 |
It is also possible to make symbolic links of the main Isabelle executables |
394 |
manually, but making separate copies outside the Isabelle distribution |
|
395 |
directory will not work! |
|
396 |
\<close> |
|
28224 | 397 |
|
398 |
||
58618 | 399 |
section \<open>Creating instances of the Isabelle logo\<close> |
28224 | 400 |
|
61575 | 401 |
text \<open> |
73399 | 402 |
The @{tool_def logo} tool creates variants of the Isabelle logo, for |
403 |
inclusion in PDF{\LaTeX} documents. |
|
404 |
||
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
405 |
@{verbatim [display] |
73399 | 406 |
\<open>Usage: isabelle logo [OPTIONS] [NAME] |
28224 | 407 |
|
408 |
Options are: |
|
73399 | 409 |
-o FILE alternative output file |
410 |
-q quiet mode |
|
411 |
||
412 |
Create variant NAME of the Isabelle logo as "isabelle_name.pdf".\<close>} |
|
48936 | 413 |
|
73399 | 414 |
Option \<^verbatim>\<open>-o\<close> provides an alternative output file, instead of the default in |
415 |
the current directory: \<^verbatim>\<open>isabelle_\<close>\<open>name\<close>\<^verbatim>\<open>.pdf\<close> with the lower-case version |
|
416 |
of the given name. |
|
48936 | 417 |
|
73399 | 418 |
\<^medskip> |
72316
3cc6aa405858
clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents:
72309
diff
changeset
|
419 |
Option \<^verbatim>\<open>-q\<close> omits printing of the resulting output file name. |
48936 | 420 |
|
61406 | 421 |
\<^medskip> |
61575 | 422 |
Implementors of Isabelle tools and applications are encouraged to make |
73399 | 423 |
derived Isabelle logos for their own projects using this template. The |
424 |
license is the same as for the regular Isabelle distribution (BSD). |
|
61575 | 425 |
\<close> |
28224 | 426 |
|
427 |
||
75555
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
428 |
section \<open>Isabelle and AFP repository synchronization\<close> |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
429 |
|
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
430 |
text \<open> |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
431 |
The @{tool_def sync} tool synchronizes a local Isabelle and AFP repository, |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
432 |
potentially including its prebuilt \<^verbatim>\<open>.jar\<close> files and session images. |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
433 |
|
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
434 |
@{verbatim [display] |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
435 |
\<open>Usage: isabelle sync [OPTIONS] TARGET |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
436 |
|
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
437 |
Options are: |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
438 |
-A ROOT include AFP with given root directory (":" for $AFP_BASE) |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
439 |
-H purge heaps directory on target |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
440 |
-I NAME include session heap image and build database |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
441 |
(based on accidental local state) |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
442 |
-J preserve *.jar files |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
443 |
-S robust (but less portable) treatment of spaces in |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
444 |
file and directory names on the target |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
445 |
-T thorough treatment of file content and directory times |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
446 |
-a REV explicit AFP revision (default: state of working directory) |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
447 |
-n no changes: dry-run |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
448 |
-r REV explicit revision (default: state of working directory) |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
449 |
-p PORT explicit SSH port (default: 22) |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
450 |
-v verbose |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
451 |
|
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
452 |
Synchronize Isabelle + AFP repositories, based on "isabelle hg_sync".\<close>} |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
453 |
|
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
454 |
The approach is to apply @{tool hg_sync} (\secref{sec:tool-hg-sync}) on the |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
455 |
underlying Isabelle repository plus a given AFP repository (optional). This |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
456 |
means that the Isabelle installation needs to be a Mercurial repository |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
457 |
clone: a regular download of the Isabelle distribution is not sufficient! |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
458 |
|
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
459 |
On the target side, AFP is placed into @{setting ISABELLE_HOME} as immediate |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
460 |
sub-directory with the literal name \<^verbatim>\<open>AFP\<close>; thus it can be easily included |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
461 |
elsewhere, e.g. @{tool build}~\<^verbatim>\<open>-d\<close>~\<^verbatim>\<open>'~~/AFP'\<close> on the remote side. |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
462 |
|
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
463 |
\<^medskip> Options \<^verbatim>\<open>-T\<close>, \<^verbatim>\<open>-n\<close>, \<^verbatim>\<open>-p\<close>, \<^verbatim>\<open>-v\<close> are the same as the underlying |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
464 |
@{tool hg_sync}. |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
465 |
|
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
466 |
\<^medskip> Options \<^verbatim>\<open>-r\<close> and \<^verbatim>\<open>-a\<close> are the same as option \<^verbatim>\<open>-r\<close> for @{tool hg_sync}, |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
467 |
but for the Isabelle and AFP repositories, respectively. The AFP version is |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
468 |
only used if a corresponding repository is given via option \<^verbatim>\<open>-A\<close>, either |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
469 |
with explicit root directory, or as \<^verbatim>\<open>-A:\<close> to refer to \<^verbatim>\<open>$AFP_BASE\<close> (this |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
470 |
assumes AFP as component of the local Isabelle installation). |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
471 |
|
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
472 |
\<^medskip> Option \<^verbatim>\<open>-J\<close> uploads existing \<^verbatim>\<open>.jar\<close> files, which are usually |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
473 |
Isabelle/Scala/Java modules under control of \<^verbatim>\<open>etc/build.props\<close> (see also |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
474 |
\secref{sec:scala-build}). Normally, the underlying dependency management is |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
475 |
accurate: bad uploads will be rebuilt on the remote side (or ignored). For |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
476 |
historic Isabelle versions, going far back into the past via option \<^verbatim>\<open>-r\<close>, |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
477 |
it is better to omit option \<^verbatim>\<open>-J\<close> and thus purge \<^verbatim>\<open>.jar\<close> files on the target |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
478 |
(because they do not belong to the repository). |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
479 |
|
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
480 |
\<^medskip> Option \<^verbatim>\<open>-I\<close> uploads a collection of session images. The set of \<^verbatim>\<open>-I\<close> |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
481 |
options specifies the end-points in the session build graph, including all |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
482 |
required ancestors. The result collection is uploaded using the underlying |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
483 |
\<^verbatim>\<open>rsync\<close> policies: unchanged images are ignored. Session images are |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
484 |
assembled within the target \<^verbatim>\<open>heaps\<close> directory: this scheme fits together |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
485 |
with @{tool build}~\<^verbatim>\<open>-o system_heaps\<close>. Images are taken as-is from the local |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
486 |
Isabelle installation, regardless of option \<^verbatim>\<open>-r\<close>. Bad images do not cause |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
487 |
any harm, apart from wasting network bandwidth and file-system space: |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
488 |
running e.g. @{tool build} on the target will check dependencies accurately, |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
489 |
and rebuild outdated images on demand. |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
490 |
|
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
491 |
\<^medskip> Option \<^verbatim>\<open>-H\<close> tells the underlying \<^verbatim>\<open>rsync\<close> process to purge the \<^verbatim>\<open>heaps\<close> |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
492 |
directory on the target, before uploading new images from \<^verbatim>\<open>-I\<close> options. The |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
493 |
default is to work monotonically: old material that is not overwritten |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
494 |
remains unchanged, it is never deleted. Over time, this may lead to |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
495 |
unreachable garbage, due to changes in session names or Poly/ML versions. |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
496 |
Option \<^verbatim>\<open>-H\<close> helps to avoid wasting file-system space, although @{tool |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
497 |
build} does not require it, due to its precise checking of all dependencies. |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
498 |
|
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
499 |
\<^medskip> Option \<^verbatim>\<open>-S\<close> uses \<^verbatim>\<open>rsync --protect-args\<close>, but this requires at least |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
500 |
\<^verbatim>\<open>rsync 3.0.0\<close>, while many versions of macOS still ship \<^verbatim>\<open>rsync 2.9.x\<close>. |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
501 |
Since Isabelle + AFP don't use spaces or other special characters, it is |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
502 |
usually safe to omit this non-portable option. |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
503 |
\<close> |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
504 |
|
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
505 |
subsubsection \<open>Examples\<close> |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
506 |
|
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
507 |
text \<open> |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
508 |
Quick testing of Isabelle + AFP on a remote machine: upload changed sources, |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
509 |
jars, and local sessions images for \<^verbatim>\<open>HOL\<close>: |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
510 |
@{verbatim [display] \<open> isabelle sync -A: -I HOL -J testmachine:test/isabelle_afp\<close>} |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
511 |
Assuming that the local \<^verbatim>\<open>HOL\<close> hierarchy has been up-to-date, and the local |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
512 |
and remote ML platforms coincide, a remote @{tool build} will proceed |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
513 |
without building \<^verbatim>\<open>HOL\<close> again. |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
514 |
|
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
515 |
\<^medskip> A variation for accurate testing of Isabelle + AFP: no option \<^verbatim>\<open>-J\<close>, but |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
516 |
option \<^verbatim>\<open>-T\<close> to disable the default ``quick check'' of \<^verbatim>\<open>rsync\<close> (which only |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
517 |
inspects file sizes and date stamps): |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
518 |
@{verbatim [display] \<open> isabelle sync -A: -T testmachine:test/isabelle_afp\<close>} |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
519 |
\<close> |
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
520 |
|
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75511
diff
changeset
|
521 |
|
58618 | 522 |
section \<open>Output the version identifier of the Isabelle distribution\<close> |
28224 | 523 |
|
58618 | 524 |
text \<open> |
48602 | 525 |
The @{tool_def version} tool displays Isabelle version information: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
526 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
527 |
\<open>Usage: isabelle version [OPTIONS] |
41511 | 528 |
|
529 |
Options are: |
|
530 |
-i short identification (derived from Mercurial id) |
|
73481 | 531 |
-t symbolic tags (derived from Mercurial id) |
41511 | 532 |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
533 |
Display Isabelle version information.\<close>} |
41511 | 534 |
|
61406 | 535 |
\<^medskip> |
61575 | 536 |
The default is to output the full version string of the Isabelle |
74427 | 537 |
distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2021-1: December 2021\<close>. |
41511 | 538 |
|
73481 | 539 |
\<^medskip> |
540 |
Option \<^verbatim>\<open>-i\<close> produces a short identification derived from the Mercurial id |
|
541 |
of the @{setting ISABELLE_HOME} directory; option \<^verbatim>\<open>-t\<close> prints version tags |
|
542 |
(if available). |
|
543 |
||
544 |
These options require either a repository clone or a repository archive |
|
545 |
(e.g. download of |
|
73480
0e880b793db1
support repository archives (without full .hg directory);
wenzelm
parents:
73399
diff
changeset
|
546 |
\<^url>\<open>https://isabelle.sketis.net/repos/isabelle/archive/tip.tar.gz\<close>). |
58618 | 547 |
\<close> |
28224 | 548 |
|
67399 | 549 |
end |