src/Pure/Tools/build.scala
author wenzelm
Sat May 05 13:56:51 2018 +0200 (12 months ago)
changeset 68086 9e1c670301b8
parent 67852 f701a1d5d852
child 68088 0763d4eb3ebc
permissions -rw-r--r--
cleanup session output before starting build job;
tuned signature;
     1 /*  Title:      Pure/Tools/build.scala
     2     Author:     Makarius
     3     Options:    :folding=explicit:
     4 
     5 Build and manage Isabelle sessions.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import scala.collection.SortedSet
    12 import scala.annotation.tailrec
    13 
    14 
    15 object Build
    16 {
    17   /** auxiliary **/
    18 
    19   /* persistent build info */
    20 
    21   sealed case class Session_Info(
    22     sources: String,
    23     input_heaps: List[String],
    24     output_heap: Option[String],
    25     return_code: Int)
    26   {
    27     def ok: Boolean = return_code == 0
    28   }
    29 
    30 
    31   /* queue with scheduling information */
    32 
    33   private object Queue
    34   {
    35     type Timings = (List[Properties.T], Double)
    36 
    37     def load_timings(progress: Progress, store: Sessions.Store, name: String): Timings =
    38     {
    39       val no_timings: Timings = (Nil, 0.0)
    40 
    41       store.find_database(name) match {
    42         case None => no_timings
    43         case Some(database) =>
    44           def ignore_error(msg: String) =
    45           {
    46             progress.echo_warning("Ignoring bad database: " +
    47               database.expand + (if (msg == "") "" else "\n" + msg))
    48             no_timings
    49           }
    50           try {
    51             using(SQLite.open_database(database))(db =>
    52             {
    53               val command_timings = store.read_command_timings(db, name)
    54               val session_timing =
    55                 store.read_session_timing(db, name) match {
    56                   case Markup.Elapsed(t) => t
    57                   case _ => 0.0
    58                 }
    59               (command_timings, session_timing)
    60             })
    61           }
    62           catch {
    63             case ERROR(msg) => ignore_error(msg)
    64             case exn: java.lang.Error => ignore_error(Exn.message(exn))
    65             case _: XML.Error => ignore_error("")
    66           }
    67       }
    68     }
    69 
    70     def apply(progress: Progress, sessions: Sessions.Structure, store: Sessions.Store): Queue =
    71     {
    72       val graph = sessions.build_graph
    73       val names = graph.keys
    74 
    75       val timings = names.map(name => (name, load_timings(progress, store, name)))
    76       val command_timings =
    77         Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
    78       val session_timing =
    79         Map(timings.map({ case (name, (_, t)) => (name, t) }): _*).withDefaultValue(0.0)
    80 
    81       def outdegree(name: String): Int = graph.imm_succs(name).size
    82 
    83       object Ordering extends scala.math.Ordering[String]
    84       {
    85         def compare_timing(name1: String, name2: String): Int =
    86         {
    87           val t1 = session_timing(name1)
    88           val t2 = session_timing(name2)
    89           if (t1 == 0.0 || t2 == 0.0) 0
    90           else t1 compare t2
    91         }
    92 
    93         def compare(name1: String, name2: String): Int =
    94           outdegree(name2) compare outdegree(name1) match {
    95             case 0 =>
    96               compare_timing(name2, name1) match {
    97                 case 0 =>
    98                   sessions(name2).timeout compare sessions(name1).timeout match {
    99                     case 0 => name1 compare name2
   100                     case ord => ord
   101                   }
   102                 case ord => ord
   103               }
   104             case ord => ord
   105           }
   106       }
   107 
   108       new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
   109     }
   110   }
   111 
   112   private class Queue(
   113     graph: Graph[String, Sessions.Info],
   114     order: SortedSet[String],
   115     val command_timings: String => List[Properties.T])
   116   {
   117     def is_inner(name: String): Boolean = !graph.is_maximal(name)
   118 
   119     def is_empty: Boolean = graph.is_empty
   120 
   121     def - (name: String): Queue =
   122       new Queue(graph.del_node(name),
   123         order - name,  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
   124         command_timings)
   125 
   126     def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
   127     {
   128       val it = order.iterator.dropWhile(name =>
   129         skip(name)
   130           || !graph.defined(name)  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
   131           || !graph.is_minimal(name))
   132       if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
   133       else None
   134     }
   135   }
   136 
   137 
   138   /* PIDE protocol handler */
   139 
   140   class Handler(progress: Progress, session: Session, session_name: String)
   141     extends Session.Protocol_Handler
   142   {
   143     val result_error: Promise[String] = Future.promise
   144 
   145     override def exit() { result_error.cancel }
   146 
   147     private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
   148     {
   149       val error_message =
   150         try { Pretty.string_of(Symbol.decode_yxml(msg.text)) }
   151         catch { case ERROR(msg) => msg }
   152       result_error.fulfill(error_message)
   153       session.send_stop()
   154       true
   155     }
   156 
   157     private def loading_theory(msg: Prover.Protocol_Output): Boolean =
   158       msg.properties match {
   159         case Markup.Loading_Theory(name) =>
   160           progress.theory(session_name, name)
   161           true
   162         case _ => false
   163       }
   164 
   165     val functions =
   166       List(
   167         Markup.BUILD_SESSION_FINISHED -> build_session_finished _,
   168         Markup.LOADING_THEORY -> loading_theory _)
   169   }
   170 
   171 
   172   /* job: running prover process */
   173 
   174   private class Job(progress: Progress,
   175     name: String,
   176     val info: Sessions.Info,
   177     sessions: Sessions.Structure,
   178     deps: Sessions.Deps,
   179     store: Sessions.Store,
   180     do_output: Boolean,
   181     verbose: Boolean,
   182     pide: Boolean,
   183     val numa_node: Option[Int],
   184     command_timings: List[Properties.T])
   185   {
   186     val output = store.output_dir + Path.basic(name)
   187     def output_path: Option[Path] = if (do_output) Some(output) else None
   188 
   189     val options =
   190       numa_node match {
   191         case None => info.options
   192         case Some(n) => info.options.string("ML_process_policy") = NUMA.policy(n)
   193       }
   194 
   195     private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
   196     isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
   197 
   198     private val future_result: Future[Process_Result] =
   199       Future.thread("build") {
   200         val parent = info.parent.getOrElse("")
   201         val base = deps(name)
   202         val args_yxml =
   203           YXML.string_of_body(
   204             {
   205               import XML.Encode._
   206               pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
   207                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
   208                 pair(string, pair(string, pair(string, pair(Path.encode,
   209                 pair(list(pair(Options.encode, list(pair(string, properties)))),
   210                 pair(list(pair(string, properties)), pair(list(string),
   211                 pair(list(pair(string, string)),
   212                 pair(list(string), pair(list(pair(string, string)), list(string))))))))))))))))))(
   213               (Symbol.codes, (command_timings, (do_output, (verbose,
   214                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
   215                 (parent, (info.chapter, (name, (Path.current,
   216                 (info.theories, (base.known.sessions.toList, (base.doc_names,
   217                 (base.global_theories.toList, (base.loaded_theories.keys, (base.dest_known_theories,
   218                 info.bibtex_entries.map(_.info)))))))))))))))))))
   219             })
   220 
   221         val env =
   222           Isabelle_System.settings() +
   223             ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
   224 
   225         def save_heap: String =
   226           (if (info.theories.isEmpty) "" else "ML_Heap.share_common_data (); ") +
   227             "ML_Heap.save_child " + ML_Syntax.print_string_bytes(File.platform_path(output))
   228 
   229         if (pide && !Sessions.is_pure(name)) {
   230           val resources = new Resources(deps(parent))
   231           val session = new Session(options, resources)
   232           val handler = new Handler(progress, session, name)
   233           session.init_protocol_handler(handler)
   234 
   235           val session_result = Future.promise[Process_Result]
   236 
   237           Isabelle_Process.start(session, options, logic = parent,
   238             cwd = info.dir.file, env = env, sessions = Some(sessions), store = store,
   239             phase_changed =
   240             {
   241               case Session.Ready => session.protocol_command("build_session", args_yxml)
   242               case Session.Terminated(result) => session_result.fulfill(result)
   243               case _ =>
   244             })
   245 
   246           val result = session_result.join
   247           handler.result_error.join match {
   248             case "" => result
   249             case msg =>
   250               result.copy(
   251                 rc = result.rc max 1,
   252                 out_lines = result.out_lines ::: split_lines(Output.error_message_text(msg)))
   253           }
   254         }
   255         else {
   256           val args_file = Isabelle_System.tmp_file("build")
   257           File.write(args_file, args_yxml)
   258 
   259           val eval =
   260             "Command_Line.tool0 (fn () => (" +
   261             "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) +
   262             (if (Sessions.is_pure(name)) "; Theory.install_pure (Thy_Info.get_theory Context.PureN)"
   263              else "") + (if (do_output) "; " + save_heap else "") + "));"
   264 
   265           val process =
   266             if (Sessions.is_pure(name)) {
   267               ML_Process(options, raw_ml_system = true, cwd = info.dir.file,
   268                 args =
   269                   (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
   270                   List("--eval", eval),
   271                 env = env, sessions = Some(sessions), store = store,
   272                 cleanup = () => args_file.delete)
   273             }
   274             else {
   275               ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
   276                 env = env, sessions = Some(sessions), store = store,
   277                 cleanup = () => args_file.delete)
   278             }
   279 
   280           process.result(
   281             progress_stdout = (line: String) =>
   282               Library.try_unprefix("\floading_theory = ", line) match {
   283                 case Some(theory) => progress.theory(name, theory)
   284                 case None =>
   285               },
   286             progress_limit =
   287               options.int("process_output_limit") match {
   288                 case 0 => None
   289                 case m => Some(m * 1000000L)
   290               },
   291             strict = false)
   292         }
   293       }
   294 
   295     def terminate: Unit = future_result.cancel
   296     def is_finished: Boolean = future_result.is_finished
   297 
   298     private val timeout_request: Option[Event_Timer.Request] =
   299     {
   300       if (info.timeout > Time.zero)
   301         Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
   302       else None
   303     }
   304 
   305     def join: Process_Result =
   306     {
   307       val result = future_result.join
   308 
   309       if (result.ok)
   310         Present.finish(progress, store.browser_info, graph_file, info, name)
   311 
   312       graph_file.delete
   313 
   314       val was_timeout =
   315         timeout_request match {
   316           case None => false
   317           case Some(request) => !request.cancel
   318         }
   319 
   320       if (result.interrupted) {
   321         if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout
   322         else result.error(Output.error_message_text("Interrupt"))
   323       }
   324       else result
   325     }
   326   }
   327 
   328 
   329 
   330   /** build with results **/
   331 
   332   class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)])
   333   {
   334     def sessions: Set[String] = results.keySet
   335     def cancelled(name: String): Boolean = results(name)._1.isEmpty
   336     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
   337     def info(name: String): Sessions.Info = results(name)._2
   338     val rc =
   339       (0 /: results.iterator.map(
   340         { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
   341     def ok: Boolean = rc == 0
   342 
   343     override def toString: String = rc.toString
   344   }
   345 
   346   def build(
   347     options: Options,
   348     progress: Progress = No_Progress,
   349     check_unknown_files: Boolean = false,
   350     build_heap: Boolean = false,
   351     clean_build: Boolean = false,
   352     dirs: List[Path] = Nil,
   353     select_dirs: List[Path] = Nil,
   354     infos: List[Sessions.Info] = Nil,
   355     numa_shuffling: Boolean = false,
   356     max_jobs: Int = 1,
   357     list_files: Boolean = false,
   358     check_keywords: Set[String] = Set.empty,
   359     fresh_build: Boolean = false,
   360     no_build: Boolean = false,
   361     soft_build: Boolean = false,
   362     system_mode: Boolean = false,
   363     verbose: Boolean = false,
   364     pide: Boolean = false,
   365     requirements: Boolean = false,
   366     all_sessions: Boolean = false,
   367     base_sessions: List[String] = Nil,
   368     exclude_session_groups: List[String] = Nil,
   369     exclude_sessions: List[String] = Nil,
   370     session_groups: List[String] = Nil,
   371     sessions: List[String] = Nil,
   372     selection: Sessions.Selection = Sessions.Selection.empty): Results =
   373   {
   374     val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
   375 
   376     val store = Sessions.store(system_mode)
   377 
   378 
   379     /* session selection and dependencies */
   380 
   381     val full_sessions =
   382       Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
   383 
   384     def sources_stamp(deps: Sessions.Deps, name: String): String =
   385     {
   386       val digests =
   387         full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name)
   388       SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
   389     }
   390 
   391     val selection1 =
   392       Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
   393         exclude_sessions, session_groups, sessions) ++ selection
   394 
   395     val (selected_sessions, deps) =
   396     {
   397       val selected_sessions0 = full_sessions.selection(selection1)
   398       val deps0 =
   399         Sessions.deps(selected_sessions0, full_sessions.global_theories,
   400           progress = progress, inlined_files = true, verbose = verbose,
   401           list_files = list_files, check_keywords = check_keywords).check_errors
   402 
   403       if (soft_build && !fresh_build) {
   404         val outdated =
   405           selected_sessions0.build_topological_order.flatMap(name =>
   406             store.find_database(name) match {
   407               case Some(database) =>
   408                 using(SQLite.open_database(database))(store.read_build(_, name)) match {
   409                   case Some(build)
   410                   if build.ok && build.sources == sources_stamp(deps0, name) => None
   411                   case _ => Some(name)
   412                 }
   413               case None => Some(name)
   414             })
   415         val selected_sessions =
   416           full_sessions.selection(Sessions.Selection(sessions = outdated))
   417         val deps =
   418           Sessions.deps(selected_sessions, full_sessions.global_theories,
   419             progress = progress, inlined_files = true).check_errors
   420         (selected_sessions, deps)
   421       }
   422       else (selected_sessions0, deps0)
   423     }
   424 
   425 
   426     /* check unknown files */
   427 
   428     if (check_unknown_files) {
   429       val source_files =
   430         (for {
   431           (_, base) <- deps.session_bases.iterator
   432           (path, _) <- base.sources.iterator
   433         } yield path).toList
   434       val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
   435       val unknown_files =
   436         Mercurial.check_files(source_files)._2.
   437           filterNot(path => exclude_files.contains(path.canonical_file))
   438       if (unknown_files.nonEmpty) {
   439         progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
   440           unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
   441       }
   442     }
   443 
   444 
   445     /* main build process */
   446 
   447     val queue = Queue(progress, selected_sessions, store)
   448 
   449     store.prepare_output()
   450 
   451     // cleanup
   452     def cleanup(name: String, echo: Boolean = false)
   453     {
   454       val files =
   455         List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
   456           map(store.output_dir + _).filter(_.is_file)
   457       if (files.nonEmpty) progress.echo_if(echo, "Cleaning " + name + " ...")
   458       val res = files.map(p => p.file.delete)
   459       if (!res.forall(ok => ok)) progress.echo_if(echo, name + " FAILED to delete")
   460     }
   461     if (clean_build) {
   462       for (name <- full_sessions.build_descendants(full_sessions.build_selection(selection1))) {
   463         cleanup(name, echo = true)
   464       }
   465     }
   466 
   467     // scheduler loop
   468     case class Result(
   469       current: Boolean,
   470       heap_stamp: Option[String],
   471       process: Option[Process_Result],
   472       info: Sessions.Info)
   473     {
   474       def ok: Boolean =
   475         process match {
   476           case None => false
   477           case Some(res) => res.rc == 0
   478         }
   479     }
   480 
   481     def sleep()
   482     {
   483       try { Thread.sleep(500) }
   484       catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
   485     }
   486 
   487     val numa_nodes = new NUMA.Nodes(numa_shuffling)
   488 
   489     @tailrec def loop(
   490       pending: Queue,
   491       running: Map[String, (List[String], Job)],
   492       results: Map[String, Result]): Map[String, Result] =
   493     {
   494       def used_node(i: Int): Boolean =
   495         running.iterator.exists(
   496           { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
   497 
   498       if (pending.is_empty) results
   499       else {
   500         if (progress.stopped)
   501           for ((_, (_, job)) <- running) job.terminate
   502 
   503         running.find({ case (_, (_, job)) => job.is_finished }) match {
   504           case Some((name, (input_heaps, job))) =>
   505             //{{{ finish job
   506 
   507             val process_result = job.join
   508 
   509             val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
   510             val process_result_tail =
   511             {
   512               val tail = job.info.options.int("process_output_tail")
   513               process_result.copy(
   514                 out_lines =
   515                   "(see also " + store.output_log(name).file.toString + ")" ::
   516                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
   517             }
   518 
   519 
   520             // write log file
   521             val heap_stamp =
   522               if (process_result.ok) {
   523                 val heap_stamp =
   524                   for (path <- job.output_path if path.is_file)
   525                     yield Sessions.write_heap_digest(path)
   526 
   527                 File.write_gzip(store.output_log_gz(name), terminate_lines(log_lines))
   528 
   529                 heap_stamp
   530               }
   531               else {
   532                 File.write(store.output_log(name), terminate_lines(log_lines))
   533 
   534                 None
   535               }
   536 
   537             // write database
   538             {
   539               val build_log =
   540                 Build_Log.Log_File(name, process_result.out_lines).
   541                   parse_session_info(
   542                     command_timings = true,
   543                     theory_timings = true,
   544                     ml_statistics = true,
   545                     task_statistics = true)
   546 
   547               using(SQLite.open_database(store.output_database(name)))(db =>
   548                 store.write_session_info(db, name,
   549                   build_log =
   550                     if (process_result.timeout) build_log.error("Timeout") else build_log,
   551                   build =
   552                     Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
   553                       process_result.rc)))
   554             }
   555 
   556             // messages
   557             process_result.err_lines.foreach(progress.echo(_))
   558 
   559             if (process_result.ok)
   560               progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
   561             else {
   562               progress.echo(name + " FAILED")
   563               if (!process_result.interrupted) progress.echo(process_result_tail.out)
   564             }
   565 
   566             loop(pending - name, running - name,
   567               results + (name -> Result(false, heap_stamp, Some(process_result_tail), job.info)))
   568             //}}}
   569           case None if running.size < (max_jobs max 1) =>
   570             //{{{ check/start next job
   571             pending.dequeue(running.isDefinedAt(_)) match {
   572               case Some((name, info)) =>
   573                 val ancestor_results =
   574                   selected_sessions.build_requirements(List(name)).filterNot(_ == name).
   575                     map(results(_))
   576                 val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
   577 
   578                 val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
   579 
   580                 val (current, heap_stamp) =
   581                 {
   582                   store.find_database_heap(name) match {
   583                     case Some((database, heap_stamp)) =>
   584                       using(SQLite.open_database(database))(store.read_build(_, name)) match {
   585                         case Some(build) =>
   586                           val current =
   587                             !fresh_build &&
   588                             build.ok &&
   589                             build.sources == sources_stamp(deps, name) &&
   590                             build.input_heaps == ancestor_heaps &&
   591                             build.output_heap == heap_stamp &&
   592                             !(do_output && heap_stamp.isEmpty)
   593                           (current, heap_stamp)
   594                         case None => (false, None)
   595                       }
   596                     case None => (false, None)
   597                   }
   598                 }
   599                 val all_current = current && ancestor_results.forall(_.current)
   600 
   601                 if (all_current)
   602                   loop(pending - name, running,
   603                     results + (name -> Result(true, heap_stamp, Some(Process_Result(0)), info)))
   604                 else if (no_build) {
   605                   if (verbose) progress.echo("Skipping " + name + " ...")
   606                   loop(pending - name, running,
   607                     results + (name -> Result(false, heap_stamp, Some(Process_Result(1)), info)))
   608                 }
   609                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
   610                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   611 
   612                   cleanup(name)
   613                   using(SQLite.open_database(store.output_database(name)))(db =>
   614                     store.init_session_info(db, name))
   615 
   616                   val numa_node = numa_nodes.next(used_node(_))
   617                   val job =
   618                     new Job(progress, name, info, selected_sessions, deps, store, do_output,
   619                       verbose, pide, numa_node, queue.command_timings(name))
   620                   loop(pending, running + (name -> (ancestor_heaps, job)), results)
   621                 }
   622                 else {
   623                   progress.echo(name + " CANCELLED")
   624                   loop(pending - name, running,
   625                     results + (name -> Result(false, heap_stamp, None, info)))
   626                 }
   627               case None => sleep(); loop(pending, running, results)
   628             }
   629             ///}}}
   630           case None => sleep(); loop(pending, running, results)
   631         }
   632       }
   633     }
   634 
   635 
   636     /* build results */
   637 
   638     val results0 =
   639       if (deps.is_empty) {
   640         progress.echo_warning("Nothing to build")
   641         Map.empty[String, Result]
   642       }
   643       else loop(queue, Map.empty, Map.empty)
   644 
   645     val results =
   646       new Results(
   647         (for ((name, result) <- results0.iterator)
   648           yield (name, (result.process, result.info))).toMap)
   649 
   650     if (results.rc != 0 && (verbose || !no_build)) {
   651       val unfinished =
   652         (for {
   653           name <- results.sessions.iterator
   654           if !results(name).ok
   655          } yield name).toList.sorted
   656       progress.echo("Unfinished session(s): " + commas(unfinished))
   657     }
   658 
   659 
   660     /* global browser info */
   661 
   662     if (!no_build) {
   663       val browser_chapters =
   664         (for {
   665           (name, result) <- results0.iterator
   666           if result.ok
   667           info = full_sessions(name)
   668           if info.options.bool("browser_info")
   669         } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
   670             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
   671 
   672       for ((chapter, entries) <- browser_chapters)
   673         Present.update_chapter_index(store.browser_info, chapter, entries)
   674 
   675       if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info)
   676     }
   677 
   678     results
   679   }
   680 
   681 
   682   /* Isabelle tool wrapper */
   683 
   684   val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
   685   {
   686     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
   687 
   688     var base_sessions: List[String] = Nil
   689     var select_dirs: List[Path] = Nil
   690     var numa_shuffling = false
   691     var pide = false
   692     var requirements = false
   693     var soft_build = false
   694     var exclude_session_groups: List[String] = Nil
   695     var all_sessions = false
   696     var build_heap = false
   697     var clean_build = false
   698     var dirs: List[Path] = Nil
   699     var fresh_build = false
   700     var session_groups: List[String] = Nil
   701     var max_jobs = 1
   702     var check_keywords: Set[String] = Set.empty
   703     var list_files = false
   704     var no_build = false
   705     var options = Options.init(opts = build_options)
   706     var system_mode = false
   707     var verbose = false
   708     var exclude_sessions: List[String] = Nil
   709 
   710     val getopts = Getopts("""
   711 Usage: isabelle build [OPTIONS] [SESSIONS ...]
   712 
   713   Options are:
   714     -B NAME      include session NAME and all descendants
   715     -D DIR       include session directory and select its sessions
   716     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
   717     -P           build via PIDE protocol
   718     -R           operate on requirements of selected sessions
   719     -S           soft build: only observe changes of sources, not heap images
   720     -X NAME      exclude sessions from group NAME and all descendants
   721     -a           select all sessions
   722     -b           build heap images
   723     -c           clean build
   724     -d DIR       include session directory
   725     -f           fresh build
   726     -g NAME      select session group NAME
   727     -j INT       maximum number of parallel jobs (default 1)
   728     -k KEYWORD   check theory sources for conflicts with proposed keywords
   729     -l           list session source files
   730     -n           no build -- test dependencies only
   731     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   732     -s           system build mode: produce output in ISABELLE_HOME
   733     -v           verbose
   734     -x NAME      exclude session NAME and all descendants
   735 
   736   Build and manage Isabelle sessions, depending on implicit settings:
   737 
   738 """ + Library.prefix_lines("  ", Build_Log.Settings.show()) + "\n",
   739       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
   740       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   741       "N" -> (_ => numa_shuffling = true),
   742       "P" -> (_ => pide = true),
   743       "R" -> (_ => requirements = true),
   744       "S" -> (_ => soft_build = true),
   745       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   746       "a" -> (_ => all_sessions = true),
   747       "b" -> (_ => build_heap = true),
   748       "c" -> (_ => clean_build = true),
   749       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   750       "f" -> (_ => fresh_build = true),
   751       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   752       "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
   753       "k:" -> (arg => check_keywords = check_keywords + arg),
   754       "l" -> (_ => list_files = true),
   755       "n" -> (_ => no_build = true),
   756       "o:" -> (arg => options = options + arg),
   757       "s" -> (_ => system_mode = true),
   758       "v" -> (_ => verbose = true),
   759       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   760 
   761     val sessions = getopts(args)
   762 
   763     val progress = new Console_Progress(verbose = verbose)
   764 
   765     val start_date = Date.now()
   766 
   767     if (verbose) {
   768       progress.echo(
   769         "Started at " + Build_Log.print_date(start_date) +
   770           " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
   771       progress.echo(Build_Log.Settings.show() + "\n")
   772     }
   773 
   774     val results =
   775       progress.interrupt_handler {
   776         build(options,
   777           progress = progress,
   778           check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
   779           build_heap = build_heap,
   780           clean_build = clean_build,
   781           dirs = dirs,
   782           select_dirs = select_dirs,
   783           numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
   784           max_jobs = max_jobs,
   785           list_files = list_files,
   786           check_keywords = check_keywords,
   787           fresh_build = fresh_build,
   788           no_build = no_build,
   789           soft_build = soft_build,
   790           system_mode = system_mode,
   791           verbose = verbose,
   792           pide = pide,
   793           requirements = requirements,
   794           all_sessions = all_sessions,
   795           base_sessions = base_sessions,
   796           exclude_session_groups = exclude_session_groups,
   797           exclude_sessions = exclude_sessions,
   798           session_groups = session_groups,
   799           sessions = sessions)
   800       }
   801     val end_date = Date.now()
   802     val elapsed_time = end_date.time - start_date.time
   803 
   804     if (verbose) {
   805       progress.echo("\nFinished at " + Build_Log.print_date(end_date))
   806     }
   807 
   808     val total_timing =
   809       (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
   810         copy(elapsed = elapsed_time)
   811     progress.echo(total_timing.message_resources)
   812 
   813     sys.exit(results.rc)
   814   })
   815 }