src/Doc/System/Misc.thy
author wenzelm
Mon, 28 Sep 2020 13:53:50 +0200
changeset 72316 3cc6aa405858
parent 72309 564012e31db1
child 72525 8eb0b663fa20
permissions -rw-r--r--
clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
61656
cfabbc083977 more uniform jEdit properties;
wenzelm
parents: 61575
diff changeset
     1
(*:maxLineLen=78:*)
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
     2
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     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
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     5
begin
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     6
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
     7
chapter \<open>Miscellaneous tools \label{ch:tools}\<close>
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     8
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
     9
text \<open>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    10
  Subsequently we describe various Isabelle related utilities, given in
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    11
  alphabetical order.
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
    12
\<close>
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    13
71579
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    14
section \<open>Building Isabelle docker images\<close>
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    15
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    16
text \<open>
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    17
  Docker\<^footnote>\<open>\<^url>\<open>https://docs.docker.com\<close>\<close> provides a self-contained environment
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    18
  for complex applications called \<^emph>\<open>container\<close>, although it does not fully
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    19
  contain the program in a strict sense of the word. This includes basic
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    20
  operating system services (usually based on Linux), shared libraries and
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    21
  other required packages. Thus Docker is a light-weight alternative to
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    22
  regular virtual machines, or a heavy-weight alternative to conventional
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    23
  self-contained applications.
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    24
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    25
  Although Isabelle can be easily run on a variety of OS environments without
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    26
  extra containment, Docker images may occasionally be useful when a
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    27
  standardized Linux environment is required, even on
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    28
  Windows\<^footnote>\<open>\<^url>\<open>https://docs.docker.com/docker-for-windows\<close>\<close> and
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    29
  macOS\<^footnote>\<open>\<^url>\<open>https://docs.docker.com/docker-for-mac\<close>\<close>. Further uses are in
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    30
  common cloud computing environments, where applications need to be submitted
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    31
  as Docker images in the first place.
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    32
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    33
  \<^medskip>
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    34
  The @{tool_def build_docker} tool builds docker images from a standard
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    35
  Isabelle application archive for Linux:
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    36
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    37
  @{verbatim [display]
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    38
\<open>Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    39
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    40
  Options are:
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    41
    -B NAME      base image (default "ubuntu")
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    42
    -E           set bin/isabelle as entrypoint
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    43
    -P NAME      additional Ubuntu package collection ("X11", "latex")
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    44
    -l NAME      default logic (default ISABELLE_LOGIC="HOL")
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    45
    -n           no docker build
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    46
    -o FILE      output generated Dockerfile
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    47
    -p NAME      additional Ubuntu package
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    48
    -t TAG       docker build tag
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    49
    -v           verbose
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    50
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    51
  Build Isabelle docker image with default logic image, using a standard
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    52
  Isabelle application archive for Linux (local file or remote URL).\<close>}
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    53
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    54
  Option \<^verbatim>\<open>-E\<close> sets \<^verbatim>\<open>bin/isabelle\<close> of the contained Isabelle distribution as
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    55
  the standard entry point of the Docker image. Thus \<^verbatim>\<open>docker run\<close> will
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    56
  imitate the \<^verbatim>\<open>isabelle\<close> command-line tool (\secref{sec:isabelle-tool}) of a
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    57
  regular local installation, but it lacks proper GUI support: \<^verbatim>\<open>isabelle jedit\<close>
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    58
  will not work without further provisions. Note that the default entrypoint
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    59
  may be changed later via \<^verbatim>\<open>docker run --entrypoint="..."\<close>.
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    60
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    61
  Option \<^verbatim>\<open>-t\<close> specifies the Docker image tag: this a symbolic name within the
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    62
  local Docker name space, but also relevant for Docker
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    63
  Hub\<^footnote>\<open>\<^url>\<open>https://hub.docker.com\<close>\<close>.
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    64
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    65
  Option \<^verbatim>\<open>-l\<close> specifies the default logic image of the Isabelle distribution
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    66
  contained in the Docker environment: it will be produced by \<^verbatim>\<open>isabelle build -b\<close>
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    67
  as usual (\secref{sec:tool-build}) and stored within the image.
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    68
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    69
  \<^medskip>
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    70
  Option \<^verbatim>\<open>-B\<close> specifies the Docker image taken as starting point for the
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    71
  Isabelle installation: it needs to be a suitable version of Ubuntu Linux.
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    72
  The default \<^verbatim>\<open>ubuntu\<close> refers to the latest LTS version provided by Canonical
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    73
  as the official Ubuntu vendor\<^footnote>\<open>\<^url>\<open>https://hub.docker.com/_/ubuntu\<close>\<close>. For
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    74
  Isabelle2020 this should be Ubuntu 18.04 LTS.
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    75
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    76
  Option \<^verbatim>\<open>-p\<close> includes additional Ubuntu packages, using the terminology
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    77
  of \<^verbatim>\<open>apt-get install\<close> within the underlying Linux distribution.
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    78
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    79
  Option \<^verbatim>\<open>-P\<close> refers to high-level package collections: \<^verbatim>\<open>X11\<close> or \<^verbatim>\<open>latex\<close> as
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    80
  provided by \<^verbatim>\<open>isabelle build_docker\<close> (assuming Ubuntu 18.04 LTS). This
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    81
  imposes extra weight on the resulting Docker images. Note that \<^verbatim>\<open>X11\<close> will
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    82
  only provide remote X11 support according to the modest GUI quality
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    83
  standards of the late 1990-ies.
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    84
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    85
  \<^medskip>
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    86
  Option \<^verbatim>\<open>-n\<close> suppresses the actual \<^verbatim>\<open>docker build\<close> process. Option \<^verbatim>\<open>-o\<close>
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    87
  outputs the generated \<^verbatim>\<open>Dockerfile\<close>. Both options together produce a
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    88
  Dockerfile only, which might be useful for informative purposes or other
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    89
  tools.
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    90
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    91
  Option \<^verbatim>\<open>-v\<close> disables quiet-mode of the underlying \<^verbatim>\<open>docker build\<close> process.
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    92
\<close>
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    93
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    94
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    95
subsubsection \<open>Examples\<close>
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    96
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    97
text \<open>
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    98
  Produce a Dockerfile (without image) from a remote Isabelle distribution:
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
    99
  @{verbatim [display]
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   100
\<open>  isabelle build_docker -E -n -o Dockerfile
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   101
    https://isabelle.in.tum.de/website-Isabelle2020/dist/Isabelle2020_linux.tar.gz\<close>}
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   102
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   103
  Build a standard Isabelle Docker image from a local Isabelle distribution,
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   104
  with \<^verbatim>\<open>bin/isabelle\<close> as executable entry point:
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   105
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   106
  @{verbatim [display]
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   107
\<open>  isabelle build_docker -E -t test/isabelle:Isabelle2020 Isabelle2020_linux.tar.gz\<close>}
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   108
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   109
  Invoke the raw Isabelle/ML process within that image:
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   110
  @{verbatim [display]
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   111
\<open>  docker run test/isabelle:Isabelle2020 process -e "Session.welcome ()"\<close>}
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   112
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   113
  Invoke a Linux command-line tool within the contained Isabelle system
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   114
  environment:
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   115
  @{verbatim [display]
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   116
\<open>  docker run test/isabelle:Isabelle2020 env uname -a\<close>}
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   117
  The latter should always report a Linux operating system, even when running
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   118
  on Windows or macOS.
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   119
\<close>
9b49538845cc documentation for "isabelle build_docker";
wenzelm
parents: 71578
diff changeset
   120
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   121
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   122
section \<open>Resolving Isabelle components \label{sec:tool-components}\<close>
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   123
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   124
text \<open>
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   125
  The @{tool_def components} tool resolves 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
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   128
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   129
  Options are:
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 50132
diff changeset
   130
    -I           init user settings
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   131
    -R URL       component repository
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   132
                 (default $ISABELLE_COMPONENT_REPOSITORY)
53435
wenzelm
parents: 52550
diff changeset
   133
    -a           resolve all missing components
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   134
    -l           list status
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   135
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   136
  Resolve Isabelle components via download and installation.
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   137
  COMPONENTS are identified via base name.
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   138
68224
1f7308050349 prefer HTTPS;
wenzelm
parents: 68219
diff changeset
   139
  ISABELLE_COMPONENT_REPOSITORY="https://isabelle.in.tum.de/components"\<close>}
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   140
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   141
  Components are initialized as described in \secref{sec:components} in a
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   142
  permissive manner, which can mark components as ``missing''. This state is
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   143
  amended by letting @{tool "components"} download and unpack components that
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 62588
diff changeset
   144
  are published on the default component repository
