src/Doc/System/Sessions.thy
author blanchet
Tue, 10 Sep 2013 15:56:51 +0200
changeset 53500 53b9326196fe
parent 52735 842b5e7dcac8
child 53519 3c977c570e20
permissions -rw-r--r--
don't be so verbose about SMT solver failures
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
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
     8
  theories that may be associated with formal documents
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
     9
  (\chref{ch:present}).  There is also a notion of \emph{persistent
48604
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
51417
d266f9329368 sessions may be organized via 'chapter' in ROOT;
wenzelm
parents: 51055
diff changeset
    41
  etc.  The grammar for @{syntax session_chapter} and @{syntax
d266f9329368 sessions may be organized via 'chapter' in ROOT;
wenzelm
parents: 51055
diff changeset
    42
  session_entry} is given as syntax diagram below; each ROOT file may
d266f9329368 sessions may be organized via 'chapter' in ROOT;
wenzelm
parents: 51055
diff changeset
    43
  contain multiple specifications like this.  Chapters help to
d266f9329368 sessions may be organized via 'chapter' in ROOT;
wenzelm
parents: 51055
diff changeset
    44
  organize browser info (\secref{sec:info}), but have no formal
d266f9329368 sessions may be organized via 'chapter' in ROOT;
wenzelm
parents: 51055
diff changeset
    45
  meaning.  The default chapter is ``@{text "Unsorted"}''.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    46
48582
wenzelm
parents: 48580
diff changeset
    47
  Isabelle/jEdit (\secref{sec:tool-jedit}) includes a simple editing
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
    48
  mode @{verbatim "isabelle-root"} for session ROOT files, which is
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
    49
  enabled by default for any file of that name.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    50
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    51
  @{rail "
51417
d266f9329368 sessions may be organized via 'chapter' in ROOT;
wenzelm
parents: 51055
diff changeset
    52
    @{syntax_def session_chapter}: @'chapter' @{syntax name}
d266f9329368 sessions may be organized via 'chapter' in ROOT;
wenzelm
parents: 51055
diff changeset
    53
    ;
d266f9329368 sessions may be organized via 'chapter' in ROOT;
wenzelm
parents: 51055
diff changeset
    54
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    55
    @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    56
    ;
48916
f45ccc0d1ace clarified syntax boundary cases and errors;
wenzelm
parents: 48903
diff changeset
    57
    body: description? options? ( theories + ) files?
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    58
    ;
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48737
diff changeset
    59
    spec: @{syntax name} groups? dir?
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    60
    ;
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    61
    groups: '(' (@{syntax name} +) ')'
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    62
    ;
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    63
    dir: @'in' @{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
    description: @'description' @{syntax text}
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    66
    ;
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    67
    options: @'options' opts
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    68
    ;
48605
e777363440d6 allow negative int values as well, according to real = int | float;
wenzelm
parents: 48604
diff changeset
    69
    opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'
e777363440d6 allow negative int values as well, according to real = int | float;
wenzelm
parents: 48604
diff changeset
    70
    ;
e777363440d6 allow negative int values as well, according to real = int | float;
wenzelm
parents: 48604
diff changeset
    71
    value: @{syntax name} | @{syntax real}
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    72
    ;
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48738
diff changeset
    73
    theories: @'theories' opts? ( @{syntax name} * )
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    74
    ;
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    75
    files: @'files' ( @{syntax name} + )
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    76
    "}
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    77
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    78
  \begin{description}
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    79
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    80
  \item \isakeyword{session}~@{text "A = B + body"} defines a new
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    81
  session @{text "A"} based on parent session @{text "B"}, with its
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    82
  content given in @{text body} (theories and auxiliary source files).
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    83
  Note that a parent (like @{text "HOL"}) is mandatory in practical
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    84
  applications: only Isabelle/Pure can bootstrap itself from nothing.
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    85
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    86
  All such session specifications together describe a hierarchy (tree)
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48737
diff changeset
    87
  of sessions, with globally unique names.  The new session name
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
    88
  @{text "A"} should be sufficiently long and descriptive to stand on
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
    89
  its own in a potentially large library.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    90
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    91
  \item \isakeyword{session}~@{text "A (groups)"} indicates a
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    92
  collection of groups where the new session is a member.  Group names
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    93
  are uninterpreted and merely follow certain conventions.  For
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    94
  example, the Isabelle distribution tags some important sessions by
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    95
  the group name called ``@{text "main"}''.  Other projects may invent
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    96
  their own conventions, but this requires some care to avoid clashes
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    97
  within this unchecked name space.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    98
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    99
  \item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"}
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48737
diff changeset
   100
  specifies an explicit directory for this session; by default this is
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48737
diff changeset
   101
  the current directory of the @{verbatim ROOT} file.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   102
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   103
  All theories and auxiliary source files are located relatively to
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   104
  the session directory.  The prover process is run within the same as
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   105
  its current working directory.
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   106
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   107
  \item \isakeyword{description}~@{text "text"} is a free-form
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   108
  annotation for this session.
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   109
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   110
  \item \isakeyword{options}~@{text "[x = a, y = b, z]"} defines
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   111
  separate options (\secref{sec:system-options}) that are used when
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   112
  processing this session, but \emph{without} propagation to child
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   113
  sessions.  Note that @{text "z"} abbreviates @{text "z = true"} for
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   114
  Boolean options.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   115
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   116
  \item \isakeyword{theories}~@{text "options names"} specifies a
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   117
  block of theories that are processed within an environment that is
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   118
  augmented by the given options, in addition to the global session
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   119
  options given before.  Any number of blocks of \isakeyword{theories}
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   120
  may be given.  Options are only active for each
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   121
  \isakeyword{theories} block separately.
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{files}~@{text "files"} lists additional source
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   124
  files that are involved in the processing of this session.  This
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   125
  should cover anything outside the formal content of the theory
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   126
  sources, say some auxiliary {\TeX} files that are required for
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   127
  document processing.  In contrast, files that are loaded formally
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   128
  within a theory, e.g.\ via @{keyword "ML_file"}, need not be
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   129
  declared again.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   130
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   131
  \end{description}
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48579
diff changeset
   132
*}
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   133
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   134
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48579
diff changeset
   135
subsubsection {* Examples *}
9df76dd45900 some description of main build options;
wenzelm
parents: 48579
diff changeset
   136
9df76dd45900 some description of main build options;
wenzelm
parents: 48579
diff changeset
   137
text {* See @{file "~~/src/HOL/ROOT"} for a diversity of practically
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   138
  relevant situations, although it uses relatively complex
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   139
  quasi-hierarchic naming conventions like @{text "HOL\<dash>SPARK"},
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   140
  @{text "HOL\<dash>SPARK\<dash>Examples"}.  An alternative is to use
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48737
diff changeset
   141
  unqualified names that are relatively long and descriptive, as in
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48737
diff changeset
   142
  the Archive of Formal Proofs (\url{http://afp.sf.net}), for
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48737
diff changeset
   143
  example. *}
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   144
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   145
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   146
section {* System build options \label{sec:system-options} *}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   147
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48579
diff changeset
   148
text {* See @{file "~~/etc/options"} for the main defaults provided by
48582
wenzelm
parents: 48580
diff changeset
   149
  the Isabelle distribution.  Isabelle/jEdit (\secref{sec:tool-jedit})
wenzelm
parents: 48580
diff changeset
   150
  includes a simple editing mode @{verbatim "isabelle-options"} for
wenzelm
parents: 48580
diff changeset
   151
  this file-format.
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   152
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   153
  The following options are particulary relevant to build Isabelle
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   154
  sessions, in particular with document preparation
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   155
  (\chref{ch:present}).
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   156
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   157
  \begin{itemize}
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   158
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   159
  \item @{system_option_def "browser_info"} controls output of HTML
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   160
  browser info, see also \secref{sec:info}.
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   161
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   162
  \item @{system_option_def "document"} specifies the document output
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   163
  format, see @{tool document} option @{verbatim "-o"} in
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   164
  \secref{sec:tool-document}.  In practice, the most relevant values
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   165
  are @{verbatim "document=false"} or @{verbatim "document=pdf"}.
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   166
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   167
  \item @{system_option_def "document_output"} specifies an
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   168
  alternative directory for generated output of the document
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   169
  preparation system; the default is within the @{setting
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   170
  "ISABELLE_BROWSER_INFO"} hierarchy as explained in
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   171
  \secref{sec:info}.  See also @{tool mkroot}, which generates a
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   172
  default configuration with output readily available to the author of
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   173
  the document.
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   174
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   175
  \item @{system_option_def "document_variants"} specifies document
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   176
  variants as a colon-separated list of @{text "name=tags"} entries,
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   177
  corresponding to @{tool document} options @{verbatim "-n"} and
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   178
  @{verbatim "-t"}.
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   179
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   180
  For example, @{verbatim
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   181
  "document_variants=document:outline=/proof,/ML"} indicates two
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   182
  documents: the one called @{verbatim document} with default tags,
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   183
  and the other called @{verbatim outline} where proofs and ML
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   184
  sections are folded.
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   185
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   186
  Document variant names are just a matter of conventions.  It is also
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   187
  possible to use different document variant names (without tags) for
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   188
  different document root entries, see also
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   189
  \secref{sec:tool-document}.
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   190
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   191
  \item @{system_option_def "document_graph"} tells whether the
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   192
  generated document files should include a theory graph (cf.\
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   193
  \secref{sec:browse} and \secref{sec:info}).  The resulting EPS or
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   194
  PDF file can be included as graphics in {\LaTeX}.
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   195
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   196
  Note that this option is usually determined as static parameter of
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   197
  some session (e.g.\ within its @{verbatim ROOT} file) and \emph{not}
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   198
  given globally or on the command line of @{tool build}.
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   199
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   200
  \item @{system_option_def "threads"} determines the number of worker
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   201
  threads for parallel checking of theories and proofs.  The default
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   202
  @{text "0"} means that a sensible maximum value is determined by the
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   203
  underlying hardware.  For machines with many cores or with
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   204
  hyperthreading, this is often requires manual adjustment (on the
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   205
  command-line or within personal settings or preferences, not within
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   206
  a session @{verbatim ROOT}).
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   207
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   208
  \item @{system_option_def "condition"} specifies a comma-separated
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   209
  list of process environment variables (or Isabelle settings) that
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   210
  are required for the subsequent theories to be processed.
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   211
  Conditions are considered ``true'' if the corresponding environment
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   212
  value is defined and non-empty.
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   213
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   214
  For example, the @{verbatim "condition=ISABELLE_FULL_TEST"} may be
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   215
  used to guard extraordinary theories, which are meant to be enabled
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   216
  explicitly via some shell prefix @{verbatim "env ISABELLE_FULL_TEST=true"}
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   217
  before invoking @{tool build}.
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   218
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   219
  \item @{system_option_def "timeout"} specifies a real wall-clock
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   220
  timeout (in seconds) for the session as a whole.  The timer is
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   221
  controlled outside the ML process by the JVM that runs
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   222
  Isabelle/Scala.  Thus it is relatively reliable in canceling
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   223
  processes that get out of control, even if there is a deadlock
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   224
  without CPU time usage.
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   225
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   226
  \end{itemize}
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   227
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   228
  The @{tool_def options} tool prints Isabelle system options.  Its
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   229
  command-line usage is:
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   230
\begin{ttbox}
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   231
Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   232
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   233
  Options are:
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   234
    -b           include $ISABELLE_BUILD_OPTIONS
52735
842b5e7dcac8 support isabelle options -g;
wenzelm
parents: 52056
diff changeset
   235
    -g OPTION    get value of OPTION
50531
f841ac0cb757 clarified "isabelle options" command line, to make it more close to "isabelle components";
wenzelm
parents: 50406
diff changeset
   236
    -l           list options
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   237
    -x FILE      export to FILE in YXML format
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   238
50531
f841ac0cb757 clarified "isabelle options" command line, to make it more close to "isabelle components";
wenzelm
parents: 50406
diff changeset
   239
  Report Isabelle system options, augmented by MORE_OPTIONS given as
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   240
  arguments NAME=VAL or NAME.
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   241
\end{ttbox}
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   242
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   243
  The command line arguments provide additional system options of the
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   244
  form @{text "name"}@{verbatim "="}@{text "value"} or @{text name}
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   245
  for Boolean options.
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   246
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   247
  Option @{verbatim "-b"} augments the implicit environment of system
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   248
  options by the ones of @{setting ISABELLE_BUILD_OPTIONS}, cf.\
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   249
  \secref{sec:tool-build}.
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   250
52735
842b5e7dcac8 support isabelle options -g;
wenzelm
parents: 52056
diff changeset
   251
  Option @{verbatim "-g"} prints the value of the given option.
842b5e7dcac8 support isabelle options -g;
wenzelm
parents: 52056
diff changeset
   252
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   253
  Option @{verbatim "-x"} specifies a file to export the result in
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   254
  YXML format, instead of printing it in human-readable form.
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48579
diff changeset
   255
*}
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   256
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   257
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   258
section {* Invoking the build process \label{sec:tool-build} *}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   259
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48595
diff changeset
   260
text {* The @{tool_def build} tool invokes the build process for
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   261
  Isabelle sessions.  It manages dependencies between sessions,
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   262
  related sources of theories and auxiliary files, and target heap
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   263
  images.  Accordingly, it runs instances of the prover process with
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   264
  optional document preparation.  Its command-line usage
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   265
  is:\footnote{Isabelle/Scala provides the same functionality via
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   266
  \texttt{isabelle.Build.build}.}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48595
diff changeset
   267
\begin{ttbox}
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48595
diff changeset
   268
Usage: isabelle build [OPTIONS] [SESSIONS ...]
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   269
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   270
  Options are:
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   271
    -D DIR       include session directory and select its sessions
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   272
    -R           operate on requirements of selected sessions
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   273
    -a           select all sessions
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   274
    -b           build heap images
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   275
    -c           clean build
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   276
    -d DIR       include session directory
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   277
    -g NAME      select session group NAME
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   278
    -j INT       maximum number of parallel jobs (default 1)
48903
1621b3f26095 added build option -l (list files);
wenzelm
parents: 48814
diff changeset
   279
    -l           list session source files
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   280
    -n           no build -- test dependencies only
52056
fc458f304f93 added isabelle-process option -o;
wenzelm
parents: 51417
diff changeset
   281
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   282
    -s           system build mode: produce output in ISABELLE_HOME
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   283
    -v           verbose
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   284
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   285
  Build and manage Isabelle sessions, depending on implicit
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   286
  ISABELLE_BUILD_OPTIONS="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   287
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   288
  ML_PLATFORM="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   289
  ML_HOME="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   290
  ML_SYSTEM="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   291
  ML_OPTIONS="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   292
\end{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   293
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   294
  \medskip Isabelle sessions are defined via session ROOT files as
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   295
  described in (\secref{sec:session-root}).  The totality of sessions
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   296
  is determined by collecting such specifications from all Isabelle
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   297
  component directories (\secref{sec:components}), augmented by more
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   298
  directories given via options @{verbatim "-d"}~@{text "DIR"} on the
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   299
  command line.  Each such directory may contain a session
48650
47330b712f8f discontinued unused etc/sessions catalog;
wenzelm
parents: 48605
diff changeset
   300
  \texttt{ROOT} file with several session specifications.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   301
48684
9170e10c651e re-introduced ROOTS catalog files (cf. 47330b712f8f) which help to organize AFP or make -d options persistent;
wenzelm
parents: 48683
diff changeset
   302
  Any session root directory may refer recursively to further
9170e10c651e re-introduced ROOTS catalog files (cf. 47330b712f8f) which help to organize AFP or make -d options persistent;
wenzelm
parents: 48683
diff changeset
   303
  directories of the same kind, by listing them in a catalog file
9170e10c651e re-introduced ROOTS catalog files (cf. 47330b712f8f) which help to organize AFP or make -d options persistent;
wenzelm
parents: 48683
diff changeset
   304
  @{verbatim "ROOTS"} line-by-line.  This helps to organize large
9170e10c651e re-introduced ROOTS catalog files (cf. 47330b712f8f) which help to organize AFP or make -d options persistent;
wenzelm
parents: 48683
diff changeset
   305
  collections of session specifications, or to make @{verbatim "-d"}
9170e10c651e re-introduced ROOTS catalog files (cf. 47330b712f8f) which help to organize AFP or make -d options persistent;
wenzelm
parents: 48683
diff changeset
   306
  command line options persistent (say within @{verbatim
9170e10c651e re-introduced ROOTS catalog files (cf. 47330b712f8f) which help to organize AFP or make -d options persistent;
wenzelm
parents: 48683
diff changeset
   307
  "$ISABELLE_HOME_USER/ROOTS"}).
9170e10c651e re-introduced ROOTS catalog files (cf. 47330b712f8f) which help to organize AFP or make -d options persistent;
wenzelm
parents: 48683
diff changeset
   308
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   309
  \medskip The subset of sessions to be managed is determined via
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   310
  individual @{text "SESSIONS"} given as command-line arguments, or
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   311
  session groups that are given via one or more options @{verbatim
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   312
  "-g"}~@{text "NAME"}.  Option @{verbatim "-a"} selects all sessions.
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   313
  The build tool takes session dependencies into account: the set of
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   314
  selected sessions is completed by including all ancestors.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   315
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   316
  \medskip Option @{verbatim "-R"} reverses the selection in the sense
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   317
  that it refers to its requirements: all ancestor sessions excluding
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   318
  the original selection.  This allows to prepare the stage for some
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   319
  build process with different options, before running the main build
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   320
  itself (without option @{verbatim "-R"}).
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   321
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   322
  \medskip Option @{verbatim "-D"} is similar to @{verbatim "-d"}, but
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   323
  selects all sessions that are defined in the given directories.
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   324
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   325
  \medskip The build process depends on additional options
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   326
  (\secref{sec:system-options}) that are passed to the prover
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   327
  eventually.  The settings variable @{setting_ref
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   328
  ISABELLE_BUILD_OPTIONS} allows to provide additional defaults, e.g.\
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   329
  \texttt{ISABELLE_BUILD_OPTIONS="document=pdf threads=4"}. Moreover,
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   330
  the environment of system build options may be augmented on the
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   331
  command line via @{verbatim "-o"}~@{text "name"}@{verbatim
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   332
  "="}@{text "value"} or @{verbatim "-o"}~@{text "name"}, which
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   333
  abbreviates @{verbatim "-o"}~@{text "name"}@{verbatim"=true"} for
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   334
  Boolean options.  Multiple occurrences of @{verbatim "-o"} on the
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   335
  command-line are applied in the given order.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   336
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   337
  \medskip Option @{verbatim "-b"} ensures that heap images are
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   338
  produced for all selected sessions.  By default, images are only
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   339
  saved for inner nodes of the hierarchy of sessions, as required for
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   340
  other sessions to continue later on.
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   341
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   342
  \medskip Option @{verbatim "-c"} cleans all descendants of the
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   343
  selected sessions before performing the specified build operation.
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   344
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   345
  \medskip Option @{verbatim "-n"} omits the actual build process
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   346
  after the preparatory stage (including optional cleanup).  Note that
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   347
  the return code always indicates the status of the set of selected
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   348
  sessions.
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   349
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   350
  \medskip Option @{verbatim "-j"} specifies the maximum number of
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   351
  parallel build jobs (prover processes).  Each prover process is
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   352
  subject to a separate limit of parallel worker threads, cf.\ system
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   353
  option @{system_option_ref threads}.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   354
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   355
  \medskip Option @{verbatim "-s"} enables \emph{system mode}, which
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   356
  means that resulting heap images and log files are stored in
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   357
  @{verbatim "$ISABELLE_HOME/heaps"} instead of the default location
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   358
  @{setting ISABELLE_OUTPUT} (which is normally in @{setting
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   359
  ISABELLE_HOME_USER}, i.e.\ the user's home directory).
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   360
48903
1621b3f26095 added build option -l (list files);
wenzelm
parents: 48814
diff changeset
   361
  \medskip Option @{verbatim "-v"} increases the general level of
1621b3f26095 added build option -l (list files);
wenzelm
parents: 48814
diff changeset
   362
  verbosity.  Option @{verbatim "-l"} lists the source files that
1621b3f26095 added build option -l (list files);
wenzelm
parents: 48814
diff changeset
   363
  contribute to a session.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   364
*}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   365
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   366
subsubsection {* Examples *}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   367
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   368
text {*
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   369
  Build a specific logic image:
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   370
\begin{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   371
isabelle build -b HOLCF
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   372
\end{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   373
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   374
  \smallskip Build the main group of logic images:
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   375
\begin{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   376
isabelle build -b -g main
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   377
\end{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   378
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   379
  \smallskip Provide a general overview of the status of all Isabelle
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   380
  sessions, without building anything:
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   381
\begin{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   382
isabelle build -a -n -v
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   383
\end{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   384
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   385
  \smallskip Build all sessions with HTML browser info and PDF
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   386
  document preparation:
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   387
\begin{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   388
isabelle build -a -o browser_info -o document=pdf
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   389
\end{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   390
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   391
  \smallskip Build all sessions with a maximum of 8 parallel prover
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   392
  processes and 4 worker threads each (on a machine with many cores):
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   393
\begin{ttbox}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   394
isabelle build -a -j8 -o threads=4
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   395
\end{ttbox}
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   396
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   397
  \smallskip Build some session images with cleanup of their
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   398
  descendants, while retaining their ancestry:
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   399
\begin{ttbox}
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   400
isabelle build -b -c HOL-Boogie HOL-SPARK
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   401
\end{ttbox}
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   402
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   403
  \smallskip Clean all sessions without building anything:
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   404
\begin{ttbox}
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   405
isabelle build -a -n -c
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   406
\end{ttbox}
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   407
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   408
  \smallskip Build all sessions from some other directory hierarchy,
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   409
  according to the settings variable @{verbatim "AFP"} that happens to
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   410
  be defined inside the Isabelle environment:
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   411
\begin{ttbox}
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   412
isabelle build -D '$AFP'
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   413
\end{ttbox}
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   414
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   415
  \smallskip Inform about the status of all sessions required for AFP,
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   416
  without building anything yet:
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   417
\begin{ttbox}
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   418
isabelle build -D '$AFP' -R -v -n
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   419
\end{ttbox}
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   420
*}
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   421
50406
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   422
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   423
section {* Build dialog *}
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   424
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   425
text {* The @{tool_def build_dialog} provides a simple GUI wrapper to
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   426
  the tool Isabelle @{tool build} tool.  This enables user interfaces
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   427
  like Isabelle/jEdit \secref{sec:tool-jedit} to provide read-made
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   428
  logic image on startup.  Its command-line usage is:
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   429
\begin{ttbox}
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   430
Usage: isabelle build_dialog [OPTIONS] LOGIC
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   431
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   432
  Options are:
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   433
    -L OPTION    default logic via system option
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   434
    -d DIR       include session directory
50546
1b01a57d2749 clarified build_dialog command line;
wenzelm
parents: 50531
diff changeset
   435
    -l NAME      logic session name
50406
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   436
    -s           system build mode: produce output in ISABELLE_HOME
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   437
50546
1b01a57d2749 clarified build_dialog command line;
wenzelm
parents: 50531
diff changeset
   438
  Build Isabelle logic session image via GUI dialog (default: \$ISABELLE_LOGIC).
50406
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   439
\end{ttbox}
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   440
50546
1b01a57d2749 clarified build_dialog command line;
wenzelm
parents: 50531
diff changeset
   441
  \medskip Option @{verbatim "-l"} specifies an explicit logic session
1b01a57d2749 clarified build_dialog command line;
wenzelm
parents: 50531
diff changeset
   442
  name.  Option @{verbatim "-L"} specifies a system option name as
1b01a57d2749 clarified build_dialog command line;
wenzelm
parents: 50531
diff changeset
   443
  fall-back to determine the logic session name.  If both are omitted
1b01a57d2749 clarified build_dialog command line;
wenzelm
parents: 50531
diff changeset
   444
  or have empty value, @{setting ISABELLE_LOGIC} is used as default.
50406
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   445
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   446
  \medskip Options @{verbatim "-d"} and @{verbatim "-s"} have the same
50546
1b01a57d2749 clarified build_dialog command line;
wenzelm
parents: 50531
diff changeset
   447
  meaning as for the command-line @{tool build} tool itself.  *}
50406
c28753665b8e documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents: 49131
diff changeset
   448
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   449
end