doc-src/System/Thy/Sessions.thy
author wenzelm
Mon, 30 Jul 2012 14:38:45 +0200
changeset 48604 f651323139f0
parent 48602 342ca8f3197b
child 48605 e777363440d6
permissions -rw-r--r--
misc tuning;
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
48584
8026c852cc10 some introduction on sessions;
wenzelm
parents: 48582
diff changeset
     5
chapter {* Isabelle sessions and build management \label{ch:session} *}
8026c852cc10 some introduction on sessions;
wenzelm
parents: 48582
diff changeset
     6
8026c852cc10 some introduction on sessions;
wenzelm
parents: 48582
diff changeset
     7
text {* An Isabelle \emph{session} consists of a collection of related
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
     8
  theories that may be associated with formal documents (see also
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
     9
  \chref{ch:present}).  There is also a notion of \emph{persistent
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    10
  heap} image to capture the state of a session, similar to
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    11
  object-code in compiled programming languages.  Thus the concept of
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    12
  session resembles that of a ``project'' in common IDE environments,
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    13
  but the specific name emphasizes the connection to interactive
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    14
  theorem proving: the session wraps-up the results of
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    15
  user-interaction with the prover in a persistent form.
48584
8026c852cc10 some introduction on sessions;
wenzelm
parents: 48582
diff changeset
    16
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    17
  Application sessions are built on a given parent session, which may
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    18
  be built recursively on other parents.  Following this path in the
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    19
  hierarchy eventually leads to some major object-logic session like
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    20
  @{text "HOL"}, which itself is based on @{text "Pure"} as the common
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    21
  root of all sessions.
48584
8026c852cc10 some introduction on sessions;
wenzelm
parents: 48582
diff changeset
    22
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    23
  Processing sessions may take considerable time.  Isabelle build
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    24
  management helps to organize this efficiently.  This includes
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    25
  support for parallel build jobs, in addition to the multithreaded
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    26
  theory and proof checking that is already provided by the prover
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    27
  process itself.  *}
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    28
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    29
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    30
section {* Session ROOT specifications \label{sec:session-root} *}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    31
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    32
text {* Session specifications reside in files called @{verbatim ROOT}
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    33
  within certain directories, such as the home locations of registered
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    34
  Isabelle components or additional project directories given by the
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    35
  user.
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    36
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    37
  The ROOT file format follows the lexical conventions of the
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    38
  \emph{outer syntax} of Isabelle/Isar, see also
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    39
  \cite{isabelle-isar-ref}.  This defines common forms like
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    40
  identifiers, names, quoted strings, verbatim text, nested comments
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    41
  etc.  The grammar for a single @{syntax session_entry} is given as
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    42
  syntax diagram below; each ROOT file may contain multiple session
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    43
  specifications like this.
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    44
48582
wenzelm
parents: 48580
diff changeset
    45
  Isabelle/jEdit (\secref{sec:tool-jedit}) includes a simple editing
wenzelm
parents: 48580
diff changeset
    46
  mode @{verbatim "isabelle-root"} for session ROOT files.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    47
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    48
  @{rail "
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    49
    @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    50
    ;
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    51
    body: description? options? ( theories * ) files?
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    52
    ;
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    53
    spec: @{syntax name} '!'? groups? dir?
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    54
    ;
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    55
    groups: '(' (@{syntax name} +) ')'
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    56
    ;
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    57
    dir: @'in' @{syntax name}
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    58
    ;
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    59
    description: @'description' @{syntax text}
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    60
    ;
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    61
    options: @'options' opts
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    62
    ;
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    63
    opts: '[' ( (@{syntax name} '=' @{syntax name} | @{syntax name}) + ',' ) ']'
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    64
    ;
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    65
    theories: @'theories' opts? ( @{syntax name} + )
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    66
    ;
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    67
    files: @'files' ( @{syntax name} + )
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    68
    "}
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    69
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    70
  \begin{description}
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    71
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    72
  \item \isakeyword{session}~@{text "A = B + body"} defines a new
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    73
  session @{text "A"} based on parent session @{text "B"}, with its
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    74
  content given in @{text body} (theories and auxiliary source files).
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    75
  Note that a parent (like @{text "HOL"}) is mandatory in practical
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    76
  applications: only Isabelle/Pure can bootstrap itself from nothing.
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    77
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    78
  All such session specifications together describe a hierarchy (tree)
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    79
  of sessions, with globally unique names.  By default, names are
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    80
  derived from parent ones by concatenation, i.e.\ @{text "B\<dash>A"}
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    81
  above.  Cumulatively, this leads to session paths of the form @{text
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    82
  "X\<dash>Y\<dash>Z\<dash>W"}.  Note that in the specification,
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    83
  @{text B} is already such a fully-qualified name, while @{text "A"}
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    84
  is the new base name.
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    85
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    86
  \item \isakeyword{session}~@{text "A! = B"} indicates a fresh start
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    87
  in the naming scheme: the session is called just @{text "A"} instead
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    88
  of @{text "B\<dash>A"}.  Here the name @{text "A"} should be
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    89
  sufficiently long to stand on its own in a potentially large
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    90
  library.
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    91
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    92
  \item \isakeyword{session}~@{text "A (groups)"} indicates a
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    93
  collection of groups where the new session is a member.  Group names
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    94
  are uninterpreted and merely follow certain conventions.  For
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    95
  example, the Isabelle distribution tags some important sessions by
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    96
  the group name called ``@{text "main"}''.  Other projects may invent
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    97
  their own conventions, but this requires some care to avoid clashes
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    98
  within this unchecked name space.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    99
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   100
  \item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"}
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   101
  specifies an explicit directory for this session.  By default,
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   102
  \isakeyword{session}~@{text "A"} abbreviates
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   103
  \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "A"}.  This
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   104
  accommodates the common scheme where some base directory contains
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   105
  several sessions in sub-directories of corresponding names.  Another
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   106
  common scheme is \isakeyword{session}~@{text
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   107
  "A"}~\isakeyword{in}~@{verbatim "\".\""} to refer to the current
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   108
  directory of the ROOT file.
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   109
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   110
  All theories and auxiliary source files are located relatively to
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   111
  the session directory.  The prover process is run within the same as
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   112
  its current working directory.
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   113
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   114
  \item \isakeyword{description}~@{text "text"} is a free-form
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   115
  annotation for this session.
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   116
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   117
  \item \isakeyword{options}~@{text "[x = a, y = b, z]"} defines
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   118
  separate options (\secref{sec:system-options}) that are used when
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   119
  processing this session, but \emph{without} propagation to child
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   120
  sessions.  Note that @{text "z"} abbreviates @{text "z = true"} for
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   121
  Boolean options.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   122
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   123
  \item \isakeyword{theories}~@{text "options names"} specifies a
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   124
  block of theories that are processed within an environment that is
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   125
  augmented by the given options, in addition to the global session
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   126
  options given before.  Any number of blocks of \isakeyword{theories}
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   127
  may be given.  Options are only active for each
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   128
  \isakeyword{theories} block separately.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   129
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   130
  \item \isakeyword{files}~@{text "files"} lists additional source
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   131
  files that are involved in the processing of this session.  This
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   132
  should cover anything outside the formal content of the theory
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   133
  sources, say some auxiliary {\TeX} files that are required for
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   134
  document processing.  In contrast, files that are specified in
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   135
  formal theory headers as @{keyword "uses"} need not be declared
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   136
  again.
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   137
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   138
  \end{description}
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48579
diff changeset
   139
*}
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   140
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48579
diff changeset
   141
