# HG changeset patch # User wenzelm # Date 1343481709 -7200 # Node ID 21361b6189a6ead5c0e33fa07f49608d23fbca52 # Parent 1edc81c7807916537e1046f5014d89c50614e24b some description of isabelle build; diff -r 1edc81c78079 -r 21361b6189a6 doc-src/ROOT --- a/doc-src/ROOT Sat Jul 28 14:52:56 2012 +0200 +++ b/doc-src/ROOT Sat Jul 28 15:21:49 2012 +0200 @@ -111,8 +111,9 @@ theories Basics Interfaces + Sessions + Presentation Scala - Presentation Misc session Tutorial (doc) in "TutorialI" = HOL + diff -r 1edc81c78079 -r 21361b6189a6 doc-src/System/IsaMakefile --- a/doc-src/System/IsaMakefile Sat Jul 28 14:52:56 2012 +0200 +++ b/doc-src/System/IsaMakefile Sat Jul 28 15:21:49 2012 +0200 @@ -23,7 +23,7 @@ $(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/Base.thy \ Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy \ - Thy/Scala.thy + Thy/Scala.thy Thy/Sessions.thy @$(USEDIR) -s System Pure Thy @rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \ Thy/document/pdfsetup.sty Thy/document/session.tex diff -r 1edc81c78079 -r 21361b6189a6 doc-src/System/Thy/ROOT.ML --- a/doc-src/System/Thy/ROOT.ML Sat Jul 28 14:52:56 2012 +0200 +++ b/doc-src/System/Thy/ROOT.ML Sat Jul 28 15:21:49 2012 +0200 @@ -1,1 +1,1 @@ -use_thys ["Basics", "Interfaces", "Scala", "Presentation", "Misc"]; +use_thys ["Basics", "Interfaces", "Scala", "Sessions", "Presentation", "Misc"]; diff -r 1edc81c78079 -r 21361b6189a6 doc-src/System/Thy/Sessions.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/Thy/Sessions.thy Sat Jul 28 15:21:49 2012 +0200 @@ -0,0 +1,139 @@ +theory Sessions +imports Base +begin + +chapter {* Isabelle sessions and build management *} + +text {* FIXME *} + +section {* Session ROOT specifications \label{sec:session-root} *} + +text {* FIXME *} + + +section {* System build options \label{sec:system-options} *} + +text {* FIXME *} + + +section {* Invoking the build process \label{sec:tool-build} *} + +text {* The @{tool_def build} utility invokes the build process for + Isabelle sessions. It manages dependencies between sessions, + related sources of theories and auxiliary files, and target heap + images. Accordingly, it runs instances of the prover process with + optional document preparation. Its command-line usage + is:\footnote{Isabelle/Scala provides the same functionality via + \texttt{isabelle.Build.build}.} +\begin{ttbox} Usage: isabelle build [OPTIONS] [SESSIONS ...] + + Options are: + -a select all sessions + -b build heap images + -d DIR include session directory with ROOT file + -g NAME select session group NAME + -j INT maximum number of parallel jobs (default 1) + -n no build -- test dependencies only + -o OPTION override session configuration OPTION + (via NAME=VAL or NAME) + -s system build mode: produce output in ISABELLE_HOME + -v verbose + + Build and manage Isabelle sessions, depending on implicit + ISABELLE_BUILD_OPTIONS="..." + + ML_PLATFORM="..." + ML_HOME="..." + ML_SYSTEM="..." + ML_OPTIONS="..." +\end{ttbox} + + \medskip Isabelle sessions are defined via session ROOT files as + described in (\secref{sec:session-root}). The totality of sessions + is determined by collecting such specifications from all Isabelle + component directories (\secref{sec:components}), augmented by more + directories given via options @{verbatim "-d"}~@{text "DIR"} on the + command line. Each such directory may contain a session + \texttt{ROOT} file and an additional catalog file @{verbatim + "etc/sessions"} with further sub-directories (list of lines). Note + that a single \texttt{ROOT} file usually defines many sessions; + catalogs are are only required for extra scalability and modularity + of large libraries. + + \medskip The subset of sessions to be managed is selected via + individual @{text "SESSIONS"} given as command-line arguments, or + session groups that are specified via one or more options @{verbatim + "-g"}~@{text "NAME"}. Option @{verbatim "-a"} selects all sessions. + The build tool takes the hierarchy of sessions into account: the + selected set of sessions is completed by including all ancestors + according to the dependency structure. + + \medskip The build process depends on additional options that are + passed to the prover session eventually, see also + (\secref{sec:system-options}). The settings variable @{setting_ref + ISABELLE_BUILD_OPTIONS} allows to provide additional defaults. + Moreover, the environment of system build options may be augmented + on the command line via @{verbatim "-o"}~@{text "NAME=VALUE"} or + @{verbatim "-o"}~@{text "NAME"}, which abbreviates @{verbatim + "-o"}~@{text "NAME=true"} for Boolean options. Multiple occurrences + of @{verbatim "-o"} on the command-line are applied in the given + order. + + \medskip Option @{verbatim "-b"} ensures that heap images are + produced for all selected sessions. By default, images are only + saved for inner nodes of the hierarchy of sessions, as required for + other sessions to continue later on. + + \medskip Option @{verbatim "-j"} specifies the maximum number of + parallel build jobs (prover processes). Note that each process is + subject to a separate limit of parallel threads, cf.\ system option + @{system_option_ref threads}. + + \medskip Option @{verbatim "-s"} enables \emph{system mode}, which + means that resulting heap images and log files are stored in + @{verbatim "$ISABELLE_HOME/heaps"} instead of the default location + @{setting ISABELLE_OUTPUT} (which is normally in @{setting + ISABELLE_HOME_USER}, i.e.\ the user's home directory). + + \medskip Option @{verbatim "-n"} omits the actual build process + after performing all dependency checks. The return code indicates + the status of the set of selected sessions. + + \medskip Option @{verbatim "-v"} enables verbose mode. +*} + +subsubsection {* Examples *} + +text {* + Build a specific logic image: +\begin{ttbox} +isabelle build -b HOLCF +\end{ttbox} + + Build the main group of logic images (as determined by the session + ROOT specifications of the Isabelle distribution): +\begin{ttbox} +isabelle build -b -g main +\end{ttbox} + + Provide a general overview of the status of all Isabelle sessions, + without building anything: +\begin{ttbox} +isabelle build -a -n -v +\end{ttbox} + + Build all sessions with HTML browser info and PDF document + preparation: +\begin{ttbox} +isabelle build -a -o browser_info -o document=pdf +\end{ttbox} + + Build all sessions with a maximum of 8 prover processes and 4 + threads each (on a machine with many cores): + +\begin{ttbox} +isabelle build -a -j8 -o threads=4 +\end{ttbox} +*} + +end diff -r 1edc81c78079 -r 21361b6189a6 doc-src/System/system.tex --- a/doc-src/System/system.tex Sat Jul 28 14:52:56 2012 +0200 +++ b/doc-src/System/system.tex Sat Jul 28 15:21:49 2012 +0200 @@ -30,6 +30,7 @@ \input{Thy/document/Basics.tex} \input{Thy/document/Interfaces.tex} +\input{Thy/document/Sessions.tex} \input{Thy/document/Presentation.tex} \input{Thy/document/Scala.tex} \input{Thy/document/Misc.tex} diff -r 1edc81c78079 -r 21361b6189a6 doc-src/antiquote_setup.ML --- a/doc-src/antiquote_setup.ML Sat Jul 28 14:52:56 2012 +0200 +++ b/doc-src/antiquote_setup.ML Sat Jul 28 15:21:49 2012 +0200 @@ -205,6 +205,7 @@ entity_antiqs (thy_check Thy_Output.intern_option Thy_Output.defined_option) "" "antiquotation option" #> entity_antiqs no_check "isatt" "setting" #> + entity_antiqs no_check "isatt" "system option" #> entity_antiqs no_check "" "inference" #> entity_antiqs no_check "isatt" "executable" #> entity_antiqs (K check_tool) "isatt" "tool" #> diff -r 1edc81c78079 -r 21361b6189a6 lib/Tools/build --- a/lib/Tools/build Sat Jul 28 14:52:56 2012 +0200 +++ b/lib/Tools/build Sat Jul 28 15:21:49 2012 +0200 @@ -30,7 +30,7 @@ echo " -b build heap images" echo " -d DIR include session directory with ROOT file" echo " -g NAME select session group NAME" - echo " -j INT maximum number of jobs (default 1)" + echo " -j INT maximum number of parallel jobs (default 1)" echo " -n no build -- test dependencies only" echo " -o OPTION override session configuration OPTION (via NAME=VAL or NAME)" echo " -s system build mode: produce output in ISABELLE_HOME"