src/Doc/System/Basics.thy
 author wenzelm Sun Sep 21 20:22:12 2014 +0200 (2014-09-21) changeset 58413 22dd971f6938 parent 57581 74bbe9317aa4 child 58553 3876a1a9ee42 permissions -rw-r--r--
renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;
     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 @{file_unchecked "$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.   105 Typically, a user settings file contains only a few lines, with some   106 assignments that are actually changed. Never copy the central   107 @{file "$ISABELLE_HOME/etc/settings"} file!

   108

   109   \end{enumerate}

   110

   111   Since settings files are regular GNU @{executable_def bash} scripts,

   112   one may use complex shell commands, such as @{verbatim "if"} or

   113   @{verbatim "case"} statements to set variables depending on the

   114   system architecture or other environment variables.  Such advanced

   115   features should be added only with great care, though. In

   116   particular, external environment references should be kept at a

   117   minimum.

   118

   119   \medskip A few variables are somewhat special:

   120

   121   \begin{itemize}

   122

   123   \item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set

   124   automatically to the absolute path names of the @{executable

   125   "isabelle_process"} and @{executable isabelle} executables,

   126   respectively.

   127

   128   \item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of

   129   the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and

   130   the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically

   131   to its value.

   132

   133   \end{itemize}

   134

   135   \medskip Note that the settings environment may be inspected with

   136   the @{tool getenv} tool.  This might help to figure out the effect

   137   of complex settings scripts.  *}

   138

   139

   140 subsection {* Common variables *}

   141

   142 text {*

   143   This is a reference of common Isabelle settings variables. Note that

   144   the list is somewhat open-ended. Third-party utilities or interfaces

   145   may add their own selection. Variables that are special in some

   146   sense are marked with @{text "\<^sup>*"}.

   147

   148   \begin{description}

   149

   150   \item[@{setting_def USER_HOME}@{text "\<^sup>*"}] Is the cross-platform

   151   user home directory.  On Unix systems this is usually the same as

   152   @{setting HOME}, but on Windows it is the regular home directory of

   153   the user, not the one of within the Cygwin root

   154   file-system.\footnote{Cygwin itself offers another choice whether

   155   its HOME should point to the \texttt{/home} directory tree or the

   156   Windows user home.}

   157

   158  \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the location of the

   159   top-level Isabelle distribution directory. This is automatically

   160   determined from the Isabelle executable that has been invoked.  Do

   161   not attempt to set @{setting ISABELLE_HOME} yourself from the shell!

   162

   163   \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific

   164   counterpart of @{setting ISABELLE_HOME}. The default value is

   165   relative to @{file_unchecked "$USER_HOME/.isabelle"}, under rare   166 circumstances this may be changed in the global setting file.   167 Typically, the @{setting ISABELLE_HOME_USER} directory mimics   168 @{setting ISABELLE_HOME} to some extend. In particular, site-wide   169 defaults may be overridden by a private @{verbatim   170 "$ISABELLE_HOME_USER/etc/settings"}.

   171

   172   \item[@{setting_def ISABELLE_PLATFORM_FAMILY}@{text "\<^sup>*"}] is

   173   automatically set to the general platform family: @{verbatim linux},

   174   @{verbatim macos}, @{verbatim windows}.  Note that

   175   platform-dependent tools usually need to refer to the more specific

   176   identification according to @{setting ISABELLE_PLATFORM}, @{setting

   177   ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}.

   178

   179   \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically

   180   set to a symbolic identifier for the underlying hardware and

   181   operating system.  The Isabelle platform identification always

   182   refers to the 32 bit variant, even this is a 64 bit machine.  Note

   183   that the ML or Java runtime may have a different idea, depending on

   184   which binaries are actually run.

   185

   186   \item[@{setting_def ISABELLE_PLATFORM64}@{text "\<^sup>*"}] is similar to

   187   @{setting ISABELLE_PLATFORM} but refers to the proper 64 bit variant

   188   on a platform that supports this; the value is empty for 32 bit.

   189   Note that the following bash expression (including the quotes)

   190   prefers the 64 bit platform, if that is available:

   191

   192   @{verbatim [display] "\"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}\""}

   193

   194   \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting

   195   ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path

   196   names of the @{executable "isabelle_process"} and @{executable

   197   isabelle} executables, respectively.  Thus other tools and scripts

   198   need not assume that the @{file "$ISABELLE_HOME/bin"} directory is   199 on the current search path of the shell.   200   201 \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers   202 to the name of this Isabelle distribution, e.g.\ @{verbatim   203 Isabelle2012}''.   204   205 \item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},   206 @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def   207 ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system   208 to be used for Isabelle. There is only a fixed set of admissable   209 @{setting ML_SYSTEM} names (see the @{file   210 "$ISABELLE_HOME/etc/settings"} file of the distribution).

   211

   212   The actual compiler binary will be run from the directory @{setting

   213   ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the

   214   command line.  The optional @{setting ML_PLATFORM} may specify the

   215   binary format of ML heap images, which is useful for cross-platform

   216   installations.  The value of @{setting ML_IDENTIFIER} is

   217   automatically obtained by composing the values of @{setting

   218   ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.

   219

   220   \item[@{setting_def ML_SYSTEM_POLYML}@{text "\<^sup>*"}] is @{verbatim true}

   221   for @{setting ML_SYSTEM} values derived from Poly/ML, as opposed to

   222   SML/NJ where it is empty.  This is particularly useful with the

   223   build option @{system_option condition}

   224   (\secref{sec:system-options}) to restrict big sessions to something

   225   that SML/NJ can still handle.

   226

   227   \item[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK

   228   (Java Development Kit) installation with @{verbatim javac} and

   229   @{verbatim jar} executables.  This is essential for Isabelle/Scala

   230   and other JVM-based tools to work properly.  Note that conventional

   231   @{verbatim JAVA_HOME} usually points to the JRE (Java Runtime

   232   Environment), not JDK.

   233

   234   \item[@{setting_def ISABELLE_PATH}] is a list of directories

   235   (separated by colons) where Isabelle logic images may reside.  When

   236   looking up heaps files, the value of @{setting ML_IDENTIFIER} is

   237   appended to each component internally.

   238

   239   \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a

   240   directory where output heap files should be stored by default. The

   241   ML system and Isabelle version identifier is appended here, too.

   242

   243   \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where

   244   theory browser information (HTML text, graph data, and printable

   245   documents) is stored (see also \secref{sec:info}).  The default

   246   value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}.   247   248 \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to   249 load if none is given explicitely by the user. The default value is   250 @{verbatim HOL}.   251   252 \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the   253 line editor for the @{tool_ref console} interface.   254   255 \item[@{setting_def ISABELLE_LATEX}, @{setting_def   256 ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX}   257 related tools for Isabelle document preparation (see also   258 \secref{sec:tool-latex}).   259   260 \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of   261 directories that are scanned by @{executable isabelle} for external   262 utility programs (see also \secref{sec:isabelle-tool}).   263   264 \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of   265 directories with documentation files.   266   267 \item[@{setting_def PDF_VIEWER}] specifies the program to be used   268 for displaying @{verbatim pdf} files.   269   270 \item[@{setting_def DVI_VIEWER}] specifies the program to be used   271 for displaying @{verbatim dvi} files.   272   273 \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the   274 prefix from which any running @{executable "isabelle_process"}   275 derives an individual directory for temporary files. The default is   276 somewhere in @{file_unchecked "/tmp"}.   277   278 \end{description}   279 *}   280   281   282 subsection {* Additional components \label{sec:components} *}   283   284 text {* Any directory may be registered as an explicit \emph{Isabelle   285 component}. The general layout conventions are that of the main   286 Isabelle distribution itself, and the following two files (both   287 optional) have a special meaning:   288   289 \begin{itemize}   290   291 \item @{verbatim "etc/settings"} holds additional settings that are   292 initialized when bootstrapping the overall Isabelle environment,   293 cf.\ \secref{sec:boot}. As usual, the content is interpreted as a   294 @{verbatim bash} script. It may refer to the component's enclosing   295 directory via the @{verbatim "COMPONENT"} shell variable.   296   297 For example, the following setting allows to refer to files within   298 the component later on, without having to hardwire absolute paths:   299   300 \begin{ttbox}   301 MY_COMPONENT_HOME="$COMPONENT"

   302 \end{ttbox}

   303

   304   Components can also add to existing Isabelle settings such as

   305   @{setting_def ISABELLE_TOOLS}, in order to provide

   306   component-specific tools that can be invoked by end-users.  For

   307   example:

   308

   309 \begin{ttbox}

   310 ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"

   311 \end{ttbox}

   312

   313   \item @{verbatim "etc/components"} holds a list of further

   314   sub-components of the same structure.  The directory specifications

   315   given here can be either absolute (with leading @{verbatim "/"}) or

   316   relative to the component's main directory.

   317

   318   \end{itemize}

   319

   320   The root of component initialization is @{setting ISABELLE_HOME}

   321   itself.  After initializing all of its sub-components recursively,

   322   @{setting ISABELLE_HOME_USER} is included in the same manner (if

   323   that directory exists).  This allows to install private components

   324   via @{file_unchecked "$ISABELLE_HOME_USER/etc/components"}, although it is   325 often more convenient to do that programmatically via the   326 \verb,init_component, shell function in the \verb,etc/settings,   327 script of \verb,$ISABELLE_HOME_USER, (or any other component

   328   directory).  For example:

   329 \begin{ttbox}

   330 init_component "$HOME/screwdriver-2.0"   331 \end{ttbox}   332   333 This is tolerant wrt.\ missing component directories, but might   334 produce a warning.   335   336 \medskip More complex situations may be addressed by initializing   337 components listed in a given catalog file, relatively to some base   338 directory:   339   340 \begin{ttbox}   341 init_components "$HOME/my_component_store" "some_catalog_file"

   342 \end{ttbox}

   343

   344   The component directories listed in the catalog file are treated as

   345   relative to the given base directory.

   346

   347   See also \secref{sec:tool-components} for some tool-support for

   348   resolving components that are formally initialized but not installed

   349   yet.

   350 *}

   351

   352

   353 section {* The raw Isabelle process \label{sec:isabelle-process} *}

   354

   355 text {*

   356   The @{executable_def "isabelle_process"} executable runs bare-bones

   357   Isabelle logic sessions --- either interactively or in batch mode.

   358   It provides an abstraction over the underlying ML system, and over

   359   the actual heap file locations.  Its usage is:

   360

   361 \begin{ttbox}

   362 Usage: isabelle_process [OPTIONS] [INPUT] [OUTPUT]

   363

   364   Options are:

   365     -I           startup Isar interaction mode

   366     -O           system options from given YXML file

   367     -P           startup Proof General interaction mode

   368     -S           secure mode -- disallow critical operations

   369     -T ADDR      startup process wrapper, with socket address

   370     -W IN:OUT    startup process wrapper, with input/output fifos

   371     -e MLTEXT    pass MLTEXT to the ML session

   372     -m MODE      add print mode for output

   373     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)

   374     -q           non-interactive session

   375     -r           open heap file read-only

   376     -w           reset write permissions on OUTPUT

   377

   378   INPUT (default "\\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.

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

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

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

   382 \end{ttbox}

   383

   384   Input files without path specifications are looked up in the

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

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

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

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

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

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

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

   392   refer to the current directory).

   393 *}

   394

   395

   396 subsubsection {* Options *}

   397

   398 text {*

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

   400   the @{verbatim "-r"} option is given explicitly, then the session

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

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

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

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

   405   line).

   406

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

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

   409   require considerable amounts of disk space (approximately

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

   411   heap files when they are no longer needed.

   412

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

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

   415   logic image to be read-only automatically.

   416

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

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

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

   420   may happen when erroneous ML code is provided. Also make sure that

   421   the ML commands are terminated properly by semicolon.

   422

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

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

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

   426   symbols.

   427

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

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

   430   option inhibits interaction, thus providing a pure batch mode

   431   facility.

   432

   433   \medskip Option @{verbatim "-o"} allows to override Isabelle system

   434   options for this process, see also \secref{sec:system-options}.

   435   Alternatively, option @{verbatim "-O"} specifies the full environment of

   436   system options as a file in YXML format (according to the Isabelle/Scala

   437   function @{verbatim isabelle.Options.encode}).

   438

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

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

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

   442   interaction with the Proof General user interface.

   443

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

   445   Isabelle enter a special process wrapper for interaction via

   446   Isabelle/Scala, see also @{file

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

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

   449

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

   451   secure by disabling some critical operations, notably runtime

   452   compilation and evaluation of ML source code.

   453 *}

   454

   455

   456 subsubsection {* Examples *}

   457

   458 text {*

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

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

   461 \begin{ttbox}

   462 isabelle_process

   463 \end{ttbox}

   464

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

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

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

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

   469   may be invoked as follows:

   470 \begin{ttbox}

   471 isabelle_process HOL Test

   472 \end{ttbox}

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

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

   475   than 100\,MB):

   476

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

   478   writable state) by:

   479 \begin{ttbox}

   480 isabelle_process Test

   481 \end{ttbox}

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

   483 \begin{ttbox}

   484 isabelle_process -r Test

   485 \end{ttbox}

   486

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

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

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

   490   vs.\ ML):

   491 \begin{ttbox}

   492 isabelle_process -e 'Thy_Info.get_theory "Main";' -q -r HOL

   493 \end{ttbox}

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

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

   496   allows to communicate with the Isabelle process via an external

   497   program in a more robust fashion.

   498 *}

   499

   500

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

   502

   503 text {*

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

   505   wrapper --- @{executable isabelle}:

   506

   507 \begin{ttbox}

   508 Usage: isabelle TOOL [ARGS ...]

   509

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

   511

   512 Available tools:

   513   \dots

   514 \end{ttbox}

   515

   516   In principle, Isabelle tools are ordinary executable scripts that

   517   are run within the Isabelle settings environment, see

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

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

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

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

   522   shell's search path!

   523 *}

   524

   525

   526 subsubsection {* Examples *}

   527

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

   529   distribution:

   530

   531 \begin{ttbox}

   532   isabelle doc

   533 \end{ttbox}

   534

   535   View a certain document as follows:

   536 \begin{ttbox}

   537   isabelle doc system

   538 \end{ttbox}

   539

   540   Query the Isabelle settings environment:

   541 \begin{ttbox}

   542   isabelle getenv ISABELLE_HOME_USER

   543 \end{ttbox}

   544 *}

   545

   546 end