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