src/Pure/Tools/build.scala
author wenzelm
Sat May 19 16:13:39 2018 +0200 (17 months ago)
changeset 68220 8fc4e3d1df86
parent 68219 c0341c0080e2
child 68221 dbef88c2b6c5
permissions -rw-r--r--
clarified store.clean_output: cleanup user_output_dir even in system_mode;
     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     if (clean_build) {
   471       for (name <- full_sessions.build_descendants(full_sessions.build_selection(selection1))) {
   472         val (relevant, ok) = store.clean_output(name)
   473         if (relevant) {
   474           if (ok) progress.echo("Cleaned " + name)
   475           else progress.echo(name + " FAILED to clean")
   476         }
   477       }
   478     }
   479 
   480     // scheduler loop
   481     case class Result(
   482       current: Boolean,
   483       heap_digest: Option[String],
   484       process: Option[Process_Result],
   485       info: Sessions.Info)
   486     {
   487       def ok: Boolean =
   488         process match {
   489           case None => false
   490           case Some(res) => res.rc == 0
   491         }
   492     }
   493 
   494     def sleep()
   495     {
   496       try { Thread.sleep(500) }
   497       catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
   498     }
   499 
   500     val numa_nodes = new NUMA.Nodes(numa_shuffling)
   501 
   502     @tailrec def loop(
   503       pending: Queue,
   504       running: Map[String, (List[String], Job)],
   505       results: Map[String, Result]): Map[String, Result] =
   506     {
   507       def used_node(i: Int): Boolean =
   508         running.iterator.exists(
   509           { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
   510 
   511       if (pending.is_empty) results
   512       else {
   513         if (progress.stopped)
   514           for ((_, (_, job)) <- running) job.terminate
   515 
   516         running.find({ case (_, (_, job)) => job.is_finished }) match {
   517           case Some((name, (input_heaps, job))) =>
   518             //{{{ finish job
   519 
   520             val (process_result, heap_digest) = job.join
   521 
   522             val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
   523             val process_result_tail =
   524             {
   525               val tail = job.info.options.int("process_output_tail")
   526               process_result.copy(
   527                 out_lines =
   528                   "(see also " + store.output_log(name).file.toString + ")" ::
   529                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
   530             }
   531 
   532 
   533             // write log file
   534             if (process_result.ok) {
   535               File.write_gzip(store.output_log_gz(name), terminate_lines(log_lines))
   536             }
   537             else File.write(store.output_log(name), terminate_lines(log_lines))
   538 
   539             // write database
   540             {
   541               val build_log =
   542                 Build_Log.Log_File(name, process_result.out_lines).
   543                   parse_session_info(
   544                     command_timings = true,
   545                     theory_timings = true,
   546                     ml_statistics = true,
   547                     task_statistics = true)
   548 
   549               using(store.open_output_database(name))(db =>
   550                 store.write_session_info(db, name,
   551                   build_log =
   552                     if (process_result.timeout) build_log.error("Timeout") else build_log,
   553                   build =
   554                     Session_Info(sources_stamp(deps, name), input_heaps, heap_digest,
   555                       process_result.rc)))
   556             }
   557 
   558             // messages
   559             process_result.err_lines.foreach(progress.echo(_))
   560 
   561             if (process_result.ok)
   562               progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
   563             else {
   564               progress.echo(name + " FAILED")
   565               if (!process_result.interrupted) progress.echo(process_result_tail.out)
   566             }
   567 
   568             loop(pending - name, running - name,
   569               results + (name -> Result(false, heap_digest, Some(process_result_tail), job.info)))
   570             //}}}
   571           case None if running.size < (max_jobs max 1) =>
   572             //{{{ check/start next job
   573             pending.dequeue(running.isDefinedAt(_)) match {
   574               case Some((name, info)) =>
   575                 val ancestor_results =
   576                   deps.sessions_structure.build_requirements(List(name)).filterNot(_ == name).
   577                     map(results(_))
   578                 val ancestor_heaps = ancestor_results.flatMap(_.heap_digest)
   579 
   580                 val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
   581 
   582                 val (current, heap_digest) =
   583                 {
   584                   store.try_open_database(name) match {
   585                     case Some(db) =>
   586                       using(db)(store.read_build(_, name)) match {
   587                         case Some(build) =>
   588                           val heap_digest = store.find_heap_digest(name)
   589                           val current =
   590                             !fresh_build &&
   591                             build.ok &&
   592                             build.sources == sources_stamp(deps, name) &&
   593                             build.input_heaps == ancestor_heaps &&
   594                             build.output_heap == heap_digest &&
   595                             !(do_output && heap_digest.isEmpty)
   596                           (current, heap_digest)
   597                         case None => (false, None)
   598                       }
   599                     case None => (false, None)
   600                   }
   601                 }
   602                 val all_current = current && ancestor_results.forall(_.current)
   603 
   604                 if (all_current)
   605                   loop(pending - name, running,
   606                     results + (name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
   607                 else if (no_build) {
   608                   if (verbose) progress.echo("Skipping " + name + " ...")
   609                   loop(pending - name, running,
   610                     results + (name -> Result(false, heap_digest, Some(Process_Result(1)), info)))
   611                 }
   612                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
   613                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   614 
   615                   store.clean_output(name)
   616                   using(store.open_output_database(name))(store.init_session_info(_, name))
   617 
   618                   val numa_node = numa_nodes.next(used_node(_))
   619                   val job =
   620                     new Job(progress, name, info, deps, store, do_output,
   621                       verbose, pide, numa_node, queue.command_timings(name))
   622                   loop(pending, running + (name -> (ancestor_heaps, job)), results)
   623                 }
   624                 else {
   625                   progress.echo(name + " CANCELLED")
   626                   loop(pending - name, running,
   627                     results + (name -> Result(false, heap_digest, None, info)))
   628                 }
   629               case None => sleep(); loop(pending, running, results)
   630             }
   631             ///}}}
   632           case None => sleep(); loop(pending, running, results)
   633         }
   634       }
   635     }
   636 
   637 
   638     /* build results */
   639 
   640     val results0 =
   641       if (deps.is_empty) {
   642         progress.echo_warning("Nothing to build")
   643         Map.empty[String, Result]
   644       }
   645       else loop(queue, Map.empty, Map.empty)
   646 
   647     val results =
   648       new Results(
   649         (for ((name, result) <- results0.iterator)
   650           yield (name, (result.process, result.info))).toMap)
   651 
   652     if (results.rc != 0 && (verbose || !no_build)) {
   653       val unfinished =
   654         (for {
   655           name <- results.sessions.iterator
   656           if !results(name).ok
   657          } yield name).toList.sorted
   658       progress.echo("Unfinished session(s): " + commas(unfinished))
   659     }
   660 
   661 
   662     /* global browser info */
   663 
   664     if (!no_build) {
   665       val browser_chapters =
   666         (for {
   667           (name, result) <- results0.iterator
   668           if result.ok
   669           info = full_sessions(name)
   670           if info.options.bool("browser_info")
   671         } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
   672             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
   673 
   674       for ((chapter, entries) <- browser_chapters)
   675         Present.update_chapter_index(store.browser_info, chapter, entries)
   676 
   677       if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info)
   678     }
   679 
   680     results
   681   }
   682 
   683 
   684   /* Isabelle tool wrapper */
   685 
   686   val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
   687   {
   688     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
   689 
   690     var base_sessions: List[String] = Nil
   691     var select_dirs: List[Path] = Nil
   692     var numa_shuffling = false
   693     var pide = false
   694     var requirements = false
   695     var soft_build = false
   696     var exclude_session_groups: List[String] = Nil
   697     var all_sessions = false
   698     var build_heap = false
   699     var clean_build = false
   700     var dirs: List[Path] = Nil
   701     var fresh_build = false
   702     var session_groups: List[String] = Nil
   703     var max_jobs = 1
   704     var check_keywords: Set[String] = Set.empty
   705     var list_files = false
   706     var no_build = false
   707     var options = Options.init(opts = build_options)
   708     var system_mode = false
   709     var verbose = false
   710     var exclude_sessions: List[String] = Nil
   711 
   712     val getopts = Getopts("""
   713 Usage: isabelle build [OPTIONS] [SESSIONS ...]
   714 
   715   Options are:
   716     -B NAME      include session NAME and all descendants
   717     -D DIR       include session directory and select its sessions
   718     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
   719     -P           build via PIDE protocol
   720     -R           operate on requirements of selected sessions
   721     -S           soft build: only observe changes of sources, not heap images
   722     -X NAME      exclude sessions from group NAME and all descendants
   723     -a           select all sessions
   724     -b           build heap images
   725     -c           clean build
   726     -d DIR       include session directory
   727     -f           fresh build
   728     -g NAME      select session group NAME
   729     -j INT       maximum number of parallel jobs (default 1)
   730     -k KEYWORD   check theory sources for conflicts with proposed keywords
   731     -l           list session source files
   732     -n           no build -- test dependencies only
   733     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   734     -s           system build mode: produce output in ISABELLE_HOME
   735     -v           verbose
   736     -x NAME      exclude session NAME and all descendants
   737 
   738   Build and manage Isabelle sessions, depending on implicit settings:
   739 
   740 """ + Library.prefix_lines("  ", Build_Log.Settings.show()) + "\n",
   741       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
   742       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   743       "N" -> (_ => numa_shuffling = true),
   744       "P" -> (_ => pide = true),
   745       "R" -> (_ => requirements = true),
   746       "S" -> (_ => soft_build = true),
   747       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   748       "a" -> (_ => all_sessions = true),
   749       "b" -> (_ => build_heap = true),
   750       "c" -> (_ => clean_build = true),
   751       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   752       "f" -> (_ => fresh_build = true),
   753       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   754       "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
   755       "k:" -> (arg => check_keywords = check_keywords + arg),
   756       "l" -> (_ => list_files = true),
   757       "n" -> (_ => no_build = true),
   758       "o:" -> (arg => options = options + arg),
   759       "s" -> (_ => system_mode = true),
   760       "v" -> (_ => verbose = true),
   761       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   762 
   763     val sessions = getopts(args)
   764 
   765     val progress = new Console_Progress(verbose = verbose)
   766 
   767     val start_date = Date.now()
   768 
   769     if (verbose) {
   770       progress.echo(
   771         "Started at " + Build_Log.print_date(start_date) +
   772           " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
   773       progress.echo(Build_Log.Settings.show() + "\n")
   774     }
   775 
   776     val results =
   777       progress.interrupt_handler {
   778         build(options,
   779           progress = progress,
   780           check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
   781           build_heap = build_heap,
   782           clean_build = clean_build,
   783           dirs = dirs,
   784           select_dirs = select_dirs,
   785           numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
   786           max_jobs = max_jobs,
   787           list_files = list_files,
   788           check_keywords = check_keywords,
   789           fresh_build = fresh_build,
   790           no_build = no_build,
   791           soft_build = soft_build,
   792           system_mode = system_mode,
   793           verbose = verbose,
   794           pide = pide,
   795           requirements = requirements,
   796           all_sessions = all_sessions,
   797           base_sessions = base_sessions,
   798           exclude_session_groups = exclude_session_groups,
   799           exclude_sessions = exclude_sessions,
   800           session_groups = session_groups,
   801           sessions = sessions)
   802       }
   803     val end_date = Date.now()
   804     val elapsed_time = end_date.time - start_date.time
   805 
   806     if (verbose) {
   807       progress.echo("\nFinished at " + Build_Log.print_date(end_date))
   808     }
   809 
   810     val total_timing =
   811       (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
   812         copy(elapsed = elapsed_time)
   813     progress.echo(total_timing.message_resources)
   814 
   815     sys.exit(results.rc)
   816   })
   817 }