support PIDE option (inactive);
authorwenzelm
Sat Mar 18 16:43:40 2017 +0100 (2017-03-18)
changeset 653088f58102afa22
parent 65307 c1ba192b4f96
child 65309 3024fcd5a7f4
support PIDE option (inactive);
misc tuning;
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.scala	Sat Mar 18 16:15:37 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Sat Mar 18 16:43:40 2017 +0100
     1.3 @@ -130,33 +130,34 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* jobs */
     1.8 +  /* job: running prover process */
     1.9  
    1.10 -  private class Job(progress: Progress, name: String, val info: Sessions.Info, tree: Sessions.Tree,
    1.11 -    store: Sessions.Store, do_output: Boolean, verbose: Boolean, val numa_node: Option[Int],
    1.12 -    session_graph: Graph_Display.Graph, command_timings: List[Properties.T])
    1.13 +  private class Job(progress: Progress,
    1.14 +    name: String,
    1.15 +    val info: Sessions.Info,
    1.16 +    tree: Sessions.Tree,
    1.17 +    store: Sessions.Store,
    1.18 +    do_output: Boolean,
    1.19 +    verbose: Boolean,
    1.20 +    pide: Boolean,
    1.21 +    val numa_node: Option[Int],
    1.22 +    session_graph: Graph_Display.Graph,
    1.23 +    command_timings: List[Properties.T])
    1.24    {
    1.25      val output = store.output_dir + Path.basic(name)
    1.26      def output_path: Option[Path] = if (do_output) Some(output) else None
    1.27 -    def output_save_state: String =
    1.28 -      if (do_output) "ML_Heap.save_child " + ML_Syntax.print_string0(File.platform_path(output))
    1.29 -      else ""
    1.30      output.file.delete
    1.31  
    1.32 -    private val parent = info.parent.getOrElse("")
    1.33 -
    1.34      private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
    1.35      try { isabelle.graphview.Graph_File.write(info.options, graph_file, session_graph) }
    1.36      catch { case ERROR(_) => /*error should be exposed in ML*/ }
    1.37  
    1.38 -    private val env =
    1.39 -      Isabelle_System.settings() +
    1.40 -        ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
    1.41 -
    1.42      private val future_result: Future[Process_Result] =
    1.43        Future.thread("build") {
    1.44 -        val args_file = Isabelle_System.tmp_file("build")
    1.45 -        File.write(args_file, YXML.string_of_body(
    1.46 +        val parent = info.parent.getOrElse("")
    1.47 +
    1.48 +        val args_yxml =
    1.49 +          YXML.string_of_body(
    1.50              {
    1.51                val theories = info.theories.map(x => (x._2, x._3))
    1.52                import XML.Encode._
    1.53 @@ -168,44 +169,59 @@
    1.54                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
    1.55                  (parent, (info.chapter, (name, (Path.current,
    1.56                  theories))))))))))))
    1.57 -            }))
    1.58 +            })
    1.59 +
    1.60 +        val env =
    1.61 +          Isabelle_System.settings() +
    1.62 +            ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
    1.63 +
    1.64 +        def save_heap: String =
    1.65 +          "ML_Heap.share_common_data (); ML_Heap.save_child " +
    1.66 +            ML_Syntax.print_string0(File.platform_path(output))
    1.67  
    1.68 -        val eval =
    1.69 -          "Command_Line.tool0 (fn () => (" +
    1.70 -          "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) +
    1.71 -          (if (do_output) "; ML_Heap.share_common_data (); " + output_save_state
    1.72 -           else "") + "));"
    1.73 +        if (pide) {
    1.74 +          error("FIXME")
    1.75 +        }
    1.76 +        else {
    1.77 +          val args_file = Isabelle_System.tmp_file("build")
    1.78 +          File.write(args_file, args_yxml)
    1.79 +
    1.80 +          val eval =
    1.81 +            "Command_Line.tool0 (fn () => (" +
    1.82 +            "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) +
    1.83 +            (if (do_output) "; " + save_heap else "") + "));"
    1.84  
    1.85 -        val process_options =
    1.86 -          numa_node match {
    1.87 -            case None => info.options
    1.88 -            case Some(n) => info.options.string("ML_process_policy") = NUMA.policy(n)
    1.89 -          }
    1.90 -        val process =
    1.91 -          if (Sessions.pure_name(name)) {
    1.92 -            ML_Process(process_options, raw_ml_system = true, cwd = info.dir.file,
    1.93 -              args =
    1.94 -                (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
    1.95 -                List("--eval", eval),
    1.96 -              env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
    1.97 -          }
    1.98 -          else {
    1.99 -            ML_Process(process_options, parent, List("--eval", eval), cwd = info.dir.file,
   1.100 -              env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
   1.101 -          }
   1.102 +          val process_options =
   1.103 +            numa_node match {
   1.104 +              case None => info.options
   1.105 +              case Some(n) => info.options.string("ML_process_policy") = NUMA.policy(n)
   1.106 +            }
   1.107 +          val process =
   1.108 +            if (Sessions.pure_name(name)) {
   1.109 +              ML_Process(process_options, raw_ml_system = true, cwd = info.dir.file,
   1.110 +                args =
   1.111 +                  (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
   1.112 +                  List("--eval", eval),
   1.113 +                env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
   1.114 +            }
   1.115 +            else {
   1.116 +              ML_Process(process_options, parent, List("--eval", eval), cwd = info.dir.file,
   1.117 +                env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
   1.118 +            }
   1.119  
   1.120 -        process.result(
   1.121 -          progress_stdout = (line: String) =>
   1.122 -            Library.try_unprefix("\floading_theory = ", line) match {
   1.123 -              case Some(theory) => progress.theory(name, theory)
   1.124 -              case None =>
   1.125 -            },
   1.126 -          progress_limit =
   1.127 -            info.options.int("process_output_limit") match {
   1.128 -              case 0 => None
   1.129 -              case m => Some(m * 1000000L)
   1.130 -            },
   1.131 -          strict = false)
   1.132 +          process.result(
   1.133 +            progress_stdout = (line: String) =>
   1.134 +              Library.try_unprefix("\floading_theory = ", line) match {
   1.135 +                case Some(theory) => progress.theory(name, theory)
   1.136 +                case None =>
   1.137 +              },
   1.138 +            progress_limit =
   1.139 +              info.options.int("process_output_limit") match {
   1.140 +                case 0 => None
   1.141 +                case m => Some(m * 1000000L)
   1.142 +              },
   1.143 +            strict = false)
   1.144 +        }
   1.145        }
   1.146  
   1.147      def terminate: Unit = future_result.cancel
   1.148 @@ -269,6 +285,7 @@
   1.149      no_build: Boolean = false,
   1.150      system_mode: Boolean = false,
   1.151      verbose: Boolean = false,
   1.152 +    pide: Boolean = false,
   1.153      requirements: Boolean = false,
   1.154      all_sessions: Boolean = false,
   1.155      exclude_session_groups: List[String] = Nil,
   1.156 @@ -290,6 +307,7 @@
   1.157        no_build = no_build,
   1.158        system_mode = system_mode,
   1.159        verbose = verbose,
   1.160 +      pide = pide,
   1.161        selection = { full_tree =>
   1.162          full_tree.selection(requirements, all_sessions,
   1.163            exclude_session_groups, exclude_sessions, session_groups, sessions) })
   1.164 @@ -309,6 +327,7 @@
   1.165      no_build: Boolean = false,
   1.166      system_mode: Boolean = false,
   1.167      verbose: Boolean = false,
   1.168 +    pide: Boolean = false,
   1.169      selection: Sessions.Tree => (List[String], Sessions.Tree) =
   1.170        (_.selection(all_sessions = true))): Results =
   1.171    {
   1.172 @@ -477,7 +496,7 @@
   1.173                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   1.174                    val job =
   1.175                      new Job(progress, name, info, selected_tree, store, do_output, verbose,
   1.176 -                      numa_node, deps(name).session_graph, queue.command_timings(name))
   1.177 +                      pide, numa_node, deps(name).session_graph, queue.command_timings(name))
   1.178                    loop(pending, running + (name -> (ancestor_heaps, job)), results)
   1.179                  }
   1.180                  else {
   1.181 @@ -548,6 +567,7 @@
   1.182  
   1.183      var select_dirs: List[Path] = Nil
   1.184      var numa_shuffling = false
   1.185 +    var pide = false
   1.186      var requirements = false
   1.187      var exclude_session_groups: List[String] = Nil
   1.188      var all_sessions = false
   1.189 @@ -570,6 +590,7 @@
   1.190    Options are:
   1.191      -D DIR       include session directory and select its sessions
   1.192      -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
   1.193 +    -P           build via PIDE protocol
   1.194      -R           operate on requirements of selected sessions
   1.195      -X NAME      exclude sessions from group NAME and all descendants
   1.196      -a           select all sessions
   1.197 @@ -591,6 +612,7 @@
   1.198  """ + Library.prefix_lines("  ", Build_Log.Settings.show()) + "\n",
   1.199        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   1.200        "N" -> (_ => numa_shuffling = true),
   1.201 +      "P" -> (_ => pide = true),
   1.202        "R" -> (_ => requirements = true),
   1.203        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   1.204        "a" -> (_ => all_sessions = true),
   1.205 @@ -634,6 +656,7 @@
   1.206            no_build = no_build,
   1.207            system_mode = system_mode,
   1.208            verbose = verbose,
   1.209 +          pide = pide,
   1.210            requirements = requirements,
   1.211            all_sessions = all_sessions,
   1.212            exclude_session_groups = exclude_session_groups,