src/Doc/System/Sessions.thy
author wenzelm
Sat, 10 Jun 2017 21:48:02 +0200
changeset 66061 880db47fed30
parent 65505 741fad555d82
child 66576 7d4da1c62de7
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
61656
cfabbc083977 more uniform jEdit properties;
wenzelm
parents: 61602
diff changeset
     1
(*:maxLineLen=78:*)
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
     2
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
     3
theory Sessions
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
     4
imports Base
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
     5
begin
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
     6
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
     7
chapter \<open>Isabelle sessions and build management \label{ch:session}\<close>
48584
8026c852cc10 some introduction on sessions;
wenzelm
parents: 48582
diff changeset
     8
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
     9
text \<open>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    10
  An Isabelle \<^emph>\<open>session\<close> consists of a collection of related theories that may
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    11
  be associated with formal documents (\chref{ch:present}). There is also a
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    12
  notion of \<^emph>\<open>persistent heap\<close> image to capture the state of a session,
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    13
  similar to object-code in compiled programming languages. Thus the concept
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    14
  of session resembles that of a ``project'' in common IDE environments, but
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    15
  the specific name emphasizes the connection to interactive theorem proving:
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    16
  the session wraps-up the results of user-interaction with the prover in a
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    17
  persistent form.
48584
8026c852cc10 some introduction on sessions;
wenzelm
parents: 48582
diff changeset
    18
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    19
  Application sessions are built on a given parent session, which may be built
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    20
  recursively on other parents. Following this path in the hierarchy
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    21
  eventually leads to some major object-logic session like \<open>HOL\<close>, which itself
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    22
  is based on \<open>Pure\<close> as the common root of all sessions.
48584
8026c852cc10 some introduction on sessions;
wenzelm
parents: 48582
diff changeset
    23
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    24
  Processing sessions may take considerable time. Isabelle build management
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    25
  helps to organize this efficiently. This includes support for parallel build
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    26
  jobs, in addition to the multithreaded theory and proof checking that is
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    27
  already provided by the prover process itself.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    28
\<close>
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    29
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    30
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    31
section \<open>Session ROOT specifications \label{sec:session-root}\<close>
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
    32
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    33
text \<open>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    34
  Session specifications reside in files called \<^verbatim>\<open>ROOT\<close> within certain
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    35
  directories, such as the home locations of registered Isabelle components or
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    36
  additional project directories given by the user.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    37
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    38
  The ROOT file format follows the lexical conventions of the \<^emph>\<open>outer syntax\<close>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    39
  of Isabelle/Isar, see also @{cite "isabelle-isar-ref"}. This defines common
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    40
  forms like identifiers, names, quoted strings, verbatim text, nested
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    41
  comments etc. The grammar for @{syntax session_chapter} and @{syntax
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    42
  session_entry} is given as syntax diagram below; each ROOT file may contain
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    43
  multiple specifications like this. Chapters help to organize browser info
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    44
  (\secref{sec:info}), but have no formal meaning. The default chapter is
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    45
  ``\<open>Unsorted\<close>''.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    46
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    47
  Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing mode
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    48
  \<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is enabled by default for any
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    49
  file of that name.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    50
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 54705
diff changeset
    51
  @{rail \<open>
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
    ;
56533
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 55112
diff changeset
    57
    body: description? options? (theories+) \<newline> files? (document_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
    ;
65504
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
    73
    sessions: @'sessions' (@{syntax name}+)
65374
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 64308
diff changeset
    74
    ;
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 64308
diff changeset
    75
    theories: @'theories' opts? (theory_entry*)
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    76
    ;
65504
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
    77
    theory_entry: @{syntax name} ('(' @'global' ')')?
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
    78
    ;
56533
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 55112
diff changeset
    79
    files: @'files' (@{syntax name}+)
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 55112
diff changeset
    80
    ;
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 55112
diff changeset
    81
    document_files: @'document_files' ('(' dir ')')? (@{syntax name}+)
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 54705
diff changeset
    82
  \<close>}
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    83
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    84
  \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
65504
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
    85
  parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions,
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
    86
  theories and auxiliary source files). Note that a parent (like \<open>HOL\<close>) is
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
    87
  mandatory in practical applications: only Isabelle/Pure can bootstrap itself
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
    88
  from nothing.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    89
