src/Doc/System/Sessions.thy
 author wenzelm Fri May 17 19:04:52 2013 +0200 (2013-05-17) changeset 52056 fc458f304f93 parent 51417 d266f9329368 child 52735 842b5e7dcac8 permissions -rw-r--r--
     1 theory Sessions

     2 imports Base

     3 begin

     4

     5 chapter {* Isabelle sessions and build management \label{ch:session} *}

     6

     7 text {* An Isabelle \emph{session} consists of a collection of related

     8   theories that may be associated with formal documents

     9   (\chref{ch:present}).  There is also a notion of \emph{persistent

    10   heap} image to capture the state of a session, similar to

    11   object-code in compiled programming languages.  Thus the concept of

    12   session resembles that of a project'' in common IDE environments,

    13   but the specific name emphasizes the connection to interactive

    14   theorem proving: the session wraps-up the results of

    15   user-interaction with the prover in a persistent form.

    16

    17   Application sessions are built on a given parent session, which may

    18   be built recursively on other parents.  Following this path in the

    19   hierarchy eventually leads to some major object-logic session like

    20   @{text "HOL"}, which itself is based on @{text "Pure"} as the common

    21   root of all sessions.

    22

    23   Processing sessions may take considerable time.  Isabelle build

    24   management helps to organize this efficiently.  This includes

    25   support for parallel build jobs, in addition to the multithreaded

    26   theory and proof checking that is already provided by the prover

    27   process itself.  *}

    28

    29

    30 section {* Session ROOT specifications \label{sec:session-root} *}

    31

    32 text {* Session specifications reside in files called @{verbatim ROOT}

    33   within certain directories, such as the home locations of registered

    34   Isabelle components or additional project directories given by the

    35   user.

    36

    37   The ROOT file format follows the lexical conventions of the

    38   \emph{outer syntax} of Isabelle/Isar, see also

    39   \cite{isabelle-isar-ref}.  This defines common forms like

    40   identifiers, names, quoted strings, verbatim text, nested comments

    41   etc.  The grammar for @{syntax session_chapter} and @{syntax

    42   session_entry} is given as syntax diagram below; each ROOT file may

    43   contain multiple specifications like this.  Chapters help to

    44   organize browser info (\secref{sec:info}), but have no formal

    45   meaning.  The default chapter is @{text "Unsorted"}''.

    46

    47   Isabelle/jEdit (\secref{sec:tool-jedit}) includes a simple editing

    48   mode @{verbatim "isabelle-root"} for session ROOT files, which is

    49   enabled by default for any file of that name.

    50

    51   @{rail "

    52     @{syntax_def session_chapter}: @'chapter' @{syntax name}

    53     ;

    54

    55     @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body

    56     ;

    57     body: description? options? ( theories + ) files?

    58     ;

    59     spec: @{syntax name} groups? dir?

    60     ;

    61     groups: '(' (@{syntax name} +) ')'

    62     ;

    63     dir: @'in' @{syntax name}

    64     ;

    65     description: @'description' @{syntax text}

    66     ;

    67     options: @'options' opts

    68     ;

    69     opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'

    70     ;

    71     value: @{syntax name} | @{syntax real}

    72     ;

    73     theories: @'theories' opts? ( @{syntax name} * )

    74     ;

    75     files: @'files' ( @{syntax name} + )

    76     "}

    77

    78   \begin{description}

    79

    80   \item \isakeyword{session}~@{text "A = B + body"} defines a new

    81   session @{text "A"} based on parent session @{text "B"}, with its

    82   content given in @{text body} (theories and auxiliary source files).

    83   Note that a parent (like @{text "HOL"}) is mandatory in practical

    84   applications: only Isabelle/Pure can bootstrap itself from nothing.

    85

    86   All such session specifications together describe a hierarchy (tree)

    87   of sessions, with globally unique names.  The new session name

    88   @{text "A"} should be sufficiently long and descriptive to stand on

    89   its own in a potentially large library.

    90

    91   \item \isakeyword{session}~@{text "A (groups)"} indicates a

    92   collection of groups where the new session is a member.  Group names

    93   are uninterpreted and merely follow certain conventions.  For

    94   example, the Isabelle distribution tags some important sessions by

    95   the group name called @{text "main"}''.  Other projects may invent

    96   their own conventions, but this requires some care to avoid clashes

    97   within this unchecked name space.

    98

    99   \item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"}

   100   specifies an explicit directory for this session; by default this is

   101   the current directory of the @{verbatim ROOT} file.

   102

   103   All theories and auxiliary source files are located relatively to

   104   the session directory.  The prover process is run within the same as

   105   its current working directory.

   106

   107   \item \isakeyword{description}~@{text "text"} is a free-form

   108   annotation for this session.

   109

   110   \item \isakeyword{options}~@{text "[x = a, y = b, z]"} defines

   111   separate options (\secref{sec:system-options}) that are used when

   112   processing this session, but \emph{without} propagation to child

   113   sessions.  Note that @{text "z"} abbreviates @{text "z = true"} for

   114   Boolean options.

   115

   116   \item \isakeyword{theories}~@{text "options names"} specifies a

   117   block of theories that are processed within an environment that is

   118   augmented by the given options, in addition to the global session

   119   options given before.  Any number of blocks of \isakeyword{theories}

   120   may be given.  Options are only active for each

   121   \isakeyword{theories} block separately.

   122

   123   \item \isakeyword{files}~@{text "files"} lists additional source

   124   files that are involved in the processing of this session.  This

   125   should cover anything outside the formal content of the theory

   126   sources, say some auxiliary {\TeX} files that are required for

   127   document processing.  In contrast, files that are loaded formally

   128   within a theory, e.g.\ via @{keyword "ML_file"}, need not be

   129   declared again.

   130

   131   \end{description}

   132 *}

   133

   134

   135 subsubsection {* Examples *}

   136

   137 text {* See @{file "~~/src/HOL/ROOT"} for a diversity of practically

   138   relevant situations, although it uses relatively complex

   139   quasi-hierarchic naming conventions like @{text "HOL\<dash>SPARK"},

   140   @{text "HOL\<dash>SPARK\<dash>Examples"}.  An alternative is to use

   141   unqualified names that are relatively long and descriptive, as in

   142   the Archive of Formal Proofs (\url{http://afp.sf.net}), for

   143   example. *}

   144

   145

   146 section {* System build options \label{sec:system-options} *}

   147

   148 text {* See @{file "~~/etc/options"} for the main defaults provided by

   149   the Isabelle distribution.  Isabelle/jEdit (\secref{sec:tool-jedit})

   150   includes a simple editing mode @{verbatim "isabelle-options"} for

   151   this file-format.

   152

   153   The following options are particulary relevant to build Isabelle

   154   sessions, in particular with document preparation

   155   (\chref{ch:present}).

   156

   157   \begin{itemize}

   158

   159   \item @{system_option_def "browser_info"} controls output of HTML

   160   browser info, see also \secref{sec:info}.

   161

   162   \item @{system_option_def "document"} specifies the document output

   163   format, see @{tool document} option @{verbatim "-o"} in

   164   \secref{sec:tool-document}.  In practice, the most relevant values

   165   are @{verbatim "document=false"} or @{verbatim "document=pdf"}.

   166

   167   \item @{system_option_def "document_output"} specifies an

   168   alternative directory for generated output of the document

   169   preparation system; the default is within the @{setting

   170   "ISABELLE_BROWSER_INFO"} hierarchy as explained in

   171   \secref{sec:info}.  See also @{tool mkroot}, which generates a

   172   default configuration with output readily available to the author of

   173   the document.

   174

   175   \item @{system_option_def "document_variants"} specifies document

   176   variants as a colon-separated list of @{text "name=tags"} entries,

   177   corresponding to @{tool document} options @{verbatim "-n"} and

   178   @{verbatim "-t"}.

   179

   180   For example, @{verbatim

   181   "document_variants=document:outline=/proof,/ML"} indicates two

   182   documents: the one called @{verbatim document} with default tags,

   183   and the other called @{verbatim outline} where proofs and ML

   184   sections are folded.

   185

   186   Document variant names are just a matter of conventions.  It is also

   187   possible to use different document variant names (without tags) for

   188   different document root entries, see also

   189   \secref{sec:tool-document}.

   190

   191   \item @{system_option_def "document_graph"} tells whether the

   192   generated document files should include a theory graph (cf.\

   193   \secref{sec:browse} and \secref{sec:info}).  The resulting EPS or

   194   PDF file can be included as graphics in {\LaTeX}.

   195

   196   Note that this option is usually determined as static parameter of

   197   some session (e.g.\ within its @{verbatim ROOT} file) and \emph{not}

   198   given globally or on the command line of @{tool build}.

   199

   200   \item @{system_option_def "threads"} determines the number of worker

   201   threads for parallel checking of theories and proofs.  The default

   202   @{text "0"} means that a sensible maximum value is determined by the

   203   underlying hardware.  For machines with many cores or with

   204   hyperthreading, this is often requires manual adjustment (on the

   205   command-line or within personal settings or preferences, not within

   206   a session @{verbatim ROOT}).

   207

   208   \item @{system_option_def "condition"} specifies a comma-separated

   209   list of process environment variables (or Isabelle settings) that

   210   are required for the subsequent theories to be processed.

   211   Conditions are considered true'' if the corresponding environment

   212   value is defined and non-empty.

   213

   214   For example, the @{verbatim "condition=ISABELLE_FULL_TEST"} may be

   215   used to guard extraordinary theories, which are meant to be enabled

   216   explicitly via some shell prefix @{verbatim "env ISABELLE_FULL_TEST=true"}

   217   before invoking @{tool build}.

   218

   219   \item @{system_option_def "timeout"} specifies a real wall-clock

   220   timeout (in seconds) for the session as a whole.  The timer is

   221   controlled outside the ML process by the JVM that runs

   222   Isabelle/Scala.  Thus it is relatively reliable in canceling

   223   processes that get out of control, even if there is a deadlock

   224   without CPU time usage.

   225

   226   \end{itemize}

   227

   228   The @{tool_def options} tool prints Isabelle system options.  Its

   229   command-line usage is:

   230 \begin{ttbox}

   231 Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]

   232

   233   Options are:

   234     -b           include $ISABELLE_BUILD_OPTIONS   235 -l list options   236 -x FILE export to FILE in YXML format   237   238 Report Isabelle system options, augmented by MORE_OPTIONS given as   239 arguments NAME=VAL or NAME.   240 \end{ttbox}   241   242 The command line arguments provide additional system options of the   243 form @{text "name"}@{verbatim "="}@{text "value"} or @{text name}   244 for Boolean options.   245   246 Option @{verbatim "-b"} augments the implicit environment of system   247 options by the ones of @{setting ISABELLE_BUILD_OPTIONS}, cf.\   248 \secref{sec:tool-build}.   249   250 Option @{verbatim "-x"} specifies a file to export the result in   251 YXML format, instead of printing it in human-readable form.   252 *}   253   254   255 section {* Invoking the build process \label{sec:tool-build} *}   256   257 text {* The @{tool_def build} tool invokes the build process for   258 Isabelle sessions. It manages dependencies between sessions,   259 related sources of theories and auxiliary files, and target heap   260 images. Accordingly, it runs instances of the prover process with   261 optional document preparation. Its command-line usage   262 is:\footnote{Isabelle/Scala provides the same functionality via   263 \texttt{isabelle.Build.build}.}   264 \begin{ttbox}   265 Usage: isabelle build [OPTIONS] [SESSIONS ...]   266   267 Options are:   268 -D DIR include session directory and select its sessions   269 -R operate on requirements of selected sessions   270 -a select all sessions   271 -b build heap images   272 -c clean build   273 -d DIR include session directory   274 -g NAME select session group NAME   275 -j INT maximum number of parallel jobs (default 1)   276 -l list session source files   277 -n no build -- test dependencies only   278 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)   279 -s system build mode: produce output in ISABELLE_HOME   280 -v verbose   281   282 Build and manage Isabelle sessions, depending on implicit   283 ISABELLE_BUILD_OPTIONS="..."   284   285 ML_PLATFORM="..."   286 ML_HOME="..."   287 ML_SYSTEM="..."   288 ML_OPTIONS="..."   289 \end{ttbox}   290   291 \medskip Isabelle sessions are defined via session ROOT files as   292 described in (\secref{sec:session-root}). The totality of sessions   293 is determined by collecting such specifications from all Isabelle   294 component directories (\secref{sec:components}), augmented by more   295 directories given via options @{verbatim "-d"}~@{text "DIR"} on the   296 command line. Each such directory may contain a session   297 \texttt{ROOT} file with several session specifications.   298   299 Any session root directory may refer recursively to further   300 directories of the same kind, by listing them in a catalog file   301 @{verbatim "ROOTS"} line-by-line. This helps to organize large   302 collections of session specifications, or to make @{verbatim "-d"}   303 command line options persistent (say within @{verbatim   304 "$ISABELLE_HOME_USER/ROOTS"}).

   305

   306   \medskip The subset of sessions to be managed is determined via

   307   individual @{text "SESSIONS"} given as command-line arguments, or

   308   session groups that are given via one or more options @{verbatim

   309   "-g"}~@{text "NAME"}.  Option @{verbatim "-a"} selects all sessions.

   310   The build tool takes session dependencies into account: the set of

   311   selected sessions is completed by including all ancestors.

   312

   313   \medskip Option @{verbatim "-R"} reverses the selection in the sense

   314   that it refers to its requirements: all ancestor sessions excluding

   315   the original selection.  This allows to prepare the stage for some

   316   build process with different options, before running the main build

   317   itself (without option @{verbatim "-R"}).

   318

   319   \medskip Option @{verbatim "-D"} is similar to @{verbatim "-d"}, but

   320   selects all sessions that are defined in the given directories.

   321

   322   \medskip The build process depends on additional options

   323   (\secref{sec:system-options}) that are passed to the prover

   324   eventually.  The settings variable @{setting_ref

   325   ISABELLE_BUILD_OPTIONS} allows to provide additional defaults, e.g.\

   326   \texttt{ISABELLE_BUILD_OPTIONS="document=pdf threads=4"}. Moreover,

   327   the environment of system build options may be augmented on the

   328   command line via @{verbatim "-o"}~@{text "name"}@{verbatim

   329   "="}@{text "value"} or @{verbatim "-o"}~@{text "name"}, which

   330   abbreviates @{verbatim "-o"}~@{text "name"}@{verbatim"=true"} for

   331   Boolean options.  Multiple occurrences of @{verbatim "-o"} on the

   332   command-line are applied in the given order.

   333

   334   \medskip Option @{verbatim "-b"} ensures that heap images are

   335   produced for all selected sessions.  By default, images are only

   336   saved for inner nodes of the hierarchy of sessions, as required for

   337   other sessions to continue later on.

   338

   339   \medskip Option @{verbatim "-c"} cleans all descendants of the

   340   selected sessions before performing the specified build operation.

   341

   342   \medskip Option @{verbatim "-n"} omits the actual build process

   343   after the preparatory stage (including optional cleanup).  Note that

   344   the return code always indicates the status of the set of selected

   345   sessions.

   346

   347   \medskip Option @{verbatim "-j"} specifies the maximum number of

   348   parallel build jobs (prover processes).  Each prover process is

   349   subject to a separate limit of parallel worker threads, cf.\ system

   350   option @{system_option_ref threads}.

   351

   352   \medskip Option @{verbatim "-s"} enables \emph{system mode}, which

   353   means that resulting heap images and log files are stored in

   354   @{verbatim "$ISABELLE_HOME/heaps"} instead of the default location   355 @{setting ISABELLE_OUTPUT} (which is normally in @{setting   356 ISABELLE_HOME_USER}, i.e.\ the user's home directory).   357   358 \medskip Option @{verbatim "-v"} increases the general level of   359 verbosity. Option @{verbatim "-l"} lists the source files that   360 contribute to a session.   361 *}   362   363 subsubsection {* Examples *}   364   365 text {*   366 Build a specific logic image:   367 \begin{ttbox}   368 isabelle build -b HOLCF   369 \end{ttbox}   370   371 \smallskip Build the main group of logic images:   372 \begin{ttbox}   373 isabelle build -b -g main   374 \end{ttbox}   375   376 \smallskip Provide a general overview of the status of all Isabelle   377 sessions, without building anything:   378 \begin{ttbox}   379 isabelle build -a -n -v   380 \end{ttbox}   381   382 \smallskip Build all sessions with HTML browser info and PDF   383 document preparation:   384 \begin{ttbox}   385 isabelle build -a -o browser_info -o document=pdf   386 \end{ttbox}   387   388 \smallskip Build all sessions with a maximum of 8 parallel prover   389 processes and 4 worker threads each (on a machine with many cores):   390 \begin{ttbox}   391 isabelle build -a -j8 -o threads=4   392 \end{ttbox}   393   394 \smallskip Build some session images with cleanup of their   395 descendants, while retaining their ancestry:   396 \begin{ttbox}   397 isabelle build -b -c HOL-Boogie HOL-SPARK   398 \end{ttbox}   399   400 \smallskip Clean all sessions without building anything:   401 \begin{ttbox}   402 isabelle build -a -n -c   403 \end{ttbox}   404   405 \smallskip Build all sessions from some other directory hierarchy,   406 according to the settings variable @{verbatim "AFP"} that happens to   407 be defined inside the Isabelle environment:   408 \begin{ttbox}   409 isabelle build -D '$AFP'

   410 \end{ttbox}

   411

   412   \smallskip Inform about the status of all sessions required for AFP,

   413   without building anything yet:

   414 \begin{ttbox}

   415 isabelle build -D '$AFP' -R -v -n   416 \end{ttbox}   417 *}   418   419   420 section {* Build dialog *}   421   422 text {* The @{tool_def build_dialog} provides a simple GUI wrapper to   423 the tool Isabelle @{tool build} tool. This enables user interfaces   424 like Isabelle/jEdit \secref{sec:tool-jedit} to provide read-made   425 logic image on startup. Its command-line usage is:   426 \begin{ttbox}   427 Usage: isabelle build_dialog [OPTIONS] LOGIC   428   429 Options are:   430 -L OPTION default logic via system option   431 -d DIR include session directory   432 -l NAME logic session name   433 -s system build mode: produce output in ISABELLE_HOME   434   435 Build Isabelle logic session image via GUI dialog (default: \$ISABELLE_LOGIC).

   436 \end{ttbox}

   437

   438   \medskip Option @{verbatim "-l"} specifies an explicit logic session

   439   name.  Option @{verbatim "-L"} specifies a system option name as

   440   fall-back to determine the logic session name.  If both are omitted

   441   or have empty value, @{setting ISABELLE_LOGIC} is used as default.

   442

   443   \medskip Options @{verbatim "-d"} and @{verbatim "-s"} have the same

   444   meaning as for the command-line @{tool build} tool itself.  *}

   445

   446 end