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