# HG changeset patch # User wenzelm # Date 1527861215 -7200 # Node ID 2ac3a5c07dfae9c6bec3ae4088be0c00c243e975 # Parent 9e6e7ab77434a6d2768b4419b55be0e6c8b0a027 documentation for "isabelle dump"; diff -r 9e6e7ab77434 -r 2ac3a5c07dfa NEWS --- a/NEWS Fri Jun 01 11:51:03 2018 +0200 +++ b/NEWS Fri Jun 01 15:53:35 2018 +0200 @@ -380,6 +380,11 @@ and concurrent use of theories, based on Isabelle/PIDE infrastructure. See also the "system" manual. +* The command-line tool "dump" dumps information from the cumulative +PIDE session database: many sessions may be loaded into a given logic +image, results from all loaded theories are written to the output +directory. + * The command-line tool "isabelle update_comments" normalizes formal comments in outer syntax as follows: \ \text\ (whith a single space to approximate the appearance in document output). This is more specific diff -r 9e6e7ab77434 -r 2ac3a5c07dfa src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Fri Jun 01 11:51:03 2018 +0200 +++ b/src/Doc/System/Sessions.thy Fri Jun 01 15:53:35 2018 +0200 @@ -595,4 +595,85 @@ own sub-directory hierarchy, using the session-qualified theory name. \ + +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 operate on 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 + -l NAME logic session name (default ISABELLE_LOGIC="HOL") + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -s system build mode for logic image + -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>\-l\ specifies a logic image for the underlying prover process: + its theories are not processed again, and their PIDE session database is + excluded from the dump. Option \<^verbatim>\-s\ enables \<^emph>\system mode\ when building + the logic image (\secref{sec:tool-build}). + + \<^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 function + \<^verbatim>\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, using main Isabelle/HOL + as starting point: + @{verbatim [display] \isabelle dump -v -l HOL HOL-Analysis\} + + \<^smallskip> + Dump all sessions connected to HOL-Analysis, including a full bootstrap of + Isabelle/HOL from Isabelle/Pure: + @{verbatim [display] \isabelle dump -v -l Pure -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" +\} + +\ + end diff -r 9e6e7ab77434 -r 2ac3a5c07dfa src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Fri Jun 01 11:51:03 2018 +0200 +++ b/src/Pure/Tools/dump.scala Fri Jun 01 15:53:35 2018 +0200 @@ -1,7 +1,7 @@ /* Title: Pure/Tools/dump.scala Author: Makarius -Dump build database produced by PIDE session. +Dump cumulative PIDE session database. */ package isabelle @@ -135,7 +135,7 @@ /* Isabelle tool wrapper */ val isabelle_tool = - Isabelle_Tool("dump", "dump build database produced by PIDE session.", args => + Isabelle_Tool("dump", "dump cumulative PIDE session database", args => { var aspects: List[Aspect] = known_aspects var base_sessions: List[String] = Nil @@ -171,8 +171,7 @@ -v verbose -x NAME exclude session NAME and all descendants - Dump build database produced by PIDE session. The following dump aspects - are available: + Dump cumulative PIDE session database, with the following aspects: """ + Library.prefix_lines(" ", show_aspects) + "\n", "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),