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