doc-src/System/Thy/Basics.thy
 author wenzelm Wed Sep 21 22:18:17 2011 +0200 (2011-09-21) changeset 45028 d608dd8cd409 parent 43564 9864182c6bad child 47661 012a887997f3 permissions -rw-r--r--
alternative Socket_Channel;
use BinIO for fifos uniformly;
     1 theory Basics

     2 imports Base

     3 begin

     4

     5 chapter {* The Isabelle system environment *}

     6

     7 text {*

     8   This manual describes Isabelle together with related tools and user

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

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

    11   the actual Isabelle input language and related concepts.

    12

    13   \medskip The Isabelle system environment provides the following

    14   basic infrastructure to integrate tools smoothly.

    15

    16   \begin{enumerate}

    17

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

    19   environment variables to all Isabelle executables (including tools

    20   and user interfaces).

    21

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

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

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

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

    26   care about the low-level process.

    27

    28   \item The \emph{Isabelle tools wrapper} (@{executable_ref isabelle})

    29   provides a generic startup environment Isabelle related utilities,

    30   user interfaces etc.  Such tools automatically benefit from the

    31   settings mechanism.

    32

    33   \end{enumerate}

    34 *}

    35

    36

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

    38

    39 text {*

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

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

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

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

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

    45   though.  Isabelle employs a somewhat more sophisticated scheme of

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

    47   additional user-specific modifications.  With all configuration

    48   variables in at most two places, this scheme is more maintainable

    49   and user-friendly than global shell environment variables.

    50

    51   In particular, we avoid the typical situation where prospective

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

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

    54   program. Isabelle requires none such administrative chores of its

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

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

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

    83

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

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

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

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

    99   "$HOME/.isabelle/IsabelleXXXX"}.   100   101 Thus individual users may override the site-wide defaults. See also   102 file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the

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

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

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

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

   161   this may be changed in the global setting file.  Typically, the

   162   @{setting ISABELLE_HOME_USER} directory mimics @{setting

   163   ISABELLE_HOME} to some extend. In particular, site-wide defaults may

   164   be overridden by a private @{verbatim

   165   "$ISABELLE_HOME_USER/etc/settings"}.   166   167 \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically   168 set to a symbolic identifier for the underlying hardware and   169 operating system. The Isabelle platform identification always   170 refers to the 32 bit variant, even this is a 64 bit machine. Note   171 that the ML or Java runtime may have a different idea, depending on   172 which binaries are actually run.   173   174 \item[@{setting_def ISABELLE_PLATFORM64}@{text "\<^sup>*"}] is similar to   175 @{setting ISABELLE_PLATFORM} but refers to the proper 64 bit variant   176 on a platform that supports this; the value is empty for 32 bit.   177   178 \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting   179 ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path   180 names of the @{executable "isabelle-process"} and @{executable   181 isabelle} executables, respectively. Thus other tools and scripts   182 need not assume that the @{file "$ISABELLE_HOME/bin"} directory is

   183   on the current search path of the shell.

   184

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

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

   187   Isabelle2011}''.

   188

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

   190   @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def

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

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

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

   194   "$ISABELLE_HOME/etc/settings"} file of the distribution).   195   196 The actual compiler binary will be run from the directory @{setting   197 ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the   198 command line. The optional @{setting ML_PLATFORM} may specify the   199 binary format of ML heap images, which is useful for cross-platform   200 installations. The value of @{setting ML_IDENTIFIER} is   201 automatically obtained by composing the values of @{setting   202 ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.   203   204 \item[@{setting_def ISABELLE_PATH}] is a list of directories   205 (separated by colons) where Isabelle logic images may reside. When   206 looking up heaps files, the value of @{setting ML_IDENTIFIER} is   207 appended to each component internally.   208   209 \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a   210 directory where output heap files should be stored by default. The   211 ML system and Isabelle version identifier is appended here, too.   212   213 \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where   214 theory browser information (HTML text, graph data, and printable   215 documents) is stored (see also \secref{sec:info}). The default   216 value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}.

   217

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

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

   220   @{verbatim HOL}.

   221

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

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

   224

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

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

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

   228   usedir} is the basic utility for managing logic sessions (cf.\ the

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

   230

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

   232   ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def

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

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

   235

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

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

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

   239

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

   241   directories with documentation files.

   242

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

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

   245

   246   \item[@{setting_def DVI_VIEWER}] specifies the command to be used

   247   for displaying @{verbatim dvi} files.

   248

   249   \item[@{setting_def PDF_VIEWER}] specifies the command to be used

   250   for displaying @{verbatim pdf} files.

   251

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

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

   254

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

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

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

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

   259

   260   \end{description}

   261 *}

   262

   263

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

   265

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

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

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

   269   optional) have a special meaning:

   270

   271   \begin{itemize}

   272

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

   274   initialized when bootstrapping the overall Isabelle environment,

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

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

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

   278

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

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

   281

   282   \begin{ttbox}

   283   MY_COMPONENT_HOME="$COMPONENT"   284 \end{ttbox}   285   286 Components can also add to existing Isabelle settings such as   287 @{setting_def ISABELLE_TOOLS}, in order to provide   288 component-specific tools that can be invoked by end-users. For   289 example:   290   291 \begin{ttbox}   292 ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"   293 \end{ttbox}   294   295 \item @{verbatim "etc/components"} holds a list of further   296 sub-components of the same structure. The directory specifications   297 given here can be either absolute (with leading @{verbatim "/"}) or   298 relative to the component's main directory.   299   300 \end{itemize}   301   302 The root of component initialization is @{setting ISABELLE_HOME}   303 itself. After initializing all of its sub-components recursively,   304 @{setting ISABELLE_HOME_USER} is included in the same manner (if   305 that directory exists). This allows to install private components   306 via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is

   307   often more convenient to do that programmatically via the

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

   309   script of \verb,$ISABELLE_HOME_USER, (or any other component   310 directory). For example:   311 \begin{verbatim}   312 if [ -d "$HOME/screwdriver-2.0" ]

   313   then

   314     init_component "$HOME/screwdriver-2.0"   315 else   316 \end{verbatim}   317 *}   318   319   320 section {* The raw Isabelle process *}   321   322 text {*   323 The @{executable_def "isabelle-process"} executable runs bare-bones   324 Isabelle logic sessions --- either interactively or in batch mode.   325 It provides an abstraction over the underlying ML system, and over   326 the actual heap file locations. Its usage is:   327   328 \begin{ttbox}   329 Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]   330   331 Options are:   332 -I startup Isar interaction mode   333 -P startup Proof General interaction mode   334 -S secure mode -- disallow critical operations   335 -T ADDR startup process wrapper, with socket address   336 -W IN:OUT startup process wrapper, with input/output fifos   337 -X startup PGIP interaction mode   338 -e MLTEXT pass MLTEXT to the ML session   339 -f pass 'Session.finish();' to the ML session   340 -m MODE add print mode for output   341 -q non-interactive session   342 -r open heap file read-only   343 -u pass 'use"ROOT.ML";' to the ML session   344 -w reset write permissions on OUTPUT   345   346 INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.

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

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

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

   350 \end{ttbox}

   351

   352   Input files without path specifications are looked up in the

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

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

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

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

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

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

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

   360   refer to the current directory).

   361 *}

   362

   363

   364 subsubsection {* Options *}

   365

   366 text {*

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

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

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

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

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

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

   373   line).

   374

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

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

   377   require considerable amounts of disk space (approximately

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

   379   heap files when they are no longer needed.

   380

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

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

   383   logic image to be read-only automatically.

   384

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

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

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

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

   389   the ML commands are terminated properly by semicolon.

   390

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

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

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

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

   395   purposes.

   396

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

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

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

   400   symbols.

   401

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

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

   404   option inhibits interaction, thus providing a pure batch mode

   405   facility.

   406

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

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

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

   410   interaction with the Proof General user interface, and the

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

   412

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

   414   Isabelle enter a special process wrapper for interaction via the

   415   Isabelle/Scala layer, see also @{file

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

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

   418

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

   420   secure by disabling some critical operations, notably runtime

   421   compilation and evaluation of ML source code.

   422 *}

   423

   424

   425 subsubsection {* Examples *}

   426

   427 text {*

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

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

   430 \begin{ttbox}

   431 isabelle-process

   432 \end{ttbox}

   433

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

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

   436   --- based on @{verbatim FOL}, but output to @{verbatim Foo} (in the

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

   438   may be invoked as follows:

   439 \begin{ttbox}

   440 isabelle-process FOL Foo

   441 \end{ttbox}

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

   443   whole ML system state into @{verbatim Foo}. Be prepared for several

   444   tens of megabytes.

   445

   446   The @{verbatim Foo} session may be continued later (still in

   447   writable state) by:

   448 \begin{ttbox}

   449 isabelle-process Foo

   450 \end{ttbox}

   451   A read-only @{verbatim Foo} session may be started by:

   452 \begin{ttbox}

   453 isabelle-process -r Foo

   454 \end{ttbox}

   455

   456   \medskip Note that manual session management like this does

   457   \emph{not} provide proper setup for theory presentation.  This would

   458   require the @{tool usedir} utility.

   459

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

   461   We retrieve the @{verbatim FOL} theory value from the theory loader

   462   within ML:

   463 \begin{ttbox}

   464 isabelle-process -e 'theory "FOL";' -q -r FOL

   465 \end{ttbox}

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

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

   468   allows to communicate with the Isabelle process via an external

   469   program in a more robust fashion.

   470 *}

   471

   472

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

   474

   475 text {*

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

   477   wrapper --- @{executable isabelle}:

   478

   479 \begin{ttbox}

   480 Usage: isabelle TOOL [ARGS ...]

   481

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

   483

   484   Available tools are:

   485

   486     browser - Isabelle graph browser

   487     \dots

   488 \end{ttbox}

   489

   490   In principle, Isabelle tools are ordinary executable scripts that

   491   are run within the Isabelle settings environment, see

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

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

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

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

   496   shell's search path!

   497 *}

   498

   499

   500 subsubsection {* Examples *}

   501

   502 text {*

   503   Show the list of available documentation of the current Isabelle

   504   installation like this:

   505

   506 \begin{ttbox}

   507   isabelle doc

   508 \end{ttbox}

   509

   510   View a certain document as follows:

   511 \begin{ttbox}

   512   isabelle doc isar-ref

   513 \end{ttbox}

   514

   515   Create an Isabelle session derived from HOL (see also

   516   \secref{sec:tool-mkdir} and \secref{sec:tool-make}):

   517 \begin{ttbox}

   518   isabelle mkdir HOL Test && isabelle make

   519 \end{ttbox}

   520   Note that @{verbatim "isabelle mkdir"} is usually only invoked once;

   521   existing sessions (including document output etc.) are then updated

   522   by @{verbatim "isabelle make"} alone.

   523 *}

   524

   525 end