[isabelle-dev] NEWS: isabelle dump

[Makarius]

*** System ***

* 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.


This refers to Isabelle/2ac3a5c07dfa. It is a spin-off from various
subtle changes of PIDE session management, the Thy_Resources session
from the "isabelle server", and the blob export facility. It also
depends on the session-qualified theory reform from the last release.

The section about "isabelle dump" in the "system" manual contains
further explanations with examples. Just for the fun of it, here is
another one (lxcisa0, threads=6):

  ISABELLE_TOOL_JAVA_OPTIONS=-Djava.awt.headless=true -Xms2g -Xmx32g -Xss16m

  ML_PLATFORM="x86_64-linux"
  ML_HOME="/home/isabelle/contrib/polyml-5.7.1-5/x86_64-linux"
  ML_SYSTEM="polyml-5.7.1"
  ML_OPTIONS="--minheap 4G --maxheap 32G"

  isabelle dump -v -l Pure -B HOL-Analysis -d '$AFP'
  6:03:34 elapsed time, 20:50:34 cpu time, factor 3.44
  6.2G dump

These are all sessions connected to HOL-Analysis, starting from Pure;
overall 1121 theories. Thus we can now fill our file-systems with funny
YXML data. It also shows how far we are in the project "Prover IDE for
all of AFP as one big document", here as a headless version.

Actual applications of this should come eventually: over the years
people have often asked me how to externalize PIDE markup and turn it
into some use elsewhere, lets say for formal data mining. Another
application could be OpenTheory export, but that also works with plain
"isabelle build" + "isabelle export", instead of the more ambitious
"isabelle dump -A theory".


	Makarius