diff --git a/src/Doc/System/Sessions.thy b/src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy +++ b/src/Doc/System/Sessions.thy @@ -1,758 +1,758 @@ (*:maxLineLen=78:*) theory Sessions imports Base begin chapter \Isabelle sessions and build management \label{ch:session}\ text \ An Isabelle \<^emph>\session\ consists of a collection of related theories that may be associated with formal documents (\chref{ch:present}). There is also a notion of \<^emph>\persistent heap\ image to capture the state of a session, similar to object-code in compiled programming languages. Thus the concept of session resembles that of a ``project'' in common IDE environments, but the specific name emphasizes the connection to interactive theorem proving: the session wraps-up the results of user-interaction with the prover in a persistent form. Application sessions are built on a given parent session, which may be built recursively on other parents. Following this path in the hierarchy eventually leads to some major object-logic session like \HOL\, which itself is based on \Pure\ as the common root of all sessions. Processing sessions may take considerable time. Isabelle build management helps to organize this efficiently. This includes support for parallel build jobs, in addition to the multithreaded theory and proof checking that is already provided by the prover process itself. \ section \Session ROOT specifications \label{sec:session-root}\ text \ Session specifications reside in files called \<^verbatim>\ROOT\ within certain directories, such as the home locations of registered Isabelle components or additional project directories given by the user. The ROOT file format follows the lexical conventions of the \<^emph>\outer syntax\ of Isabelle/Isar, see also @{cite "isabelle-isar-ref"}. This defines common forms like identifiers, names, quoted strings, verbatim text, nested comments etc. The grammar for @{syntax session_chapter} and @{syntax session_entry} is given as syntax diagram below; each ROOT file may contain multiple specifications like this. Chapters help to organize browser info (\secref{sec:info}), but have no formal meaning. The default chapter is ``\Unsorted\''. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing mode \<^verbatim>\isabelle-root\ for session ROOT files, which is enabled by default for any file of that name. \<^rail>\ @{syntax_def session_chapter}: @'chapter' @{syntax name} ; @{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \ (@{syntax system_name} '+')? description? options? \ sessions? directories? (theories*) \ (document_files*) (export_files*) ; groups: '(' (@{syntax name} +) ')' ; dir: @'in' @{syntax embedded} ; description: @'description' @{syntax text} ; options: @'options' opts ; opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']' ; value: @{syntax name} | @{syntax real} ; sessions: @'sessions' (@{syntax system_name}+) ; directories: @'directories' (dir+) ; theories: @'theories' opts? (theory_entry+) ; theory_entry: @{syntax system_name} ('(' @'global' ')')? ; document_files: @'document_files' ('(' dir ')')? (@{syntax embedded}+) ; export_files: @'export_files' ('(' dir ')')? ('[' nat ']')? \ (@{syntax embedded}+) \ \<^descr> \isakeyword{session}~\A = B + body\ defines a new session \A\ based on parent session \B\, with its content given in \body\ (imported sessions and theories). Note that a parent (like \HOL\) is mandatory in practical applications: only Isabelle/Pure can bootstrap itself from nothing. All such session specifications together describe a hierarchy (graph) of sessions, with globally unique names. The new session name \A\ should be sufficiently long and descriptive to stand on its own in a potentially large library. \<^descr> \isakeyword{session}~\A (groups)\ indicates a collection of groups where the new session is a member. Group names are uninterpreted and merely follow certain conventions. For example, the Isabelle distribution tags some important sessions by the group name called ``\main\''. Other projects may invent their own conventions, but this requires some care to avoid clashes within this unchecked name space. \<^descr> \isakeyword{session}~\A\~\isakeyword{in}~\dir\ specifies an explicit directory for this session; by default this is the current directory of the \<^verbatim>\ROOT\ file. All theory files are located relatively to the session directory. The prover process is run within the same as its current working directory. \<^descr> \isakeyword{description}~\text\ is a free-form annotation for this session. \<^descr> \isakeyword{options}~\[x = a, y = b, z]\ defines separate options (\secref{sec:system-options}) that are used when processing this session, but \<^emph>\without\ propagation to child sessions. Note that \z\ abbreviates \z = true\ for Boolean options. \<^descr> \isakeyword{sessions}~\names\ specifies sessions that are \<^emph>\imported\ into the current name space of theories. This allows to refer to a theory \A\ from session \B\ by the qualified name \B.A\ --- although it is loaded again into the current ML process, which is in contrast to a theory that is already present in the \<^emph>\parent\ session. Theories that are imported from other sessions are excluded from the current session document. \<^descr> \isakeyword{directories}~\dirs\ specifies additional directories for import of theory files via \isakeyword{theories} within \<^verbatim>\ROOT\ or \<^theory_text>\imports\ within a theory; \dirs\ are relative to the main session directory (cf.\ \isakeyword{session} \dots \isakeyword{in}~\dir\). These directories need to be exclusively assigned to a unique session, without implicit sharing of file-system locations. \<^descr> \isakeyword{theories}~\options names\ specifies a block of theories that are processed within an environment that is augmented by the given options, in addition to the global session options given before. Any number of blocks of \isakeyword{theories} may be given. Options are only active for each \isakeyword{theories} block separately. A theory name that is followed by \(\\isakeyword{global}\)\ is treated literally in other session specifications or theory imports --- the normal situation is to qualify theory names by the session name; this ensures globally unique names in big session graphs. Global theories are usually the entry points to major logic sessions: \Pure\, \Main\, \Complex_Main\, \HOLCF\, \IFOL\, \FOL\, \ZF\, \ZFC\ etc. Regular Isabelle applications should not claim any global theory names. \<^descr> \isakeyword{document_files}~\(\\isakeyword{in}~\base_dir) files\ lists source files for document preparation, typically \<^verbatim>\.tex\ and \<^verbatim>\.sty\ for {\LaTeX}. Only these explicitly given files are copied from the base directory to the document output directory, before formal document processing is started (see also \secref{sec:tool-document}). The local path structure of the \files\ is preserved, which allows to reconstruct the original directory hierarchy of \base_dir\. The default \base_dir\ is \<^verbatim>\document\ within the session root directory. \<^descr> \isakeyword{export_files}~\(\\isakeyword{in}~\target_dir) [number] patterns\ specifies theory exports that may get written to the file-system, e.g. via @{tool_ref build} with option \<^verbatim>\-e\ (\secref{sec:tool-build}). The \target_dir\ specification is relative to the session root directory; its default is \<^verbatim>\export\. Exports are selected via \patterns\ as in @{tool_ref export} (\secref{sec:tool-export}). The number given in brackets (default: 0) specifies elements that should be pruned from each name: it allows to reduce the resulting directory hierarchy at the danger of overwriting files due to loss of uniqueness. \ subsubsection \Examples\ text \ See \<^file>\~~/src/HOL/ROOT\ for a diversity of practically relevant situations, although it uses relatively complex quasi-hierarchic naming conventions like \<^verbatim>\HOL-SPARK\, \<^verbatim>\HOL-SPARK-Examples\. An alternative is to use unqualified names that are relatively long and descriptive, as in the Archive of Formal Proofs (\<^url>\https://isa-afp.org\), for example. \ section \System build options \label{sec:system-options}\ text \ See \<^file>\~~/etc/options\ for the main defaults provided by the Isabelle distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing mode \<^verbatim>\isabelle-options\ for this file-format. The following options are particularly relevant to build Isabelle sessions, in particular with document preparation (\chref{ch:present}). \<^item> @{system_option_def "browser_info"} controls output of HTML browser info, see also \secref{sec:info}. \<^item> @{system_option_def "document"} specifies the document output format, see @{tool document} option \<^verbatim>\-o\ in \secref{sec:tool-document}. In practice, the most relevant values are \<^verbatim>\document=false\ or \<^verbatim>\document=pdf\. \<^item> @{system_option_def "document_output"} specifies an alternative directory for generated output of the document preparation system; the default is within the @{setting "ISABELLE_BROWSER_INFO"} hierarchy as explained in \secref{sec:info}. See also @{tool mkroot}, which generates a default configuration with output readily available to the author of the document. \<^item> @{system_option_def "document_variants"} specifies document variants as a colon-separated list of \name=tags\ entries, corresponding to @{tool document} options \<^verbatim>\-n\ and \<^verbatim>\-t\. For example, \<^verbatim>\document_variants=document:outline=/proof,/ML\ indicates two documents: the one called \<^verbatim>\document\ with default tags, and the other called \<^verbatim>\outline\ where proofs and ML sections are folded. Document variant names are just a matter of conventions. It is also possible to use different document variant names (without tags) for different document root entries, see also \secref{sec:tool-document}. \<^item> @{system_option_def "document_tags"} specifies alternative command tags as a comma-separated list of items: either ``\command\\<^verbatim>\%\\tag\'' for a specific command, or ``\<^verbatim>\%\\tag\'' as default for all other commands. This is occasionally useful to control the global visibility of commands via session options (e.g.\ in \<^verbatim>\ROOT\). \<^item> @{system_option_def "threads"} determines the number of worker threads for parallel checking of theories and proofs. The default \0\ means that a sensible maximum value is determined by the underlying hardware. For machines with many cores or with hyperthreading, this is often requires manual adjustment (on the command-line or within personal settings or preferences, not within a session \<^verbatim>\ROOT\). \<^item> @{system_option_def "condition"} specifies a comma-separated list of process environment variables (or Isabelle settings) that are required for the subsequent theories to be processed. Conditions are considered ``true'' if the corresponding environment value is defined and non-empty. \<^item> @{system_option_def "timeout"} and @{system_option_def "timeout_scale"} specify a real wall-clock timeout for the session as a whole: the two values are multiplied and taken as the number of seconds. Typically, @{system_option "timeout"} is given for individual sessions, and @{system_option "timeout_scale"} as global adjustment to overall hardware performance. The timer is controlled outside the ML process by the JVM that runs Isabelle/Scala. Thus it is relatively reliable in canceling processes that get out of control, even if there is a deadlock without CPU time usage. \<^item> @{system_option_def "profiling"} specifies a mode for global ML profiling. Possible values are the empty string (disabled), \<^verbatim>\time\ for \<^ML>\profile_time\ and \<^verbatim>\allocations\ for \<^ML>\profile_allocations\. Results appear near the bottom of the session log file. \<^item> @{system_option_def "system_heaps"} determines the directories for session heap images: \<^path>\$ISABELLE_HEAPS\ is the user directory and \<^path>\$ISABELLE_HEAPS_SYSTEM\ the system directory (usually within the Isabelle application). For \<^verbatim>\system_heaps=false\, heaps are stored in the user directory and may be loaded from both directories. For \<^verbatim>\system_heaps=true\, store and load happens only in the system directory. The @{tool_def options} tool prints Isabelle system options. Its command-line usage is: @{verbatim [display] \Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...] Options are: -b include $ISABELLE_BUILD_OPTIONS -g OPTION get value of OPTION -l list options -x FILE export to FILE in YXML format Report Isabelle system options, augmented by MORE_OPTIONS given as arguments NAME=VAL or NAME.\} The command line arguments provide additional system options of the form \name\\<^verbatim>\=\\value\ or \name\ for Boolean options. Option \<^verbatim>\-b\ augments the implicit environment of system options by the ones of @{setting ISABELLE_BUILD_OPTIONS}, cf.\ \secref{sec:tool-build}. Option \<^verbatim>\-g\ prints the value of the given option. Option \<^verbatim>\-l\ lists all options with their declaration and current value. Option \<^verbatim>\-x\ specifies a file to export the result in YXML format, instead of printing it in human-readable form. \ section \Invoking the build process \label{sec:tool-build}\ text \ The @{tool_def build} tool 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 - \<^verbatim>\isabelle.Build.build\.\ + \<^scala_method>\isabelle.Build.build\.\ @{verbatim [display] \Usage: isabelle build [OPTIONS] [SESSIONS ...] Options are: -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -N cyclic shuffling of NUMA CPU nodes (performance tuning) -R refer to requirements of selected sessions -S soft build: only observe changes of sources, not heap images -X NAME exclude sessions from group NAME and all descendants -a select all sessions -b build heap images -c clean build -d DIR include session directory -e export files from session specification into file-system -f fresh build -g NAME select session group NAME -j INT maximum number of parallel jobs (default 1) -k KEYWORD check theory sources for conflicts with proposed keywords -l list session source files -n no build -- test dependencies only -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose -x NAME exclude session NAME and all descendants Build and manage Isabelle sessions, depending on implicit settings: ISABELLE_BUILD_OPTIONS="..." ML_PLATFORM="..." ML_HOME="..." ML_SYSTEM="..." ML_OPTIONS="..."\} \<^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\~\DIR\ on the command line. Each such directory may contain a session \<^verbatim>\ROOT\ file with several session specifications. Any session root directory may refer recursively to further directories of the same kind, by listing them in a catalog file \<^verbatim>\ROOTS\ line-by-line. This helps to organize large collections of session specifications, or to make \<^verbatim>\-d\ command line options persistent (e.g.\ in \<^verbatim>\$ISABELLE_HOME_USER/ROOTS\). \<^medskip> The subset of sessions to be managed is determined via individual \SESSIONS\ given as command-line arguments, or session groups that are given via one or more options \<^verbatim>\-g\~\NAME\. Option \<^verbatim>\-a\ selects all sessions. The build tool takes session dependencies into account: the set of selected sessions is completed by including all ancestors. \<^medskip> One or more options \<^verbatim>\-B\~\NAME\ specify base sessions to be included (all descendants wrt.\ the session parent or import graph). \<^medskip> One or more options \<^verbatim>\-x\~\NAME\ specify sessions to be excluded (all descendants wrt.\ the session parent or import graph). Option \<^verbatim>\-X\ is analogous to this, but excluded sessions are specified by session group membership. \<^medskip> Option \<^verbatim>\-R\ reverses the selection in the sense that it refers to its requirements: all ancestor sessions excluding the original selection. This allows to prepare the stage for some build process with different options, before running the main build itself (without option \<^verbatim>\-R\). \<^medskip> Option \<^verbatim>\-D\ is similar to \<^verbatim>\-d\, but selects all sessions that are defined in the given directories. \<^medskip> Option \<^verbatim>\-S\ indicates a ``soft build'': the selection is restricted to those sessions that have changed sources (according to actually imported theories). The status of heap images is ignored. \<^medskip> The build process depends on additional options (\secref{sec:system-options}) that are passed to the prover eventually. The settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide additional defaults, e.g.\ \<^verbatim>\ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\. Moreover, the environment of system build options may be augmented on the command line via \<^verbatim>\-o\~\name\\<^verbatim>\=\\value\ or \<^verbatim>\-o\~\name\, which abbreviates \<^verbatim>\-o\~\name\\<^verbatim>\=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>\-c\ cleans the selected sessions (all descendants wrt.\ the session parent or import graph) before performing the specified build operation. \<^medskip> Option \<^verbatim>\-e\ executes the \isakeyword{export_files} directives from the ROOT specification of all explicitly selected sessions: the status of the session build database needs to be OK, but the session could have been built earlier. Using \isakeyword{export_files}, a session may serve as abstract interface for add-on build artefacts, but these are only materialized on explicit request: without option \<^verbatim>\-e\ there is no effect on the physical file-system yet. \<^medskip> Option \<^verbatim>\-f\ forces a fresh build of all selected sessions and their requirements. \<^medskip> Option \<^verbatim>\-n\ omits the actual build process after the preparatory stage (including optional cleanup). Note that the return code always indicates the status of the set of selected sessions. \<^medskip> Option \<^verbatim>\-j\ specifies the maximum number of parallel build jobs (prover processes). Each prover process is subject to a separate limit of parallel worker threads, cf.\ system option @{system_option_ref threads}. \<^medskip> Option \<^verbatim>\-N\ enables cyclic shuffling of NUMA CPU nodes. This may help performance tuning on Linux servers with separate CPU/memory modules. \<^medskip> Option \<^verbatim>\-v\ increases the general level of verbosity. Option \<^verbatim>\-l\ lists the source files that contribute to a session. \<^medskip> Option \<^verbatim>\-k\ specifies a newly proposed keyword for outer syntax (multiple uses allowed). The theory sources are checked for conflicts wrt.\ this hypothetical change of syntax, e.g.\ to reveal occurrences of identifiers that need to be quoted. \ subsubsection \Examples\ text \ Build a specific logic image: @{verbatim [display] \isabelle build -b HOLCF\} \<^smallskip> Build the main group of logic images: @{verbatim [display] \isabelle build -b -g main\} \<^smallskip> Build all descendants (and requirements) of \<^verbatim>\FOL\ and \<^verbatim>\ZF\: @{verbatim [display] \isabelle build -B FOL -B ZF\} \<^smallskip> Build all sessions where sources have changed (ignoring heaps): @{verbatim [display] \isabelle build -a -S\} \<^smallskip> Provide a general overview of the status of all Isabelle sessions, without building anything: @{verbatim [display] \isabelle build -a -n -v\} \<^smallskip> Build all sessions with HTML browser info and PDF document preparation: @{verbatim [display] \isabelle build -a -o browser_info -o document=pdf\} \<^smallskip> Build all sessions with a maximum of 8 parallel prover processes and 4 worker threads each (on a machine with many cores): @{verbatim [display] \isabelle build -a -j8 -o threads=4\} \<^smallskip> Build some session images with cleanup of their descendants, while retaining their ancestry: @{verbatim [display] \isabelle build -b -c HOL-Algebra HOL-Word\} \<^smallskip> Clean all sessions without building anything: @{verbatim [display] \isabelle build -a -n -c\} \<^smallskip> Build all sessions from some other directory hierarchy, according to the settings variable \<^verbatim>\AFP\ that happens to be defined inside the Isabelle environment: @{verbatim [display] \isabelle build -D '$AFP'\} \<^smallskip> Inform about the status of all sessions required for AFP, without building anything yet: @{verbatim [display] \isabelle build -D '$AFP' -R -v -n\} \ section \Retrieve theory exports \label{sec:tool-export}\ text \ The @{tool_def "export"} tool retrieves theory exports from the session database. Its command-line usage is: @{verbatim [display] \Usage: isabelle export [OPTIONS] SESSION Options are: -O DIR output directory for exported files (default: "export") -d DIR include session directory -l list exports -n no build of session -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -p NUM prune path of exported files by NUM elements -x PATTERN extract files matching pattern (e.g.\ "*:**" for all) List or export theory exports for SESSION: named blobs produced by isabelle build. Option -l or -x is required; option -x may be repeated. The PATTERN language resembles glob patterns in the shell, with ? and * (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc], and variants {pattern1,pattern2,pattern3}.\} \<^medskip> The specified session is updated via @{tool build} (\secref{sec:tool-build}), with the same options \<^verbatim>\-d\, \<^verbatim>\-o\. The option \<^verbatim>\-n\ suppresses the implicit build process: it means that a potentially outdated session database is used! \<^medskip> Option \<^verbatim>\-l\ lists all stored exports, with compound names \theory\\<^verbatim>\:\\name\. \<^medskip> Option \<^verbatim>\-x\ extracts stored exports whose compound name matches the given pattern. Note that wild cards ``\<^verbatim>\?\'' and ``\<^verbatim>\*\'' do not match the separators ``\<^verbatim>\:\'' and ``\<^verbatim>\/\''; the wild card \<^verbatim>\**\ matches over directory name hierarchies separated by ``\<^verbatim>\/\''. Thus the pattern ``\<^verbatim>\*:**\'' matches \<^emph>\all\ theory exports. Multiple options \<^verbatim>\-x\ refer to the union of all specified patterns. Option \<^verbatim>\-O\ specifies an alternative output directory for option \<^verbatim>\-x\: the default is \<^verbatim>\export\ within the current directory. Each theory creates its own sub-directory hierarchy, using the session-qualified theory name. Option \<^verbatim>\-p\ specifies the number of elements that should be pruned from each name: it allows to reduce the resulting directory hierarchy at the danger of overwriting files due to loss of uniqueness. \ section \Dump PIDE session database \label{sec:tool-dump}\ text \ The @{tool_def "dump"} tool dumps information from the cumulative PIDE session database (which is processed on the spot). Its command-line usage is: @{verbatim [display] \Usage: isabelle dump [OPTIONS] [SESSIONS ...] Options are: -A NAMES dump named aspects (default: ...) -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -O DIR output directory for dumped files (default: "dump") -R refer to requirements of selected sessions -X NAME exclude sessions from group NAME and all descendants -a select all sessions -b NAME base logic image (default "Pure") -d DIR include session directory -g NAME select session group NAME -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose -x NAME exclude session NAME and all descendants Dump cumulative PIDE session database, with the following aspects: ...\} \<^medskip> Options \<^verbatim>\-B\, \<^verbatim>\-D\, \<^verbatim>\-R\, \<^verbatim>\-X\, \<^verbatim>\-a\, \<^verbatim>\-d\, \<^verbatim>\-g\, \<^verbatim>\-x\ and the remaining command-line arguments specify sessions as in @{tool build} (\secref{sec:tool-build}): the cumulative PIDE database of all their loaded theories is dumped to the output directory of option \<^verbatim>\-O\ (default: \<^verbatim>\dump\ in the current directory). \<^medskip> Option \<^verbatim>\-b\ specifies an optional base logic image, for improved scalability of the PIDE session. Its theories are only processed if it is included in the overall session selection. \<^medskip> Option \<^verbatim>\-o\ overrides Isabelle system options as for @{tool build} (\secref{sec:tool-build}). \<^medskip> Option \<^verbatim>\-v\ increases the general level of verbosity. \<^medskip> Option \<^verbatim>\-A\ specifies named aspects of the dump, as a comma-separated list. The default is to dump all known aspects, as given in the command-line usage of the tool. The underlying Isabelle/Scala operation \<^scala_method>\isabelle.Dump.dump\ takes aspects as user-defined operations on the final PIDE state and document version. This allows to imitate Prover IDE rendering under program control. \ subsubsection \Examples\ text \ Dump all Isabelle/ZF sessions (which are rather small): @{verbatim [display] \isabelle dump -v -B ZF\} \<^smallskip> Dump the quite substantial \<^verbatim>\HOL-Analysis\ session, with full bootstrap from Isabelle/Pure: @{verbatim [display] \isabelle dump -v HOL-Analysis\} \<^smallskip> Dump all sessions connected to HOL-Analysis, using main Isabelle/HOL as basis: @{verbatim [display] \isabelle dump -v -b HOL -B HOL-Analysis\} This results in uniform PIDE markup for everything, except for the Isabelle/Pure bootstrap process itself. Producing that on the spot requires several GB of heap space, both for the Isabelle/Scala and Isabelle/ML process (in 64bit mode). Here are some relevant settings (\secref{sec:boot}) for such ambitious applications: @{verbatim [display] \ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx32g -Xss16m" ML_OPTIONS="--minheap 4G --maxheap 32G" \} \ section \Update theory sources based on PIDE markup \label{sec:tool-update}\ text \ The @{tool_def "update"} tool updates theory sources based on markup that is produced from a running PIDE session (similar to @{tool dump} \secref{sec:tool-dump}). Its command-line usage is: @{verbatim [display] \Usage: isabelle update [OPTIONS] [SESSIONS ...] Options are: -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -R refer to requirements of selected sessions -X NAME exclude sessions from group NAME and all descendants -a select all sessions -b NAME base logic image (default "Pure") -d DIR include session directory -g NAME select session group NAME -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -u OPT overide update option: shortcut for "-o update_OPT" -v verbose -x NAME exclude session NAME and all descendants Update theory sources based on PIDE markup.\} \<^medskip> Options \<^verbatim>\-B\, \<^verbatim>\-D\, \<^verbatim>\-R\, \<^verbatim>\-X\, \<^verbatim>\-a\, \<^verbatim>\-d\, \<^verbatim>\-g\, \<^verbatim>\-x\ and the remaining command-line arguments specify sessions as in @{tool build} (\secref{sec:tool-build}) or @{tool dump} (\secref{sec:tool-dump}). \<^medskip> Option \<^verbatim>\-b\ specifies an optional base logic image, for improved scalability of the PIDE session. Its theories are only processed if it is included in the overall session selection. \<^medskip> Option \<^verbatim>\-v\ increases the general level of verbosity. \<^medskip> Option \<^verbatim>\-o\ overrides Isabelle system options as for @{tool build} (\secref{sec:tool-build}). Option \<^verbatim>\-u\ refers to specific \<^verbatim>\update\ options, by relying on naming convention: ``\<^verbatim>\-u\~\OPT\'' is a shortcut for ``\<^verbatim>\-o\~\<^verbatim>\update_\\OPT\''. \<^medskip> The following update options are supported: \<^item> @{system_option update_inner_syntax_cartouches} to update inner syntax (types, terms, etc.)~to use cartouches, instead of double-quoted strings or atomic identifiers. For example, ``\<^theory_text>\lemma \x = x\\'' is replaced by ``\<^theory_text>\lemma \x = x\\'', and ``\<^theory_text>\assume A\'' is replaced by ``\<^theory_text>\assume \A\\''. \<^item> @{system_option update_mixfix_cartouches} to update mixfix templates to use cartouches instead of double-quoted strings. For example, ``\<^theory_text>\(infixl \+\ 65)\'' is replaced by ``\<^theory_text>\(infixl \+\ 65)\''. \<^item> @{system_option update_control_cartouches} to update antiquotations to use the compact form with control symbol and cartouche argument. For example, ``\@{term \x + y\}\'' is replaced by ``\\<^term>\x + y\\'' (the control symbol is literally \<^verbatim>\\<^term>\.) \<^item> @{system_option update_path_cartouches} to update file-system paths to use cartouches: this depends on language markup provided by semantic processing of parsed input. It is also possible to produce custom updates in Isabelle/ML, by reporting \<^ML>\Markup.update\ with the precise source position and a replacement text. This operation should be made conditional on specific system options, similar to the ones above. Searching the above option names in ML sources of \<^dir>\$ISABELLE_HOME/src/Pure\ provides some examples. Updates can be in conflict by producing nested or overlapping edits: this may require to run @{tool update} multiple times. \ subsubsection \Examples\ text \ Update some cartouche notation in all theory sources required for session \<^verbatim>\HOL-Analysis\ (and ancestors): @{verbatim [display] \isabelle update -u mixfix_cartouches HOL-Analysis\} \<^smallskip> Update the same for all application sessions based on \<^verbatim>\HOL-Analysis\ --- using its image is taken starting point (for reduced resource requirements): @{verbatim [display] \isabelle update -u mixfix_cartouches -b HOL-Analysis -B HOL-Analysis\} \<^smallskip> Update sessions that build on \<^verbatim>\HOL-Proofs\, which need to be run separately with special options as follows: @{verbatim [display] \isabelle update -u mixfix_cartouches -l HOL-Proofs -B HOL-Proofs -o record_proofs=2\} \<^smallskip> See also the end of \secref{sec:tool-dump} for hints on increasing Isabelle/ML heap sizes for very big PIDE processes that include many sessions, notably from the Archive of Formal Proofs. \ section \Explore sessions structure\ text \ The @{tool_def "sessions"} tool explores the sessions structure. Its command-line usage is: @{verbatim [display] \Usage: isabelle sessions [OPTIONS] [SESSIONS ...] Options are: -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -R refer to requirements of selected sessions -X NAME exclude sessions from group NAME and all descendants -a select all sessions -d DIR include session directory -g NAME select session group NAME -x NAME exclude session NAME and all descendants Explore the structure of Isabelle sessions and print result names in topological order (on stdout).\} Arguments and options for session selection resemble @{tool build} (\secref{sec:tool-build}). \ subsubsection \Examples\ text \ All sessions of the Isabelle distribution: @{verbatim [display] \isabelle sessions -a\} \<^medskip> Sessions that are based on \<^verbatim>\ZF\ (and required by it): @{verbatim [display] \isabelle sessions -B ZF\} \<^medskip> All sessions of Isabelle/AFP (based in directory \<^path>\AFP\): @{verbatim [display] \isabelle sessions -D AFP/thys\} \<^medskip> Sessions required by Isabelle/AFP (based in directory \<^path>\AFP\): @{verbatim [display] \isabelle sessions -R -D AFP/thys\} \ end diff --git a/src/Pure/Admin/build_doc.scala b/src/Pure/Admin/build_doc.scala --- a/src/Pure/Admin/build_doc.scala +++ b/src/Pure/Admin/build_doc.scala @@ -1,106 +1,107 @@ /* Title: Pure/Admin/build_doc.scala Author: Makarius Build Isabelle documentation. */ package isabelle import java.io.{File => JFile} object Build_Doc { /* build_doc */ def build_doc( options: Options, progress: Progress = new Progress, all_docs: Boolean = false, max_jobs: Int = 1, docs: List[String] = Nil): Int = { val sessions_structure = Sessions.load_structure(options) val selection = for { name <- sessions_structure.build_topological_order info = sessions_structure(name) if info.groups.contains("doc") doc = info.options.string("document_variants") if all_docs || docs.contains(doc) } yield (doc, name) val selected_docs = selection.map(_._1) val sessions = selection.map(_._2) docs.filter(doc => !selected_docs.contains(doc)) match { case Nil => case bad => error("No documentation session for " + commas_quote(bad)) } progress.echo("Build started for documentation " + commas_quote(selected_docs)) val res1 = - Build.build(options, progress, requirements = true, build_heap = true, - max_jobs = max_jobs, sessions = sessions) + Build.build(options, Sessions.Selection(requirements = true, sessions = sessions), + progress = progress, build_heap = true, max_jobs = max_jobs) if (res1.ok) { Isabelle_System.with_tmp_dir("document_output")(output => { val res2 = Build.build( options.bool.update("browser_info", false). string.update("document", "pdf"). string.update("document_output", output.implode), - progress, clean_build = true, max_jobs = max_jobs, sessions = sessions) + Sessions.Selection(sessions = sessions), + progress = progress, clean_build = true, max_jobs = max_jobs) if (res2.ok) { val doc_dir = Path.explode("~~/doc") for (doc <- selected_docs) { val name = Path.explode(doc + ".pdf") File.copy(output + name, doc_dir + name) } } res2.rc }) } else res1.rc } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_doc", "build Isabelle documentation", args => { var all_docs = false var max_jobs = 1 var options = Options.init() val getopts = Getopts(""" Usage: isabelle build_doc [OPTIONS] [DOCS ...] Options are: -a select all documentation sessions -j INT maximum number of parallel jobs (default 1) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) Build Isabelle documentation from documentation sessions with suitable document_variants entry. """, "a" -> (_ => all_docs = true), "j:" -> (arg => max_jobs = Value.Int.parse(arg)), "o:" -> (arg => options = options + arg)) val docs = getopts(args) if (!all_docs && docs.isEmpty) getopts.usage() val progress = new Console_Progress() val rc = progress.interrupt_handler { build_doc(options, progress, all_docs, max_jobs, docs) } sys.exit(rc) }) } diff --git a/src/Pure/Admin/ci_profile.scala b/src/Pure/Admin/ci_profile.scala --- a/src/Pure/Admin/ci_profile.scala +++ b/src/Pure/Admin/ci_profile.scala @@ -1,163 +1,163 @@ /* Title: Pure/Admin/ci_profile.scala Author: Lars Hupel Build profile for continuous integration services. */ package isabelle import java.time.{Instant, ZoneId} import java.time.format.DateTimeFormatter import java.util.{Properties => JProperties, Map => JMap} abstract class CI_Profile extends Isabelle_Tool.Body { private def build(options: Options): (Build.Results, Time) = { val progress = new Console_Progress(verbose = true) val start_time = Time.now() val results = progress.interrupt_handler { Build.build( - options = options + "system_heaps", + options + "system_heaps", + selection, progress = progress, clean_build = clean, verbose = true, numa_shuffling = numa, max_jobs = jobs, dirs = include, - select_dirs = select, - selection = selection) + select_dirs = select) } val end_time = Time.now() (results, end_time - start_time) } private def load_properties(): JProperties = { val props = new JProperties() val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES") if (file_name != "") { val file = Path.explode(file_name).file if (file.exists()) props.load(new java.io.FileReader(file)) props } else props } private def compute_timing(results: Build.Results, group: Option[String]): Timing = { val timings = results.sessions.collect { case session if group.forall(results.info(session).groups.contains(_)) => results(session).timing } (Timing.zero /: timings)(_ + _) } private def with_documents(options: Options): Options = { if (documents) options .bool.update("browser_info", true) .string.update("document", "pdf") .string.update("document_variants", "document:outline=/proof,/ML") else options } final def hg_id(path: Path): String = Mercurial.repository(path).id() final def print_section(title: String): Unit = println(s"\n=== $title ===\n") final val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME")) final val isabelle_id = hg_id(isabelle_home) final val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME) override final def apply(args: List[String]): Unit = { print_section("CONFIGURATION") println(Build_Log.Settings.show()) val props = load_properties() System.getProperties().asInstanceOf[JMap[AnyRef, AnyRef]].putAll(props) val options = with_documents(Options.init()) .int.update("parallel_proofs", 1) .int.update("threads", threads) println(s"jobs = $jobs, threads = $threads, numa = $numa") print_section("BUILD") println(s"Build started at $start_time") println(s"Isabelle id $isabelle_id") pre_hook(args) print_section("LOG") val (results, elapsed_time) = build(options) print_section("TIMING") val groups = results.sessions.map(results.info).flatMap(_.groups) for (group <- groups) println(s"Group $group: " + compute_timing(results, Some(group)).message_resources) val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time) println("Overall: " + total_timing.message_resources) if (!results.ok) { print_section("FAILED SESSIONS") for (name <- results.sessions) { if (results.cancelled(name)) { println(s"Session $name: CANCELLED") } else { val result = results(name) if (!result.ok) println(s"Session $name: FAILED ${result.rc}") } } } post_hook(results) System.exit(results.rc) } /* profile */ def threads: Int = Isabelle_System.hostname() match { case "hpcisabelle" => 8 case "lxcisa1" => 4 case _ => 2 } def jobs: Int = Isabelle_System.hostname() match { case "hpcisabelle" => 8 case "lxcisa1" => 10 case _ => 2 } def numa: Boolean = Isabelle_System.hostname() == "hpcisabelle" def documents: Boolean = true def clean: Boolean = true def include: List[Path] def select: List[Path] def pre_hook(args: List[String]): Unit def post_hook(results: Build.Results): Unit def selection: Sessions.Selection } diff --git a/src/Pure/Tools/build.scala b/src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala +++ b/src/Pure/Tools/build.scala @@ -1,965 +1,955 @@ /* Title: Pure/Tools/build.scala Author: Makarius Options: :folding=explicit: Build and manage Isabelle sessions. */ package isabelle import scala.collection.{SortedSet, mutable} import scala.annotation.tailrec object Build { /** auxiliary **/ /* persistent build info */ sealed case class Session_Info( sources: String, input_heaps: List[String], output_heap: Option[String], return_code: Int) { def ok: Boolean = return_code == 0 } /* queue with scheduling information */ private object Queue { type Timings = (List[Properties.T], Double) def load_timings(progress: Progress, store: Sessions.Store, session_name: String): Timings = { val no_timings: Timings = (Nil, 0.0) store.access_database(session_name) match { case None => no_timings case Some(db) => def ignore_error(msg: String) = { progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg)) no_timings } try { val command_timings = store.read_command_timings(db, session_name) val session_timing = store.read_session_timing(db, session_name) match { case Markup.Elapsed(t) => t case _ => 0.0 } (command_timings, session_timing) } catch { case ERROR(msg) => ignore_error(msg) case exn: java.lang.Error => ignore_error(Exn.message(exn)) case _: XML.Error => ignore_error("") } finally { db.close } } } def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double]) : Map[String, Double] = { val maximals = sessions_structure.build_graph.maximals.toSet def desc_timing(session_name: String): Double = { if (maximals.contains(session_name)) timing(session_name) else { val descendants = sessions_structure.build_descendants(List(session_name)).toSet val g = sessions_structure.build_graph.restrict(descendants) (0.0 :: g.maximals.flatMap(desc => { val ps = g.all_preds(List(desc)) if (ps.exists(p => !timing.isDefinedAt(p))) None else Some(ps.map(timing(_)).sum) })).max } } timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0) } def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store) : Queue = { val graph = sessions_structure.build_graph val names = graph.keys val timings = names.map(name => (name, load_timings(progress, store, name))) val command_timings = timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil) val session_timing = make_session_timing(sessions_structure, timings.map({ case (name, (_, t)) => (name, t) }).toMap) object Ordering extends scala.math.Ordering[String] { def compare_timing(name1: String, name2: String): Int = { val t1 = session_timing(name1) val t2 = session_timing(name2) if (t1 == 0.0 || t2 == 0.0) 0 else t1 compare t2 } def compare(name1: String, name2: String): Int = compare_timing(name2, name1) match { case 0 => sessions_structure(name2).timeout compare sessions_structure(name1).timeout match { case 0 => name1 compare name2 case ord => ord } case ord => ord } } new Queue(graph, SortedSet(names: _*)(Ordering), command_timings) } } private class Queue( graph: Graph[String, Sessions.Info], order: SortedSet[String], val command_timings: String => List[Properties.T]) { def is_inner(name: String): Boolean = !graph.is_maximal(name) def is_empty: Boolean = graph.is_empty def - (name: String): Queue = new Queue(graph.del_node(name), order - name, // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!? command_timings) def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] = { val it = order.iterator.dropWhile(name => skip(name) || !graph.defined(name) // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!? || !graph.is_minimal(name)) if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) } else None } } /* PIDE protocol handler */ /* job: running prover process */ private class Job(progress: Progress, session_name: String, val info: Sessions.Info, deps: Sessions.Deps, store: Sessions.Store, do_store: Boolean, verbose: Boolean, val numa_node: Option[Int], command_timings: List[Properties.T]) { val options: Options = NUMA.policy_options(info.options, numa_node) private val sessions_structure = deps.sessions_structure private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf") graphview.Graph_File.write(options, graph_file, deps(session_name).session_graph_display) private val export_tmp_dir = Isabelle_System.tmp_dir("export") private val export_consumer = Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache) private val future_result: Future[Process_Result] = Future.thread("build", uninterruptible = true) { val parent = info.parent.getOrElse("") val base = deps(parent) val args_yxml = YXML.string_of_body( { import XML.Encode._ pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string, pair(string, pair(Path.encode, pair(list(pair(Options.encode, list(pair(string, properties)))), pair(list(pair(string, properties)), pair(list(pair(string, string)), pair(list(string), pair(list(pair(string, string)), pair(list(string), list(string)))))))))))))))))( (Symbol.codes, (command_timings, (verbose, (store.browser_info, (info.document_files, (File.standard_path(graph_file), (parent, (info.chapter, (session_name, (Path.current, (info.theories, (sessions_structure.session_positions, (sessions_structure.dest_session_directories, (base.doc_names, (base.global_theories.toList, (base.loaded_theories.keys, info.bibtex_entries.map(_.info)))))))))))))))))) }) val env = Isabelle_System.settings() + ("ISABELLE_EXPORT_TMP" -> File.standard_path(export_tmp_dir)) + ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString) val is_pure = Sessions.is_pure(session_name) val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil val eval_store = if (do_store) { (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) ::: List("ML_Heap.save_child " + ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name)))) } else Nil if (options.bool("pide_session")) { val resources = new Resources(sessions_structure, deps(parent)) val session = new Session(options, resources) val build_session_errors: Promise[List[String]] = Future.promise val stdout = new StringBuilder(1000) val messages = new mutable.ListBuffer[String] val command_timings = new mutable.ListBuffer[Properties.T] val theory_timings = new mutable.ListBuffer[Properties.T] val runtime_statistics = new mutable.ListBuffer[Properties.T] val task_statistics = new mutable.ListBuffer[Properties.T] session.init_protocol_handler(new Session.Protocol_Handler { override def exit() { build_session_errors.cancel } private def build_session_finished(msg: Prover.Protocol_Output): Boolean = { val (rc, errors) = try { val (rc, errs) = { import XML.Decode._ pair(int, list(x => x))(Symbol.decode_yxml(msg.text)) } val errors = for (err <- errs) yield { val prt = Protocol_Message.expose_no_reports(err) Pretty.string_of(prt, metric = Symbol.Metric) } (rc, errors) } catch { case ERROR(err) => (2, List(err)) } session.protocol_command("Prover.stop", rc.toString) build_session_errors.fulfill(errors) true } private def loading_theory(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.Loading_Theory(name) => progress.theory(Progress.Theory(name, session = session_name)) true case _ => false } private def export(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Protocol.Export(args) => export_consumer(session_name, args, msg.bytes) true case _ => false } private def command_timing(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.Command_Timing(props) => command_timings += props; true case _ => false } private def theory_timing(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.Theory_Timing(props) => theory_timings += props; true case _ => false } private def ml_stats(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.ML_Statistics(props) => runtime_statistics += props; true case _ => false } private def task_stats(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.Task_Statistics(props) => task_statistics += props; true case _ => false } val functions = List( Markup.Build_Session_Finished.name -> build_session_finished, Markup.Loading_Theory.name -> loading_theory, Markup.EXPORT -> export, Markup.Command_Timing.name -> command_timing, Markup.Theory_Timing.name -> theory_timing, Markup.ML_Statistics.name -> ml_stats, Markup.Task_Statistics.name -> task_stats) }) session.all_messages += Session.Consumer[Any]("build_session_output") { case msg: Prover.Output => val message = msg.message if (msg.is_stdout) { stdout ++= Symbol.encode(XML.content(message)) } else if (Protocol.is_exported(message)) { messages += Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric)) } case _ => } val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) val process = Isabelle_Process(session, options, sessions_structure, store, logic = parent, raw_ml_system = is_pure, use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env) val errors = Isabelle_Thread.interrupt_handler(_ => process.terminate) { Exn.capture { process.await_startup } match { case Exn.Res(_) => session.protocol_command("build_session", args_yxml) build_session_errors.join_result case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn))) } } val process_result = Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown } val process_output = stdout.toString :: messages.toList ::: command_timings.toList.map(Protocol.Command_Timing_Marker.apply) ::: theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) ::: runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) ::: task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) val result = process_result.output(process_output) errors match { case Exn.Res(Nil) => result case Exn.Res(errs) => result.error_rc.output( errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: errs.map(Protocol.Error_Message_Marker.apply)) case Exn.Exn(Exn.Interrupt()) => if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result case Exn.Exn(exn) => throw exn } } else { val args_file = Isabelle_System.tmp_file("build") File.write(args_file, args_yxml) val eval_build = "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) val eval_main = Command_Line.ML_tool(eval_build :: eval_store) val process = ML_Process(options, deps.sessions_structure, store, logic = parent, raw_ml_system = is_pure, use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env, cleanup = () => args_file.delete) Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.result( progress_stdout = { case Protocol.Loading_Theory_Marker(theory) => progress.theory(Progress.Theory(theory, session = session_name)) case Protocol.Export.Marker((args, path)) => val body = try { Bytes.read(path) } catch { case ERROR(msg) => error("Failed to read export " + quote(args.compound_name) + "\n" + msg) } path.file.delete export_consumer(session_name, args, body) case _ => }, progress_limit = options.int("process_output_limit") match { case 0 => None case m => Some(m * 1000000L) }, strict = false) } } } def terminate: Unit = future_result.cancel def is_finished: Boolean = future_result.is_finished private val timeout_request: Option[Event_Timer.Request] = { if (info.timeout > Time.zero) Some(Event_Timer.request(Time.now() + info.timeout) { terminate }) else None } def join: (Process_Result, Option[String]) = { val result0 = future_result.join val result1 = export_consumer.shutdown(close = true).map(Output.error_message_text) match { case Nil => result0 case errs => result0.errors(errs).error_rc } Isabelle_System.rm_tree(export_tmp_dir) if (result1.ok) Present.finish(progress, store.browser_info, graph_file, info, session_name) graph_file.delete val was_timeout = timeout_request match { case None => false case Some(request) => !request.cancel } val result2 = if (result1.interrupted) { if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout else result1.error(Output.error_message_text("Interrupt")) } else result1 val heap_digest = if (result2.ok && do_store && store.output_heap(session_name).is_file) Some(Sessions.write_heap_digest(store.output_heap(session_name))) else None (result2, heap_digest) } } /** build with results **/ class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)]) { def sessions: Set[String] = results.keySet def cancelled(name: String): Boolean = results(name)._1.isEmpty def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1)) def info(name: String): Sessions.Info = results(name)._2 val rc: Int = (0 /: results.iterator.map( { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _) def ok: Boolean = rc == 0 override def toString: String = rc.toString } def build( options: Options, + selection: Sessions.Selection, progress: Progress = new Progress, check_unknown_files: Boolean = false, build_heap: Boolean = false, clean_build: Boolean = false, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, infos: List[Sessions.Info] = Nil, numa_shuffling: Boolean = false, max_jobs: Int = 1, list_files: Boolean = false, check_keywords: Set[String] = Set.empty, fresh_build: Boolean = false, no_build: Boolean = false, soft_build: Boolean = false, verbose: Boolean = false, - export_files: Boolean = false, - requirements: Boolean = false, - all_sessions: Boolean = false, - base_sessions: List[String] = Nil, - exclude_session_groups: List[String] = Nil, - exclude_sessions: List[String] = Nil, - session_groups: List[String] = Nil, - sessions: List[String] = Nil, - selection: Sessions.Selection = Sessions.Selection.empty): Results = + export_files: Boolean = false): Results = { val build_options = options + "ML_statistics" + "completion_limit=0" + "editor_tracing_messages=0" + "pide_reports=false" val store = Sessions.store(build_options) Isabelle_Fonts.init() /* session selection and dependencies */ val full_sessions = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos) def sources_stamp(deps: Sessions.Deps, session_name: String): String = { val digests = full_sessions(session_name).meta_digest :: deps.sources(session_name) ::: deps.imported_sources(session_name) SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString } - val selection1 = - Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups, - exclude_sessions, session_groups, sessions) ++ selection - val deps = { val deps0 = - Sessions.deps(full_sessions.selection(selection1), + Sessions.deps(full_sessions.selection(selection), progress = progress, inlined_files = true, verbose = verbose, list_files = list_files, check_keywords = check_keywords).check_errors if (soft_build && !fresh_build) { val outdated = deps0.sessions_structure.build_topological_order.flatMap(name => store.access_database(name) match { case Some(db) => using(db)(store.read_build(_, name)) match { case Some(build) if build.ok && build.sources == sources_stamp(deps0, name) => None case _ => Some(name) } case None => Some(name) }) Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)), progress = progress, inlined_files = true).check_errors } else deps0 } /* check unknown files */ if (check_unknown_files) { val source_files = (for { (_, base) <- deps.session_bases.iterator (path, _) <- base.sources.iterator } yield path).toList val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file) val unknown_files = Mercurial.check_files(source_files)._2. filterNot(path => exclude_files.contains(path.canonical_file)) if (unknown_files.nonEmpty) { progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" + unknown_files.map(path => path.expand.implode).sorted.mkString("\n ", "\n ", "")) } } /* main build process */ val queue = Queue(progress, deps.sessions_structure, store) store.prepare_output_dir() if (clean_build) { - for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection1))) { + for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection))) { val (relevant, ok) = store.clean_output(name) if (relevant) { if (ok) progress.echo("Cleaned " + name) else progress.echo(name + " FAILED to clean") } } } // scheduler loop case class Result( current: Boolean, heap_digest: Option[String], process: Option[Process_Result], info: Sessions.Info) { def ok: Boolean = process match { case None => false case Some(res) => res.rc == 0 } } def sleep() { Isabelle_Thread.interrupt_handler(_ => progress.stop) { Time.seconds(0.5).sleep } } val numa_nodes = new NUMA.Nodes(numa_shuffling) @tailrec def loop( pending: Queue, running: Map[String, (List[String], Job)], results: Map[String, Result]): Map[String, Result] = { def used_node(i: Int): Boolean = running.iterator.exists( { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i }) if (pending.is_empty) results else { if (progress.stopped) { for ((_, (_, job)) <- running) job.terminate } running.find({ case (_, (_, job)) => job.is_finished }) match { case Some((session_name, (input_heaps, job))) => //{{{ finish job val (process_result, heap_digest) = job.join val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test) val process_result_tail = { val tail = job.info.options.int("process_output_tail") process_result.copy( out_lines = "(see also " + store.output_log(session_name).file.toString + ")" :: (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0))) } // write log file if (process_result.ok) { File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines)) } else File.write(store.output_log(session_name), terminate_lines(log_lines)) // write database { val build_log = Build_Log.Log_File(session_name, process_result.out_lines). parse_session_info( command_timings = true, theory_timings = true, ml_statistics = true, task_statistics = true) using(store.open_database(session_name, output = true))(db => store.write_session_info(db, session_name, build_log = if (process_result.timeout) build_log.error("Timeout") else build_log, build = Session_Info(sources_stamp(deps, session_name), input_heaps, heap_digest, process_result.rc))) } // messages process_result.err_lines.foreach(progress.echo) if (process_result.ok) progress.echo( "Finished " + session_name + " (" + process_result.timing.message_resources + ")") else { progress.echo(session_name + " FAILED") if (!process_result.interrupted) progress.echo(process_result_tail.out) } loop(pending - session_name, running - session_name, results + (session_name -> Result(false, heap_digest, Some(process_result_tail), job.info))) //}}} case None if running.size < (max_jobs max 1) => //{{{ check/start next job pending.dequeue(running.isDefinedAt) match { case Some((session_name, info)) => val ancestor_results = deps.sessions_structure.build_requirements(List(session_name)). filterNot(_ == session_name).map(results(_)) val ancestor_heaps = ancestor_results.flatMap(_.heap_digest) val do_store = build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name) val (current, heap_digest) = { store.access_database(session_name) match { case Some(db) => using(db)(store.read_build(_, session_name)) match { case Some(build) => val heap_digest = store.find_heap_digest(session_name) val current = !fresh_build && build.ok && build.sources == sources_stamp(deps, session_name) && build.input_heaps == ancestor_heaps && build.output_heap == heap_digest && !(do_store && heap_digest.isEmpty) (current, heap_digest) case None => (false, None) } case None => (false, None) } } val all_current = current && ancestor_results.forall(_.current) if (all_current) loop(pending - session_name, running, results + (session_name -> Result(true, heap_digest, Some(Process_Result(0)), info))) else if (no_build) { progress.echo_if(verbose, "Skipping " + session_name + " ...") loop(pending - session_name, running, results + (session_name -> Result(false, heap_digest, Some(Process_Result(1)), info))) } else if (ancestor_results.forall(_.ok) && !progress.stopped) { progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...") store.clean_output(session_name) using(store.open_database(session_name, output = true))( store.init_session_info(_, session_name)) val numa_node = numa_nodes.next(used_node) val job = new Job(progress, session_name, info, deps, store, do_store, verbose, numa_node, queue.command_timings(session_name)) loop(pending, running + (session_name -> (ancestor_heaps, job)), results) } else { progress.echo(session_name + " CANCELLED") loop(pending - session_name, running, results + (session_name -> Result(false, heap_digest, None, info))) } case None => sleep(); loop(pending, running, results) } ///}}} case None => sleep(); loop(pending, running, results) } } } /* build results */ val results0 = if (deps.is_empty) { progress.echo_warning("Nothing to build") Map.empty[String, Result] } else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) } val results = new Results( (for ((name, result) <- results0.iterator) yield (name, (result.process, result.info))).toMap) if (export_files) { - for (name <- full_sessions.imports_selection(selection1).iterator if results(name).ok) { + for (name <- full_sessions.imports_selection(selection).iterator if results(name).ok) { val info = results.info(name) if (info.export_files.nonEmpty) { progress.echo("Exporting " + info.name + " ...") for ((dir, prune, pats) <- info.export_files) { Export.export_files(store, name, info.dir + dir, progress = if (verbose) progress else new Progress, export_prune = prune, export_patterns = pats) } } } } if (results.rc != 0 && (verbose || !no_build)) { val unfinished = (for { name <- results.sessions.iterator if !results(name).ok } yield name).toList.sorted progress.echo("Unfinished session(s): " + commas(unfinished)) } /* global browser info */ if (!no_build) { val browser_chapters = (for { (name, result) <- results0.iterator if result.ok info = full_sessions(name) if info.options.bool("browser_info") } yield (info.chapter, (name, info.description))).toList.groupBy(_._1). map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty) for ((chapter, entries) <- browser_chapters) Present.update_chapter_index(store.browser_info, chapter, entries) if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info) } results } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args => { val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")) var base_sessions: List[String] = Nil var select_dirs: List[Path] = Nil var numa_shuffling = false var requirements = false var soft_build = false var exclude_session_groups: List[String] = Nil var all_sessions = false var build_heap = false var clean_build = false var dirs: List[Path] = Nil var export_files = false var fresh_build = false var session_groups: List[String] = Nil var max_jobs = 1 var check_keywords: Set[String] = Set.empty var list_files = false var no_build = false var options = Options.init(opts = build_options) var verbose = false var exclude_sessions: List[String] = Nil val getopts = Getopts(""" Usage: isabelle build [OPTIONS] [SESSIONS ...] Options are: -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -N cyclic shuffling of NUMA CPU nodes (performance tuning) -R refer to requirements of selected sessions -S soft build: only observe changes of sources, not heap images -X NAME exclude sessions from group NAME and all descendants -a select all sessions -b build heap images -c clean build -d DIR include session directory -e export files from session specification into file-system -f fresh build -g NAME select session group NAME -j INT maximum number of parallel jobs (default 1) -k KEYWORD check theory sources for conflicts with proposed keywords -l list session source files -n no build -- test dependencies only -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose -x NAME exclude session NAME and all descendants Build and manage Isabelle sessions, depending on implicit settings: """ + Library.prefix_lines(" ", Build_Log.Settings.show()) + "\n", "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "N" -> (_ => numa_shuffling = true), "R" -> (_ => requirements = true), "S" -> (_ => soft_build = true), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), "a" -> (_ => all_sessions = true), "b" -> (_ => build_heap = true), "c" -> (_ => clean_build = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "e" -> (_ => export_files = true), "f" -> (_ => fresh_build = true), "g:" -> (arg => session_groups = session_groups ::: List(arg)), "j:" -> (arg => max_jobs = Value.Int.parse(arg)), "k:" -> (arg => check_keywords = check_keywords + arg), "l" -> (_ => list_files = true), "n" -> (_ => no_build = true), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose = true), "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) val sessions = getopts(args) val progress = new Console_Progress(verbose = verbose) val start_date = Date.now() if (verbose) { progress.echo( "Started at " + Build_Log.print_date(start_date) + " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")") progress.echo(Build_Log.Settings.show() + "\n") } val results = progress.interrupt_handler { build(options, + Sessions.Selection( + requirements = requirements, + all_sessions = all_sessions, + base_sessions = base_sessions, + exclude_session_groups = exclude_session_groups, + exclude_sessions = exclude_sessions, + session_groups = session_groups, + sessions = sessions), progress = progress, check_unknown_files = Mercurial.is_repository(Path.explode("~~")), build_heap = build_heap, clean_build = clean_build, dirs = dirs, select_dirs = select_dirs, numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling), max_jobs = max_jobs, list_files = list_files, check_keywords = check_keywords, fresh_build = fresh_build, no_build = no_build, soft_build = soft_build, verbose = verbose, - export_files = export_files, - requirements = requirements, - all_sessions = all_sessions, - base_sessions = base_sessions, - exclude_session_groups = exclude_session_groups, - exclude_sessions = exclude_sessions, - session_groups = session_groups, - sessions = sessions) + export_files = export_files) } val end_date = Date.now() val elapsed_time = end_date.time - start_date.time if (verbose) { progress.echo("\nFinished at " + Build_Log.print_date(end_date)) } val total_timing = (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _). copy(elapsed = elapsed_time) progress.echo(total_timing.message_resources) sys.exit(results.rc) }) /* build logic image */ def build_logic(options: Options, logic: String, progress: Progress = new Progress, build_heap: Boolean = false, dirs: List[Path] = Nil, fresh: Boolean = false, strict: Boolean = false): Int = { + val selection = Sessions.Selection.session(logic) val rc = - if (!fresh && build(options, build_heap = build_heap, no_build = true, dirs = dirs, - sessions = List(logic)).ok) 0 + if (!fresh && + build(options, selection, build_heap = build_heap, no_build = true, dirs = dirs).ok) 0 else { progress.echo("Build started for Isabelle/" + logic + " ...") - Build.build(options, progress = progress, build_heap = build_heap, fresh_build = fresh, - dirs = dirs, sessions = List(logic)).rc + Build.build(options, selection, progress = progress, build_heap = build_heap, + fresh_build = fresh, dirs = dirs).rc } - if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc } } diff --git a/src/Pure/Tools/server_commands.scala b/src/Pure/Tools/server_commands.scala --- a/src/Pure/Tools/server_commands.scala +++ b/src/Pure/Tools/server_commands.scala @@ -1,276 +1,275 @@ /* Title: Pure/Tools/server_commands.scala Author: Makarius Miscellaneous Isabelle server commands. */ package isabelle object Server_Commands { def default_preferences: String = Options.read_prefs() object Cancel { sealed case class Args(task: UUID.T) def unapply(json: JSON.T): Option[Args] = for { task <- JSON.uuid(json, "task") } yield Args(task) } object Session_Build { sealed case class Args( session: String, preferences: String = default_preferences, options: List[String] = Nil, dirs: List[String] = Nil, include_sessions: List[String] = Nil, verbose: Boolean = false) def unapply(json: JSON.T): Option[Args] = for { session <- JSON.string(json, "session") preferences <- JSON.string_default(json, "preferences", default_preferences) options <- JSON.strings_default(json, "options") dirs <- JSON.strings_default(json, "dirs") include_sessions <- JSON.strings_default(json, "include_sessions") verbose <- JSON.bool_default(json, "verbose") } yield { Args(session, preferences = preferences, options = options, dirs = dirs, include_sessions = include_sessions, verbose = verbose) } def command(args: Args, progress: Progress = new Progress) : (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) = { val options = Options.init(prefs = args.preferences, opts = args.options) val dirs = args.dirs.map(Path.explode) val base_info = Sessions.base_info(options, args.session, progress = progress, dirs = dirs, include_sessions = args.include_sessions) val base = base_info.check_base val results = - Build.build(options, + Build.build(options, Sessions.Selection.session(args.session), progress = progress, build_heap = true, dirs = dirs, infos = base_info.infos, - verbose = args.verbose, - sessions = List(args.session)) + verbose = args.verbose) val sessions_order = base_info.sessions_structure.imports_topological_order.zipWithIndex. toMap.withDefaultValue(-1) val results_json = JSON.Object( "ok" -> results.ok, "return_code" -> results.rc, "sessions" -> results.sessions.toList.sortBy(sessions_order).map(session => { val result = results(session) JSON.Object( "session" -> session, "ok" -> result.ok, "return_code" -> result.rc, "timeout" -> result.timeout, "timing" -> result.timing.json) })) if (results.ok) (results_json, results, options, base_info) else { throw new Server.Error("Session build failed: " + Process_Result.print_rc(results.rc), results_json) } } } object Session_Start { sealed case class Args( build: Session_Build.Args, print_mode: List[String] = Nil) def unapply(json: JSON.T): Option[Args] = for { build <- Session_Build.unapply(json) print_mode <- JSON.strings_default(json, "print_mode") } yield Args(build = build, print_mode = print_mode) def command(args: Args, progress: Progress = new Progress, log: Logger = No_Logger) : (JSON.Object.T, (UUID.T, Headless.Session)) = { val (_, _, options, base_info) = try { Session_Build.command(args.build, progress = progress) } catch { case exn: Server.Error => error(exn.message) } val resources = Headless.Resources(options, base_info, log = log) val session = resources.start_session(print_mode = args.print_mode, progress = progress) val id = UUID.random() val res = JSON.Object( "session_id" -> id.toString, "tmp_dir" -> File.path(session.tmp_dir).implode) (res, id -> session) } } object Session_Stop { def unapply(json: JSON.T): Option[UUID.T] = JSON.uuid(json, "session_id") def command(session: Headless.Session): (JSON.Object.T, Process_Result) = { val result = session.stop() val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc) if (result.ok) (result_json, result) else throw new Server.Error("Session shutdown failed: " + result.print_rc, result_json) } } object Use_Theories { sealed case class Args( session_id: UUID.T, theories: List[String], master_dir: String = "", pretty_margin: Double = Pretty.default_margin, unicode_symbols: Boolean = false, export_pattern: String = "", check_delay: Option[Time] = None, check_limit: Option[Int] = None, watchdog_timeout: Option[Time] = None, nodes_status_delay: Option[Time] = None, commit_cleanup_delay: Option[Time] = None) def unapply(json: JSON.T): Option[Args] = for { session_id <- JSON.uuid(json, "session_id") theories <- JSON.strings(json, "theories") master_dir <- JSON.string_default(json, "master_dir") pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin) unicode_symbols <- JSON.bool_default(json, "unicode_symbols") export_pattern <- JSON.string_default(json, "export_pattern") check_delay = JSON.seconds(json, "check_delay") check_limit = JSON.int(json, "check_limit") watchdog_timeout = JSON.seconds(json, "watchdog_timeout") nodes_status_delay = JSON.seconds(json, "nodes_status_delay") commit_cleanup_delay = JSON.seconds(json, "commit_cleanup_delay") } yield { Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin, unicode_symbols = unicode_symbols, export_pattern = export_pattern, check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout, nodes_status_delay = nodes_status_delay, commit_cleanup_delay = commit_cleanup_delay) } def command(args: Args, session: Headless.Session, id: UUID.T = UUID.random(), progress: Progress = new Progress): (JSON.Object.T, Headless.Use_Theories_Result) = { val result = session.use_theories(args.theories, master_dir = args.master_dir, check_delay = args.check_delay.getOrElse(session.default_check_delay), check_limit = args.check_limit.getOrElse(session.default_check_limit), watchdog_timeout = args.watchdog_timeout.getOrElse(session.default_watchdog_timeout), nodes_status_delay = args.nodes_status_delay.getOrElse(session.default_nodes_status_delay), commit_cleanup_delay = args.commit_cleanup_delay.getOrElse(session.default_commit_cleanup_delay), id = id, progress = progress) def output_text(s: String): String = if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s) def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T = { val position = "pos" -> Position.JSON(pos) tree match { case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position case elem: XML.Elem => val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin)) val kind = Markup.messages.collectFirst({ case (a, b) if b == elem.name => if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse "" Server.Reply.message(output_text(msg), kind = kind) + position } } val result_json = JSON.Object( "ok" -> result.ok, "errors" -> (for { (name, status) <- result.nodes if !status.ok (tree, pos) <- result.snapshot(name).messages if Protocol.is_error(tree) } yield output_message(tree, pos)), "nodes" -> (for ((name, status) <- result.nodes) yield { val snapshot = result.snapshot(name) name.json + ("status" -> status.json) + ("messages" -> (for { (tree, pos) <- snapshot.messages if Protocol.is_exported(tree) } yield output_message(tree, pos))) + ("exports" -> (if (args.export_pattern == "") Nil else { val matcher = Export.make_matcher(args.export_pattern) for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) } yield { val (base64, body) = entry.uncompressed().maybe_base64 JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body) } })) })) (result_json, result) } } object Purge_Theories { sealed case class Args( session_id: UUID.T, theories: List[String] = Nil, master_dir: String = "", all: Boolean = false) def unapply(json: JSON.T): Option[Args] = for { session_id <- JSON.uuid(json, "session_id") theories <- JSON.strings_default(json, "theories") master_dir <- JSON.string_default(json, "master_dir") all <- JSON.bool_default(json, "all") } yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) } def command(args: Args, session: Headless.Session) : (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) = { val (purged, retained) = session.purge_theories( theories = args.theories, master_dir = args.master_dir, all = args.all) val result_json = JSON.Object("purged" -> purged.map(_.json), "retained" -> retained.map(_.json)) (result_json, (purged, retained)) } } } diff --git a/src/Tools/VSCode/src/server.scala b/src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala +++ b/src/Tools/VSCode/src/server.scala @@ -1,561 +1,561 @@ /* Title: Tools/VSCode/src/server.scala Author: Makarius Server for VS Code Language Server Protocol 2.0/3.0, see also https://github.com/Microsoft/language-server-protocol https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md PIDE protocol extensions depend on system option "vscode_pide_extensions". */ package isabelle.vscode import isabelle._ import java.io.{PrintStream, OutputStream, File => JFile} import scala.annotation.tailrec import scala.collection.mutable object Server { type Editor = isabelle.Editor[Unit] /* Isabelle tool wrapper */ private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args => { try { var logic_ancestor: Option[String] = None var log_file: Option[Path] = None var logic_requirements = false var dirs: List[Path] = Nil var include_sessions: List[String] = Nil var logic = default_logic var modes: List[String] = Nil var options = Options.init() var verbose = false val getopts = Getopts(""" Usage: isabelle vscode_server [OPTIONS] Options are: -A NAME ancestor session for option -R (default: parent) -L FILE logging on FILE -R NAME build image with requirements from other sessions -d DIR include session directory -i NAME include session in name-space of theories -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """) -m MODE add print mode for output -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose logging Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout. """, "A:" -> (arg => logic_ancestor = Some(arg)), "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))), "R:" -> (arg => { logic = arg; logic_requirements = true }), "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))), "i:" -> (arg => include_sessions = include_sessions ::: List(arg)), "l:" -> (arg => logic = arg), "m:" -> (arg => modes = arg :: modes), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val log = Logger.make(log_file) val channel = new Channel(System.in, System.out, log, verbose) val server = new Server(channel, options, session_name = logic, session_dirs = dirs, include_sessions = include_sessions, session_ancestor = logic_ancestor, session_requirements = logic_requirements, modes = modes, log = log) // prevent spurious garbage on the main protocol channel val orig_out = System.out try { System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} })) server.start() } finally { System.setOut(orig_out) } } catch { case exn: Throwable => val channel = new Channel(System.in, System.out, No_Logger) channel.error_message(Exn.message(exn)) throw(exn) } }) } class Server( val channel: Channel, options: Options, session_name: String = Server.default_logic, session_dirs: List[Path] = Nil, include_sessions: List[String] = Nil, session_ancestor: Option[String] = None, session_requirements: Boolean = false, modes: List[String] = Nil, log: Logger = No_Logger) { server => /* prover session */ private val session_ = Synchronized(None: Option[Session]) def session: Session = session_.value getOrElse error("Server inactive") def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] = for { model <- resources.get_model(new JFile(node_pos.name)) rendering = model.rendering() offset <- model.content.doc.offset(node_pos.pos) } yield (rendering, offset) private val dynamic_output = Dynamic_Output(server) /* input from client or file-system */ private val delay_input: Delay = Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger) { resources.flush_input(session, channel) } private val delay_load: Delay = Delay.last(options.seconds("vscode_load_delay"), channel.Error_Logger) { val (invoke_input, invoke_load) = resources.resolve_dependencies(session, editor, file_watcher) if (invoke_input) delay_input.invoke() if (invoke_load) delay_load.invoke } private val file_watcher = File_Watcher(sync_documents, options.seconds("vscode_load_delay")) private def close_document(file: JFile) { if (resources.close_model(file)) { file_watcher.register_parent(file) sync_documents(Set(file)) delay_input.invoke() delay_output.invoke() } } private def sync_documents(changed: Set[JFile]) { resources.sync_models(changed) delay_input.invoke() delay_output.invoke() } private def change_document(file: JFile, version: Long, changes: List[Protocol.TextDocumentChange]) { val norm_changes = new mutable.ListBuffer[Protocol.TextDocumentChange] @tailrec def norm(chs: List[Protocol.TextDocumentChange]) { if (chs.nonEmpty) { val (full_texts, rest1) = chs.span(_.range.isEmpty) val (edits, rest2) = rest1.span(_.range.nonEmpty) norm_changes ++= full_texts norm_changes ++= edits.sortBy(_.range.get.start)(Line.Position.Ordering).reverse norm(rest2) } } norm(changes) norm_changes.foreach(change => resources.change_model(session, editor, file, version, change.text, change.range)) delay_input.invoke() delay_output.invoke() } /* caret handling */ private val delay_caret_update: Delay = Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger) { session.caret_focus.post(Session.Caret_Focus) } private def update_caret(caret: Option[(JFile, Line.Position)]) { resources.update_caret(caret) delay_caret_update.invoke() delay_input.invoke() } /* preview */ private lazy val preview_panel = new Preview_Panel(resources) private lazy val delay_preview: Delay = Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger) { if (preview_panel.flush(channel)) delay_preview.invoke() } private def request_preview(file: JFile, column: Int) { preview_panel.request(file, column) delay_preview.invoke() } /* output to client */ private val delay_output: Delay = Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger) { if (resources.flush_output(channel)) delay_output.invoke() } def update_output(changed_nodes: Traversable[JFile]) { resources.update_output(changed_nodes) delay_output.invoke() } def update_output_visible() { resources.update_output_visible() delay_output.invoke() } private val prover_output = Session.Consumer[Session.Commands_Changed](getClass.getName) { case changed => update_output(changed.nodes.toList.map(resources.node_file(_))) } private val syslog_messages = Session.Consumer[Prover.Output](getClass.getName) { case output => channel.log_writeln(resources.output_xml(output.message)) } /* init and exit */ def init(id: Protocol.Id) { def reply_ok(msg: String) { channel.write(Protocol.Initialize.reply(id, "")) channel.writeln(msg) } def reply_error(msg: String) { channel.write(Protocol.Initialize.reply(id, msg)) channel.error_message(msg) } val try_session = try { val base_info = Sessions.base_info( options, session_name, dirs = session_dirs, include_sessions = include_sessions, session_ancestor = session_ancestor, session_requirements = session_requirements) base_info.check_base def build(no_build: Boolean = false): Build.Results = - Build.build(options, build_heap = true, no_build = no_build, dirs = session_dirs, - infos = base_info.infos, sessions = List(base_info.session)) + Build.build(options, Sessions.Selection.session(base_info.session), + build_heap = true, no_build = no_build, dirs = session_dirs, infos = base_info.infos) if (!build(no_build = true).ok) { val start_msg = "Build started for Isabelle/" + base_info.session + " ..." val fail_msg = "Session build failed -- prover process remains inactive!" val progress = channel.progress(verbose = true) progress.echo(start_msg); channel.writeln(start_msg) if (!build().ok) { progress.echo(fail_msg); error(fail_msg) } } val resources = new VSCode_Resources(options, base_info, log) { override def commit(change: Session.Change): Unit = if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty) delay_load.invoke() } val session_options = options.bool("editor_output_state") = true val session = new Session(session_options, resources) Some((base_info, session)) } catch { case ERROR(msg) => reply_error(msg); None } for ((base_info, session) <- try_session) { session_.change(_ => Some(session)) session.commands_changed += prover_output session.syslog_messages += syslog_messages dynamic_output.init() try { Isabelle_Process(session, options, base_info.sessions_structure, Sessions.store(options), modes = modes, logic = base_info.session).await_startup reply_ok("Welcome to Isabelle/" + base_info.session + " (" + Distribution.version + ")") } catch { case ERROR(msg) => reply_error(msg) } } } def shutdown(id: Protocol.Id) { def reply(err: String): Unit = channel.write(Protocol.Shutdown.reply(id, err)) session_.change({ case Some(session) => session.commands_changed -= prover_output session.syslog_messages -= syslog_messages dynamic_output.exit() delay_load.revoke() file_watcher.shutdown() delay_input.revoke() delay_output.revoke() delay_caret_update.revoke() delay_preview.revoke() val result = session.stop() if (result.ok) reply("") else reply("Prover shutdown failed: " + result.rc) None case None => reply("Prover inactive") None }) } def exit() { log("\n") sys.exit(if (session_.value.isDefined) 2 else 0) } /* completion */ def completion(id: Protocol.Id, node_pos: Line.Node_Position) { val result = (for ((rendering, offset) <- rendering_offset(node_pos)) yield rendering.completion(node_pos.pos, offset)) getOrElse Nil channel.write(Protocol.Completion.reply(id, result)) } /* spell-checker dictionary */ def update_dictionary(include: Boolean, permanent: Boolean) { for { spell_checker <- resources.spell_checker.get caret <- resources.get_caret() rendering = caret.model.rendering() range = rendering.before_caret_range(caret.offset) Text.Info(_, word) <- Spell_Checker.current_word(rendering, range) } { spell_checker.update(word, include, permanent) update_output_visible() } } def reset_dictionary() { for (spell_checker <- resources.spell_checker.get) { spell_checker.reset() update_output_visible() } } /* hover */ def hover(id: Protocol.Id, node_pos: Line.Node_Position) { val result = for { (rendering, offset) <- rendering_offset(node_pos) info <- rendering.tooltips(VSCode_Rendering.tooltip_elements, Text.Range(offset, offset + 1)) } yield { val range = rendering.model.content.doc.range(info.range) val contents = info.info.map(t => Protocol.MarkedString(resources.output_pretty_tooltip(List(t)))) (range, contents) } channel.write(Protocol.Hover.reply(id, result)) } /* goto definition */ def goto_definition(id: Protocol.Id, node_pos: Line.Node_Position) { val result = (for ((rendering, offset) <- rendering_offset(node_pos)) yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil channel.write(Protocol.GotoDefinition.reply(id, result)) } /* document highlights */ def document_highlights(id: Protocol.Id, node_pos: Line.Node_Position) { val result = (for ((rendering, offset) <- rendering_offset(node_pos)) yield { val model = rendering.model rendering.caret_focus_ranges(Text.Range(offset, offset + 1), model.content.text_range) .map(r => Protocol.DocumentHighlight.text(model.content.doc.range(r))) }) getOrElse Nil channel.write(Protocol.DocumentHighlights.reply(id, result)) } /* main loop */ def start() { log("Server started " + Date.now()) def handle(json: JSON.T) { try { json match { case Protocol.Initialize(id) => init(id) case Protocol.Initialized(()) => case Protocol.Shutdown(id) => shutdown(id) case Protocol.Exit(()) => exit() case Protocol.DidOpenTextDocument(file, _, version, text) => change_document(file, version, List(Protocol.TextDocumentChange(None, text))) delay_load.invoke() case Protocol.DidChangeTextDocument(file, version, changes) => change_document(file, version, changes) case Protocol.DidCloseTextDocument(file) => close_document(file) case Protocol.Completion(id, node_pos) => completion(id, node_pos) case Protocol.Include_Word(()) => update_dictionary(true, false) case Protocol.Include_Word_Permanently(()) => update_dictionary(true, true) case Protocol.Exclude_Word(()) => update_dictionary(false, false) case Protocol.Exclude_Word_Permanently(()) => update_dictionary(false, true) case Protocol.Reset_Words(()) => reset_dictionary() case Protocol.Hover(id, node_pos) => hover(id, node_pos) case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos) case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos) case Protocol.Caret_Update(caret) => update_caret(caret) case Protocol.State_Init(()) => State_Panel.init(server) case Protocol.State_Exit(id) => State_Panel.exit(id) case Protocol.State_Locate(id) => State_Panel.locate(id) case Protocol.State_Update(id) => State_Panel.update(id) case Protocol.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled) case Protocol.Preview_Request(file, column) => request_preview(file, column) case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols()) case _ => if (!Protocol.ResponseMessage.is_empty(json)) log("### IGNORED") } } catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) } } @tailrec def loop() { channel.read() match { case Some(json) => json match { case bulk: List[_] => bulk.foreach(handle) case _ => handle(json) } loop() case None => log("### TERMINATE") } } loop() } /* abstract editor operations */ object editor extends Server.Editor { /* session */ override def session: Session = server.session override def flush(): Unit = resources.flush_input(session, channel) override def invoke(): Unit = delay_input.invoke() /* current situation */ override def current_node(context: Unit): Option[Document.Node.Name] = resources.get_caret().map(_.model.node_name) override def current_node_snapshot(context: Unit): Option[Document.Snapshot] = resources.get_caret().map(_.model.snapshot()) override def node_snapshot(name: Document.Node.Name): Document.Snapshot = { resources.get_model(name) match { case Some(model) => model.snapshot() case None => session.snapshot(name) } } def current_command(snapshot: Document.Snapshot): Option[Command] = { resources.get_caret() match { case Some(caret) => snapshot.current_command(caret.node_name, caret.offset) case None => None } } override def current_command(context: Unit, snapshot: Document.Snapshot): Option[Command] = current_command(snapshot) /* overlays */ override def node_overlays(name: Document.Node.Name): Document.Node.Overlays = resources.node_overlays(name) override def insert_overlay(command: Command, fn: String, args: List[String]): Unit = resources.insert_overlay(command, fn, args) override def remove_overlay(command: Command, fn: String, args: List[String]): Unit = resources.remove_overlay(command, fn, args) /* hyperlinks */ override def hyperlink_command( focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0): Option[Hyperlink] = { if (snapshot.is_outdated) None else snapshot.find_command_position(id, offset).map(node_pos => new Hyperlink { def follow(unit: Unit) { channel.write(Protocol.Caret_Update(node_pos, focus)) } }) } /* dispatcher thread */ override def assert_dispatcher[A](body: => A): A = session.assert_dispatcher(body) override def require_dispatcher[A](body: => A): A = session.require_dispatcher(body) override def send_dispatcher(body: => Unit): Unit = session.send_dispatcher(body) override def send_wait_dispatcher(body: => Unit): Unit = session.send_wait_dispatcher(body) } } diff --git a/src/Tools/jEdit/src/jedit_sessions.scala b/src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala +++ b/src/Tools/jEdit/src/jedit_sessions.scala @@ -1,151 +1,151 @@ /* Title: Tools/jEdit/src/jedit_sessions.scala Author: Makarius Isabelle/jEdit session information, based on implicit process environment and explicit options. */ package isabelle.jedit import isabelle._ import scala.swing.ComboBox import scala.swing.event.SelectionChanged object JEdit_Sessions { /* session options */ def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).filterNot(p => p.implode == "-") def session_no_build(): Boolean = Isabelle_System.getenv("JEDIT_NO_BUILD") == "true" def session_options(options: Options): Options = { val options1 = Isabelle_System.getenv("JEDIT_BUILD_MODE") match { case "default" => options case mode => options.bool.update("system_heaps", mode == "system") } val options2 = Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match { case "" => options1 case s => options1.string.update("ML_process_policy", s) } options2 } def sessions_structure(options: Options, dirs: List[Path] = session_dirs()): Sessions.Structure = Sessions.load_structure(session_options(options), dirs = dirs) /* raw logic info */ private val jedit_logic_option = "jedit_logic" def logic_name(options: Options): String = Isabelle_System.default_logic( Isabelle_System.getenv("JEDIT_LOGIC"), options.string(jedit_logic_option)) def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR")) def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true" def logic_include_sessions: List[String] = space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS")) def logic_info(options: Options): Option[Sessions.Info] = try { sessions_structure(options).get(logic_name(options)) } catch { case ERROR(_) => None } def logic_root(options: Options): Position.T = if (logic_requirements) logic_info(options).map(_.pos) getOrElse Position.none else Position.none /* logic selector */ private class Logic_Entry(val name: String, val description: String) { override def toString: String = description } def logic_selector(options: Options_Variable, autosave: Boolean): Option_Component = { GUI_Thread.require {} val session_list = { val sessions = sessions_structure(options.value) val (main_sessions, other_sessions) = sessions.imports_topological_order.partition(name => sessions(name).groups.contains("main")) main_sessions.sorted ::: other_sessions.sorted } val entries = new Logic_Entry("", "default (" + logic_name(options.value) + ")") :: session_list.map(name => new Logic_Entry(name, name)) val component = new ComboBox(entries) with Option_Component { name = jedit_logic_option val title = "Logic" def load: Unit = { val logic = options.string(jedit_logic_option) entries.find(_.name == logic) match { case Some(entry) => selection.item = entry case None => } } def save: Unit = options.string(jedit_logic_option) = selection.item.name } component.load() if (autosave) { component.listenTo(component.selection) component.reactions += { case SelectionChanged(_) => component.save() } } component.tooltip = "Logic session name (change requires restart)" component } /* session build process */ def session_base_info(options: Options): Sessions.Base_Info = Sessions.base_info(options, dirs = JEdit_Sessions.session_dirs(), include_sessions = logic_include_sessions, session = logic_name(options), session_ancestor = logic_ancestor, session_requirements = logic_requirements) def session_build( options: Options, progress: Progress = new Progress, no_build: Boolean = false): Int = { - Build.build(session_options(options), progress = progress, build_heap = true, - no_build = no_build, dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos, - sessions = List(PIDE.resources.session_name)).rc + Build.build(session_options(options), Sessions.Selection.session(PIDE.resources.session_name), + progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs(), + infos = PIDE.resources.session_base_info.infos).rc } def session_start(options0: Options) { val session = PIDE.session val options = session_options(options0) val sessions_structure = PIDE.resources.session_base_info.sessions_structure val store = Sessions.store(options) session.phase_changed += PIDE.plugin.session_phase_changed Isabelle_Process(session, options, sessions_structure, store, logic = PIDE.resources.session_name, modes = (space_explode(',', options.string("jedit_print_mode")) ::: space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse) } }