src/Doc/System/Sessions.thy
author wenzelm
Tue, 05 Dec 2017 16:03:58 +0100
changeset 67140 386a31d6d17a
parent 66993 2c2a346cfe70
child 67605 3dd0dfe04fcb
permissions -rw-r--r--
more documentation;
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
66971
43b2aac6053c tuned diagram;
wenzelm
parents: 66970
diff changeset
    55
    @{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \<newline>
43b2aac6053c tuned diagram;
wenzelm
parents: 66970
diff changeset
    56
      (@{syntax system_name} '+')? description? options? \<newline>
43b2aac6053c tuned diagram;
wenzelm
parents: 66970
diff changeset
    57
      (sessions?) (theories*) (document_files*)
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    58
    ;
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    59
    groups: '(' (@{syntax name} +) ')'
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    60
    ;
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    61
    dir: @'in' @{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
    description: @'description' @{syntax text}
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    64
    ;
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    65
    options: @'options' opts
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    66
    ;
48605
e777363440d6 allow negative int values as well, according to real = int | float;
wenzelm
parents: 48604
diff changeset
    67
    opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'
e777363440d6 allow negative int values as well, according to real = int | float;
wenzelm
parents: 48604
diff changeset
    68
    ;
e777363440d6 allow negative int values as well, according to real = int | float;
wenzelm
parents: 48604
diff changeset
    69
    value: @{syntax name} | @{syntax real}
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    70
    ;
66916
aca50a1572c5 more documentation;
wenzelm
parents: 66851
diff changeset
    71
    sessions: @'sessions' (@{syntax system_name}+)
65374
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 64308
diff changeset
    72
    ;
66970
13857f49d215 clarified ROOT syntax: 'sessions' and 'theories' are optional, but need to be non-empty;
wenzelm
parents: 66916
diff changeset
    73
    theories: @'theories' opts? (theory_entry+)
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    74
    ;
66916
aca50a1572c5 more documentation;
wenzelm
parents: 66851
diff changeset
    75
    theory_entry: @{syntax system_name} ('(' @'global' ')')?
65504
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
    76
    ;
56533
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 55112
diff changeset
    77
    document_files: @'document_files' ('(' dir ')')? (@{syntax name}+)
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 54705
diff changeset
    78
  \<close>}
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    79
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    80
  \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
66759
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66748
diff changeset
    81
  parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions and
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66748
diff changeset
    82
  theories). Note that a parent (like \<open>HOL\<close>) is mandatory in practical
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66748
diff changeset
    83
  applications: only Isabelle/Pure can bootstrap itself from nothing.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    84
65504
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
    85
  All such session specifications together describe a hierarchy (graph) of
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    86
  sessions, with globally unique names. The new session name \<open>A\<close> should be
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    87
  sufficiently long and descriptive to stand on its own in a potentially large
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    88
  library.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    89
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    90
  \<^descr> \isakeyword{session}~\<open>A (groups)\<close> indicates a collection of groups where
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    91
  the new session is a member. Group names are uninterpreted and merely follow
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    92
  certain conventions. For example, the Isabelle distribution tags some
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    93
  important sessions by the group name called ``\<open>main\<close>''. Other projects may
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    94
  invent their own conventions, but this requires some care to avoid clashes
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
    95
  within this unchecked name space.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
    96
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    97
  \<^descr> \isakeyword{session}~\<open>A\<close>~\isakeyword{in}~\<open>dir\<close> specifies an explicit
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    98
  directory for this session; by default this is the current directory of the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    99
  \<^verbatim>\<open>ROOT\<close> file.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   100
66759
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66748
diff changeset
   101
  All theory files are located relatively to the session directory. The prover
918f15c9367a discontinued obsolete 'files' in session ROOT;
wenzelm
parents: 66748
diff changeset
   102
  process is run within the same as its current working directory.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   103
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   104
  \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   105
  session.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   106
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   107
  \<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   108
  (\secref{sec:system-options}) that are used when processing this session,
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   109
  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
   110
  true\<close> for Boolean options.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   111