68224
1f7308050349 prefer HTTPS;
wenzelm
parents: 68219
diff changeset
   145
  \<^url>\<open>https://isabelle.in.tum.de/components\<close> in particular.
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   146
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   147
  Option \<^verbatim>\<open>-R\<close> specifies an alternative component repository. Note that
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   148
  \<^verbatim>\<open>file:///\<close> URLs can be used for local directories.
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   149
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   150
  Option \<^verbatim>\<open>-a\<close> selects all missing components to be resolved. Explicit
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   151
  components may be named as command line-arguments as well. Note that
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   152
  components are uniquely identified by their base name, while the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   153
  installation takes place in the location that was specified in the attempt
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   154
  to initialize the component before.
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   155
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   156
  Option \<^verbatim>\<open>-l\<close> lists the current state of available and missing components
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   157
  with their location (full name) within the file-system.
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 50132
diff changeset
   158
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   159
  Option \<^verbatim>\<open>-I\<close> initializes the user settings file to subscribe to the standard
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   160
  components specified in the Isabelle repository clone --- this does not make
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   161
  any sense for regular Isabelle releases. If the file already exists, it
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   162
  needs to be edited manually according to the printed explanation.
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   163
\<close>
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   164
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
   165
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   166
section \<open>Viewing documentation \label{sec:tool-doc}\<close>
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   167
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   168
text \<open>
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52052
diff changeset
   169
  The @{tool_def doc} tool displays Isabelle documentation:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   170
  @{verbatim [display]
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   171
\<open>Usage: isabelle doc [DOC ...]
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   172
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   173
  View Isabelle documentation.\<close>}
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   174
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   175
  If called without arguments, it lists all available documents. Each line
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   176
  starts with an identifier, followed by a short description. Any of these
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   177
  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
   178
  corresponding document.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   179
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 58618
diff changeset
   180
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   181
  The @{setting ISABELLE_DOCS} setting specifies the list of directories
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   182
  (separated by colons) to be scanned for documentations.
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   183
\<close>
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   184
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   185
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   186
section \<open>Shell commands within the settings environment \label{sec:tool-env}\<close>
47828
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   187
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   188
text \<open>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   189
  The @{tool_def env} tool is a direct wrapper for the standard
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   190
  \<^verbatim>\<open>/usr/bin/env\<close> command on POSIX systems, running within the Isabelle
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   191
  settings environment (\secref{sec:settings}).
