# HG changeset patch
# User wenzelm
# Date 1567091629 -7200
# Node ID 0f8742b5a9e8f40a51cbfd50e657a60bf35cf4d6
# Parent  b99b925dbd84d0c70e4899d8c0c715a2d4cda12c
more scalable isabelle dump (and derivatives): mark individual theories to share common data in ML;

diff -r b99b925dbd84 -r 0f8742b5a9e8 etc/options
--- a/etc/options	Thu Aug 29 15:43:05 2019 +0200
+++ b/etc/options	Thu Aug 29 17:13:49 2019 +0200
@@ -219,6 +219,9 @@
 option execution_eager : bool = false
   -- "prefer theories with shorter stack of decendants"
 
+option dump_checkpoint : bool = false
+  -- "mark individual theories to share common data in ML"
+
 
 section "Miscellaneous Tools"
 
diff -r b99b925dbd84 -r 0f8742b5a9e8 src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Aug 29 15:43:05 2019 +0200
+++ b/src/HOL/ROOT	Thu Aug 29 17:13:49 2019 +0200
@@ -5,7 +5,7 @@
     Classical Higher-order Logic.
   "
   options [strict_facts]
-  theories
+  theories [dump_checkpoint]
     Main (global)
     Complex_Main (global)
   document_files
@@ -64,7 +64,7 @@
   sessions
     "HOL-Library"
     "HOL-Computational_Algebra"
-  theories
+  theories [dump_checkpoint]
     Analysis
   document_files
     "root.tex"
diff -r b99b925dbd84 -r 0f8742b5a9e8 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Aug 29 15:43:05 2019 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu Aug 29 17:13:49 2019 +0200
@@ -135,6 +135,13 @@
   def import_name(info: Sessions.Info, s: String): Document.Node.Name =
     import_name(info.name, info.dir.implode, s)
 
+  def dump_checkpoint(info: Sessions.Info): List[Document.Node.Name] =
+    for {
+      (options, thys) <- info.theories
+      if options.bool("dump_checkpoint")
+      (thy, _) <- thys
+    } yield import_name(info, thy)
+
   def standard_import(base: Sessions.Base, qualifier: String, dir: String, s: String): String =
   {
     val name = import_name(qualifier, dir, s)
diff -r b99b925dbd84 -r 0f8742b5a9e8 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Aug 29 15:43:05 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Aug 29 17:13:49 2019 +0200
@@ -148,6 +148,7 @@
     global_theories: Map[String, String] = Map.empty,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     used_theories: List[(Options, Document.Node.Name)] = Nil,
+    dump_checkpoint: List[Document.Node.Name] = Nil,
     known: Known = Known.empty,
     overall_syntax: Outer_Syntax = Outer_Syntax.empty,
     imported_sources: List[(Path, SHA1.Digest)] = Nil,
@@ -200,6 +201,12 @@
     def imported_sources(name: String): List[SHA1.Digest] =
       session_bases(name).imported_sources.map(_._2)
 
+    def dump_checkpoint: List[Document.Node.Name] =
+      (for {
+        (_, base) <- session_bases.iterator
+        name <- base.dump_checkpoint.iterator
+      } yield name).toList
+
     def used_theories_condition(default_options: Options, progress: Progress = No_Progress)
       : List[(Options, Document.Node.Name)] =
     {
@@ -301,6 +308,8 @@
 
             val dependencies = resources.session_dependencies(info)
 
+            val dump_checkpoint = resources.dump_checkpoint(info)
+
             val overall_syntax = dependencies.overall_syntax
 
             val theory_files = dependencies.theories.map(_.path)
@@ -379,6 +388,7 @@
                 global_theories = global_theories,
                 loaded_theories = dependencies.loaded_theories,
                 used_theories = dependencies.adjunct_theories,
+                dump_checkpoint = dump_checkpoint,
                 known = known,
                 overall_syntax = overall_syntax,
                 imported_sources = check_sources(imported_files),
diff -r b99b925dbd84 -r 0f8742b5a9e8 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Thu Aug 29 15:43:05 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Thu Aug 29 17:13:49 2019 +0200
@@ -167,13 +167,22 @@
     /* run session */
 
     try {
+      val dump_checkpoint = deps.dump_checkpoint.toSet
+      def commit(snapshot: Document.Snapshot, status: Document_Status.Node_Status)
+      {
+        if (dump_checkpoint(snapshot.node_name)) {
+          session.protocol_command("ML_Heap.share_common_data")
+        }
+        Consumer.apply(snapshot, status)
+      }
+
       val use_theories = resources.used_theories(deps).map(_.theory)
       val use_theories_result =
         session.use_theories(use_theories,
           unicode_symbols = unicode_symbols,
           share_common_data = true,
           progress = progress,
-          commit = Some(Consumer.apply _))
+          commit = Some(commit _))
 
       val bad_theories = Consumer.shutdown()
       val bad_msgs =
diff -r b99b925dbd84 -r 0f8742b5a9e8 src/ZF/ROOT
--- a/src/ZF/ROOT	Thu Aug 29 15:43:05 2019 +0200
+++ b/src/ZF/ROOT	Thu Aug 29 17:13:49 2019 +0200
@@ -46,6 +46,7 @@
     FOL
   theories
     ZF (global)
+  theories [dump_checkpoint]
     ZFC (global)
   document_files "root.tex"