65504
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
   112
  \<^descr> \isakeyword{sessions}~\<open>names\<close> specifies sessions that are \<^emph>\<open>imported\<close> into
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
   113
  the current name space of theories. This allows to refer to a theory \<open>A\<close>
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
   114
  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
   115
  into the current ML process, which is in contrast to a theory that is
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
   116
  already present in the \<^emph>\<open>parent\<close> session.
b80477da30eb some documentation;
wenzelm
parents: 65374
diff changeset
   117
65505
741fad555d82 exclude theories from other sessions;
wenzelm
parents: 65504
diff changeset
   118
  Theories that are imported from other sessions are excluded from the current
741fad555d82 exclude theories from other sessions;
wenzelm
parents: 65504
diff changeset
   119
  session document.
741fad555d82 exclude theories from other sessions;
wenzelm
parents: 65504
diff changeset
   120
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   121
  \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   122
  are processed within an environment that is augmented by the given options,
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   123
  in addition to the global session options given before. Any number of blocks
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   124
  of \isakeyword{theories} may be given. Options are only active for each
48604
f651323139f0 misc tuning;
wenzelm
parents: 48602
diff changeset
   125
  \isakeyword{theories} block separately.
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   126
65374
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 64308
diff changeset
   127
  A theory name that is followed by \<open>(\<close>\isakeyword{global}\<open>)\<close> is treated
66993
2c2a346cfe70 clarified situation of global theory names;
wenzelm
parents: 66971
diff changeset
   128
  literally in other session specifications or theory imports --- the normal
2c2a346cfe70 clarified situation of global theory names;
wenzelm
parents: 66971
diff changeset
   129
  situation is to qualify theory names by the session name; this ensures
2c2a346cfe70 clarified situation of global theory names;
wenzelm
parents: 66971
diff changeset
   130
  globally unique names in big session graphs. Global theories are usually the
2c2a346cfe70 clarified situation of global theory names;
wenzelm
parents: 66971
diff changeset
   131
  entry points to major logic sessions: \<open>Pure\<close>, \<open>Main\<close>, \<open>Complex_Main\<close>,
2c2a346cfe70 clarified situation of global theory names;
wenzelm
parents: 66971
diff changeset
   132
  \<open>HOLCF\<close>, \<open>IFOL\<close>, \<open>FOL\<close>, \<open>ZF\<close>, \<open>ZFC\<close> etc. Regular Isabelle applications
2c2a346cfe70 clarified situation of global theory names;
wenzelm
parents: 66971
diff changeset
   133
  should not claim any global theory names.
65374
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 64308
diff changeset
   134
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   135
  \<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   136
  source files for document preparation, typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   137
  {\LaTeX}. Only these explicitly given files are copied from the base
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   138
  directory to the document output directory, before formal document
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   139
  processing is started (see also \secref{sec:tool-document}). The local path
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   140
  structure of the \<open>files\<close> is preserved, which allows to reconstruct the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   141
  original directory hierarchy of \<open>base_dir\<close>.
56533
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 55112
diff changeset
   142
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   143
  \<^descr> \isakeyword{document_files}~\<open>files\<close> abbreviates
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   144
  \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>document) files\<close>, i.e.\
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   145
  document sources are taken from the base directory \<^verbatim>\<open>document\<close> within the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   146
  session root directory.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   147
