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