support for Poly/ML heap hierarchy, which saves a lot of disk space;
authorwenzelm
Wed Mar 16 15:08:22 2016 +0100 (2016-03-16)
changeset 626370189fe0f6452
parent 62636 e676ae9f1bf6
child 62638 751cf9f3d433
support for Poly/ML heap hierarchy, which saves a lot of disk space;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Pure/Tools/ml_process.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Wed Mar 16 14:24:51 2016 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Wed Mar 16 15:08:22 2016 +0100
     1.3 @@ -318,7 +318,8 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* persistent store */
     1.8 +
     1.9 +  /** persistent store **/
    1.10  
    1.11    def log(name: String): Path = Path.basic("log") + Path.basic(name)
    1.12    def log_gz(name: String): Path = log(name).ext("gz")
    1.13 @@ -327,15 +328,22 @@
    1.14  
    1.15    class Store private [Sessions](system_mode: Boolean)
    1.16    {
    1.17 -    val output_dir: Path =
    1.18 -      if (system_mode) Path.explode("~~/heaps/$ML_IDENTIFIER")
    1.19 -      else Path.explode("$ISABELLE_OUTPUT")
    1.20 +    /* output */
    1.21  
    1.22      val browser_info: Path =
    1.23        if (system_mode) Path.explode("~~/browser_info")
    1.24        else Path.explode("$ISABELLE_BROWSER_INFO")
    1.25  
    1.26 -    val input_dirs =
    1.27 +    val output_dir: Path =
    1.28 +      if (system_mode) Path.explode("~~/heaps/$ML_IDENTIFIER")
    1.29 +      else Path.explode("$ISABELLE_OUTPUT")
    1.30 +
    1.31 +    def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
    1.32 +
    1.33 +
    1.34 +    /* input */
    1.35 +
    1.36 +    private val input_dirs =
    1.37        if (system_mode) List(output_dir)
    1.38        else {
    1.39          val ml_ident = Path.explode("$ML_IDENTIFIER").expand
    1.40 @@ -346,15 +354,18 @@
    1.41        input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir =>
    1.42          (dir + log_gz(name), File.time_stamp(dir + Path.basic(name))))
    1.43  
    1.44 -    def find_heap(name: String): Option[Path] =
    1.45 -      input_dirs.map(_ + Path.basic(name)).find(_.is_file)
    1.46 -
    1.47      def find_log(name: String): Option[Path] =
    1.48        input_dirs.map(_ + log(name)).find(_.is_file)
    1.49  
    1.50      def find_log_gz(name: String): Option[Path] =
    1.51        input_dirs.map(_ + log_gz(name)).find(_.is_file)
    1.52  
    1.53 -    def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
    1.54 +    def find_heap(name: String): Option[Path] =
    1.55 +      input_dirs.map(_ + Path.basic(name)).find(_.is_file)
    1.56 +
    1.57 +    def heap(name: String): Path =
    1.58 +      find_heap(name) getOrElse
    1.59 +        error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +
    1.60 +          cat_lines(input_dirs.map(dir => "  " + dir.implode)))
    1.61    }
    1.62  }
     2.1 --- a/src/Pure/Tools/build.scala	Wed Mar 16 14:24:51 2016 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Wed Mar 16 15:08:22 2016 +0100
     2.3 @@ -228,7 +228,7 @@
     2.4  
     2.5    /* jobs */
     2.6  
     2.7 -  private class Job(progress: Progress, name: String, val info: Sessions.Info,
     2.8 +  private class Job(progress: Progress, name: String, val info: Sessions.Info, tree: Sessions.Tree,
     2.9      store: Sessions.Store, do_output: Boolean, verbose: Boolean,
    2.10      session_graph: Graph_Display.Graph, command_timings: List[Properties.T])
    2.11    {
    2.12 @@ -236,7 +236,8 @@
    2.13      def output_path: Option[Path] = if (do_output) Some(output) else None
    2.14      def output_save_state: String =
    2.15        if (do_output)
    2.16 -        "PolyML.SaveState.saveState " + ML_Syntax.print_string_raw(File.platform_path(output))
    2.17 +        "PolyML.SaveState.saveChild (" + ML_Syntax.print_string_raw(File.platform_path(output)) +
    2.18 +          ", List.length (PolyML.SaveState.showHierarchy ()))"
    2.19        else ""
    2.20      output.file.delete
    2.21  
    2.22 @@ -258,7 +259,7 @@
    2.23                "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default ();" +
    2.24                " Session.shutdown (); ML_Heap.share_common_data (); " + output_save_state + "));"
    2.25              ML_Process(info.options, "RAW_ML_SYSTEM", List("--use", "ROOT.ML", "--eval", eval),
    2.26 -              cwd = info.dir.file, env = env, store = store)
    2.27 +              cwd = info.dir.file, env = env, tree = Some(tree), store = store)
    2.28            }
    2.29            else {
    2.30              val args_file = Isabelle_System.tmp_file("build")
    2.31 @@ -281,7 +282,7 @@
    2.32                (if (do_output) "; ML_Heap.share_common_data (); " + output_save_state
    2.33                 else "") + "));"
    2.34              ML_Process(info.options, parent, List("--eval", eval), cwd = info.dir.file,
    2.35 -              env = env, cleanup = () => args_file.delete, store = store)
    2.36 +              env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
    2.37            }
    2.38          process.result(
    2.39            progress_stdout = (line: String) =>
    2.40 @@ -622,7 +623,7 @@
    2.41                  else if (ancestor_results.forall(_.ok) && !progress.stopped) {
    2.42                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
    2.43                    val job =
    2.44 -                    new Job(progress, name, info, store, do_output, verbose,
    2.45 +                    new Job(progress, name, info, selected_tree, store, do_output, verbose,
    2.46                        deps(name).session_graph, queue.command_timings(name))
    2.47                    loop(pending, running + (name -> (ancestor_heaps, job)), results)
    2.48                  }
     3.1 --- a/src/Pure/Tools/ml_process.scala	Wed Mar 16 14:24:51 2016 +0100
     3.2 +++ b/src/Pure/Tools/ml_process.scala	Wed Mar 16 15:08:22 2016 +0100
     3.3 @@ -15,6 +15,7 @@
     3.4    def apply(options: Options,
     3.5      logic: String = "",
     3.6      args: List[String] = Nil,
     3.7 +    dirs: List[Path] = Nil,
     3.8      modes: List[String] = Nil,
     3.9      secure: Boolean = false,
    3.10      cwd: JFile = null,
    3.11 @@ -22,28 +23,19 @@
    3.12      redirect: Boolean = false,
    3.13      cleanup: () => Unit = () => (),
    3.14      channel: Option[System_Channel] = None,
    3.15 +    tree: Option[Sessions.Tree] = None,
    3.16      store: Sessions.Store = Sessions.store()): Bash.Process =
    3.17    {
    3.18 -    val heaps =
    3.19 -      Isabelle_System.default_logic(logic) match {
    3.20 -        case "RAW_ML_SYSTEM" => Nil
    3.21 -        case name =>
    3.22 -          store.find_heap(name) match {
    3.23 -            case Some(path) => List(path)
    3.24 -            case None =>
    3.25 -              error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +
    3.26 -                cat_lines(store.input_dirs.map(dir => "  " + dir.implode)))
    3.27 -          }
    3.28 +    val logic_name = Isabelle_System.default_logic(logic)
    3.29 +    val heaps: List[String] =
    3.30 +      if (logic_name == "RAW_ML_SYSTEM") Nil
    3.31 +      else {
    3.32 +        val session_tree = tree.getOrElse(Sessions.load(options, dirs))
    3.33 +        (session_tree.ancestors(logic_name) ::: List(logic_name)).
    3.34 +          map(a => File.platform_path(store.heap(a)))
    3.35        }
    3.36  
    3.37 -    val eval_heaps =
    3.38 -      heaps.map(heap =>
    3.39 -        "(PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(heap)) +
    3.40 -        "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
    3.41 -        ML_Syntax.print_string_raw(": " + heap.toString + "\n") +
    3.42 -        "); OS.Process.exit OS.Process.failure)")
    3.43 -
    3.44 -    val eval_initial =
    3.45 +    val eval_init =
    3.46        if (heaps.isEmpty) {
    3.47          List(
    3.48            if (Platform.is_windows)
    3.49 @@ -55,7 +47,13 @@
    3.50            "PolyML.Compiler.prompt1 := \"Poly/ML> \"",
    3.51            "PolyML.Compiler.prompt2 := \"Poly/ML# \"")
    3.52        }
    3.53 -      else Nil
    3.54 +      else
    3.55 +        List(
    3.56 +          "(PolyML.SaveState.loadHierarchy " +
    3.57 +            ML_Syntax.print_list(ML_Syntax.print_string_raw)(heaps) +
    3.58 +          "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
    3.59 +          ML_Syntax.print_string_raw(": " + logic_name + "\n") +
    3.60 +          "); OS.Process.exit OS.Process.failure)")
    3.61  
    3.62      val eval_modes =
    3.63        if (modes.isEmpty) Nil
    3.64 @@ -88,7 +86,7 @@
    3.65      // bash
    3.66      val bash_args =
    3.67        Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
    3.68 -      (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
    3.69 +      (eval_init ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
    3.70          map(eval => List("--eval", eval)).flatten ::: args
    3.71  
    3.72      Bash.process("""exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args),