65504
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
    90
  All such session specifications together describe a hierarchy (graph) of
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    91
  sessions, with globally unique names. The new session name \<open>A\<close> should be
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    92
  sufficiently long and descriptive to stand on its own in a potentially large
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    93
  library.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    94
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    95
  \<^descr> \isakeyword{session}~\<open>A (groups)\<close> indicates a collection of groups where
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    96
  the new session is a member. Group names are uninterpreted and merely follow
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    97
  certain conventions. For example, the Isabelle distribution tags some
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    98
  important sessions by the group name called ``\<open>main\<close>''. Other projects may
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    99
  invent their own conventions, but this requires some care to avoid clashes
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   100
  within this unchecked name space.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   101
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   102
  \<^descr> \isakeyword{session}~\<open>A\<close>~\isakeyword{in}~\<open>dir\<close> specifies an explicit
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   103
  directory for this session; by default this is the current directory of the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   104
  \<^verbatim>\<open>ROOT\<close> file.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   105
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   106
  All theories and auxiliary source files are located relatively to the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   107
  session directory. The prover process is run within the same as its current
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   108
  working directory.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   109
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   110
  \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   111
  session.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   112
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   113
  \<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   114
  (\secref{sec:system-options}) that are used when processing this session,
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   115
  but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z =
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   116
  true\<close> for Boolean options.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   117
65504
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
   118
  \<^descr> \isakeyword{sessions}~\<open>names\<close> specifies sessions that are \<^emph>\<open>imported\<close> into
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
   119
  the current name space of theories. This allows to refer to a theory \<open>A\<close>
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
   120
  from session \<open>B\<close> by the qualified name \<open>B.A\<close> --- although it is loaded again
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
   121
  into the current ML process, which is in contrast to a theory that is
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
   122
  already present in the \<^emph>\<open>parent\<close> session.
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
   123
65505
741fad555d82 exclude theories from other sessions;
wenzelm
parents: 65504
diff changeset
   124
  Theories that are imported from other sessions are excluded from the current
741fad555d82 exclude theories from other sessions;
wenzelm
parents: 65504
diff changeset
   125
  session document.
741fad555d82 exclude theories from other sessions;
wenzelm
parents: 65504
diff changeset
   126
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   127
  \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   128
  are processed within an environment that is augmented by the given options,
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   129
  in addition to the global session options given before. Any number of blocks
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   130
  of \isakeyword{theories} may be given. Options are only active for each
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   131
  \isakeyword{theories} block separately.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   132
65374
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 64308
diff changeset
   133
  A theory name that is followed by \<open>(\<close>\isakeyword{global}\<open>)\<close> is treated
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 64308
diff changeset
   134
  literally in other session specifications or theory imports. In contrast,
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 64308
diff changeset
   135
  the default is to qualify theory names by the session name, in order to
65504
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
   136
  ensure globally unique names in big session graphs.
65374
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 64308
diff changeset
   137
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   138
  \<^descr> \isakeyword{files}~\<open>files\<close> lists additional source files that are involved
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   139
  in the processing of this session. This should cover anything outside the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   140
  formal content of the theory sources. In contrast, files that are loaded
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   141
  formally within a theory, e.g.\ via @{command "ML_file"}, need not be
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   142
  declared again.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   143
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   144
  \<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   145
  source files for document preparation, typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   146
  {\LaTeX}. Only these explicitly given files are copied from the base
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   147
  directory to the document output directory, before formal document
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   148
  processing is started (see also \secref{sec:tool-document}). The local path
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   149
  structure of the \<open>files\<close> is preserved, which allows to reconstruct the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   150
  original directory hierarchy of \<open>base_dir\<close>.
56533
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 55112
diff changeset
   151
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   152
  \<^descr> \isakeyword{document_files}~\<open>files\<close> abbreviates
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   153
  \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>document) files\<close>, i.e.\
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   154
  document sources are taken from the base directory \<^verbatim>\<open>document\<close> within the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   155
  session root directory.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   156
