src/Doc/System/Basics.thy
 author wenzelm Sat Jan 26 16:10:50 2013 +0100 (2013-01-26) changeset 51057 a22b134f862e parent 50197 b385d134926d child 51434 e19a22974c72 permissions -rw-r--r--
updated explanations of document preparation;
     1 theory Basics

     2 imports Base

     3 begin

     4

     5 chapter {* The Isabelle system environment *}

     6

     7 text {* This manual describes Isabelle together with related tools and

     8   user interfaces as seen from a system oriented view.  See also the

     9   \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for

    10   the actual Isabelle input language and related concepts, and

    11   \emph{The Isabelle/Isar Implementation

    12   Manual}~\cite{isabelle-implementation} for the main concepts of the

    13   underlying implementation in Isabelle/ML.

    14

    15   \medskip The Isabelle system environment provides the following

    16   basic infrastructure to integrate tools smoothly.

    17

    18   \begin{enumerate}

    19

    20   \item The \emph{Isabelle settings} mechanism provides process

    21   environment variables to all Isabelle executables (including tools

    22   and user interfaces).

    23

    24   \item The raw \emph{Isabelle process} (@{executable_ref

    25   "isabelle-process"}) runs logic sessions either interactively or in

    26   batch mode.  In particular, this view abstracts over the invocation

    27   of the actual ML system to be used.  Regular users rarely need to

    28   care about the low-level process.

    29

    30   \item The main \emph{Isabelle tool wrapper} (@{executable_ref

    31   isabelle}) provides a generic startup environment Isabelle related

    32   utilities, user interfaces etc.  Such tools automatically benefit

    33   from the settings mechanism.

    34

    35   \end{enumerate}

    36 *}

    37

    38

    39 section {* Isabelle settings \label{sec:settings} *}

    40

    41 text {*

    42   The Isabelle system heavily depends on the \emph{settings

    43   mechanism}\indexbold{settings}.  Essentially, this is a statically

    44   scoped collection of environment variables, such as @{setting

    45   ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting ML_HOME}.  These

    46   variables are \emph{not} intended to be set directly from the shell,

    47   though.  Isabelle employs a somewhat more sophisticated scheme of

    48   \emph{settings files} --- one for site-wide defaults, another for

    49   additional user-specific modifications.  With all configuration

    50   variables in clearly defined places, this scheme is more

    51   maintainable and user-friendly than global shell environment

    52   variables.

    53

    54   In particular, we avoid the typical situation where prospective

    55   users of a software package are told to put several things into

    56   their shell startup scripts, before being able to actually run the

    57   program. Isabelle requires none such administrative chores of its

    58   end-users --- the executables can be invoked straight away.

    59   Occasionally, users would still want to put the @{file

    60   "$ISABELLE_HOME/bin"} directory into their shell's search path, but   61 this is not required.   62 *}   63   64   65 subsection {* Bootstrapping the environment \label{sec:boot} *}   66   67 text {* Isabelle executables need to be run within a proper settings   68 environment. This is bootstrapped as described below, on the first   69 invocation of one of the outer wrapper scripts (such as   70 @{executable_ref isabelle}). This happens only once for each   71 process tree, i.e.\ the environment is passed to subprocesses   72 according to regular Unix conventions.   73   74 \begin{enumerate}   75   76 \item The special variable @{setting_def ISABELLE_HOME} is   77 determined automatically from the location of the binary that has   78 been run.   79   80 You should not try to set @{setting ISABELLE_HOME} manually. Also   81 note that the Isabelle executables either have to be run from their   82 original location in the distribution directory, or via the   83 executable objects created by the @{tool install} tool. Symbolic   84 links are admissible, but a plain copy of the @{file   85 "$ISABELLE_HOME/bin"} files will not work!

    86

    87   \item The file @{file "$ISABELLE_HOME/etc/settings"} is run as a   88 @{executable_ref bash} shell script with the auto-export option for   89 variables enabled.   90   91 This file holds a rather long list of shell variable assigments,   92 thus providing the site-wide default settings. The Isabelle   93 distribution already contains a global settings file with sensible   94 defaults for most variables. When installing the system, only a few   95 of these may have to be adapted (probably @{setting ML_SYSTEM}   96 etc.).   97   98 \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it

    99   exists) is run in the same way as the site default settings. Note

   100   that the variable @{setting ISABELLE_HOME_USER} has already been set

   101   before --- usually to something like @{verbatim

   102   "$USER_HOME/.isabelle/IsabelleXXXX"}.   103   104 Thus individual users may override the site-wide defaults. See also   105 file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the

   106   distribution.  Typically, a user settings file would contain only a

   107   few lines, just the assigments that are really changed.  One should

   108   definitely \emph{not} start with a full copy the basic @{file

   109   "$ISABELLE_HOME/etc/settings"}. This could cause very annoying   110 maintainance problems later, when the Isabelle installation is   111 updated or changed otherwise.   112   113 \end{enumerate}   114   115 Since settings files are regular GNU @{executable_def bash} scripts,   116 one may use complex shell commands, such as @{verbatim "if"} or   117 @{verbatim "case"} statements to set variables depending on the   118 system architecture or other environment variables. Such advanced   119 features should be added only with great care, though. In   120 particular, external environment references should be kept at a   121 minimum.   122   123 \medskip A few variables are somewhat special:   124   125 \begin{itemize}   126   127 \item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set   128 automatically to the absolute path names of the @{executable   129 "isabelle-process"} and @{executable isabelle} executables,   130 respectively.   131   132 \item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of   133 the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and   134 the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically   135 to its value.   136   137 \end{itemize}   138   139 \medskip Note that the settings environment may be inspected with   140 the @{tool getenv} tool. This might help to figure out the effect   141 of complex settings scripts. *}   142   143   144 subsection {* Common variables *}   145   146 text {*   147 This is a reference of common Isabelle settings variables. Note that   148 the list is somewhat open-ended. Third-party utilities or interfaces   149 may add their own selection. Variables that are special in some   150 sense are marked with @{text "\<^sup>*"}.   151   152 \begin{description}   153   154 \item[@{setting_def USER_HOME}@{text "\<^sup>*"}] Is the cross-platform   155 user home directory. On Unix systems this is usually the same as   156 @{setting HOME}, but on Windows it is the regular home directory of   157 the user, not the one of within the Cygwin root   158 file-system.\footnote{Cygwin itself offers another choice whether   159 its HOME should point to the \texttt{/home} directory tree or the   160 Windows user home.}   161   162 \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the location of the   163 top-level Isabelle distribution directory. This is automatically   164 determined from the Isabelle executable that has been invoked. Do   165 not attempt to set @{setting ISABELLE_HOME} yourself from the shell!   166   167 \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific   168 counterpart of @{setting ISABELLE_HOME}. The default value is   169 relative to @{verbatim "$USER_HOME/.isabelle"}, under rare

   170   circumstances this may be changed in the global setting file.

   171   Typically, the @{setting ISABELLE_HOME_USER} directory mimics

   172   @{setting ISABELLE_HOME} to some extend. In particular, site-wide

   173   defaults may be overridden by a private @{verbatim

   174   "$ISABELLE_HOME_USER/etc/settings"}.   175   176 \item[@{setting_def ISABELLE_PLATFORM_FAMILY}@{text "\<^sup>*"}] is   177 automatically set to the general platform family: @{verbatim linux},   178 @{verbatim macos}, @{verbatim windows}. Note that   179 platform-dependent tools usually need to refer to the more specific   180 identification according to @{setting ISABELLE_PLATFORM}, @{setting   181 ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}.   182   183 \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically   184 set to a symbolic identifier for the underlying hardware and   185 operating system. The Isabelle platform identification always   186 refers to the 32 bit variant, even this is a 64 bit machine. Note   187 that the ML or Java runtime may have a different idea, depending on   188 which binaries are actually run.   189   190 \item[@{setting_def ISABELLE_PLATFORM64}@{text "\<^sup>*"}] is similar to   191 @{setting ISABELLE_PLATFORM} but refers to the proper 64 bit variant   192 on a platform that supports this; the value is empty for 32 bit.   193 Note that the following bash expression (including the quotes)   194 prefers the 64 bit platform, if that is available:   195   196 @{verbatim [display] "\"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}\""}   197   198 \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting   199 ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path   200 names of the @{executable "isabelle-process"} and @{executable   201 isabelle} executables, respectively. Thus other tools and scripts   202 need not assume that the @{file "$ISABELLE_HOME/bin"} directory is

   203   on the current search path of the shell.

   204

   205   \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers

   206   to the name of this Isabelle distribution, e.g.\ @{verbatim

   207   Isabelle2012}''.

   208

   209   \item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},

   210   @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def

   211   ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system

   212   to be used for Isabelle.  There is only a fixed set of admissable

   213   @{setting ML_SYSTEM} names (see the @{file

   214   "$ISABELLE_HOME/etc/settings"} file of the distribution).   215   216 The actual compiler binary will be run from the directory @{setting   217 ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the   218 command line. The optional @{setting ML_PLATFORM} may specify the   219 binary format of ML heap images, which is useful for cross-platform   220 installations. The value of @{setting ML_IDENTIFIER} is   221 automatically obtained by composing the values of @{setting   222 ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.   223   224 \item[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK   225 (Java Development Kit) installation with @{verbatim javac} and   226 @{verbatim jar} executables. This is essential for Isabelle/Scala   227 and other JVM-based tools to work properly. Note that conventional   228 @{verbatim JAVA_HOME} usually points to the JRE (Java Runtime   229 Environment), not JDK.   230   231 \item[@{setting_def ISABELLE_PATH}] is a list of directories   232 (separated by colons) where Isabelle logic images may reside. When   233 looking up heaps files, the value of @{setting ML_IDENTIFIER} is   234 appended to each component internally.   235   236 \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a   237 directory where output heap files should be stored by default. The   238 ML system and Isabelle version identifier is appended here, too.   239   240 \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where   241 theory browser information (HTML text, graph data, and printable   242 documents) is stored (see also \secref{sec:info}). The default   243 value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}.

   244

   245   \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to

   246   load if none is given explicitely by the user.  The default value is

   247   @{verbatim HOL}.

   248

   249   \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default

   250   line editor for the @{tool_ref tty} interface.

   251

   252   \item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed

   253   to the command line of any @{tool_ref usedir} invocation. This

   254   typically contains compilation options for object-logics --- @{tool

   255   usedir} is the basic tool for managing logic sessions (cf.\ the

   256   @{verbatim IsaMakefile}s in the distribution).

   257

   258   \item[@{setting_def ISABELLE_LATEX}, @{setting_def

   259   ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def

   260   ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle

   261   document preparation (see also \secref{sec:tool-latex}).

   262

   263   \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of

   264   directories that are scanned by @{executable isabelle} for external

   265   utility programs (see also \secref{sec:isabelle-tool}).

   266

   267   \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of

   268   directories with documentation files.

   269

   270   \item[@{setting_def ISABELLE_DOC_FORMAT}] specifies the preferred

   271   document format, typically @{verbatim pdf} or @{verbatim dvi}.

   272

   273   \item[@{setting_def PDF_VIEWER}] specifies the command-line to be

   274   used for displaying @{verbatim pdf} files.

   275

   276   \item[@{setting_def DVI_VIEWER}] specifies the command-line to be

   277   used for displaying @{verbatim dvi} files.

   278

   279   \item[@{setting_def PRINT_COMMAND}] specifies the standard printer

   280   spool command, which is expected to accept @{verbatim ps} files.

   281

   282   \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the

   283   prefix from which any running @{executable "isabelle-process"}

   284   derives an individual directory for temporary files.  The default is

   285   somewhere in @{verbatim "/tmp"}.

   286

   287   \end{description}

   288 *}

   289

   290

   291 subsection {* Additional components \label{sec:components} *}

   292

   293 text {* Any directory may be registered as an explicit \emph{Isabelle

   294   component}.  The general layout conventions are that of the main

   295   Isabelle distribution itself, and the following two files (both

   296   optional) have a special meaning:

   297

   298   \begin{itemize}

   299

   300   \item @{verbatim "etc/settings"} holds additional settings that are

   301   initialized when bootstrapping the overall Isabelle environment,

   302   cf.\ \secref{sec:boot}.  As usual, the content is interpreted as a

   303   @{verbatim bash} script.  It may refer to the component's enclosing

   304   directory via the @{verbatim "COMPONENT"} shell variable.

   305

   306   For example, the following setting allows to refer to files within

   307   the component later on, without having to hardwire absolute paths:

   308

   309 \begin{ttbox}

   310 MY_COMPONENT_HOME="$COMPONENT"   311 \end{ttbox}   312   313 Components can also add to existing Isabelle settings such as   314 @{setting_def ISABELLE_TOOLS}, in order to provide   315 component-specific tools that can be invoked by end-users. For   316 example:   317   318 \begin{ttbox}   319 ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"   320 \end{ttbox}   321   322 \item @{verbatim "etc/components"} holds a list of further   323 sub-components of the same structure. The directory specifications   324 given here can be either absolute (with leading @{verbatim "/"}) or   325 relative to the component's main directory.   326   327 \end{itemize}   328   329 The root of component initialization is @{setting ISABELLE_HOME}   330 itself. After initializing all of its sub-components recursively,   331 @{setting ISABELLE_HOME_USER} is included in the same manner (if   332 that directory exists). This allows to install private components   333 via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is

   334   often more convenient to do that programmatically via the

   335   \verb,init_component, shell function in the \verb,etc/settings,

   336   script of \verb,$ISABELLE_HOME_USER, (or any other component   337 directory). For example:   338 \begin{ttbox}   339 init_component "$HOME/screwdriver-2.0"

   340 \end{ttbox}

   341

   342   This is tolerant wrt.\ missing component directories, but might

   343   produce a warning.

   344

   345   \medskip More complex situations may be addressed by initializing

   346   components listed in a given catalog file, relatively to some base

   347   directory:

   348

   349 \begin{ttbox}

   350 init_components "$HOME/my_component_store" "some_catalog_file"   351 \end{ttbox}   352   353 The component directories listed in the catalog file are treated as   354 relative to the given base directory.   355   356 See also \secref{sec:tool-components} for some tool-support for   357 resolving components that are formally initialized but not installed   358 yet.   359 *}   360   361   362 section {* The raw Isabelle process *}   363   364 text {*   365 The @{executable_def "isabelle-process"} executable runs bare-bones   366 Isabelle logic sessions --- either interactively or in batch mode.   367 It provides an abstraction over the underlying ML system, and over   368 the actual heap file locations. Its usage is:   369   370 \begin{ttbox}   371 Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]   372   373 Options are:   374 -I startup Isar interaction mode   375 -P startup Proof General interaction mode   376 -S secure mode -- disallow critical operations   377 -T ADDR startup process wrapper, with socket address   378 -W IN:OUT startup process wrapper, with input/output fifos   379 -X startup PGIP interaction mode   380 -e MLTEXT pass MLTEXT to the ML session   381 -f pass 'Session.finish();' to the ML session   382 -m MODE add print mode for output   383 -q non-interactive session   384 -r open heap file read-only   385 -u pass 'use"ROOT.ML";' to the ML session   386 -w reset write permissions on OUTPUT   387   388 INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.

   389   These are either names to be searched in the Isabelle path, or

   390   actual file names (containing at least one /).

   391   If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.

   392 \end{ttbox}

   393

   394   Input files without path specifications are looked up in the

   395   @{setting ISABELLE_PATH} setting, which may consist of multiple

   396   components separated by colons --- these are tried in the given

   397   order with the value of @{setting ML_IDENTIFIER} appended

   398   internally.  In a similar way, base names are relative to the

   399   directory specified by @{setting ISABELLE_OUTPUT}.  In any case,

   400   actual file locations may also be given by including at least one

   401   slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to

   402   refer to the current directory).

   403 *}

   404

   405

   406 subsubsection {* Options *}

   407

   408 text {*

   409   If the input heap file does not have write permission bits set, or

   410   the @{verbatim "-r"} option is given explicitely, then the session

   411   started will be read-only.  That is, the ML world cannot be

   412   committed back into the image file.  Otherwise, a writable session

   413   enables commits into either the input file, or into another output

   414   heap file (if that is given as the second argument on the command

   415   line).

   416

   417   The read-write state of sessions is determined at startup only, it

   418   cannot be changed intermediately. Also note that heap images may

   419   require considerable amounts of disk space (approximately

   420   50--200~MB). Users are responsible for themselves to dispose their

   421   heap files when they are no longer needed.

   422

   423   \medskip The @{verbatim "-w"} option makes the output heap file

   424   read-only after terminating.  Thus subsequent invocations cause the

   425   logic image to be read-only automatically.

   426

   427   \medskip Using the @{verbatim "-e"} option, arbitrary ML code may be

   428   passed to the Isabelle session from the command line. Multiple

   429   @{verbatim "-e"}'s are evaluated in the given order. Strange things

   430   may happen when errorneous ML code is provided. Also make sure that

   431   the ML commands are terminated properly by semicolon.

   432

   433   \medskip The @{verbatim "-u"} option is a shortcut for @{verbatim

   434   "-e"} passing @{verbatim "use \"ROOT.ML\";"}'' to the ML session.

   435   The @{verbatim "-f"} option passes @{verbatim

   436   "Session.finish();"}'', which is intended mainly for administrative

   437   purposes.

   438

   439   \medskip The @{verbatim "-m"} option adds identifiers of print modes

   440   to be made active for this session. Typically, this is used by some

   441   user interface, e.g.\ to enable output of proper mathematical

   442   symbols.

   443

   444   \medskip Isabelle normally enters an interactive top-level loop

   445   (after processing the @{verbatim "-e"} texts). The @{verbatim "-q"}

   446   option inhibits interaction, thus providing a pure batch mode

   447   facility.

   448

   449   \medskip The @{verbatim "-I"} option makes Isabelle enter Isar

   450   interaction mode on startup, instead of the primitive ML top-level.

   451   The @{verbatim "-P"} option configures the top-level loop for

   452   interaction with the Proof General user interface, and the

   453   @{verbatim "-X"} option enables XML-based PGIP communication.

   454

   455   \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes

   456   Isabelle enter a special process wrapper for interaction via

   457   Isabelle/Scala, see also @{file

   458   "~~/src/Pure/System/isabelle_process.scala"}.  The protocol between

   459   the ML and JVM process is private to the implementation.

   460

   461   \medskip The @{verbatim "-S"} option makes the Isabelle process more

   462   secure by disabling some critical operations, notably runtime

   463   compilation and evaluation of ML source code.

   464 *}

   465

   466

   467 subsubsection {* Examples *}

   468

   469 text {*

   470   Run an interactive session of the default object-logic (as specified

   471   by the @{setting ISABELLE_LOGIC} setting) like this:

   472 \begin{ttbox}

   473 isabelle-process

   474 \end{ttbox}

   475

   476   Usually @{setting ISABELLE_LOGIC} refers to one of the standard

   477   logic images, which are read-only by default.  A writable session

   478   --- based on @{verbatim HOL}, but output to @{verbatim Test} (in the

   479   directory specified by the @{setting ISABELLE_OUTPUT} setting) ---

   480   may be invoked as follows:

   481 \begin{ttbox}

   482 isabelle-process HOL Test

   483 \end{ttbox}

   484   Ending this session normally (e.g.\ by typing control-D) dumps the

   485   whole ML system state into @{verbatim Test} (be prepared for more

   486   than 100\,MB):

   487

   488   The @{verbatim Test} session may be continued later (still in

   489   writable state) by:

   490 \begin{ttbox}

   491 isabelle-process Test

   492 \end{ttbox}

   493   A read-only @{verbatim Test} session may be started by:

   494 \begin{ttbox}

   495 isabelle-process -r Test

   496 \end{ttbox}

   497

   498   \bigskip The next example demonstrates batch execution of Isabelle.

   499   We retrieve the @{verbatim Main} theory value from the theory loader

   500   within ML (observe the delicate quoting rules for the Bash shell

   501   vs.\ ML):

   502 \begin{ttbox}

   503 isabelle-process -e 'Thy_Info.get_theory "Main";' -q -r HOL

   504 \end{ttbox}

   505   Note that the output text will be interspersed with additional junk

   506   messages by the ML runtime environment.  The @{verbatim "-W"} option

   507   allows to communicate with the Isabelle process via an external

   508   program in a more robust fashion.

   509 *}

   510

   511

   512 section {* The Isabelle tool wrapper \label{sec:isabelle-tool} *}

   513

   514 text {*

   515   All Isabelle related tools and interfaces are called via a common

   516   wrapper --- @{executable isabelle}:

   517

   518 \begin{ttbox}

   519 Usage: isabelle TOOL [ARGS ...]

   520

   521   Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.

   522

   523 Available tools:

   524   \dots

   525 \end{ttbox}

   526

   527   In principle, Isabelle tools are ordinary executable scripts that

   528   are run within the Isabelle settings environment, see

   529   \secref{sec:settings}.  The set of available tools is collected by

   530   @{executable isabelle} from the directories listed in the @{setting

   531   ISABELLE_TOOLS} setting.  Do not try to call the scripts directly

   532   from the shell.  Neither should you add the tool directories to your

   533   shell's search path!

   534 *}

   535

   536

   537 subsubsection {* Examples *}

   538

   539 text {* Show the list of available documentation of the Isabelle

   540   distribution:

   541

   542 \begin{ttbox}

   543   isabelle doc

   544 \end{ttbox}

   545

   546   View a certain document as follows:

   547 \begin{ttbox}

   548   isabelle doc system

   549 \end{ttbox}

   550

   551   Query the Isabelle settings environment:

   552 \begin{ttbox}

   553   isabelle getenv ISABELLE_HOME_USER

   554 \end{ttbox}

   555 *}

   556

   557 end