src/Pure/Tools/build.scala
author wenzelm
Sat May 05 22:33:35 2018 +0200 (18 months ago ago)
changeset 68090 0763d4eb3ebc
parent 68088 9e1c670301b8
child 68094 888d35a19866
permissions -rw-r--r--
protocol message for export of theory resources;
     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                   for {
   286                     text <- Library.try_unprefix("\fexport = ", line)
   287                     (args, body) <-
   288                       Markup.Export.dest_inline(XML.Decode.properties(YXML.parse_body(text)))
   289                   } { } // FIXME
   290               },
   291             progress_limit =
   292               options.int("process_output_limit") match {
   293                 case 0 => None
   294                 case m => Some(m * 1000000L)
   295               },
   296             strict = false)
   297         }
   298       }
   299 
   300     def terminate: Unit = future_result.cancel
   301     def is_finished: Boolean = future_result.is_finished
   302 
   303     private val timeout_request: Option[Event_Timer.Request] =
   304     {
   305       if (info.timeout > Time.zero)
   306         Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
   307       else None
   308     }
   309 
   310     def join: Process_Result =
   311     {
   312       val result = future_result.join
   313 
   314       if (result.ok)
   315         Present.finish(progress, store.browser_info, graph_file, info, name)
   316 
   317       graph_file.delete
   318 
   319       val was_timeout =
   320         timeout_request match {
   321           case None => false
   322           case Some(request) => !request.cancel
   323         }
   324 
   325       if (result.interrupted) {
   326         if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout
   327         else result.error(Output.error_message_text("Interrupt"))
   328       }
   329       else result
   330     }
   331   }
   332 
   333 
   334 
   335   /** build with results **/
   336 
   337   class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)])
   338   {
   339     def sessions: Set[String] = results.keySet
   340     def cancelled(name: String): Boolean = results(name)._1.isEmpty
   341     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
   342     def info(name: String): Sessions.Info = results(name)._2
   343     val rc =
   344       (0 /: results.iterator.map(
   345         { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
   346     def ok: Boolean = rc == 0
   347 
   348     override def toString: String = rc.toString
   349   }
   350 
   351   def build(
   352     options: Options,
   353     progress: Progress = No_Progress,
   354     check_unknown_files: Boolean = false,
   355     build_heap: Boolean = false,
   356     clean_build: Boolean = false,
   357     dirs: List[Path] = Nil,
   358     select_dirs: List[Path] = Nil,
   359     infos: List[Sessions.Info] = Nil,
   360     numa_shuffling: Boolean = false,
   361     max_jobs: Int = 1,
   362     list_files: Boolean = false,
   363     check_keywords: Set[String] = Set.empty,
   364     fresh_build: Boolean = false,
   365     no_build: Boolean = false,
   366     soft_build: Boolean = false,
   367     system_mode: Boolean = false,
   368     verbose: Boolean = false,
   369     pide: Boolean = false,
   370     requirements: Boolean = false,
   371     all_sessions: Boolean = false,
   372     base_sessions: List[String] = Nil,
   373     exclude_session_groups: List[String] = Nil,
   374     exclude_sessions: List[String] = Nil,
   375     session_groups: List[String] = Nil,
   376     sessions: List[String] = Nil,
   377     selection: Sessions.Selection = Sessions.Selection.empty): Results =
   378   {
   379     val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
   380 
   381     val store = Sessions.store(system_mode)
   382 
   383 
   384     /* session selection and dependencies */
   385 
   386     val full_sessions =
   387       Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
   388 
   389     def sources_stamp(deps: Sessions.Deps, name: String): String =
   390     {
   391       val digests =
   392         full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name)
   393       SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
   394     }
   395 
   396     val selection1 =
   397       Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
   398         exclude_sessions, session_groups, sessions) ++ selection
   399 
   400     val (selected_sessions, deps) =
   401     {
   402       val selected_sessions0 = full_sessions.selection(selection1)
   403       val deps0 =
   404         Sessions.deps(selected_sessions0, full_sessions.global_theories,
   405           progress = progress, inlined_files = true, verbose = verbose,
   406           list_files = list_files, check_keywords = check_keywords).check_errors
   407 
   408       if (soft_build && !fresh_build) {
   409         val outdated =
   410           selected_sessions0.build_topological_order.flatMap(name =>
   411             store.find_database(name) match {
   412               case Some(database) =>
   413                 using(SQLite.open_database(database))(store.read_build(_, name)) match {
   414                   case Some(build)
   415                   if build.ok && build.sources == sources_stamp(deps0, name) => None
   416                   case _ => Some(name)
   417                 }
   418               case None => Some(name)
   419             })
   420         val selected_sessions =
   421           full_sessions.selection(Sessions.Selection(sessions = outdated))
   422         val deps =
   423           Sessions.deps(selected_sessions, full_sessions.global_theories,
   424             progress = progress, inlined_files = true).check_errors
   425         (selected_sessions, deps)
   426       }
   427       else (selected_sessions0, deps0)
   428     }
   429 
   430 
   431     /* check unknown files */
   432 
   433     if (check_unknown_files) {
   434       val source_files =
   435         (for {
   436           (_, base) <- deps.session_bases.iterator
   437           (path, _) <- base.sources.iterator
   438         } yield path).toList
   439       val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
   440       val unknown_files =
   441         Mercurial.check_files(source_files)._2.
   442           filterNot(path => exclude_files.contains(path.canonical_file))
   443       if (unknown_files.nonEmpty) {
   444         progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
   445           unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
   446       }
   447     }
   448 
   449 
   450     /* main build process */
   451 
   452     val queue = Queue(progress, selected_sessions, store)
   453 
   454     store.prepare_output()
   455 
   456     // cleanup
   457     def cleanup(name: String, echo: Boolean = false)
   458     {
   459       val files =
   460         List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
   461           map(store.output_dir + _).filter(_.is_file)
   462       if (files.nonEmpty) progress.echo_if(echo, "Cleaning " + name + " ...")
   463       val res = files.map(p => p.file.delete)
   464       if (!res.forall(ok => ok)) progress.echo_if(echo, name + " FAILED to delete")
   465     }
   466     if (clean_build) {
   467       for (name <- full_sessions.build_descendants(full_sessions.build_selection(selection1))) {
   468         cleanup(name, echo = true)
   469       }
   470     }
   471 
   472     // scheduler loop
   473     case class Result(
   474       current: Boolean,
   475       heap_stamp: Option[String],
   476       process: Option[Process_Result],
   477       info: Sessions.Info)
   478     {
   479       def ok: Boolean =
   480         process match {
   481           case None => false
   482           case Some(res) => res.rc == 0
   483         }
   484     }
   485 
   486     def sleep()
   487     {
   488       try { Thread.sleep(500) }
   489       catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
   490     }
   491 
   492     val numa_nodes = new NUMA.Nodes(numa_shuffling)
   493 
   494     @tailrec def loop(
   495       pending: Queue,
   496       running: Map[String, (List[String], Job)],
   497       results: Map[String, Result]): Map[String, Result] =
   498     {
   499       def used_node(i: Int): Boolean =
   500         running.iterator.exists(
   501           { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
   502 
   503       if (pending.is_empty) results
   504       else {
   505         if (progress.stopped)
   506           for ((_, (_, job)) <- running) job.terminate
   507 
   508         running.find({ case (_, (_, job)) => job.is_finished }) match {
   509           case Some((name, (input_heaps, job))) =>
   510             //{{{ finish job
   511 
   512             val process_result = job.join
   513 
   514             val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
   515             val process_result_tail =
   516             {
   517               val tail = job.info.options.int("process_output_tail")
   518               process_result.copy(
   519                 out_lines =
   520                   "(see also " + store.output_log(name).file.toString + ")" ::
   521                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
   522             }
   523 
   524 
   525             // write log file
   526             val heap_stamp =
   527               if (process_result.ok) {
   528                 val heap_stamp =
   529                   for (path <- job.output_path if path.is_file)
   530                     yield Sessions.write_heap_digest(path)
   531 
   532                 File.write_gzip(store.output_log_gz(name), terminate_lines(log_lines))
   533 
   534                 heap_stamp
   535               }
   536               else {
   537                 File.write(store.output_log(name), terminate_lines(log_lines))
   538 
   539                 None
   540               }
   541 
   542             // write database
   543             {
   544               val build_log =
   545                 Build_Log.Log_File(name, process_result.out_lines).
   546                   parse_session_info(
   547                     command_timings = true,
   548                     theory_timings = true,
   549                     ml_statistics = true,
   550                     task_statistics = true)
   551 
   552               using(SQLite.open_database(store.output_database(name)))(db =>
   553                 store.write_session_info(db, name,
   554                   build_log =
   555                     if (process_result.timeout) build_log.error("Timeout") else build_log,
   556                   build =
   557                     Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
   558                       process_result.rc)))
   559             }
   560 
   561             // messages
   562             process_result.err_lines.foreach(progress.echo(_))
   563 
   564             if (process_result.ok)
   565               progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
   566             else {
   567               progress.echo(name + " FAILED")
   568               if (!process_result.interrupted) progress.echo(process_result_tail.out)
   569             }
   570 
   571             loop(pending - name, running - name,
   572               results + (name -> Result(false, heap_stamp, Some(process_result_tail), job.info)))
   573             //}}}
   574           case None if running.size < (max_jobs max 1) =>
   575             //{{{ check/start next job
   576             pending.dequeue(running.isDefinedAt(_)) match {
   577               case Some((name, info)) =>
   578                 val ancestor_results =
   579                   selected_sessions.build_requirements(List(name)).filterNot(_ == name).
   580                     map(results(_))
   581                 val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
   582 
   583                 val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
   584 
   585                 val (current, heap_stamp) =
   586                 {
   587                   store.find_database_heap(name) match {
   588                     case Some((database, heap_stamp)) =>
   589                       using(SQLite.open_database(database))(store.read_build(_, name)) match {
   590                         case Some(build) =>
   591                           val current =
   592                             !fresh_build &&
   593                             build.ok &&
   594                             build.sources == sources_stamp(deps, name) &&
   595                             build.input_heaps == ancestor_heaps &&
   596                             build.output_heap == heap_stamp &&
   597                             !(do_output && heap_stamp.isEmpty)
   598                           (current, heap_stamp)
   599                         case None => (false, None)
   600                       }
   601                     case None => (false, None)
   602                   }
   603                 }
   604                 val all_current = current && ancestor_results.forall(_.current)
   605 
   606                 if (all_current)
   607                   loop(pending - name, running,
   608                     results + (name -> Result(true, heap_stamp, Some(Process_Result(0)), info)))
   609                 else if (no_build) {
   610                   if (verbose) progress.echo("Skipping " + name + " ...")
   611                   loop(pending - name, running,
   612                     results + (name -> Result(false, heap_stamp, Some(Process_Result(1)), info)))
   613                 }
   614                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
   615                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   616 
   617                   cleanup(name)
   618                   using(SQLite.open_database(store.output_database(name)))(db =>
   619                     store.init_session_info(db, name))
   620 
   621                   val numa_node = numa_nodes.next(used_node(_))
   622                   val job =
   623                     new Job(progress, name, info, selected_sessions, deps, store, do_output,
   624                       verbose, pide, numa_node, queue.command_timings(name))
   625                   loop(pending, running + (name -> (ancestor_heaps, job)), results)
   626                 }
   627                 else {
   628                   progress.echo(name + " CANCELLED")
   629                   loop(pending - name, running,
   630                     results + (name -> Result(false, heap_stamp, None, info)))
   631                 }
   632               case None => sleep(); loop(pending, running, results)
   633             }
   634             ///}}}
   635           case None => sleep(); loop(pending, running, results)
   636         }
   637       }
   638     }
   639 
   640 
   641     /* build results */
   642 
   643     val results0 =
   644       if (deps.is_empty) {
   645         progress.echo_warning("Nothing to build")
   646         Map.empty[String, Result]
   647       }
   648       else loop(queue, Map.empty, Map.empty)
   649 
   650     val results =
   651       new Results(
   652         (for ((name, result) <- results0.iterator)
   653           yield (name, (result.process, result.info))).toMap)
   654 
   655     if (results.rc != 0 && (verbose || !no_build)) {
   656       val unfinished =
   657         (for {
   658           name <- results.sessions.iterator
   659           if !results(name).ok
   660          } yield name).toList.sorted
   661       progress.echo("Unfinished session(s): " + commas(unfinished))
   662     }
   663 
   664 
   665     /* global browser info */
   666 
   667     if (!no_build) {
   668       val browser_chapters =
   669         (for {
   670           (name, result) <- results0.iterator
   671           if result.ok
   672           info = full_sessions(name)
   673           if info.options.bool("browser_info")
   674         } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
   675             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
   676 
   677       for ((chapter, entries) <- browser_chapters)
   678         Present.update_chapter_index(store.browser_info, chapter, entries)
   679 
   680       if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info)
   681     }
   682 
   683     results
   684   }
   685 
   686 
   687   /* Isabelle tool wrapper */
   688 
   689   val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
   690   {
   691     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
   692 
   693     var base_sessions: List[String] = Nil
   694     var select_dirs: List[Path] = Nil
   695     var numa_shuffling = false
   696     var pide = false
   697     var requirements = false
   698     var soft_build = false
   699     var exclude_session_groups: List[String] = Nil
   700     var all_sessions = false
   701     var build_heap = false
   702     var clean_build = false
   703     var dirs: List[Path] = Nil
   704     var fresh_build = false
   705     var session_groups: List[String] = Nil
   706     var max_jobs = 1
   707     var check_keywords: Set[String] = Set.empty
   708     var list_files = false
   709     var no_build = false
   710     var options = Options.init(opts = build_options)
   711     var system_mode = false
   712     var verbose = false
   713     var exclude_sessions: List[String] = Nil
   714 
   715     val getopts = Getopts("""
   716 Usage: isabelle build [OPTIONS] [SESSIONS ...]
   717 
   718   Options are:
   719     -B NAME      include session NAME and all descendants
   720     -D DIR       include session directory and select its sessions
   721     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
   722     -P           build via PIDE protocol
   723     -R           operate on requirements of selected sessions
   724     -S           soft build: only observe changes of sources, not heap images
   725     -X NAME      exclude sessions from group NAME and all descendants
   726     -a           select all sessions
   727     -b           build heap images
   728     -c           clean build
   729     -d DIR       include session directory
   730     -f           fresh build
   731     -g NAME      select session group NAME
   732     -j INT       maximum number of parallel jobs (default 1)
   733     -k KEYWORD   check theory sources for conflicts with proposed keywords
   734     -l           list session source files
   735     -n           no build -- test dependencies only
   736     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   737     -s           system build mode: produce output in ISABELLE_HOME
   738     -v           verbose
   739     -x NAME      exclude session NAME and all descendants
   740 
   741   Build and manage Isabelle sessions, depending on implicit settings:
   742 
   743 """ + Library.prefix_lines("  ", Build_Log.Settings.show()) + "\n",
   744       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
   745       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   746       "N" -> (_ => numa_shuffling = true),
   747       "P" -> (_ => pide = true),
   748       "R" -> (_ => requirements = true),
   749       "S" -> (_ => soft_build = true),
   750       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   751       "a" -> (_ => all_sessions = true),
   752       "b" -> (_ => build_heap = true),
   753       "c" -> (_ => clean_build = true),
   754       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   755       "f" -> (_ => fresh_build = true),
   756       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   757       "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
   758       "k:" -> (arg => check_keywords = check_keywords + arg),
   759       "l" -> (_ => list_files = true),
   760       "n" -> (_ => no_build = true),
   761       "o:" -> (arg => options = options + arg),
   762       "s" -> (_ => system_mode = true),
   763       "v" -> (_ => verbose = true),
   764       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   765 
   766     val sessions = getopts(args)
   767 
   768     val progress = new Console_Progress(verbose = verbose)
   769 
   770     val start_date = Date.now()
   771 
   772     if (verbose) {
   773       progress.echo(
   774         "Started at " + Build_Log.print_date(start_date) +
   775           " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
   776       progress.echo(Build_Log.Settings.show() + "\n")
   777     }
   778 
   779     val results =
   780       progress.interrupt_handler {
   781         build(options,
   782           progress = progress,
   783           check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
   784           build_heap = build_heap,
   785           clean_build = clean_build,
   786           dirs = dirs,
   787           select_dirs = select_dirs,
   788           numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
   789           max_jobs = max_jobs,
   790           list_files = list_files,
   791           check_keywords = check_keywords,
   792           fresh_build = fresh_build,
   793           no_build = no_build,
   794           soft_build = soft_build,
   795           system_mode = system_mode,
   796           verbose = verbose,
   797           pide = pide,
   798           requirements = requirements,
   799           all_sessions = all_sessions,
   800           base_sessions = base_sessions,
   801           exclude_session_groups = exclude_session_groups,
   802           exclude_sessions = exclude_sessions,
   803           session_groups = session_groups,
   804           sessions = sessions)
   805       }
   806     val end_date = Date.now()
   807     val elapsed_time = end_date.time - start_date.time
   808 
   809     if (verbose) {
   810       progress.echo("\nFinished at " + Build_Log.print_date(end_date))
   811     }
   812 
   813     val total_timing =
   814       (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
   815         copy(elapsed = elapsed_time)
   816     progress.echo(total_timing.message_resources)
   817 
   818     sys.exit(results.rc)
   819   })
   820 }