\<close>
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   157
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   158
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   159
subsubsection \<open>Examples\<close>
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48579
diff changeset
   160
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   161
text \<open>
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   162
  See \<^file>\<open>~~/src/HOL/ROOT\<close> for a diversity of practically relevant situations,
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   163
  although it uses relatively complex quasi-hierarchic naming conventions like
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   164
  \<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to use unqualified
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   165
  names that are relatively long and descriptive, as in the Archive of Formal
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   166
  Proofs (\<^url>\<open>http://afp.sourceforge.net\<close>), for example.
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   167
\<close>
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   168
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   169
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   170
section \<open>System build options \label{sec:system-options}\<close>
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   171
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   172
text \<open>
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   173
  See \<^file>\<open>~~/etc/options\<close> for the main defaults provided by the Isabelle
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   174
  distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   175
  editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format.
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   176
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   177
  The following options are particularly relevant to build Isabelle sessions,
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   178
  in particular with document preparation (\chref{ch:present}).
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   179
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   180
    \<^item> @{system_option_def "browser_info"} controls output of HTML browser
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   181
    info, see also \secref{sec:info}.
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   182
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   183
    \<^item> @{system_option_def "document"} specifies the document output format,
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   184
    see @{tool document} option \<^verbatim>\<open>-o\<close> in \secref{sec:tool-document}. In
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   185
    practice, the most relevant values are \<^verbatim>\<open>document=false\<close> or
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   186
    \<^verbatim>\<open>document=pdf\<close>.
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   187
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   188
    \<^item> @{system_option_def "document_output"} specifies an alternative
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   189
    directory for generated output of the document preparation system; the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   190
    default is within the @{setting "ISABELLE_BROWSER_INFO"} hierarchy as
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   191
    explained in \secref{sec:info}. See also @{tool mkroot}, which generates a
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   192
    default configuration with output readily available to the author of the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   193
    document.
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   194
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   195
    \<^item> @{system_option_def "document_variants"} specifies document variants as
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   196
    a colon-separated list of \<open>name=tags\<close> entries, corresponding to @{tool
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   197
    document} options \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-t\<close>.
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   198
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   199
    For example, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   200
    two documents: the one called \<^verbatim>\<open>document\<close> with default tags, and the other
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   201
    called \<^verbatim>\<open>outline\<close> where proofs and ML sections are folded.
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   202
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   203
    Document variant names are just a matter of conventions. It is also
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   204
    possible to use different document variant names (without tags) for
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   205
    different document root entries, see also \secref{sec:tool-document}.
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   206
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   207
    \<^item> @{system_option_def "threads"} determines the number of worker threads
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   208
    for parallel checking of theories and proofs. The default \<open>0\<close> means that a
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   209
    sensible maximum value is determined by the underlying hardware. For
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   210
    machines with many cores or with hyperthreading, this is often requires
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   211
    manual adjustment (on the command-line or within personal settings or
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   212
    preferences, not within a session \<^verbatim>\<open>ROOT\<close>).
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   213
63827
b24d0e53dd03 option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents: 63680
diff changeset
   214
    \<^item> @{system_option_def "checkpoint"} helps to fine-tune the global heap
b24d0e53dd03 option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents: 63680
diff changeset
   215
    space management. This is relevant for big sessions that may exhaust the
b24d0e53dd03 option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents: 63680
diff changeset
   216
    small 32-bit address space of the ML process (which is used by default).
b24d0e53dd03 option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents: 63680
diff changeset
   217
    When the option is enabled for some \isakeyword{theories} block, a full
b24d0e53dd03 option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents: 63680
diff changeset
   218
    sharing stage of immutable values in memory happens \<^emph>\<open>before\<close> loading the
b24d0e53dd03 option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents: 63680
diff changeset
   219
    specified theories.
b24d0e53dd03 option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents: 63680
diff changeset
   220
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   221
    \<^item> @{system_option_def "condition"} specifies a comma-separated list of
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   222
    process environment variables (or Isabelle settings) that are required for
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   223
    the subsequent theories to be processed. Conditions are considered
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   224
    ``true'' if the corresponding environment value is defined and non-empty.
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   225
61602
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   226
    \<^item> @{system_option_def "timeout"} and @{system_option_def "timeout_scale"}
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   227
    specify a real wall-clock timeout for the session as a whole: the two
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   228
    values are multiplied and taken as the number of seconds. Typically,
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   229
    @{system_option "timeout"} is given for individual sessions, and
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   230
    @{system_option "timeout_scale"} as global adjustment to overall hardware
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   231
    performance.
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   232
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   233
    The timer is controlled outside the ML process by the JVM that runs
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   234
    Isabelle/Scala. Thus it is relatively reliable in canceling processes that
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   235
    get out of control, even if there is a deadlock without CPU time usage.
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   236
64308
b00508facb4f added system option "profiling";
wenzelm
parents: 64265
diff changeset
   237
    \<^item> @{system_option_def "profiling"} specifies a mode for global ML
b00508facb4f added system option "profiling";
wenzelm
parents: 64265
diff changeset
   238
    profiling. Possible values are the empty string (disabled), \<^verbatim>\<open>time\<close> for
b00508facb4f added system option "profiling";
wenzelm
parents: 64265
diff changeset
   239
    @{ML profile_time} and \<^verbatim>\<open>allocations\<close> for @{ML profile_allocations}.
b00508facb4f added system option "profiling";
wenzelm
parents: 64265
diff changeset
   240
    Results appear near the bottom of the session log file.
b00508facb4f added system option "profiling";
wenzelm
parents: 64265
diff changeset
   241
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   242
  The @{tool_def options} tool prints Isabelle system options. Its
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   243
  command-line usage is:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   244
  @{verbatim [display]
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   245
\<open>Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
48693
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
  Options are:
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   248
    -b           include $ISABELLE_BUILD_OPTIONS
52735
842b5e7dcac8 support isabelle options -g;
wenzelm
parents: 52056
diff changeset
   249
    -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
   250
    -l           list options
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   251
    -x FILE      export to FILE in YXML format
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   252
50531
f841ac0cb757 clarified "isabelle options" command line, to make it more close to "isabelle components";
wenzelm
parents: 50406
diff changeset
   253
  Report Isabelle system options, augmented by MORE_OPTIONS given as
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   254
  arguments NAME=VAL or NAME.\<close>}
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   255
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   256
  The command line arguments provide additional system options of the form
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   257
  \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close> for Boolean options.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   258
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   259
  Option \<^verbatim>\<open>-b\<close> augments the implicit environment of system options by the ones
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   260
  of @{setting ISABELLE_BUILD_OPTIONS}, cf.\ \secref{sec:tool-build}.
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   261
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   262
  Option \<^verbatim>\<open>-g\<close> prints the value of the given option. Option \<^verbatim>\<open>-l\<close> lists all
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   263
  options with their declaration and current value.
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   264
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   265
  Option \<^verbatim>\<open>-x\<close> specifies a file to export the result in YXML format, instead
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   266
  of printing it in human-readable form.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   267
\<close>
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   268
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   269
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   270
section \<open>Invoking the build process \label{sec:tool-build}\<close>
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   271
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   272
text \<open>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   273
  The @{tool_def build} tool invokes the build process for Isabelle sessions.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   274
  It manages dependencies between sessions, related sources of theories and
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   275
  auxiliary files, and target heap images. Accordingly, it runs instances of
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   276
  the prover process with optional document preparation. Its command-line
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   277
  usage is:\<^footnote>\<open>Isabelle/Scala provides the same functionality via
61572
ddb3ac3fef45 more antiquotations;
wenzelm
parents: 61568
diff changeset
   278
  \<^verbatim>\<open>isabelle.Build.build\<close>.\<close>
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   279
  @{verbatim [display]
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   280
\<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   281
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   282
  Options are:
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   283
    -D DIR       include session directory and select its sessions
64265
8eb6365f5916 isabelle build -N;
wenzelm
parents: 63827
diff changeset
   284
    -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   285
    -R           operate on requirements of selected sessions
60106
e0d1d9203275 allow to exclude session groups;
wenzelm
parents: 59892
diff changeset
   286
    -X NAME      exclude sessions from group NAME and all descendants
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   287
    -a           select all sessions
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   288
    -b           build heap images
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   289
    -c           clean build
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   290
    -d DIR       include session directory
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   291
    -g NAME      select session group NAME
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   292
    -j INT       maximum number of parallel jobs (default 1)
59891
9ce697050455 added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents: 59446
diff changeset
   293
    -k KEYWORD   check theory sources for conflicts with proposed keywords
48903
1621b3f26095 added build option -l (list files);
wenzelm
parents: 48814
diff changeset
   294
    -l           list session source files
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   295
    -n           no build -- test dependencies only
52056
fc458f304f93 added isabelle-process option -o;
wenzelm
parents: 51417
diff changeset
   296
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   297
    -s           system build mode: produce output in ISABELLE_HOME
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   298
    -v           verbose
60106
e0d1d9203275 allow to exclude session groups;
wenzelm
parents: 59892
diff changeset
   299
    -x NAME      exclude session NAME and all descendants
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   300
62596
cf79f8866bc3 tuned messages;
wenzelm
parents: 62289
diff changeset
   301
  Build and manage Isabelle sessions, depending on implicit settings:
cf79f8866bc3 tuned messages;
wenzelm
parents: 62289
diff changeset
   302
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   303
  ISABELLE_BUILD_OPTIONS="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   304
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   305
  ML_PLATFORM="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   306
  ML_HOME="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   307
  ML_SYSTEM="..."
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   308
  ML_OPTIONS="..."\<close>}
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   309
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   310
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   311
  Isabelle sessions are defined via session ROOT files as described in
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   312
  (\secref{sec:session-root}). The totality of sessions is determined by
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   313
  collecting such specifications from all Isabelle component directories
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   314
  (\secref{sec:components}), augmented by more directories given via options
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   315
  \<^verbatim>\<open>-d\<close>~\<open>DIR\<close> on the command line. Each such directory may contain a session
61503
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   316
  \<^verbatim>\<open>ROOT\<close> file with several session specifications.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   317
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   318
  Any session root directory may refer recursively to further directories of
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   319
  the same kind, by listing them in a catalog file \<^verbatim>\<open>ROOTS\<close> line-by-line. This
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   320
  helps to organize large collections of session specifications, or to make
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   321
  \<^verbatim>\<open>-d\<close> command line options persistent (say within
61503
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   322
  \<^verbatim>\<open>$ISABELLE_HOME_USER/ROOTS\<close>).
48684
9170e10c651e re-introduced ROOTS catalog files (cf. 47330b712f8f) which help to organize AFP or make -d options persistent;
wenzelm
parents: 48683
diff changeset
   323
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   324
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   325
  The subset of sessions to be managed is determined via individual \<open>SESSIONS\<close>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   326
  given as command-line arguments, or session groups that are given via one or
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   327
  more options \<^verbatim>\<open>-g\<close>~\<open>NAME\<close>. Option \<^verbatim>\<open>-a\<close> selects all sessions. The build tool
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   328
  takes session dependencies into account: the set of selected sessions is
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   329
  completed by including all ancestors.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   330
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   331
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   332
  One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded. All
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   333
  descendents of excluded sessions are removed from the selection as specified
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   334
  above. Option \<^verbatim>\<open>-X\<close> is analogous to this, but excluded sessions are
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   335
  specified by session group membership.
59892
2a616319c171 added isabelle build option -x, to exclude sessions;
wenzelm
parents: 59891
diff changeset
   336
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   337
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   338
  Option \<^verbatim>\<open>-R\<close> reverses the selection in the sense that it refers to its
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   339
  requirements: all ancestor sessions excluding the original selection. This
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   340
  allows to prepare the stage for some build process with different options,
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   341
  before running the main build itself (without option \<^verbatim>\<open>-R\<close>).
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   342
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   343
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   344
  Option \<^verbatim>\<open>-D\<close> is similar to \<^verbatim>\<open>-d\<close>, but selects all sessions that are defined
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   345
  in the given directories.
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   346
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   347
  \<^medskip>
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   348
  The build process depends on additional options
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   349
  (\secref{sec:system-options}) that are passed to the prover eventually. The
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   350
  settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide
61602
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   351
  additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>.
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   352
  Moreover, the environment of system build options may be augmented on the
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   353
  command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>, which abbreviates
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   354
  \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean options. Multiple occurrences of \<^verbatim>\<open>-o\<close> on
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   355
  the command-line are applied in the given order.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   356
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   357
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   358
  Option \<^verbatim>\<open>-b\<close> ensures that heap images are produced for all selected
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   359
  sessions. By default, images are only saved for inner nodes of the hierarchy
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   360
  of sessions, as required for other sessions to continue later on.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   361
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   362
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   363
  Option \<^verbatim>\<open>-c\<close> cleans all descendants of the selected sessions before
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   364
  performing the specified build operation.
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   365
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   366
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   367
  Option \<^verbatim>\<open>-n\<close> omits the actual build process after the preparatory stage
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   368
  (including optional cleanup). Note that the return code always indicates the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   369
  status of the set of selected sessions.
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   370
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   371
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   372
  Option \<^verbatim>\<open>-j\<close> specifies the maximum number of parallel build jobs (prover
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   373
  processes). Each prover process is subject to a separate limit of parallel
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   374
  worker threads, cf.\ system option @{system_option_ref threads}.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   375
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   376
  \<^medskip>
64265
8eb6365f5916 isabelle build -N;
wenzelm
parents: 63827
diff changeset
   377
  Option \<^verbatim>\<open>-N\<close> enables cyclic shuffling of NUMA CPU nodes. This may help
8eb6365f5916 isabelle build -N;
wenzelm
parents: 63827
diff changeset
   378
  performance tuning on Linux servers with separate CPU/memory modules.
8eb6365f5916 isabelle build -N;
wenzelm
parents: 63827
diff changeset
   379
8eb6365f5916 isabelle build -N;
wenzelm
parents: 63827
diff changeset
   380
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   381
  Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which means that resulting heap images
63669
256fc20716f2 clarified antiquotations;
wenzelm
parents: 62840
diff changeset
   382
  and log files are stored in @{path "$ISABELLE_HOME/heaps"} instead of the
256fc20716f2 clarified antiquotations;
wenzelm
parents: 62840
diff changeset
   383
  default location @{setting ISABELLE_OUTPUT} (which is normally in @{setting
256fc20716f2 clarified antiquotations;
wenzelm
parents: 62840
diff changeset
   384
  ISABELLE_HOME_USER}, i.e.\ the user's home directory).
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   385
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   386
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   387
  Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. Option \<^verbatim>\<open>-l\<close> lists
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   388
  the source files that contribute to a session.
59891
9ce697050455 added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents: 59446
diff changeset
   389
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   390
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   391
  Option \<^verbatim>\<open>-k\<close> specifies a newly proposed keyword for outer syntax (multiple
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   392
  uses allowed). The theory sources are checked for conflicts wrt.\ this
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   393
  hypothetical change of syntax, e.g.\ to reveal occurrences of identifiers
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   394
  that need to be quoted.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   395
\<close>
59891
9ce697050455 added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents: 59446
diff changeset
   396
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   397
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   398
subsubsection \<open>Examples\<close>
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   399
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   400
text \<open>
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   401
  Build a specific logic image:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   402
  @{verbatim [display] \<open>isabelle build -b HOLCF\<close>}
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   403
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   404
  \<^smallskip>
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   405
  Build the main group of logic images:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   406
  @{verbatim [display] \<open>isabelle build -b -g main\<close>}
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   407
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   408
  \<^smallskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   409
  Provide a general overview of the status of all Isabelle sessions, without
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   410
  building anything:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   411
  @{verbatim [display] \<open>isabelle build -a -n -v\<close>}
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   412
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   413
  \<^smallskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   414
  Build all sessions with HTML browser info and PDF document preparation:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   415
  @{verbatim [display] \<open>isabelle build -a -o browser_info -o document=pdf\<close>}
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   416
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   417
  \<^smallskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   418
  Build all sessions with a maximum of 8 parallel prover processes and 4
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   419
  worker threads each (on a machine with many cores):
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   420
  @{verbatim [display] \<open>isabelle build -a -j8 -o threads=4\<close>}
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   421
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   422
  \<^smallskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   423
  Build some session images with cleanup of their descendants, while retaining
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   424
  their ancestry:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   425
  @{verbatim [display] \<open>isabelle build -b -c HOL-Algebra HOL-Word\<close>}
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   426
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   427
  \<^smallskip>
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   428
  Clean all sessions without building anything:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   429
  @{verbatim [display] \<open>isabelle build -a -n -c\<close>}
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   430
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   431
  \<^smallskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   432
  Build all sessions from some other directory hierarchy, according to the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   433
  settings variable \<^verbatim>\<open>AFP\<close> that happens to be defined inside the Isabelle
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   434
  environment:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   435
  @{verbatim [display] \<open>isabelle build -D '$AFP'\<close>}
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   436
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   437
  \<^smallskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   438
  Inform about the status of all sessions required for AFP, without building
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   439
  anything yet:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   440
  @{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>}
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   441
\<close>
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   442
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   443
end