*** 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev