src/Pure/Tools/build.scala
author wenzelm
Sat Sep 08 22:09:52 2018 +0200 (14 months ago)
changeset 68953 89a12af9c330
parent 68928 835e5d45359c
child 68957 eef4e983fd9d
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Pure/Tools/build.scala
     2     Author:     Makarius
     3     Options:    :folding=explicit:
     4 
     5 Build and manage Isabelle sessions.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import scala.collection.SortedSet
    12 import scala.annotation.tailrec
    13 
    14 
    15 object Build
    16 {
    17   /** auxiliary **/
    18 
    19   /* persistent build info */
    20 
    21   sealed case class Session_Info(
    22     sources: String,
    23     input_heaps: List[String],
    24     output_heap: Option[String],
    25     return_code: Int)
    26   {
    27     def ok: Boolean = return_code == 0
    28   }
    29 
    30 
    31   /* queue with scheduling information */
    32 
    33   private object Queue
    34   {
    35     type Timings = (List[Properties.T], Double)
    36 
    37     def load_timings(progress: Progress, store: Sessions.Store, name: String): Timings =
    38     {
    39       val no_timings: Timings = (Nil, 0.0)
    40 
    41       store.access_database(name) match {
    42         case None => no_timings
    43         case Some(db) =>
    44           def ignore_error(msg: String) =
    45           {
    46             progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg))
    47             no_timings
    48           }
    49           try {
    50             val command_timings = store.read_command_timings(db, name)
    51             val session_timing =
    52               store.read_session_timing(db, name) match {
    53                 case Markup.Elapsed(t) => t
    54                 case _ => 0.0
    55               }
    56             (command_timings, session_timing)
    57           }
    58           catch {
    59             case ERROR(msg) => ignore_error(msg)
    60             case exn: java.lang.Error => ignore_error(Exn.message(exn))
    61             case _: XML.Error => ignore_error("")
    62           }
    63           finally { db.close }
    64       }
    65     }
    66 
    67     def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double])
    68       : Map[String, Double] =
    69     {
    70       val maximals = sessions_structure.build_graph.maximals.toSet
    71       def desc_timing(name: String): Double =
    72       {
    73         if (maximals.contains(name)) timing(name)
    74         else {
    75           val descendants = sessions_structure.build_descendants(List(name)).toSet
    76           val g = sessions_structure.build_graph.restrict(descendants)
    77           (0.0 :: g.maximals.flatMap(desc => {
    78             val ps = g.all_preds(List(desc))
    79             if (ps.exists(p => timing.get(p).isEmpty)) None
    80             else Some(ps.map(timing(_)).sum)
    81           })).max
    82         }
    83       }
    84       timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
    85     }
    86 
    87     def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store)
    88       : Queue =
    89     {
    90       val graph = sessions_structure.build_graph
    91       val names = graph.keys
    92 
    93       val timings = names.map(name => (name, load_timings(progress, store, name)))
    94       val command_timings =
    95         timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
    96       val session_timing =
    97         make_session_timing(sessions_structure,
    98           timings.map({ case (name, (_, t)) => (name, t) }).toMap)
    99 
   100       object Ordering extends scala.math.Ordering[String]
   101       {
   102         def compare_timing(name1: String, name2: String): Int =
   103         {
   104           val t1 = session_timing(name1)
   105           val t2 = session_timing(name2)
   106           if (t1 == 0.0 || t2 == 0.0) 0
   107           else t1 compare t2
   108         }
   109 
   110         def compare(name1: String, name2: String): Int =
   111           compare_timing(name2, name1) match {
   112             case 0 =>
   113               sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
   114                 case 0 => name1 compare name2
   115                 case ord => ord
   116               }
   117             case ord => ord
   118           }
   119       }
   120 
   121       new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
   122     }
   123   }
   124 
   125   private class Queue(
   126     graph: Graph[String, Sessions.Info],
   127     order: SortedSet[String],
   128     val command_timings: String => List[Properties.T])
   129   {
   130     def is_inner(name: String): Boolean = !graph.is_maximal(name)
   131 
   132     def is_empty: Boolean = graph.is_empty
   133 
   134     def - (name: String): Queue =
   135       new Queue(graph.del_node(name),
   136         order - name,  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
   137         command_timings)
   138 
   139     def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
   140     {
   141       val it = order.iterator.dropWhile(name =>
   142         skip(name)
   143           || !graph.defined(name)  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
   144           || !graph.is_minimal(name))
   145       if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
   146       else None
   147     }
   148   }
   149 
   150 
   151   /* PIDE protocol handler */
   152 
   153   class Handler(progress: Progress, session: Session, session_name: String)
   154     extends Session.Protocol_Handler
   155   {
   156     val result_error: Promise[String] = Future.promise
   157 
   158     override def exit() { result_error.cancel }
   159 
   160     private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
   161     {
   162       val error_message =
   163         try { Pretty.string_of(Symbol.decode_yxml(msg.text)) }
   164         catch { case ERROR(msg) => msg }
   165       result_error.fulfill(error_message)
   166       session.send_stop()
   167       true
   168     }
   169 
   170     private def loading_theory(msg: Prover.Protocol_Output): Boolean =
   171       msg.properties match {
   172         case Markup.Loading_Theory(name) =>
   173           progress.theory(session_name, name)
   174           true
   175         case _ => false
   176       }
   177 
   178     val functions =
   179       List(
   180         Markup.BUILD_SESSION_FINISHED -> build_session_finished _,
   181         Markup.LOADING_THEORY -> loading_theory _)
   182   }
   183 
   184 
   185   /* job: running prover process */
   186 
   187   private class Job(progress: Progress,
   188     name: String,
   189     val info: Sessions.Info,
   190     deps: Sessions.Deps,
   191     store: Sessions.Store,
   192     do_output: Boolean,
   193     verbose: Boolean,
   194     pide: Boolean,
   195     val numa_node: Option[Int],
   196     command_timings: List[Properties.T])
   197   {
   198     val options = NUMA.policy_options(info.options, numa_node)
   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 export_tmp_dir = Isabelle_System.tmp_dir("export")
   204     private val export_consumer =
   205       Export.consumer(store.open_database(name, output = true), cache = store.xz_cache)
   206 
   207     private val future_result: Future[Process_Result] =
   208       Future.thread("build") {
   209         val parent = info.parent.getOrElse("")
   210         val base = deps(name)
   211         val args_yxml =
   212           YXML.string_of_body(
   213             {
   214               import XML.Encode._
   215               pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
   216                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
   217                 pair(string, pair(string, pair(string, pair(Path.encode,
   218                 pair(list(pair(Options.encode, list(pair(string, properties)))),
   219                 pair(list(pair(string, properties)), pair(list(string),
   220                 pair(list(pair(string, string)),
   221                 pair(list(string), pair(list(pair(string, string)), list(string))))))))))))))))))(
   222               (Symbol.codes, (command_timings, (do_output, (verbose,
   223                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
   224                 (parent, (info.chapter, (name, (Path.current,
   225                 (info.theories, (base.known.sessions.toList, (base.doc_names,
   226                 (base.global_theories.toList, (base.loaded_theories.keys, (base.dest_known_theories,
   227                 info.bibtex_entries.map(_.info)))))))))))))))))))
   228             })
   229 
   230         val env =
   231           Isabelle_System.settings() +
   232             ("ISABELLE_EXPORT_TMP" -> File.standard_path(export_tmp_dir)) +
   233             ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
   234 
   235         def save_heap: String =
   236           (if (info.theories.isEmpty) "" else "ML_Heap.share_common_data (); ") +
   237             "ML_Heap.save_child " +
   238             ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(name)))
   239 
   240         if (pide && !Sessions.is_pure(name)) {
   241           val resources = new Resources(deps(parent))
   242           val session = new Session(options, resources)
   243           val handler = new Handler(progress, session, name)
   244           session.init_protocol_handler(handler)
   245 
   246           val session_result = Future.promise[Process_Result]
   247 
   248           Isabelle_Process.start(session, options, logic = parent, cwd = info.dir.file, env = env,
   249             sessions_structure = Some(deps.sessions_structure), store = Some(store),
   250             phase_changed =
   251             {
   252               case Session.Ready => session.protocol_command("build_session", args_yxml)
   253               case Session.Terminated(result) => session_result.fulfill(result)
   254               case _ =>
   255             })
   256 
   257           val result = session_result.join
   258           handler.result_error.join match {
   259             case "" => result
   260             case msg =>
   261               result.copy(
   262                 rc = result.rc max 1,
   263                 out_lines = result.out_lines ::: split_lines(Output.error_message_text(msg)))
   264           }
   265         }
   266         else {
   267           val args_file = Isabelle_System.tmp_file("build")
   268           File.write(args_file, args_yxml)
   269 
   270           val eval =
   271             "Command_Line.tool0 (fn () => (" +
   272             "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) +
   273             (if (Sessions.is_pure(name)) "; Theory.install_pure (Thy_Info.get_theory Context.PureN)"
   274              else "") + (if (do_output) "; " + save_heap else "") + "));"
   275 
   276           val process =
   277             if (Sessions.is_pure(name)) {
   278               ML_Process(options, raw_ml_system = true, cwd = info.dir.file,
   279                 args =
   280                   (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
   281                   List("--eval", eval),
   282                 env = env, sessions_structure = Some(deps.sessions_structure), store = Some(store),
   283                 cleanup = () => args_file.delete)
   284             }
   285             else {
   286               ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
   287                 env = env, sessions_structure = Some(deps.sessions_structure), store = Some(store),
   288                 cleanup = () => args_file.delete)
   289             }
   290 
   291           process.result(
   292             progress_stdout = (line: String) =>
   293               Library.try_unprefix("\floading_theory = ", line) match {
   294                 case Some(theory) => progress.theory(name, theory)
   295                 case None =>
   296                   for {
   297                     text <- Library.try_unprefix("\fexport = ", line)
   298                     (args, path) <-
   299                       Markup.Export.dest_inline(XML.Decode.properties(YXML.parse_body(text)))
   300                   } {
   301                     val body = Bytes.read(path)
   302                     path.file.delete
   303                     export_consumer(name, args, body)
   304                   }
   305               },
   306             progress_limit =
   307               options.int("process_output_limit") match {
   308                 case 0 => None
   309                 case m => Some(m * 1000000L)
   310               },
   311             strict = false)
   312         }
   313       }
   314 
   315     def terminate: Unit = future_result.cancel
   316     def is_finished: Boolean = future_result.is_finished
   317 
   318     private val timeout_request: Option[Event_Timer.Request] =
   319     {
   320       if (info.timeout > Time.zero)
   321         Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
   322       else None
   323     }
   324 
   325     def join: (Process_Result, Option[String]) =
   326     {
   327       val result0 = future_result.join
   328       val result1 =
   329         export_consumer.shutdown(close = true).map(Output.error_message_text(_)) match {
   330           case Nil => result0
   331           case errs => result0.errors(errs).error_rc
   332         }
   333 
   334       Isabelle_System.rm_tree(export_tmp_dir)
   335 
   336       if (result1.ok) {
   337         for ((dir, pats) <- info.export_files) {
   338           Export.export_files(store, name, info.dir + dir,
   339             progress = if (verbose) progress else No_Progress,
   340             export_patterns = pats,
   341             export_prefix = name + ": ")
   342         }
   343         Present.finish(progress, store.browser_info, graph_file, info, name)
   344       }
   345 
   346       graph_file.delete
   347 
   348       val was_timeout =
   349         timeout_request match {
   350           case None => false
   351           case Some(request) => !request.cancel
   352         }
   353 
   354       val result2 =
   355         if (result1.interrupted) {
   356           if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout
   357           else result1.error(Output.error_message_text("Interrupt"))
   358         }
   359         else result1
   360 
   361       val heap_digest =
   362         if (result2.ok && do_output && store.output_heap(name).is_file)
   363           Some(Sessions.write_heap_digest(store.output_heap(name)))
   364         else None
   365 
   366       (result2, heap_digest)
   367     }
   368   }
   369 
   370 
   371 
   372   /** build with results **/
   373 
   374   class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)])
   375   {
   376     def sessions: Set[String] = results.keySet
   377     def cancelled(name: String): Boolean = results(name)._1.isEmpty
   378     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
   379     def info(name: String): Sessions.Info = results(name)._2
   380     val rc =
   381       (0 /: results.iterator.map(
   382         { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
   383     def ok: Boolean = rc == 0
   384 
   385     override def toString: String = rc.toString
   386   }
   387 
   388   def build(
   389     options: Options,
   390     progress: Progress = No_Progress,
   391     check_unknown_files: Boolean = false,
   392     build_heap: Boolean = false,
   393     clean_build: Boolean = false,
   394     dirs: List[Path] = Nil,
   395     select_dirs: List[Path] = Nil,
   396     infos: List[Sessions.Info] = Nil,
   397     numa_shuffling: Boolean = false,
   398     max_jobs: Int = 1,
   399     list_files: Boolean = false,
   400     check_keywords: Set[String] = Set.empty,
   401     fresh_build: Boolean = false,
   402     no_build: Boolean = false,
   403     soft_build: Boolean = false,
   404     system_mode: Boolean = false,
   405     verbose: Boolean = false,
   406     pide: Boolean = false,
   407     requirements: Boolean = false,
   408     all_sessions: Boolean = false,
   409     base_sessions: List[String] = Nil,
   410     exclude_session_groups: List[String] = Nil,
   411     exclude_sessions: List[String] = Nil,
   412     session_groups: List[String] = Nil,
   413     sessions: List[String] = Nil,
   414     selection: Sessions.Selection = Sessions.Selection.empty): Results =
   415   {
   416     val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
   417 
   418     val store = Sessions.store(build_options, system_mode)
   419 
   420 
   421     /* session selection and dependencies */
   422 
   423     val full_sessions =
   424       Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
   425 
   426     def sources_stamp(deps: Sessions.Deps, name: String): String =
   427     {
   428       val digests =
   429         full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name)
   430       SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
   431     }
   432 
   433     val selection1 =
   434       Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
   435         exclude_sessions, session_groups, sessions) ++ selection
   436 
   437     val deps =
   438     {
   439       val deps0 =
   440         Sessions.deps(full_sessions.selection(selection1), full_sessions.global_theories,
   441           progress = progress, inlined_files = true, verbose = verbose,
   442           list_files = list_files, check_keywords = check_keywords).check_errors
   443 
   444       if (soft_build && !fresh_build) {
   445         val outdated =
   446           deps0.sessions_structure.build_topological_order.flatMap(name =>
   447             store.access_database(name) match {
   448               case Some(db) =>
   449                 using(db)(store.read_build(_, name)) match {
   450                   case Some(build)
   451                   if build.ok && build.sources == sources_stamp(deps0, name) => None
   452                   case _ => Some(name)
   453                 }
   454               case None => Some(name)
   455             })
   456 
   457         Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)),
   458           full_sessions.global_theories, progress = progress, inlined_files = true).check_errors
   459       }
   460       else deps0
   461     }
   462 
   463 
   464     /* check unknown files */
   465 
   466     if (check_unknown_files) {
   467       val source_files =
   468         (for {
   469           (_, base) <- deps.session_bases.iterator
   470           (path, _) <- base.sources.iterator
   471         } yield path).toList
   472       val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
   473       val unknown_files =
   474         Mercurial.check_files(source_files)._2.
   475           filterNot(path => exclude_files.contains(path.canonical_file))
   476       if (unknown_files.nonEmpty) {
   477         progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
   478           unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
   479       }
   480     }
   481 
   482 
   483     /* main build process */
   484 
   485     val queue = Queue(progress, deps.sessions_structure, store)
   486 
   487     store.prepare_output_dir()
   488 
   489     if (clean_build) {
   490       for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection1))) {
   491         val (relevant, ok) = store.clean_output(name)
   492         if (relevant) {
   493           if (ok) progress.echo("Cleaned " + name)
   494           else progress.echo(name + " FAILED to clean")
   495         }
   496       }
   497     }
   498 
   499     // scheduler loop
   500     case class Result(
   501       current: Boolean,
   502       heap_digest: Option[String],
   503       process: Option[Process_Result],
   504       info: Sessions.Info)
   505     {
   506       def ok: Boolean =
   507         process match {
   508           case None => false
   509           case Some(res) => res.rc == 0
   510         }
   511     }
   512 
   513     def sleep()
   514     {
   515       try { Thread.sleep(500) }
   516       catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
   517     }
   518 
   519     val numa_nodes = new NUMA.Nodes(numa_shuffling)
   520 
   521     @tailrec def loop(
   522       pending: Queue,
   523       running: Map[String, (List[String], Job)],
   524       results: Map[String, Result]): Map[String, Result] =
   525     {
   526       def used_node(i: Int): Boolean =
   527         running.iterator.exists(
   528           { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
   529 
   530       if (pending.is_empty) results
   531       else {
   532         if (progress.stopped)
   533           for ((_, (_, job)) <- running) job.terminate
   534 
   535         running.find({ case (_, (_, job)) => job.is_finished }) match {
   536           case Some((name, (input_heaps, job))) =>
   537             //{{{ finish job
   538 
   539             val (process_result, heap_digest) = job.join
   540 
   541             val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
   542             val process_result_tail =
   543             {
   544               val tail = job.info.options.int("process_output_tail")
   545               process_result.copy(
   546                 out_lines =
   547                   "(see also " + store.output_log(name).file.toString + ")" ::
   548                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
   549             }
   550 
   551 
   552             // write log file
   553             if (process_result.ok) {
   554               File.write_gzip(store.output_log_gz(name), terminate_lines(log_lines))
   555             }
   556             else File.write(store.output_log(name), terminate_lines(log_lines))
   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(store.open_database(name, output = true))(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_digest,
   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_digest, 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                   deps.sessions_structure.build_requirements(List(name)).filterNot(_ == name).
   596                     map(results(_))
   597                 val ancestor_heaps = ancestor_results.flatMap(_.heap_digest)
   598 
   599                 val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
   600 
   601                 val (current, heap_digest) =
   602                 {
   603                   store.access_database(name) match {
   604                     case Some(db) =>
   605                       using(db)(store.read_build(_, name)) match {
   606                         case Some(build) =>
   607                           val heap_digest = store.find_heap_digest(name)
   608                           val current =
   609                             !fresh_build &&
   610                             build.ok &&
   611                             build.sources == sources_stamp(deps, name) &&
   612                             build.input_heaps == ancestor_heaps &&
   613                             build.output_heap == heap_digest &&
   614                             !(do_output && heap_digest.isEmpty)
   615                           (current, heap_digest)
   616                         case None => (false, None)
   617                       }
   618                     case None => (false, None)
   619                   }
   620                 }
   621                 val all_current = current && ancestor_results.forall(_.current)
   622 
   623                 if (all_current)
   624                   loop(pending - name, running,
   625                     results + (name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
   626                 else if (no_build) {
   627                   if (verbose) progress.echo("Skipping " + name + " ...")
   628                   loop(pending - name, running,
   629                     results + (name -> Result(false, heap_digest, Some(Process_Result(1)), info)))
   630                 }
   631                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
   632                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   633 
   634                   store.clean_output(name)
   635                   using(store.open_database(name, output = true))(store.init_session_info(_, name))
   636 
   637                   val numa_node = numa_nodes.next(used_node(_))
   638                   val job =
   639                     new Job(progress, name, info, 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_digest, 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 
   837 
   838   /* build logic image */
   839 
   840   def build_logic(options: Options, logic: String,
   841     progress: Progress = No_Progress,
   842     build_heap: Boolean = false,
   843     dirs: List[Path] = Nil,
   844     system_mode: Boolean = false): Int =
   845   {
   846     if (build(options, build_heap = build_heap, no_build = true, dirs = dirs,
   847         system_mode = system_mode, sessions = List(logic)).ok) 0
   848     else {
   849       progress.echo("Build started for Isabelle/" + logic + " ...")
   850       Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
   851         system_mode = system_mode, sessions = List(logic)).rc
   852     }
   853   }
   854 }