subsubsection {* Examples *}
9df76dd45900 some description of main build options;
wenzelm
parents: 48579
diff changeset
   142
9df76dd45900 some description of main build options;
wenzelm
parents: 48579
diff changeset
   143
text {* See @{file "~~/src/HOL/ROOT"} for a diversity of practically
9df76dd45900 some description of main build options;
wenzelm
parents: 48579
diff changeset
   144
  relevant situations. *}
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   145
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   146
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   147
section {* System build options \label{sec:system-options} *}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   148
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48579
diff changeset
   149
text {* See @{file "~~/etc/options"} for the main defaults provided by
48582
wenzelm
parents: 48580
diff changeset
   150
  the Isabelle distribution.  Isabelle/jEdit (\secref{sec:tool-jedit})
wenzelm
parents: 48580
diff changeset
   151
  includes a simple editing mode @{verbatim "isabelle-options"} for
wenzelm
parents: 48580
diff changeset
   152
  this file-format.
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48579
diff changeset
   153
*}
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   154
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   155
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   156
section {* Invoking the build process \label{sec:tool-build} *}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   157
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48595
diff changeset
   158
text {* The @{tool_def build} tool invokes the build process for
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   159
  Isabelle sessions.  It manages dependencies between sessions,
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   160
  related sources of theories and auxiliary files, and target heap
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   161
  images.  Accordingly, it runs instances of the prover process with
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   162
  optional document preparation.  Its command-line usage
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   163
  is:\footnote{Isabelle/Scala provides the same functionality via
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   164
  \texttt{isabelle.Build.build}.}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48595
diff changeset
   165
\begin{ttbox}
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48595
diff changeset
   166
Usage: isabelle build [OPTIONS] [SESSIONS ...]
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   167
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   168
  Options are:
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   169
    -a           select all sessions
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   170
    -b           build heap images
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   171
    -c           clean build
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   172
    -d DIR       include session directory with ROOT file
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   173
    -g NAME      select session group NAME
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   174
    -j INT       maximum number of parallel jobs (default 1)
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   175
    -n           no build -- test dependencies only
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   176
    -o OPTION    override session configuration OPTION
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   177
                 (via NAME=VAL or NAME)
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   178
    -s           system build mode: produce output in ISABELLE_HOME
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   179
    -v           verbose
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   180
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   181
  Build and manage Isabelle sessions, depending on implicit
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   182
  ISABELLE_BUILD_OPTIONS="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   183
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   184
  ML_PLATFORM="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   185
  ML_HOME="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   186
  ML_SYSTEM="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   187
  ML_OPTIONS="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   188
\end{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   189
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   190
  \medskip Isabelle sessions are defined via session ROOT files as
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   191
  described in (\secref{sec:session-root}).  The totality of sessions
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   192
  is determined by collecting such specifications from all Isabelle
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   193
  component directories (\secref{sec:components}), augmented by more
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   194
  directories given via options @{verbatim "-d"}~@{text "DIR"} on the
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   195
  command line.  Each such directory may contain a session
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   196
  \texttt{ROOT} file and an additional catalog file @{verbatim
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   197
  "etc/sessions"} with further sub-directories (list of lines).  Note
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   198
  that a single \texttt{ROOT} file usually defines many sessions;
48591
38e225bd53e4 corrected slip
haftmann
parents: 48584
diff changeset
   199
  catalogs are only required for extra scalability and modularity
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   200
  of large libraries.
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   201
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   202
  \medskip The subset of sessions to be managed is determined via
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   203
  individual @{text "SESSIONS"} given as command-line arguments, or
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   204
  session groups that are given via one or more options @{verbatim
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   205
  "-g"}~@{text "NAME"}.  Option @{verbatim "-a"} selects all sessions.
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   206
  The build tool takes session dependencies into account: the set of
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   207
  selected sessions is completed by including all ancestors.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   208
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   209
  \medskip The build process depends on additional options
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   210
  (\secref{sec:system-options}) that are passed to the prover
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   211
  eventually.  The settings variable @{setting_ref
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   212
  ISABELLE_BUILD_OPTIONS} allows to provide additional defaults, e.g.\
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   213
  \texttt{ISABELLE_BUILD_OPTIONS="document=pdf threads=4"}. Moreover,
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   214
  the environment of system build options may be augmented on the
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   215
  command line via @{verbatim "-o"}~@{text "name"}@{verbatim
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   216
  "="}@{text "value"} or @{verbatim "-o"}~@{text "name"}, which
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   217
  abbreviates @{verbatim "-o"}~@{text "name"}@{verbatim"=true"} for
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   218
  Boolean options.  Multiple occurrences of @{verbatim "-o"} on the
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   219
  command-line are applied in the given order.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   220
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   221
  \medskip Option @{verbatim "-b"} ensures that heap images are
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   222
  produced for all selected sessions.  By default, images are only
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   223
  saved for inner nodes of the hierarchy of sessions, as required for
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   224
  other sessions to continue later on.
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   225
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   226
  \medskip Option @{verbatim "-c"} cleans all descendants of the
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   227
  selected sessions before performing the specified build operation.
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   228
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   229
  \medskip Option @{verbatim "-n"} omits the actual build process
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   230
  after the preparatory stage (including optional cleanup).  Note that
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   231
  the return code always indicates the status of the set of selected
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   232
  sessions.
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   233
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   234
  \medskip Option @{verbatim "-j"} specifies the maximum number of
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   235
  parallel build jobs (prover processes).  Each prover process is
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   236
  subject to a separate limit of parallel worker threads, cf.\ system
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   237
  option @{system_option_ref threads}.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   238
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   239
  \medskip Option @{verbatim "-s"} enables \emph{system mode}, which
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   240
  means that resulting heap images and log files are stored in
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   241
  @{verbatim "$ISABELLE_HOME/heaps"} instead of the default location
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   242
  @{setting ISABELLE_OUTPUT} (which is normally in @{setting
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   243
  ISABELLE_HOME_USER}, i.e.\ the user's home directory).
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   244
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   245
  \medskip Option @{verbatim "-v"} enables verbose mode.
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   246
*}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   247
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   248
subsubsection {* Examples *}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   249
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   250
text {*
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   251
  Build a specific logic image:
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   252
\begin{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   253
isabelle build -b HOLCF
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   254
\end{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   255
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   256
  \smallskip Build the main group of logic images:
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   257
\begin{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   258
isabelle build -b -g main
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   259
\end{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   260
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   261
  \smallskip Provide a general overview of the status of all Isabelle
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   262
  sessions, without building anything:
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   263
\begin{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   264
isabelle build -a -n -v
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   265
\end{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   266
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   267
  \smallskip Build all sessions with HTML browser info and PDF
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   268
  document preparation:
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   269
\begin{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   270
isabelle build -a -o browser_info -o document=pdf
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   271
\end{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   272
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   273
  \smallskip Build all sessions with a maximum of 8 parallel prover
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   274
  processes and 4 worker threads each (on a machine with many cores):
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   275
\begin{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   276
isabelle build -a -j8 -o threads=4
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   277
\end{ttbox}
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   278
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   279
  \smallskip Build some session images with cleanup of their
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   280
  descendants, while retaining their ancestry:
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   281
\begin{ttbox}
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   282
isabelle build -b -c HOL-Boogie HOL-SPARK
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   283
\end{ttbox}
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   284
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   285
  \smallskip Clean all sessions without building anything:
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   286
\begin{ttbox}
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   287
isabelle build -a -n -c
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   288
\end{ttbox}
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   289
*}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   290
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   291
end