doc-src/System/Thy/Sessions.thy
author wenzelm
Sat, 28 Jul 2012 15:21:49 +0200
changeset 48578 21361b6189a6
child 48579 0b95a13ed90a
permissions -rw-r--r--
some description of isabelle build;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
     1
theory Sessions
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
     2
imports Base
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
     3
begin
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
     4
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
     5
chapter {* Isabelle sessions and build management *}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
     6
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
     7
text {* FIXME *}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
     8
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
     9
section {* Session ROOT specifications \label{sec:session-root} *}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    10
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    11
text {* FIXME *}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    12
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    13
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    14
section {* System build options \label{sec:system-options} *}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    15
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    16
text {* FIXME *}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    17
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    18
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    19
section {* Invoking the build process \label{sec:tool-build} *}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    20
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    21
text {* The @{tool_def build} utility invokes the build process for
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    22
  Isabelle sessions.  It manages dependencies between sessions,
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    23
  related sources of theories and auxiliary files, and target heap
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    24
  images.  Accordingly, it runs instances of the prover process with
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    25
  optional document preparation.  Its command-line usage
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    26
  is:\footnote{Isabelle/Scala provides the same functionality via
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    27
  \texttt{isabelle.Build.build}.}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    28
\begin{ttbox} Usage: isabelle build [OPTIONS] [SESSIONS ...]
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    29
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    30
  Options are:
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    31
    -a           select all sessions
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    32
    -b           build heap images
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    33
    -d DIR       include session directory with ROOT file
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    34
    -g NAME      select session group NAME
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    35
    -j INT       maximum number of parallel jobs (default 1)
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    36
    -n           no build -- test dependencies only
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    37
    -o OPTION    override session configuration OPTION
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    38
                 (via NAME=VAL or NAME)
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    39
    -s           system build mode: produce output in ISABELLE_HOME
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    40
    -v           verbose
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    41
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    42
  Build and manage Isabelle sessions, depending on implicit
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    43
  ISABELLE_BUILD_OPTIONS="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    44
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    45
  ML_PLATFORM="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    46
  ML_HOME="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    47
  ML_SYSTEM="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    48
  ML_OPTIONS="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    49
\end{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    50
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    51
  \medskip Isabelle sessions are defined via session ROOT files as
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    52
  described in (\secref{sec:session-root}).  The totality of sessions
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    53
  is determined by collecting such specifications from all Isabelle
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    54
  component directories (\secref{sec:components}), augmented by more
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    55
  directories given via options @{verbatim "-d"}~@{text "DIR"} on the
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    56
  command line.  Each such directory may contain a session
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    57
  \texttt{ROOT} file and an additional catalog file @{verbatim
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    58
  "etc/sessions"} with further sub-directories (list of lines).  Note
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    59
  that a single \texttt{ROOT} file usually defines many sessions;
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    60
  catalogs are are only required for extra scalability and modularity
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    61
  of large libraries.
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    62
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    63
  \medskip The subset of sessions to be managed is selected via
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    64
  individual @{text "SESSIONS"} given as command-line arguments, or
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    65
  session groups that are specified via one or more options @{verbatim
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    66
  "-g"}~@{text "NAME"}.  Option @{verbatim "-a"} selects all sessions.
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    67
  The build tool takes the hierarchy of sessions into account: the
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    68
  selected set of sessions is completed by including all ancestors
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    69
  according to the dependency structure.
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    70
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    71
  \medskip The build process depends on additional options that are
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    72
  passed to the prover session eventually, see also
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    73
  (\secref{sec:system-options}).  The settings variable @{setting_ref
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    74
  ISABELLE_BUILD_OPTIONS} allows to provide additional defaults.
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    75
  Moreover, the environment of system build options may be augmented
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    76
  on the command line via @{verbatim "-o"}~@{text "NAME=VALUE"} or
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    77
  @{verbatim "-o"}~@{text "NAME"}, which abbreviates @{verbatim
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    78
  "-o"}~@{text "NAME=true"} for Boolean options.  Multiple occurrences
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    79
  of @{verbatim "-o"} on the command-line are applied in the given
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    80
  order.
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    81
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    82
  \medskip Option @{verbatim "-b"} ensures that heap images are
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    83
  produced for all selected sessions.  By default, images are only
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    84
  saved for inner nodes of the hierarchy of sessions, as required for
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    85
  other sessions to continue later on.
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    86
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    87
  \medskip Option @{verbatim "-j"} specifies the maximum number of
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    88
  parallel build jobs (prover processes).  Note that each process is
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    89
  subject to a separate limit of parallel threads, cf.\ system option
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    90
  @{system_option_ref threads}.
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    91
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    92
  \medskip Option @{verbatim "-s"} enables \emph{system mode}, which
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    93
  means that resulting heap images and log files are stored in
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    94
  @{verbatim "$ISABELLE_HOME/heaps"} instead of the default location
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    95
  @{setting ISABELLE_OUTPUT} (which is normally in @{setting
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    96
  ISABELLE_HOME_USER}, i.e.\ the user's home directory).
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    97
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    98
  \medskip Option @{verbatim "-n"} omits the actual build process
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    99
  after performing all dependency checks.  The return code indicates
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   100
  the status of the set of selected sessions.
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   101
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   102
  \medskip Option @{verbatim "-v"} enables verbose mode.
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   103
*}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   104
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   105
subsubsection {* Examples *}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   106
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   107
text {*
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   108
  Build a specific logic image:
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   109
\begin{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   110
isabelle build -b HOLCF
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   111
\end{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   112
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   113
  Build the main group of logic images (as determined by the session
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   114
  ROOT specifications of the Isabelle distribution):
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   115
\begin{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   116
isabelle build -b -g main
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   117
\end{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   118
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   119
  Provide a general overview of the status of all Isabelle sessions,
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   120
  without building anything:
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   121
\begin{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   122
isabelle build -a -n -v
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   123
\end{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   124
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   125
  Build all sessions with HTML browser info and PDF document
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   126
  preparation:
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   127
\begin{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   128
isabelle build -a -o browser_info -o document=pdf
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   129
\end{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   130
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   131
  Build all sessions with a maximum of 8 prover processes and 4
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   132
  threads each (on a machine with many cores):
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   133
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   134
\begin{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   135
isabelle build -a -j8 -o threads=4
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   136
\end{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   137
*}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   138
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   139
end