47828
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   192
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   193
  The command-line arguments are that of the underlying version of \<^verbatim>\<open>env\<close>. For
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   194
  example, the following invokes an instance of the GNU Bash shell within the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   195
  Isabelle environment:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   196
  @{verbatim [display] \<open>isabelle env bash\<close>}
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   197
\<close>
47828
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   198
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   199
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   200
section \<open>Inspecting the settings environment \label{sec:tool-getenv}\<close>
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   201
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   202
text \<open>The Isabelle settings environment --- as provided by the
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   203
  site-default and user-specific settings files --- can be inspected
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   204
  with the @{tool_def getenv} tool:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   205
  @{verbatim [display]
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   206
\<open>Usage: isabelle getenv [OPTIONS] [VARNAMES ...]
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   207
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   208
  Options are:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   209
    -a           display complete environment
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   210
    -b           print values only (doesn't work for -a)
31497
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   211
    -d FILE      dump complete environment to FILE
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   212
                 (null terminated entries)
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   213
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   214
  Get value of VARNAMES from the Isabelle settings.\<close>}
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   215
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   216
  With the \<^verbatim>\<open>-a\<close> option, one may inspect the full process environment that
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   217
  Isabelle related programs are run in. This usually contains much more
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   218
  variables than are actually Isabelle settings. Normally, output is a list of
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   219
  lines of the form \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close>. The \<^verbatim>\<open>-b\<close> option causes only the values
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   220
  to be printed.
31497
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   221
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   222
  Option \<^verbatim>\<open>-d\<close> produces a dump of the complete environment to the specified
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   223
  file. Entries are terminated by the ASCII null character, i.e.\ the C string
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   224
  terminator.
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   225
\<close>
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   226
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   227
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   228
subsubsection \<open>Examples\<close>
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   229
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   230
text \<open>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   231
  Get the location of @{setting ISABELLE_HOME_USER} where user-specific
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   232
  information is stored:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   233
  @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   234
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 58618
diff changeset
   235
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   236
  Get the value only of the same settings variable, which is particularly
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   237
  useful in shell scripts:
68219
c0341c0080e2 clarified store directories;
wenzelm
parents: 67399
diff changeset
   238
  @{verbatim [display] \<open>isabelle getenv -b ISABELLE_HOME_USER\<close>}
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   239
\<close>
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   240
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   241
71322
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   242
section \<open>Mercurial repository setup \label{sec:hg-setup}\<close>
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   243
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   244
text \<open>
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   245
  The @{tool_def hg_setup} tool simplifies the setup of Mercurial
71325
wenzelm
parents: 71324
diff changeset
   246
  repositories, with hosting via Phabricator (\chref{ch:phabricator}) or SSH
wenzelm
parents: 71324
diff changeset
   247
  file server access.
71322
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   248
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   249
  @{verbatim [display]
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   250
\<open>Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   251
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   252
  Options are:
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   253
    -n NAME      remote repository name (default: base name of LOCAL_DIR)
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   254
    -p PATH      Mercurial path name (default: "default")
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   255
    -r           assume that remote repository already exists
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   256
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   257
  Setup a remote vs. local Mercurial repository: REMOTE either refers to a
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   258
  Phabricator server "user@host" or SSH file server "ssh://user@host/path".\<close>}
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   259
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   260
  The \<^verbatim>\<open>REMOTE\<close> repository specification \<^emph>\<open>excludes\<close> the actual repository
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   261
  name: that is given by the base name of \<^verbatim>\<open>LOCAL_DIR\<close>, or via option \<^verbatim>\<open>-n\<close>.
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   262
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   263
  By default, both sides of the repository are created on demand by default.
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   264
  In contrast, option \<^verbatim>\<open>-r\<close> assumes that the remote repository already exists:
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   265
  it avoids accidental creation of a persistent repository with unintended
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   266
  name.
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   267
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   268
  The local \<^verbatim>\<open>.hg/hgrc\<close> file is changed to refer to the remote repository,
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   269
  usually via the symbolic path name ``\<^verbatim>\<open>default\<close>''; option \<^verbatim>\<open>-p\<close> allows to
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   270
  provided a different name.
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   271
\<close>
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   272
71324
d0e14780b278 more documentation;
wenzelm
parents: 71322
diff changeset
   273
subsubsection \<open>Examples\<close>
d0e14780b278 more documentation;
wenzelm
parents: 71322
diff changeset
   274
d0e14780b278 more documentation;
wenzelm
parents: 71322
diff changeset
   275
text \<open>
d0e14780b278 more documentation;
wenzelm
parents: 71322
diff changeset
   276
  Setup the current directory as a repository with Phabricator server hosting:
d0e14780b278 more documentation;
wenzelm
parents: 71322
diff changeset
   277
  @{verbatim [display] \<open>  isabelle hg_setup vcs@vcs.example.org .\<close>}
d0e14780b278 more documentation;
wenzelm
parents: 71322
diff changeset
   278
d0e14780b278 more documentation;
wenzelm
parents: 71322
diff changeset
   279
  \<^medskip>
d0e14780b278 more documentation;
wenzelm
parents: 71322
diff changeset
   280
  Setup the current directory as a repository with plain SSH server hosting:
d0e14780b278 more documentation;
wenzelm
parents: 71322
diff changeset
   281
  @{verbatim [display] \<open>  isabelle hg_setup ssh://files.example.org/data/repositories .\<close>}
d0e14780b278 more documentation;
wenzelm
parents: 71322
diff changeset
   282
d0e14780b278 more documentation;
wenzelm
parents: 71322
diff changeset
   283
  \<^medskip>
d0e14780b278 more documentation;
wenzelm
parents: 71322
diff changeset
   284
  Both variants require SSH access to the target server, via public key
d0e14780b278 more documentation;
wenzelm
parents: 71322
diff changeset
   285
  without password.
d0e14780b278 more documentation;
wenzelm
parents: 71322
diff changeset
   286
\<close>
d0e14780b278 more documentation;
wenzelm
parents: 71322
diff changeset
   287
71322
0256ce61f405 more documentation;
wenzelm
parents: 68394
diff changeset
   288
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   289
section \<open>Installing standalone Isabelle executables \label{sec:tool-install}\<close>
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   290
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   291
text \<open>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   292
  By default, the main Isabelle binaries (@{executable "isabelle"} etc.) are
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   293
  just run from their location within the distribution directory, probably
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   294
  indirectly by the shell through its @{setting PATH}. Other schemes of
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   295
  installation are supported by the @{tool_def install} tool:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   296
  @{verbatim [display]
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   297
\<open>Usage: isabelle install [OPTIONS] BINDIR
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   298
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   299
  Options are:
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   300
    -d DISTDIR   refer to DISTDIR as Isabelle distribution
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   301
                 (default ISABELLE_HOME)
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   302
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   303
  Install Isabelle executables with absolute references to the
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   304
  distribution directory.\<close>}
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   305
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   306
  The \<^verbatim>\<open>-d\<close> option overrides the current Isabelle distribution directory as
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   307
  determined by @{setting ISABELLE_HOME}.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   308
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   309
  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
   310
  @{executable "isabelle"} and @{executable isabelle_scala_script} should be
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   311
  placed, which is typically a directory in the shell's @{setting PATH}, such
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   312
  as \<^verbatim>\<open>$HOME/bin\<close>.
48815
wenzelm
parents: 48814
diff changeset
   313
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 58618
diff changeset
   314
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   315
  It is also possible to make symbolic links of the main Isabelle executables
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   316
  manually, but making separate copies outside the Isabelle distribution
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   317
  directory will not work!
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   318
\<close>
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   319
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   320
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   321
section \<open>Creating instances of the Isabelle logo\<close>
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   322
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   323
text \<open>
72316
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72309
diff changeset
   324
  The @{tool_def logo} tool creates instances of the generic Isabelle logo,
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72309
diff changeset
   325
  for inclusion in PDF{\LaTeX} documents.
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   326
  @{verbatim [display]
72316
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72309
diff changeset
   327
\<open>Usage: isabelle logo [OPTIONS] [XYZ]
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   328
72316
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72309
diff changeset
   329
  Create instance XYZ of the Isabelle logo (PDF).
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   330
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   331
  Options are:
72316
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72309
diff changeset
   332
    -o FILE      alternative output file (default "isabelle_xyx.pdf")
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   333
    -q           quiet mode\<close>}
48936
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   334
72316
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72309
diff changeset
   335
  Option \<^verbatim>\<open>-o\<close> specifies an alternative output file: the default is
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72309
diff changeset
   336
  \<^verbatim>\<open>isabelle_\<close>\<open>xyz\<close>\<^verbatim>\<open>.pdf\<close> (in lower-case).
48936
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   337
72316
3cc6aa405858 clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents: 72309
diff changeset
   338
  Option \<^verbatim>\<open>-q\<close> omits printing of the resulting output file name.
48936
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   339
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 58618
diff changeset
   340
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   341
  Implementors of Isabelle tools and applications are encouraged to make
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   342
  derived Isabelle logos for their own projects using this template.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   343
\<close>
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   344
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   345
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   346
section \<open>Output the version identifier of the Isabelle distribution\<close>
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   347
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   348
text \<open>
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   349
  The @{tool_def version} tool displays Isabelle version information:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   350
  @{verbatim [display]
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   351
\<open>Usage: isabelle version [OPTIONS]
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   352
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   353
  Options are:
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   354
    -i           short identification (derived from Mercurial id)
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   355
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   356
  Display Isabelle version information.\<close>}
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   357
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 58618
diff changeset
   358
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   359
  The default is to output the full version string of the Isabelle
71578
d59d557f4ee0 updated for release;
wenzelm
parents: 71325
diff changeset
   360
  distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2020: April 2020\<close>.
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   361
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   362
  The \<^verbatim>\<open>-i\<close> option produces a short identification derived from the Mercurial
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
   363
  id of the @{setting ISABELLE_HOME} directory.
58618
782f0b662cae more cartouches;
wenzelm
parents: 57443
diff changeset
   364
\<close>
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   365
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 66785
diff changeset
   366
end