some description of isabelle build;
authorwenzelm
Sat Jul 28 15:21:49 2012 +0200 (2012-07-28)
changeset 4857821361b6189a6
parent 48577 1edc81c78079
child 48579 0b95a13ed90a
some description of isabelle build;
doc-src/ROOT
doc-src/System/IsaMakefile
doc-src/System/Thy/ROOT.ML
doc-src/System/Thy/Sessions.thy
doc-src/System/system.tex
doc-src/antiquote_setup.ML
lib/Tools/build
     1.1 --- a/doc-src/ROOT	Sat Jul 28 14:52:56 2012 +0200
     1.2 +++ b/doc-src/ROOT	Sat Jul 28 15:21:49 2012 +0200
     1.3 @@ -111,8 +111,9 @@
     1.4    theories
     1.5      Basics
     1.6      Interfaces
     1.7 +    Sessions
     1.8 +    Presentation
     1.9      Scala
    1.10 -    Presentation
    1.11      Misc
    1.12  
    1.13  session Tutorial (doc) in "TutorialI" = HOL +
     2.1 --- a/doc-src/System/IsaMakefile	Sat Jul 28 14:52:56 2012 +0200
     2.2 +++ b/doc-src/System/IsaMakefile	Sat Jul 28 15:21:49 2012 +0200
     2.3 @@ -23,7 +23,7 @@
     2.4  
     2.5  $(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/Base.thy	\
     2.6    Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy	\
     2.7 -  Thy/Scala.thy
     2.8 +  Thy/Scala.thy Thy/Sessions.thy
     2.9  	@$(USEDIR) -s System Pure Thy
    2.10  	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
    2.11  	 Thy/document/pdfsetup.sty Thy/document/session.tex
     3.1 --- a/doc-src/System/Thy/ROOT.ML	Sat Jul 28 14:52:56 2012 +0200
     3.2 +++ b/doc-src/System/Thy/ROOT.ML	Sat Jul 28 15:21:49 2012 +0200
     3.3 @@ -1,1 +1,1 @@
     3.4 -use_thys ["Basics", "Interfaces", "Scala", "Presentation", "Misc"];
     3.5 +use_thys ["Basics", "Interfaces", "Scala", "Sessions", "Presentation", "Misc"];
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/System/Thy/Sessions.thy	Sat Jul 28 15:21:49 2012 +0200
     4.3 @@ -0,0 +1,139 @@
     4.4 +theory Sessions
     4.5 +imports Base
     4.6 +begin
     4.7 +
     4.8 +chapter {* Isabelle sessions and build management *}
     4.9 +
    4.10 +text {* FIXME *}
    4.11 +
    4.12 +section {* Session ROOT specifications \label{sec:session-root} *}
    4.13 +
    4.14 +text {* FIXME *}
    4.15 +
    4.16 +
    4.17 +section {* System build options \label{sec:system-options} *}
    4.18 +
    4.19 +text {* FIXME *}
    4.20 +
    4.21 +
    4.22 +section {* Invoking the build process \label{sec:tool-build} *}
    4.23 +
    4.24 +text {* The @{tool_def build} utility invokes the build process for
    4.25 +  Isabelle sessions.  It manages dependencies between sessions,
    4.26 +  related sources of theories and auxiliary files, and target heap
    4.27 +  images.  Accordingly, it runs instances of the prover process with
    4.28 +  optional document preparation.  Its command-line usage
    4.29 +  is:\footnote{Isabelle/Scala provides the same functionality via
    4.30 +  \texttt{isabelle.Build.build}.}
    4.31 +\begin{ttbox} Usage: isabelle build [OPTIONS] [SESSIONS ...]
    4.32 +
    4.33 +  Options are:
    4.34 +    -a           select all sessions
    4.35 +    -b           build heap images
    4.36 +    -d DIR       include session directory with ROOT file
    4.37 +    -g NAME      select session group NAME
    4.38 +    -j INT       maximum number of parallel jobs (default 1)
    4.39 +    -n           no build -- test dependencies only
    4.40 +    -o OPTION    override session configuration OPTION
    4.41 +                 (via NAME=VAL or NAME)
    4.42 +    -s           system build mode: produce output in ISABELLE_HOME
    4.43 +    -v           verbose
    4.44 +
    4.45 +  Build and manage Isabelle sessions, depending on implicit
    4.46 +  ISABELLE_BUILD_OPTIONS="..."
    4.47 +
    4.48 +  ML_PLATFORM="..."
    4.49 +  ML_HOME="..."
    4.50 +  ML_SYSTEM="..."
    4.51 +  ML_OPTIONS="..."
    4.52 +\end{ttbox}
    4.53 +
    4.54 +  \medskip Isabelle sessions are defined via session ROOT files as
    4.55 +  described in (\secref{sec:session-root}).  The totality of sessions
    4.56 +  is determined by collecting such specifications from all Isabelle
    4.57 +  component directories (\secref{sec:components}), augmented by more
    4.58 +  directories given via options @{verbatim "-d"}~@{text "DIR"} on the
    4.59 +  command line.  Each such directory may contain a session
    4.60 +  \texttt{ROOT} file and an additional catalog file @{verbatim
    4.61 +  "etc/sessions"} with further sub-directories (list of lines).  Note
    4.62 +  that a single \texttt{ROOT} file usually defines many sessions;
    4.63 +  catalogs are are only required for extra scalability and modularity
    4.64 +  of large libraries.
    4.65 +
    4.66 +  \medskip The subset of sessions to be managed is selected via
    4.67 +  individual @{text "SESSIONS"} given as command-line arguments, or
    4.68 +  session groups that are specified via one or more options @{verbatim
    4.69 +  "-g"}~@{text "NAME"}.  Option @{verbatim "-a"} selects all sessions.
    4.70 +  The build tool takes the hierarchy of sessions into account: the
    4.71 +  selected set of sessions is completed by including all ancestors
    4.72 +  according to the dependency structure.
    4.73 +
    4.74 +  \medskip The build process depends on additional options that are
    4.75 +  passed to the prover session eventually, see also
    4.76 +  (\secref{sec:system-options}).  The settings variable @{setting_ref
    4.77 +  ISABELLE_BUILD_OPTIONS} allows to provide additional defaults.
    4.78 +  Moreover, the environment of system build options may be augmented
    4.79 +  on the command line via @{verbatim "-o"}~@{text "NAME=VALUE"} or
    4.80 +  @{verbatim "-o"}~@{text "NAME"}, which abbreviates @{verbatim
    4.81 +  "-o"}~@{text "NAME=true"} for Boolean options.  Multiple occurrences
    4.82 +  of @{verbatim "-o"} on the command-line are applied in the given
    4.83 +  order.
    4.84 +
    4.85 +  \medskip Option @{verbatim "-b"} ensures that heap images are
    4.86 +  produced for all selected sessions.  By default, images are only
    4.87 +  saved for inner nodes of the hierarchy of sessions, as required for
    4.88 +  other sessions to continue later on.
    4.89 +
    4.90 +  \medskip Option @{verbatim "-j"} specifies the maximum number of
    4.91 +  parallel build jobs (prover processes).  Note that each process is
    4.92 +  subject to a separate limit of parallel threads, cf.\ system option
    4.93 +  @{system_option_ref threads}.
    4.94 +
    4.95 +  \medskip Option @{verbatim "-s"} enables \emph{system mode}, which
    4.96 +  means that resulting heap images and log files are stored in
    4.97 +  @{verbatim "$ISABELLE_HOME/heaps"} instead of the default location
    4.98 +  @{setting ISABELLE_OUTPUT} (which is normally in @{setting
    4.99 +  ISABELLE_HOME_USER}, i.e.\ the user's home directory).
   4.100 +
   4.101 +  \medskip Option @{verbatim "-n"} omits the actual build process
   4.102 +  after performing all dependency checks.  The return code indicates
   4.103 +  the status of the set of selected sessions.
   4.104 +
   4.105 +  \medskip Option @{verbatim "-v"} enables verbose mode.
   4.106 +*}
   4.107 +
   4.108 +subsubsection {* Examples *}
   4.109 +
   4.110 +text {*
   4.111 +  Build a specific logic image:
   4.112 +\begin{ttbox}
   4.113 +isabelle build -b HOLCF
   4.114 +\end{ttbox}
   4.115 +
   4.116 +  Build the main group of logic images (as determined by the session
   4.117 +  ROOT specifications of the Isabelle distribution):
   4.118 +\begin{ttbox}
   4.119 +isabelle build -b -g main
   4.120 +\end{ttbox}
   4.121 +
   4.122 +  Provide a general overview of the status of all Isabelle sessions,
   4.123 +  without building anything:
   4.124 +\begin{ttbox}
   4.125 +isabelle build -a -n -v
   4.126 +\end{ttbox}
   4.127 +
   4.128 +  Build all sessions with HTML browser info and PDF document
   4.129 +  preparation:
   4.130 +\begin{ttbox}
   4.131 +isabelle build -a -o browser_info -o document=pdf
   4.132 +\end{ttbox}
   4.133 +
   4.134 +  Build all sessions with a maximum of 8 prover processes and 4
   4.135 +  threads each (on a machine with many cores):
   4.136 +
   4.137 +\begin{ttbox}
   4.138 +isabelle build -a -j8 -o threads=4
   4.139 +\end{ttbox}
   4.140 +*}
   4.141 +
   4.142 +end
     5.1 --- a/doc-src/System/system.tex	Sat Jul 28 14:52:56 2012 +0200
     5.2 +++ b/doc-src/System/system.tex	Sat Jul 28 15:21:49 2012 +0200
     5.3 @@ -30,6 +30,7 @@
     5.4  
     5.5  \input{Thy/document/Basics.tex}
     5.6  \input{Thy/document/Interfaces.tex}
     5.7 +\input{Thy/document/Sessions.tex}
     5.8  \input{Thy/document/Presentation.tex}
     5.9  \input{Thy/document/Scala.tex}
    5.10  \input{Thy/document/Misc.tex}
     6.1 --- a/doc-src/antiquote_setup.ML	Sat Jul 28 14:52:56 2012 +0200
     6.2 +++ b/doc-src/antiquote_setup.ML	Sat Jul 28 15:21:49 2012 +0200
     6.3 @@ -205,6 +205,7 @@
     6.4    entity_antiqs (thy_check Thy_Output.intern_option Thy_Output.defined_option)
     6.5      "" "antiquotation option" #>
     6.6    entity_antiqs no_check "isatt" "setting" #>
     6.7 +  entity_antiqs no_check "isatt" "system option" #>
     6.8    entity_antiqs no_check "" "inference" #>
     6.9    entity_antiqs no_check "isatt" "executable" #>
    6.10    entity_antiqs (K check_tool) "isatt" "tool" #>
     7.1 --- a/lib/Tools/build	Sat Jul 28 14:52:56 2012 +0200
     7.2 +++ b/lib/Tools/build	Sat Jul 28 15:21:49 2012 +0200
     7.3 @@ -30,7 +30,7 @@
     7.4    echo "    -b           build heap images"
     7.5    echo "    -d DIR       include session directory with ROOT file"
     7.6    echo "    -g NAME      select session group NAME"
     7.7 -  echo "    -j INT       maximum number of jobs (default 1)"
     7.8 +  echo "    -j INT       maximum number of parallel jobs (default 1)"
     7.9    echo "    -n           no build -- test dependencies only"
    7.10    echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"
    7.11    echo "    -s           system build mode: produce output in ISABELLE_HOME"