\<close>
48579
0b95a13ed90a more on "Session ROOT specifications";
wenzelm
parents: 48578
diff changeset
   148
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   149
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   150
subsubsection \<open>Examples\<close>
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48579
diff changeset
   151
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   152
text \<open>
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   153
  See \<^file>\<open>~~/src/HOL/ROOT\<close> for a diversity of practically relevant situations,
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   154
  although it uses relatively complex quasi-hierarchic naming conventions like
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   155
  \<^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
   156
  names that are relatively long and descriptive, as in the Archive of Formal
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   157
  Proofs (\<^url>\<open>http://afp.sourceforge.net\<close>), for example.
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   158
\<close>
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   159
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   160
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   161
section \<open>System build options \label{sec:system-options}\<close>
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   162
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   163
text \<open>
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   164
  See \<^file>\<open>~~/etc/options\<close> for the main defaults provided by the Isabelle
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   165
  distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   166
  editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format.
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   167
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   168
  The following options are particularly relevant to build Isabelle sessions,
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   169
  in particular with document preparation (\chref{ch:present}).
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   170
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   171
    \<^item> @{system_option_def "browser_info"} controls output of HTML browser
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   172
    info, see also \secref{sec:info}.
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   173
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   174
    \<^item> @{system_option_def "document"} specifies the document output format,
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   175
    see @{tool document} option \<^verbatim>\<open>-o\<close> in \secref{sec:tool-document}. In
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   176
    practice, the most relevant values are \<^verbatim>\<open>document=false\<close> or
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   177
    \<^verbatim>\<open>document=pdf\<close>.
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   178
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   179
    \<^item> @{system_option_def "document_output"} specifies an alternative
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   180
    directory for generated output of the document preparation system; the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   181
    default is within the @{setting "ISABELLE_BROWSER_INFO"} hierarchy as
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   182
    explained in \secref{sec:info}. See also @{tool mkroot}, which generates a
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   183
    default configuration with output readily available to the author of the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   184
    document.
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   185
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   186
    \<^item> @{system_option_def "document_variants"} specifies document variants as
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   187
    a colon-separated list of \<open>name=tags\<close> entries, corresponding to @{tool
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   188
    document} options \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-t\<close>.
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   189
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   190
    For example, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   191
    two documents: the one called \<^verbatim>\<open>document\<close> with default tags, and the other
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   192
    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
   193
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   194
    Document variant names are just a matter of conventions. It is also
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   195
    possible to use different document variant names (without tags) for
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   196
    different document root entries, see also \secref{sec:tool-document}.
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   197
67140
386a31d6d17a more documentation;
wenzelm
parents: 66993
diff changeset
   198
    \<^item> @{system_option_def "document_tags"} specifies a default for otherwise
386a31d6d17a more documentation;
wenzelm
parents: 66993
diff changeset
   199
    untagged commands. This is occasionally useful to control the global
386a31d6d17a more documentation;
wenzelm
parents: 66993
diff changeset
   200
    visibility of commands via session options (e.g. in \<^verbatim>\<open>ROOT\<close>).
386a31d6d17a more documentation;
wenzelm
parents: 66993
diff changeset
   201
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   202
    \<^item> @{system_option_def "threads"} determines the number of worker threads
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   203
    for parallel checking of theories and proofs. The default \<open>0\<close> means that a
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   204
    sensible maximum value is determined by the underlying hardware. For
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   205
    machines with many cores or with hyperthreading, this is often requires
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   206
    manual adjustment (on the command-line or within personal settings or
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   207
    preferences, not within a session \<^verbatim>\<open>ROOT\<close>).
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   208
63827
b24d0e53dd03 option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents: 63680
diff changeset
   209
    \<^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
   210
    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
   211
    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
   212
    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
   213
    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
   214
    specified theories.
b24d0e53dd03 option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents: 63680
diff changeset
   215
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   216
    \<^item> @{system_option_def "condition"} specifies a comma-separated list of
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   217
    process environment variables (or Isabelle settings) that are required for
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   218
    the subsequent theories to be processed. Conditions are considered
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   219
    ``true'' if the corresponding environment value is defined and non-empty.
51055
5c4be88f8747 some explanations of important build options;
wenzelm
parents: 50546
diff changeset
   220
61602
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   221
    \<^item> @{system_option_def "timeout"} and @{system_option_def "timeout_scale"}
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   222
    specify a real wall-clock timeout for the session as a whole: the two
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   223
    values are multiplied and taken as the number of seconds. Typically,
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   224
    @{system_option "timeout"} is given for individual sessions, and
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   225
    @{system_option "timeout_scale"} as global adjustment to overall hardware
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   226
    performance.
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   227
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   228
    The timer is controlled outside the ML process by the JVM that runs
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   229
    Isabelle/Scala. Thus it is relatively reliable in canceling processes that
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   230
    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
   231
64308
b00508facb4f added system option "profiling";
wenzelm
parents: 64265
diff changeset
   232
    \<^item> @{system_option_def "profiling"} specifies a mode for global ML
b00508facb4f added system option "profiling";
wenzelm
parents: 64265
diff changeset
   233
    profiling. Possible values are the empty string (disabled), \<^verbatim>\<open>time\<close> for
b00508facb4f added system option "profiling";
wenzelm
parents: 64265
diff changeset
   234
    @{ML profile_time} and \<^verbatim>\<open>allocations\<close> for @{ML profile_allocations}.
b00508facb4f added system option "profiling";
wenzelm
parents: 64265
diff changeset
   235
    Results appear near the bottom of the session log file.
b00508facb4f added system option "profiling";
wenzelm
parents: 64265
diff changeset
   236
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   237
  The @{tool_def options} tool prints Isabelle system options. Its
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   238
  command-line usage is:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   239
  @{verbatim [display]
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   240
\<open>Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   241
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   242
  Options are:
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   243
    -b           include $ISABELLE_BUILD_OPTIONS
52735
842b5e7dcac8 support isabelle options -g;
wenzelm
parents: 52056
diff changeset
   244
    -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
   245
    -l           list options
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   246
    -x FILE      export to FILE in YXML format
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   247
50531
f841ac0cb757 clarified "isabelle options" command line, to make it more close to "isabelle components";
wenzelm
parents: 50406
diff changeset
   248
  Report Isabelle system options, augmented by MORE_OPTIONS given as
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   249
  arguments NAME=VAL or NAME.\<close>}
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   250
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   251
  The command line arguments provide additional system options of the form
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   252
  \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close> for Boolean options.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   253
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   254
  Option \<^verbatim>\<open>-b\<close> augments the implicit environment of system options by the ones
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   255
  of @{setting ISABELLE_BUILD_OPTIONS}, cf.\ \secref{sec:tool-build}.
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   256
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   257
  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
   258
  options with their declaration and current value.
48693
ceeea46bdeba "isabelle options" prints Isabelle system options;
wenzelm
parents: 48684
diff changeset
   259
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   260
  Option \<^verbatim>\<open>-x\<close> specifies a file to export the result in YXML format, instead
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   261
  of printing it in human-readable form.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   262
\<close>
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   263
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   264
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   265
section \<open>Invoking the build process \label{sec:tool-build}\<close>
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   266
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   267
text \<open>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   268
  The @{tool_def build} tool invokes the build process for Isabelle sessions.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   269
  It manages dependencies between sessions, related sources of theories and
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   270
  auxiliary files, and target heap images. Accordingly, it runs instances of
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   271
  the prover process with optional document preparation. Its command-line
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   272
  usage is:\<^footnote>\<open>Isabelle/Scala provides the same functionality via
61572
ddb3ac3fef45 more antiquotations;
wenzelm
parents: 61568
diff changeset
   273
  \<^verbatim>\<open>isabelle.Build.build\<close>.\<close>
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   274
  @{verbatim [display]
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   275
\<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   276
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   277
  Options are:
66737
2edc0c42c883 option -B for "isabelle build" and "isabelle imports";
wenzelm
parents: 66671
diff changeset
   278
    -B NAME      include session NAME and all descendants
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   279
    -D DIR       include session directory and select its sessions
64265
8eb6365f5916 isabelle build -N;
wenzelm
parents: 63827
diff changeset
   280
    -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   281
    -R           operate on requirements of selected sessions
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66737
diff changeset
   282
    -S           soft build: only observe changes of sources, not heap images
60106
e0d1d9203275 allow to exclude session groups;
wenzelm
parents: 59892
diff changeset
   283
    -X NAME      exclude sessions from group NAME and all descendants
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   284
    -a           select all sessions
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   285
    -b           build heap images
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   286
    -c           clean build
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   287
    -d DIR       include session directory
66841
5c32a072ca8b added isablle build option -f;
wenzelm
parents: 66759
diff changeset
   288
    -f           fresh build
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   289
    -g NAME      select session group NAME
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   290
    -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
   291
    -k KEYWORD   check theory sources for conflicts with proposed keywords
48903
1621b3f26095 added build option -l (list files);
wenzelm
parents: 48814
diff changeset
   292
    -l           list session source files
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   293
    -n           no build -- test dependencies only
52056
fc458f304f93 added isabelle-process option -o;
wenzelm
parents: 51417
diff changeset
   294
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   295
    -s           system build mode: produce output in ISABELLE_HOME
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   296
    -v           verbose
60106
e0d1d9203275 allow to exclude session groups;
wenzelm
parents: 59892
diff changeset
   297
    -x NAME      exclude session NAME and all descendants
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   298
62596
cf79f8866bc3 tuned messages;
wenzelm
parents: 62289
diff changeset
   299
  Build and manage Isabelle sessions, depending on implicit settings:
cf79f8866bc3 tuned messages;
wenzelm
parents: 62289
diff changeset
   300
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   301
  ISABELLE_BUILD_OPTIONS="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   302
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   303
  ML_PLATFORM="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   304
  ML_HOME="..."
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   305
  ML_SYSTEM="..."
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   306
  ML_OPTIONS="..."\<close>}
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   307
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   308
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   309
  Isabelle sessions are defined via session ROOT files as described in
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   310
  (\secref{sec:session-root}). The totality of sessions is determined by
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   311
  collecting such specifications from all Isabelle component directories
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   312
  (\secref{sec:components}), augmented by more directories given via options
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   313
  \<^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
   314
  \<^verbatim>\<open>ROOT\<close> file with several session specifications.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   315
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   316
  Any session root directory may refer recursively to further directories of
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   317
  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
   318
  helps to organize large collections of session specifications, or to make
66576
wenzelm
parents: 65505
diff changeset
   319
  \<^verbatim>\<open>-d\<close> command line options persistent (e.g.\ in
61503
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   320
  \<^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
   321
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   322
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   323
  The subset of sessions to be managed is determined via individual \<open>SESSIONS\<close>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   324
  given as command-line arguments, or session groups that are given via one or
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   325
  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
   326
  takes session dependencies into account: the set of selected sessions is
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   327
  completed by including all ancestors.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   328
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   329
  \<^medskip>
66737
2edc0c42c883 option -B for "isabelle build" and "isabelle imports";
wenzelm
parents: 66671
diff changeset
   330
  One or more options \<^verbatim>\<open>-B\<close>~\<open>NAME\<close> specify base sessions. All descendants
2edc0c42c883 option -B for "isabelle build" and "isabelle imports";
wenzelm
parents: 66671
diff changeset
   331
  are included.
2edc0c42c883 option -B for "isabelle build" and "isabelle imports";
wenzelm
parents: 66671
diff changeset
   332
2edc0c42c883 option -B for "isabelle build" and "isabelle imports";
wenzelm
parents: 66671
diff changeset
   333
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   334
  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
   335
  descendents of excluded sessions are removed from the selection as specified
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   336
  above. Option \<^verbatim>\<open>-X\<close> is analogous to this, but excluded sessions are
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   337
  specified by session group membership.
59892
2a616319c171 added isabelle build option -x, to exclude sessions;
wenzelm
parents: 59891
diff changeset
   338
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   339
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   340
  Option \<^verbatim>\<open>-R\<close> reverses the selection in the sense that it refers to its
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   341
  requirements: all ancestor sessions excluding the original selection. This
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   342
  allows to prepare the stage for some build process with different options,
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   343
  before running the main build itself (without option \<^verbatim>\<open>-R\<close>).
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   344
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   345
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   346
  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
   347
  in the given directories.
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48693
diff changeset
   348
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   349
  \<^medskip>
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66737
diff changeset
   350
  Option \<^verbatim>\<open>-S\<close> indicates a ``soft build'': the selection is restricted to
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66737
diff changeset
   351
  those sessions that have changed sources (according to actually imported
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66737
diff changeset
   352
  theories). The status of heap images is ignored.
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66737
diff changeset
   353
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66737
diff changeset
   354
  \<^medskip>
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   355
  The build process depends on additional options
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   356
  (\secref{sec:system-options}) that are passed to the prover eventually. The
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   357
  settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide
61602
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   358
  additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>.
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   359
  Moreover, the environment of system build options may be augmented on the
a2f0f659a3c2 added option timeout_scale;
wenzelm
parents: 61575
diff changeset
   360
  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
   361
  \<^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
   362
  the command-line are applied in the given order.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   363
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   364
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   365
  Option \<^verbatim>\<open>-b\<close> ensures that heap images are produced for all selected
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   366
  sessions. By default, images are only saved for inner nodes of the hierarchy
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   367
  of sessions, as required for other sessions to continue later on.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   368
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   369
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   370
  Option \<^verbatim>\<open>-c\<close> cleans all descendants of the selected sessions before
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   371
  performing the specified build operation.
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   372
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   373
  \<^medskip>
66841
5c32a072ca8b added isablle build option -f;
wenzelm
parents: 66759
diff changeset
   374
  Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their
5c32a072ca8b added isablle build option -f;
wenzelm
parents: 66759
diff changeset
   375
  requirements.
5c32a072ca8b added isablle build option -f;
wenzelm
parents: 66759
diff changeset
   376
5c32a072ca8b added isablle build option -f;
wenzelm
parents: 66759
diff changeset
   377
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   378
  Option \<^verbatim>\<open>-n\<close> omits the actual build process after the preparatory stage
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   379
  (including optional cleanup). Note that the return code always indicates the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   380
  status of the set of selected sessions.
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   381
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   382
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   383
  Option \<^verbatim>\<open>-j\<close> specifies the maximum number of parallel build jobs (prover
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   384
  processes). Each prover process is subject to a separate limit of parallel
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   385
  worker threads, cf.\ system option @{system_option_ref threads}.
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   386
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   387
  \<^medskip>
64265
8eb6365f5916 isabelle build -N;
wenzelm
parents: 63827
diff changeset
   388
  Option \<^verbatim>\<open>-N\<close> enables cyclic shuffling of NUMA CPU nodes. This may help
8eb6365f5916 isabelle build -N;
wenzelm
parents: 63827
diff changeset
   389
  performance tuning on Linux servers with separate CPU/memory modules.
8eb6365f5916 isabelle build -N;
wenzelm
parents: 63827
diff changeset
   390
8eb6365f5916 isabelle build -N;
wenzelm
parents: 63827
diff changeset
   391
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   392
  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
   393
  and log files are stored in @{path "$ISABELLE_HOME/heaps"} instead of the
256fc20716f2 clarified antiquotations;
wenzelm
parents: 62840
diff changeset
   394
  default location @{setting ISABELLE_OUTPUT} (which is normally in @{setting
256fc20716f2 clarified antiquotations;
wenzelm
parents: 62840
diff changeset
   395
  ISABELLE_HOME_USER}, i.e.\ the user's home directory).
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   396
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   397
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   398
  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
   399
  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
   400
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   401
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   402
  Option \<^verbatim>\<open>-k\<close> specifies a newly proposed keyword for outer syntax (multiple
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   403
  uses allowed). The theory sources are checked for conflicts wrt.\ this
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   404
  hypothetical change of syntax, e.g.\ to reveal occurrences of identifiers
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   405
  that need to be quoted.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   406
\<close>
59891
9ce697050455 added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents: 59446
diff changeset
   407
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   408
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   409
subsubsection \<open>Examples\<close>
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   410
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   411
text \<open>
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   412
  Build a specific logic image:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   413
  @{verbatim [display] \<open>isabelle build -b HOLCF\<close>}
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   414
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   415
  \<^smallskip>
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   416
  Build the main group of logic images:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   417
  @{verbatim [display] \<open>isabelle build -b -g main\<close>}
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   418
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   419
  \<^smallskip>
66748
3efac90a11a7 more documentation;
wenzelm
parents: 66745
diff changeset
   420
  Build all descendants (and requirements) of \<^verbatim>\<open>FOL\<close> and \<^verbatim>\<open>ZF\<close>:
3efac90a11a7 more documentation;
wenzelm
parents: 66745
diff changeset
   421
  @{verbatim [display] \<open>isabelle build -B FOL -B ZF\<close>}
3efac90a11a7 more documentation;
wenzelm
parents: 66745
diff changeset
   422
3efac90a11a7 more documentation;
wenzelm
parents: 66745
diff changeset
   423
  \<^smallskip>
3efac90a11a7 more documentation;
wenzelm
parents: 66745
diff changeset
   424
  Build all sessions where sources have changed (ignoring heaps):
3efac90a11a7 more documentation;
wenzelm
parents: 66745
diff changeset
   425
  @{verbatim [display] \<open>isabelle build -a -S\<close>}
3efac90a11a7 more documentation;
wenzelm
parents: 66745
diff changeset
   426
3efac90a11a7 more documentation;
wenzelm
parents: 66745
diff changeset
   427
  \<^smallskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   428
  Provide a general overview of the status of all Isabelle sessions, without
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   429
  building anything:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   430
  @{verbatim [display] \<open>isabelle build -a -n -v\<close>}
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   431
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   432
  \<^smallskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   433
  Build all sessions with HTML browser info and PDF document preparation:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   434
  @{verbatim [display] \<open>isabelle build -a -o browser_info -o document=pdf\<close>}
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   435
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   436
  \<^smallskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   437
  Build all sessions with a maximum of 8 parallel prover processes and 4
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   438
  worker threads each (on a machine with many cores):
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   439
  @{verbatim [display] \<open>isabelle build -a -j8 -o threads=4\<close>}
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   440
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   441
  \<^smallskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   442
  Build some session images with cleanup of their descendants, while retaining
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   443
  their ancestry:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   444
  @{verbatim [display] \<open>isabelle build -b -c HOL-Algebra HOL-Word\<close>}
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   445
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   446
  \<^smallskip>
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   447
  Clean all sessions without building anything:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   448
  @{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
   449
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   450
  \<^smallskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   451
  Build all sessions from some other directory hierarchy, according to the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   452
  settings variable \<^verbatim>\<open>AFP\<close> that happens to be defined inside the Isabelle
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   453
  environment:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   454
  @{verbatim [display] \<open>isabelle build -D '$AFP'\<close>}
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48985
diff changeset
   455
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 60106
diff changeset
   456
  \<^smallskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   457
  Inform about the status of all sessions required for AFP, without building
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   458
  anything yet:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   459
  @{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>}
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   460
\<close>
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   461
66671
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   462
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   463
section \<open>Maintain theory imports wrt.\ session structure\<close>
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   464
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   465
text \<open>
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   466
  The @{tool_def "imports"} tool helps to maintain theory imports wrt.\
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   467
  session structure. It supports three main operations via options \<^verbatim>\<open>-I\<close>,
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   468
  \<^verbatim>\<open>-M\<close>, \<^verbatim>\<open>-U\<close>. Its command-line usage is: @{verbatim [display]
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   469
\<open>Usage: isabelle imports [OPTIONS] [SESSIONS ...]
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   470
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   471
  Options are:
66737
2edc0c42c883 option -B for "isabelle build" and "isabelle imports";
wenzelm
parents: 66671
diff changeset
   472
    -B NAME      include session NAME and all descendants
66671
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   473
    -D DIR       include session directory and select its sessions
66851
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66841
diff changeset
   474
    -I           operation: report session imports
66671
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   475
    -M           operation: Mercurial repository check for theory files
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   476
    -R           operate on requirements of selected sessions
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   477
    -U           operation: update theory imports to use session qualifiers
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   478
    -X NAME      exclude sessions from group NAME and all descendants
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   479
    -a           select all sessions
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   480
    -d DIR       include session directory
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   481
    -g NAME      select session group NAME
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   482
    -i           incremental update according to session graph structure
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   483
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   484
    -v           verbose
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   485
    -x NAME      exclude session NAME and all descendants
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   486
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   487
  Maintain theory imports wrt. session structure. At least one operation
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   488
  needs to be specified (see options -I -M -U).\<close>}
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   489
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   490
  \<^medskip>
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   491
  The selection of sessions and session directories works as for @{tool build}
66737
2edc0c42c883 option -B for "isabelle build" and "isabelle imports";
wenzelm
parents: 66671
diff changeset
   492
  via options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> (see
66671
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   493
  \secref{sec:tool-build}).
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   494
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   495
  \<^medskip>
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   496
  Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   497
  (see \secref{sec:tool-build}).
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   498
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   499
  \<^medskip>
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   500
  Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   501
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   502
  \<^medskip>
66851
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66841
diff changeset
   503
  Option \<^verbatim>\<open>-I\<close> determines reports session imports:
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66841
diff changeset
   504
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66841
diff changeset
   505
    \<^descr>[Potential session imports] are derived from old-style use of theory
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66841
diff changeset
   506
    files from other sessions via the directory structure. After declaring
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66841
diff changeset
   507
    those as \isakeyword{sessions} in the corresponding \<^verbatim>\<open>ROOT\<close> file entry, a
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66841
diff changeset
   508
    proper session-qualified theory name can be used (cf.\ option \<^verbatim>\<open>-U\<close>). For
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66841
diff changeset
   509
    example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> becomes formal
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66841
diff changeset
   510
    \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions}
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66841
diff changeset
   511
    \<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry.
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66841
diff changeset
   512
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66841
diff changeset
   513
    \<^descr>[Actual session imports] are derived from the session qualifiers of all
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66841
diff changeset
   514
    currently imported theories. This helps to minimize dependencies in the
c75769065548 more informative Imports.Report with actual session imports (minimized);
wenzelm
parents: 66841
diff changeset
   515
    session import structure to what is actually required.
66671
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   516
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   517
  \<^medskip>
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   518
  Option \<^verbatim>\<open>-M\<close> checks imported theories against the Mercurial repositories of
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   519
  the underlying session directories; non-repository directories are ignored.
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   520
  This helps to find files that are accidentally ignored, e.g.\ due to
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   521
  rearrangements of the session structure.
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   522
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   523
  \<^medskip>
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   524
  Option \<^verbatim>\<open>-U\<close> updates theory imports with old-style directory specifications
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   525
  to canonical session-qualified theory names, according to the theory name
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   526
  space imported via \isakeyword{sessions} within the \<^verbatim>\<open>ROOT\<close> specification.
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   527
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   528
  Option \<^verbatim>\<open>-i\<close> modifies the meaning of option \<^verbatim>\<open>-U\<close> to proceed incrementally,
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   529
  following to the session graph structure in bottom-up order. This may
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   530
  lead to more accurate results in complex session hierarchies.
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   531
\<close>
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   532
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   533
subsubsection \<open>Examples\<close>
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   534
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   535
text \<open>
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   536
  Determine potential session imports for some project directory:
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   537
  @{verbatim [display] \<open>isabelle imports -I -D 'some/where/My_Project'\<close>}
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   538
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   539
  \<^smallskip>
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   540
  Mercurial repository check for some project directory:
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   541
  @{verbatim [display] \<open>isabelle imports -M -D 'some/where/My_Project'\<close>}
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   542
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   543
  \<^smallskip>
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   544
  Incremental update of theory imports for some project directory:
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   545
  @{verbatim [display] \<open>isabelle imports -U -i -D 'some/where/My_Project'\<close>}
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   546
\<close>
41b64e53b6a1 more documentation;
wenzelm
parents: 66576
diff changeset
   547
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents:
diff changeset
   548
end