doc-src/System/Thy/Sessions.thy
 author wenzelm Tue Aug 14 15:42:58 2012 +0200 (2012-08-14) changeset 48805 c3ea910b3581 parent 48739 3a6c03b15916 child 48814 d488a5f25bf6 permissions -rw-r--r--
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
     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 (see also

     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 a single @{syntax session_entry} is given as

    42   syntax diagram below; each ROOT file may contain multiple session

    43   specifications like this.

    44

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

    46   mode @{verbatim "isabelle-root"} for session ROOT files.

    47

    48   @{rail "

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

    50     ;

    51     body: description? options? ( theories * ) files?

    52     ;

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

    54     ;

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

    56     ;

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

    58     ;

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

    60     ;

    61     options: @'options' opts

    62     ;

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

    64     ;

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

    66     ;

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

    68     ;

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

    70     "}

    71

    72   \begin{description}

    73

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

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

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

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

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

    79

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

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

    82   @{text "A"} should be sufficiently long to stand on its own in a

    83   potentially large library.

    84

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

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

    87   are uninterpreted and merely follow certain conventions.  For

    88   example, the Isabelle distribution tags some important sessions by

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

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

    91   within this unchecked name space.

    92

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

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

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

    96

    97   All theories and auxiliary source files are located relatively to

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

    99   its current working directory.

   100

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

   102   annotation for this session.

   103

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

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

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

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

   108   Boolean options.

   109

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

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

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

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

   114   may be given.  Options are only active for each

   115   \isakeyword{theories} block separately.

   116

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

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

   119   should cover anything outside the formal content of the theory

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

   121   document processing.  In contrast, files that are specified in

   122   formal theory headers as @{keyword "uses"} need not be declared

   123   again.

   124

   125   \end{description}

   126 *}

   127

   128 subsubsection {* Examples *}

   129

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

   131   relevant situations, but it uses relatively complex quasi-hierarchic

   132   naming conventions like @{text "HOL\<dash>SPARK"}, @{text

   133   "HOL\<dash>SPARK\<dash>Examples"}.  An alternative is to use

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

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

   136   example. *}

   137

   138

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

   140

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

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

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

   144   this file-format.

   145

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

   147   command-line usage is:

   148 \begin{ttbox}

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

   150

   151   Options are:

   152     -b           include $ISABELLE_BUILD_OPTIONS   153 -x FILE export to FILE in YXML format   154   155 Print Isabelle system options, augmented by MORE_OPTIONS given as   156 arguments NAME=VAL or NAME.   157 \end{ttbox}   158   159 The command line arguments provide additional system options of the   160 form @{text "name"}@{verbatim "="}@{text "value"} or @{text name}   161 for Boolean options.   162   163 Option @{verbatim "-b"} augments the implicit environment of system   164 options by the ones of @{setting ISABELLE_BUILD_OPTIONS}, cf.\   165 \secref{sec:tool-build}.   166   167 Option @{verbatim "-x"} specifies a file to export the result in   168 YXML format, instead of printing it in human-readable form.   169 *}   170   171   172 section {* Invoking the build process \label{sec:tool-build} *}   173   174 text {* The @{tool_def build} tool invokes the build process for   175 Isabelle sessions. It manages dependencies between sessions,   176 related sources of theories and auxiliary files, and target heap   177 images. Accordingly, it runs instances of the prover process with   178 optional document preparation. Its command-line usage   179 is:\footnote{Isabelle/Scala provides the same functionality via   180 \texttt{isabelle.Build.build}.}   181 \begin{ttbox}   182 Usage: isabelle build [OPTIONS] [SESSIONS ...]   183   184 Options are:   185 -D DIR include session directory and select its sessions   186 -a select all sessions   187 -b build heap images   188 -c clean build   189 -d DIR include session directory   190 -g NAME select session group NAME   191 -j INT maximum number of parallel jobs (default 1)   192 -n no build -- test dependencies only   193 -o OPTION override session configuration OPTION   194 (via NAME=VAL or NAME)   195 -s system build mode: produce output in ISABELLE_HOME   196 -v verbose   197   198 Build and manage Isabelle sessions, depending on implicit   199 ISABELLE_BUILD_OPTIONS="..."   200   201 ML_PLATFORM="..."   202 ML_HOME="..."   203 ML_SYSTEM="..."   204 ML_OPTIONS="..."   205 \end{ttbox}   206   207 \medskip Isabelle sessions are defined via session ROOT files as   208 described in (\secref{sec:session-root}). The totality of sessions   209 is determined by collecting such specifications from all Isabelle   210 component directories (\secref{sec:components}), augmented by more   211 directories given via options @{verbatim "-d"}~@{text "DIR"} on the   212 command line. Each such directory may contain a session   213 \texttt{ROOT} file with several session specifications.   214   215 Any session root directory may refer recursively to further   216 directories of the same kind, by listing them in a catalog file   217 @{verbatim "ROOTS"} line-by-line. This helps to organize large   218 collections of session specifications, or to make @{verbatim "-d"}   219 command line options persistent (say within @{verbatim   220 "$ISABELLE_HOME_USER/ROOTS"}).

   221

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

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

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

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

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

   227   selected sessions is completed by including all ancestors.

   228

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

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

   231

   232   \medskip The build process depends on additional options

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

   234   eventually.  The settings variable @{setting_ref

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

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

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

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

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

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

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

   242   command-line are applied in the given order.

   243

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

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

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

   247   other sessions to continue later on.

   248

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

   250   selected sessions before performing the specified build operation.

   251

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

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

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

   255   sessions.

   256

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

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

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

   260   option @{system_option_ref threads}.

   261

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

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

   264   @{verbatim "$ISABELLE_HOME/heaps"} instead of the default location   265 @{setting ISABELLE_OUTPUT} (which is normally in @{setting   266 ISABELLE_HOME_USER}, i.e.\ the user's home directory).   267   268 \medskip Option @{verbatim "-v"} enables verbose mode.   269 *}   270   271 subsubsection {* Examples *}   272   273 text {*   274 Build a specific logic image:   275 \begin{ttbox}   276 isabelle build -b HOLCF   277 \end{ttbox}   278   279 \smallskip Build the main group of logic images:   280 \begin{ttbox}   281 isabelle build -b -g main   282 \end{ttbox}   283   284 \smallskip Provide a general overview of the status of all Isabelle   285 sessions, without building anything:   286 \begin{ttbox}   287 isabelle build -a -n -v   288 \end{ttbox}   289   290 \smallskip Build all sessions with HTML browser info and PDF   291 document preparation:   292 \begin{ttbox}   293 isabelle build -a -o browser_info -o document=pdf   294 \end{ttbox}   295   296 \smallskip Build all sessions with a maximum of 8 parallel prover   297 processes and 4 worker threads each (on a machine with many cores):   298 \begin{ttbox}   299 isabelle build -a -j8 -o threads=4   300 \end{ttbox}   301   302 \smallskip Build some session images with cleanup of their   303 descendants, while retaining their ancestry:   304 \begin{ttbox}   305 isabelle build -b -c HOL-Boogie HOL-SPARK   306 \end{ttbox}   307   308 \smallskip Clean all sessions without building anything:   309 \begin{ttbox}   310 isabelle build -a -n -c   311 \end{ttbox}   312   313 \smallskip Build all sessions from some other directory hierarchy,   314 according to the settings variable @{verbatim "AFP"} that happens to   315 be defined inside the Isabelle environment:   316 \begin{ttbox}   317 isabelle build -D '$AFP'

   318 \end{ttbox}

   319 *}

   320

   321

   322 section {* Preparing session root directories \label{sec:tool-mkroot} *}

   323

   324 text {* The @{tool_def mkroot} tool configures a given directory as

   325   session root, with some @{verbatim ROOT} file and optional document

   326   source directory.  Its usage is:

   327 \begin{ttbox}

   328 Usage: isabelle mkroot [OPTIONS] [DIR]

   329

   330   Options are:

   331     -d           enable document preparation

   332     -n NAME      alternative session name (default: DIR base name)

   333

   334   Prepare session root DIR (default: current directory).

   335 \end{ttbox}

   336

   337   The results are placed in the given directory @{text dir}, which

   338   refers to the current directory by default.  The @{tool mkroot} tool

   339   is conservative in the sense that it does not overwrite existing

   340   files or directories.  Earlier attempts to generate a session root

   341   need to be deleted manually.

   342

   343   \medskip Option @{verbatim "-d"} indicates that the session shall be

   344   accompanied by a formal document, with @{text dir}@{verbatim

   345   "/document/root.tex"} as its {\LaTeX} entry point (see also

   346   \chref{ch:present}).

   347

   348   Option @{verbatim "-n"} allows to specify an alternative session

   349   name; otherwise the base name of the given directory is used.

   350

   351   \medskip The implicit Isabelle settings variable @{setting

   352   ISABELLE_LOGIC} specifies the parent session, and @{setting

   353   ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled

   354   into the generated @{verbatim ROOT} file.  *}

   355

   356

   357 subsubsection {* Examples *}

   358

   359 text {* Produce session @{verbatim Test} within a separate directory

   360   of the same name:

   361 \begin{ttbox}

   362 isabelle mkroot Test && isabelle build -D Test

   363 \end{ttbox}

   364

   365   \medskip Upgrade the current directory into a session ROOT with

   366   document preparation, and build it:

   367 \begin{ttbox}

   368 isabelle mkroot -d && isabelle build -D .

   369 \end{ttbox}

   370 *}

   371

   372 end