documentation for "isabelle dump";
authorwenzelm
Fri Jun 01 15:53:35 2018 +0200 (20 months ago ago)
changeset 683492ac3a5c07dfa
parent 68348 9e6e7ab77434
child 68350 30d6ffd0ca07
documentation for "isabelle dump";
NEWS
src/Doc/System/Sessions.thy
src/Pure/Tools/dump.scala
     1.1 --- a/NEWS	Fri Jun 01 11:51:03 2018 +0200
     1.2 +++ b/NEWS	Fri Jun 01 15:53:35 2018 +0200
     1.3 @@ -380,6 +380,11 @@
     1.4  and concurrent use of theories, based on Isabelle/PIDE infrastructure.
     1.5  See also the "system" manual.
     1.6  
     1.7 +* The command-line tool "dump" dumps information from the cumulative
     1.8 +PIDE session database: many sessions may be loaded into a given logic
     1.9 +image, results from all loaded theories are written to the output
    1.10 +directory.
    1.11 +
    1.12  * The command-line tool "isabelle update_comments" normalizes formal
    1.13  comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
    1.14  approximate the appearance in document output). This is more specific
     2.1 --- a/src/Doc/System/Sessions.thy	Fri Jun 01 11:51:03 2018 +0200
     2.2 +++ b/src/Doc/System/Sessions.thy	Fri Jun 01 15:53:35 2018 +0200
     2.3 @@ -595,4 +595,85 @@
     2.4    own sub-directory hierarchy, using the session-qualified theory name.
     2.5  \<close>
     2.6  
     2.7 +
     2.8 +section \<open>Dump PIDE session database \label{sec:tool-dump}\<close>
     2.9 +
    2.10 +text \<open>
    2.11 +  The @{tool_def "dump"} tool dumps information from the cumulative PIDE
    2.12 +  session database (which is processed on the spot). Its command-line usage
    2.13 +  is: @{verbatim [display]
    2.14 +\<open>Usage: isabelle dump [OPTIONS] [SESSIONS ...]
    2.15 +
    2.16 +  Options are:
    2.17 +    -A NAMES     dump named aspects (default: ...)
    2.18 +    -B NAME      include session NAME and all descendants
    2.19 +    -D DIR       include session directory and select its sessions
    2.20 +    -O DIR       output directory for dumped files (default: "dump")
    2.21 +    -R           operate on requirements of selected sessions
    2.22 +    -X NAME      exclude sessions from group NAME and all descendants
    2.23 +    -a           select all sessions
    2.24 +    -d DIR       include session directory
    2.25 +    -g NAME      select session group NAME
    2.26 +    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
    2.27 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    2.28 +    -s           system build mode for logic image
    2.29 +    -v           verbose
    2.30 +    -x NAME      exclude session NAME and all descendants
    2.31 +
    2.32 +  Dump cumulative PIDE session database, with the following aspects:
    2.33 +    ...\<close>}
    2.34 +
    2.35 +  \<^medskip> Options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> and the
    2.36 +  remaining command-line arguments specify sessions as in @{tool build}
    2.37 +  (\secref{sec:tool-build}): the cumulative PIDE database of all their loaded
    2.38 +  theories is dumped to the output directory of option \<^verbatim>\<open>-O\<close> (default: \<^verbatim>\<open>dump\<close>
    2.39 +  in the current directory).
    2.40 +
    2.41 +  \<^medskip> Option \<^verbatim>\<open>-l\<close> specifies a logic image for the underlying prover process:
    2.42 +  its theories are not processed again, and their PIDE session database is
    2.43 +  excluded from the dump. Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close> when building
    2.44 +  the logic image (\secref{sec:tool-build}).
    2.45 +
    2.46 +  \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
    2.47 +  (\secref{sec:tool-build}).
    2.48 +
    2.49 +  \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
    2.50 +
    2.51 +  \<^medskip> Option \<^verbatim>\<open>-A\<close> specifies named aspects of the dump, as a comma-separated
    2.52 +  list. The default is to dump all known aspects, as given in the command-line
    2.53 +  usage of the tool. The underlying Isabelle/Scala function
    2.54 +  \<^verbatim>\<open>isabelle.Dump.dump()\<close> takes aspects as user-defined operations on the
    2.55 +  final PIDE state and document version. This allows to imitate Prover IDE
    2.56 +  rendering under program control.
    2.57 +\<close>
    2.58 +
    2.59 +
    2.60 +subsubsection \<open>Examples\<close>
    2.61 +
    2.62 +text \<open>
    2.63 +  Dump all Isabelle/ZF sessions (which are rather small):
    2.64 +  @{verbatim [display] \<open>isabelle dump -v -B ZF\<close>}
    2.65 +
    2.66 +  \<^smallskip>
    2.67 +  Dump the quite substantial \<^verbatim>\<open>HOL-Analysis\<close> session, using main Isabelle/HOL
    2.68 +  as starting point:
    2.69 +  @{verbatim [display] \<open>isabelle dump -v -l HOL HOL-Analysis\<close>}
    2.70 +
    2.71 +  \<^smallskip>
    2.72 +  Dump all sessions connected to HOL-Analysis, including a full bootstrap of
    2.73 +  Isabelle/HOL from Isabelle/Pure:
    2.74 +  @{verbatim [display] \<open>isabelle dump -v -l Pure -B HOL-Analysis\<close>}
    2.75 +
    2.76 +  This results in uniform PIDE markup for everything, except for the
    2.77 +  Isabelle/Pure bootstrap process itself. Producing that on the spot requires
    2.78 +  several GB of heap space, both for the Isabelle/Scala and Isabelle/ML
    2.79 +  process (in 64bit mode). Here are some relevant settings (\secref{sec:boot})
    2.80 +  for such ambitious applications:
    2.81 +  @{verbatim [display]
    2.82 +\<open>ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx32g -Xss16m"
    2.83 +ML_OPTIONS="--minheap 4G --maxheap 32G"
    2.84 +\<close>}
    2.85 +
    2.86 +\<close>
    2.87 +
    2.88  end
     3.1 --- a/src/Pure/Tools/dump.scala	Fri Jun 01 11:51:03 2018 +0200
     3.2 +++ b/src/Pure/Tools/dump.scala	Fri Jun 01 15:53:35 2018 +0200
     3.3 @@ -1,7 +1,7 @@
     3.4  /*  Title:      Pure/Tools/dump.scala
     3.5      Author:     Makarius
     3.6  
     3.7 -Dump build database produced by PIDE session.
     3.8 +Dump cumulative PIDE session database.
     3.9  */
    3.10  
    3.11  package isabelle
    3.12 @@ -135,7 +135,7 @@
    3.13    /* Isabelle tool wrapper */
    3.14  
    3.15    val isabelle_tool =
    3.16 -    Isabelle_Tool("dump", "dump build database produced by PIDE session.", args =>
    3.17 +    Isabelle_Tool("dump", "dump cumulative PIDE session database", args =>
    3.18      {
    3.19        var aspects: List[Aspect] = known_aspects
    3.20        var base_sessions: List[String] = Nil
    3.21 @@ -171,8 +171,7 @@
    3.22      -v           verbose
    3.23      -x NAME      exclude session NAME and all descendants
    3.24  
    3.25 -  Dump build database produced by PIDE session. The following dump aspects
    3.26 -  are available:
    3.27 +  Dump cumulative PIDE session database, with the following aspects:
    3.28  
    3.29  """ + Library.prefix_lines("    ", show_aspects) + "\n",
    3.30        "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),