src/Pure/Tools/build.scala
author wenzelm
Fri Dec 29 17:40:57 2017 +0100 (16 months ago)
changeset 67297 86a099f896fc
parent 67219 81e9804b2014
child 67380 8bef51521f21
permissions -rw-r--r--
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
     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 java.io.{BufferedInputStream, FileInputStream,
    12   BufferedReader, InputStreamReader, IOException}
    13 import java.util.zip.GZIPInputStream
    14 
    15 import scala.collection.SortedSet
    16 import scala.collection.mutable
    17 import scala.annotation.tailrec
    18 
    19 
    20 object Build
    21 {
    22   /** auxiliary **/
    23 
    24   /* persistent build info */
    25 
    26   sealed case class Session_Info(
    27     sources: String,
    28     input_heaps: List[String],
    29     output_heap: Option[String],
    30     return_code: Int)
    31   {
    32     def ok: Boolean = return_code == 0
    33   }
    34 
    35 
    36   /* queue with scheduling information */
    37 
    38   private object Queue
    39   {
    40     def load_timings(progress: Progress, store: Sessions.Store, name: String)
    41       : (List[Properties.T], Double) =
    42     {
    43       val no_timings: (List[Properties.T], Double) = (Nil, 0.0)
    44 
    45       store.find_database(name) match {
    46         case None => no_timings
    47         case Some(database) =>
    48           def ignore_error(msg: String) =
    49           {
    50             progress.echo_warning("Ignoring bad database: " +
    51               database.expand + (if (msg == "") "" else "\n" + msg))
    52             no_timings
    53           }
    54           try {
    55             using(SQLite.open_database(database))(db =>
    56             {
    57               val command_timings = store.read_command_timings(db, name)
    58               val session_timing =
    59                 store.read_session_timing(db, name) match {
    60                   case Markup.Elapsed(t) => t
    61                   case _ => 0.0
    62                 }
    63               (command_timings, session_timing)
    64             })
    65           }
    66           catch {
    67             case ERROR(msg) => ignore_error(msg)
    68             case exn: java.lang.Error => ignore_error(Exn.message(exn))
    69             case _: XML.Error => ignore_error("")
    70           }
    71       }
    72     }
    73 
    74     def apply(progress: Progress, sessions: Sessions.Structure, store: Sessions.Store): Queue =
    75     {
    76       val graph = sessions.build_graph
    77       val names = graph.keys
    78 
    79       val timings = names.map(name => (name, load_timings(progress, store, name)))
    80       val command_timings =
    81         Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
    82       val session_timing =
    83         Map(timings.map({ case (name, (_, t)) => (name, t) }): _*).withDefaultValue(0.0)
    84 
    85       def outdegree(name: String): Int = graph.imm_succs(name).size
    86 
    87       object Ordering extends scala.math.Ordering[String]
    88       {
    89         def compare_timing(name1: String, name2: String): Int =
    90         {
    91           val t1 = session_timing(name1)
    92           val t2 = session_timing(name2)
    93           if (t1 == 0.0 || t2 == 0.0) 0
    94           else t1 compare t2
    95         }
    96 
    97         def compare(name1: String, name2: String): Int =
    98           outdegree(name2) compare outdegree(name1) match {
    99             case 0 =>
   100               compare_timing(name2, name1) match {
   101                 case 0 =>
   102                   sessions(name2).timeout compare sessions(name1).timeout match {
   103                     case 0 => name1 compare name2
   104                     case ord => ord
   105                   }
   106                 case ord => ord
   107               }
   108             case ord => ord
   109           }
   110       }
   111 
   112       new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
   113     }
   114   }
   115 
   116   private class Queue(
   117     graph: Graph[String, Sessions.Info],
   118     order: SortedSet[String],
   119     val command_timings: String => List[Properties.T])
   120   {
   121     def is_inner(name: String): Boolean = !graph.is_maximal(name)
   122 
   123     def is_empty: Boolean = graph.is_empty
   124 
   125     def - (name: String): Queue =
   126       new Queue(graph.del_node(name),
   127         order - name,  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
   128         command_timings)
   129 
   130     def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
   131     {
   132       val it = order.iterator.dropWhile(name =>
   133         skip(name)
   134           || !graph.defined(name)  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
   135           || !graph.is_minimal(name))
   136       if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
   137       else None
   138     }
   139   }
   140 
   141 
   142   /* PIDE protocol handler */
   143 
   144   class Handler(progress: Progress, session: Session, session_name: String)
   145     extends Session.Protocol_Handler
   146   {
   147     val result_error: Promise[String] = Future.promise
   148 
   149     override def exit() { result_error.cancel }
   150 
   151     private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
   152     {
   153       val error_message =
   154         try { Pretty.string_of(Symbol.decode_yxml(msg.text)) }
   155         catch { case ERROR(msg) => msg }
   156       result_error.fulfill(error_message)
   157       session.send_stop()
   158       true
   159     }
   160 
   161     private def loading_theory(msg: Prover.Protocol_Output): Boolean =
   162       msg.properties match {
   163         case Markup.Loading_Theory(name) =>
   164           progress.theory(session_name, name)
   165           true
   166         case _ => false
   167       }
   168 
   169     val functions =
   170       List(
   171         Markup.BUILD_SESSION_FINISHED -> build_session_finished _,
   172         Markup.LOADING_THEORY -> loading_theory _)
   173   }
   174 
   175 
   176   /* job: running prover process */
   177 
   178   private class Job(progress: Progress,
   179     name: String,
   180     val info: Sessions.Info,
   181     sessions: Sessions.Structure,
   182     deps: Sessions.Deps,
   183     store: Sessions.Store,
   184     do_output: Boolean,
   185     verbose: Boolean,
   186     pide: Boolean,
   187     val numa_node: Option[Int],
   188     command_timings: List[Properties.T])
   189   {
   190     val output = store.output_dir + Path.basic(name)
   191     def output_path: Option[Path] = if (do_output) Some(output) else None
   192     output.file.delete
   193 
   194     val options =
   195       numa_node match {
   196         case None => info.options
   197         case Some(n) => info.options.string("ML_process_policy") = NUMA.policy(n)
   198       }
   199 
   200     private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
   201     isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
   202 
   203     private val future_result: Future[Process_Result] =
   204       Future.thread("build") {
   205         val parent = info.parent.getOrElse("")
   206         val base = deps(name)
   207         val args_yxml =
   208           YXML.string_of_body(
   209             {
   210               import XML.Encode._
   211               pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
   212                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
   213                 pair(string, pair(string, pair(string, pair(Path.encode,
   214                 pair(list(pair(Options.encode, list(pair(string, properties)))),
   215                 pair(list(string), pair(list(pair(string, string)), pair(list(string),
   216                 pair(list(pair(string, string)), list(string)))))))))))))))))(
   217               (Symbol.codes, (command_timings, (do_output, (verbose,
   218                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
   219                 (parent, (info.chapter, (name, (Path.current,
   220                 (info.theories, (base.known.sessions.toList,
   221                 (base.global_theories.toList,
   222                 (base.loaded_theories.keys,
   223                 (base.dest_known_theories,
   224                 info.bibtex_entries.map(_.info))))))))))))))))))
   225             })
   226 
   227         val env =
   228           Isabelle_System.settings() +
   229             ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
   230 
   231         def save_heap: String =
   232           (if (info.theories.isEmpty) "" else "ML_Heap.share_common_data (); ") +
   233             "ML_Heap.save_child " + ML_Syntax.print_string_bytes(File.platform_path(output))
   234 
   235         if (pide && !Sessions.is_pure(name)) {
   236           val resources = new Resources(deps(parent))
   237           val session = new Session(options, resources)
   238           val handler = new Handler(progress, session, name)
   239           session.init_protocol_handler(handler)
   240 
   241           val session_result = Future.promise[Process_Result]
   242 
   243           Isabelle_Process.start(session, options, logic = parent,
   244             cwd = info.dir.file, env = env, sessions = Some(sessions), store = store,
   245             phase_changed =
   246             {
   247               case Session.Ready => session.protocol_command("build_session", args_yxml)
   248               case Session.Terminated(result) => session_result.fulfill(result)
   249               case _ =>
   250             })
   251 
   252           val result = session_result.join
   253           handler.result_error.join match {
   254             case "" => result
   255             case msg =>
   256               result.copy(
   257                 rc = result.rc max 1,
   258                 out_lines = result.out_lines ::: split_lines(Output.error_message_text(msg)))
   259           }
   260         }
   261         else {
   262           val args_file = Isabelle_System.tmp_file("build")
   263           File.write(args_file, args_yxml)
   264 
   265           val eval =
   266             "Command_Line.tool0 (fn () => (" +
   267             "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) +
   268             (if (do_output) "; " + save_heap else "") + "));"
   269 
   270           val process =
   271             if (Sessions.is_pure(name)) {
   272               ML_Process(options, raw_ml_system = true, cwd = info.dir.file,
   273                 args =
   274                   (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
   275                   List("--eval", eval),
   276                 env = env, sessions = Some(sessions), store = store,
   277                 cleanup = () => args_file.delete)
   278             }
   279             else {
   280               ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
   281                 env = env, sessions = Some(sessions), store = store,
   282                 cleanup = () => args_file.delete)
   283             }
   284 
   285           process.result(
   286             progress_stdout = (line: String) =>
   287               Library.try_unprefix("\floading_theory = ", line) match {
   288                 case Some(theory) => progress.theory(name, theory)
   289                 case None =>
   290               },
   291             progress_limit =
   292               options.int("process_output_limit") match {
   293                 case 0 => None
   294                 case m => Some(m * 1000000L)
   295               },
   296             strict = false)
   297         }
   298       }
   299 
   300     def terminate: Unit = future_result.cancel
   301     def is_finished: Boolean = future_result.is_finished
   302 
   303     private val timeout_request: Option[Event_Timer.Request] =
   304     {
   305       if (info.timeout > Time.zero)
   306         Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
   307       else None
   308     }
   309 
   310     def join: Process_Result =
   311     {
   312       val result = future_result.join
   313 
   314       if (result.ok)
   315         Present.finish(progress, store.browser_info, graph_file, info, name)
   316 
   317       graph_file.delete
   318 
   319       val was_timeout =
   320         timeout_request match {
   321           case None => false
   322           case Some(request) => !request.cancel
   323         }
   324 
   325       if (result.interrupted) {
   326         if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout
   327         else result.error(Output.error_message_text("Interrupt"))
   328       }
   329       else result
   330     }
   331   }
   332 
   333 
   334 
   335   /** build with results **/
   336 
   337   class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)])
   338   {
   339     def sessions: Set[String] = results.keySet
   340     def cancelled(name: String): Boolean = results(name)._1.isEmpty
   341     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
   342     def info(name: String): Sessions.Info = results(name)._2
   343     val rc =
   344       (0 /: results.iterator.map(
   345         { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
   346     def ok: Boolean = rc == 0
   347 
   348     override def toString: String = rc.toString
   349   }
   350 
   351   def build(
   352     options: Options,
   353     progress: Progress = No_Progress,
   354     check_unknown_files: Boolean = false,
   355     build_heap: Boolean = false,
   356     clean_build: Boolean = false,
   357     dirs: List[Path] = Nil,
   358     select_dirs: List[Path] = Nil,
   359     infos: List[Sessions.Info] = Nil,
   360     numa_shuffling: Boolean = false,
   361     max_jobs: Int = 1,
   362     list_files: Boolean = false,
   363     check_keywords: Set[String] = Set.empty,
   364     fresh_build: Boolean = false,
   365     no_build: Boolean = false,
   366     soft_build: Boolean = false,
   367     system_mode: Boolean = false,
   368     verbose: Boolean = false,
   369     pide: Boolean = false,
   370     requirements: Boolean = false,
   371     all_sessions: Boolean = false,
   372     base_sessions: List[String] = Nil,
   373     exclude_session_groups: List[String] = Nil,
   374     exclude_sessions: List[String] = Nil,
   375     session_groups: List[String] = Nil,
   376     sessions: List[String] = Nil,
   377     selection: Sessions.Selection = Sessions.Selection.empty): Results =
   378   {
   379     val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
   380 
   381     val store = Sessions.store(system_mode)
   382 
   383 
   384     /* session selection and dependencies */
   385 
   386     val full_sessions =
   387       Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
   388 
   389     def sources_stamp(deps: Sessions.Deps, name: String): String =
   390     {
   391       val digests =
   392         full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name)
   393       SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
   394     }
   395 
   396     val selection1 =
   397       Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
   398         exclude_sessions, session_groups, sessions) ++ selection
   399 
   400     val (selected_sessions, deps) =
   401     {
   402       val selected_sessions0 = full_sessions.selection(selection1)
   403       val deps0 =
   404         Sessions.deps(selected_sessions0, full_sessions.global_theories,
   405           progress = progress, inlined_files = true, verbose = verbose,
   406           list_files = list_files, check_keywords = check_keywords).check_errors
   407 
   408       if (soft_build && !fresh_build) {
   409         val outdated =
   410           selected_sessions0.build_topological_order.flatMap(name =>
   411             store.find_database(name) match {
   412               case Some(database) =>
   413                 using(SQLite.open_database(database))(store.read_build(_, name)) match {
   414                   case Some(build)
   415                   if build.ok && build.sources == sources_stamp(deps0, name) => None
   416                   case _ => Some(name)
   417                 }
   418               case None => Some(name)
   419             })
   420         val selected_sessions =
   421           full_sessions.selection(Sessions.Selection(sessions = outdated))
   422         val deps =
   423           Sessions.deps(selected_sessions, full_sessions.global_theories, inlined_files = true)
   424             .check_errors
   425         (selected_sessions, deps)
   426       }
   427       else (selected_sessions0, deps0)
   428     }
   429 
   430 
   431     /* check unknown files */
   432 
   433     if (check_unknown_files) {
   434       val source_files =
   435         (for {
   436           (_, base) <- deps.session_bases.iterator
   437           (path, _) <- base.sources.iterator
   438         } yield path).toList
   439       val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
   440       val unknown_files =
   441         Mercurial.unknown_files(source_files).
   442           filterNot(path => exclude_files.contains(path.canonical_file))
   443       if (unknown_files.nonEmpty) {
   444         progress.echo_warning("Unknown files (not part of a Mercurial repository):" +
   445           unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
   446       }
   447     }
   448 
   449 
   450     /* main build process */
   451 
   452     val queue = Queue(progress, selected_sessions, store)
   453 
   454     store.prepare_output()
   455 
   456     // optional cleanup
   457     if (clean_build) {
   458       for (name <- full_sessions.build_descendants(full_sessions.build_selection(selection1))) {
   459         val files =
   460           List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
   461             map(store.output_dir + _).filter(_.is_file)
   462         if (files.nonEmpty) progress.echo("Cleaning " + name + " ...")
   463         if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
   464       }
   465     }
   466 
   467     // scheduler loop
   468     case class Result(
   469       current: Boolean,
   470       heap_stamp: Option[String],
   471       process: Option[Process_Result],
   472       info: Sessions.Info)
   473     {
   474       def ok: Boolean =
   475         process match {
   476           case None => false
   477           case Some(res) => res.rc == 0
   478         }
   479     }
   480 
   481     def sleep()
   482     {
   483       try { Thread.sleep(500) }
   484       catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
   485     }
   486 
   487     val numa_nodes = new NUMA.Nodes(numa_shuffling)
   488 
   489     @tailrec def loop(
   490       pending: Queue,
   491       running: Map[String, (List[String], Job)],
   492       results: Map[String, Result]): Map[String, Result] =
   493     {
   494       def used_node(i: Int): Boolean =
   495         running.iterator.exists(
   496           { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
   497 
   498       if (pending.is_empty) results
   499       else {
   500         if (progress.stopped)
   501           for ((_, (_, job)) <- running) job.terminate
   502 
   503         running.find({ case (_, (_, job)) => job.is_finished }) match {
   504           case Some((name, (input_heaps, job))) =>
   505             //{{{ finish job
   506 
   507             val process_result = job.join
   508 
   509             val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
   510             val process_result_tail =
   511             {
   512               val tail = job.info.options.int("process_output_tail")
   513               process_result.copy(
   514                 out_lines =
   515                   "(see also " + (store.output_dir + store.log(name)).file.toString + ")" ::
   516                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
   517             }
   518 
   519 
   520             // write log file
   521             val heap_stamp =
   522               if (process_result.ok) {
   523                 (store.output_dir + store.log(name)).file.delete
   524                 val heap_stamp =
   525                   for (path <- job.output_path if path.is_file)
   526                     yield Sessions.write_heap_digest(path)
   527 
   528                 File.write_gzip(store.output_dir + store.log_gz(name), terminate_lines(log_lines))
   529 
   530                 heap_stamp
   531               }
   532               else {
   533                 (store.output_dir + Path.basic(name)).file.delete
   534                 (store.output_dir + store.log_gz(name)).file.delete
   535 
   536                 File.write(store.output_dir + store.log(name), terminate_lines(log_lines))
   537 
   538                 None
   539               }
   540 
   541             // write database
   542             {
   543               val database = store.output_dir + store.database(name)
   544               database.file.delete
   545 
   546               val build_log =
   547                 Build_Log.Log_File(name, process_result.out_lines).
   548                   parse_session_info(
   549                     command_timings = true,
   550                     theory_timings = true,
   551                     ml_statistics = true,
   552                     task_statistics = true)
   553 
   554               using(SQLite.open_database(database))(db =>
   555                 store.write_session_info(db, name,
   556                   build_log =
   557                     if (process_result.timeout) build_log.error("Timeout") else build_log,
   558                   build =
   559                     Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
   560                       process_result.rc)))
   561             }
   562 
   563             // messages
   564             process_result.err_lines.foreach(progress.echo(_))
   565 
   566             if (process_result.ok)
   567               progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
   568             else {
   569               progress.echo(name + " FAILED")
   570               if (!process_result.interrupted) progress.echo(process_result_tail.out)
   571             }
   572 
   573             loop(pending - name, running - name,
   574               results + (name -> Result(false, heap_stamp, Some(process_result_tail), job.info)))
   575             //}}}
   576           case None if running.size < (max_jobs max 1) =>
   577             //{{{ check/start next job
   578             pending.dequeue(running.isDefinedAt(_)) match {
   579               case Some((name, info)) =>
   580                 val ancestor_results =
   581                   selected_sessions.build_requirements(List(name)).filterNot(_ == name).
   582                     map(results(_))
   583                 val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
   584 
   585                 val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
   586 
   587                 val (current, heap_stamp) =
   588                 {
   589                   store.find_database_heap(name) match {
   590                     case Some((database, heap_stamp)) =>
   591                       using(SQLite.open_database(database))(store.read_build(_, name)) match {
   592                         case Some(build) =>
   593                           val current =
   594                             !fresh_build &&
   595                             build.ok &&
   596                             build.sources == sources_stamp(deps, name) &&
   597                             build.input_heaps == ancestor_heaps &&
   598                             build.output_heap == heap_stamp &&
   599                             !(do_output && heap_stamp.isEmpty)
   600                           (current, heap_stamp)
   601                         case None => (false, None)
   602                       }
   603                     case None => (false, None)
   604                   }
   605                 }
   606                 val all_current = current && ancestor_results.forall(_.current)
   607 
   608                 if (all_current)
   609                   loop(pending - name, running,
   610                     results + (name -> Result(true, heap_stamp, Some(Process_Result(0)), info)))
   611                 else if (no_build) {
   612                   if (verbose) progress.echo("Skipping " + name + " ...")
   613                   loop(pending - name, running,
   614                     results + (name -> Result(false, heap_stamp, Some(Process_Result(1)), info)))
   615                 }
   616                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
   617                   val numa_node = numa_nodes.next(used_node(_))
   618                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   619                   val job =
   620                     new Job(progress, name, info, selected_sessions, 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_stamp, 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() /: 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, progress,
   779           check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
   780           build_heap = build_heap,
   781           clean_build = clean_build,
   782           dirs = dirs,
   783           select_dirs = select_dirs,
   784           numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
   785           max_jobs = max_jobs,
   786           list_files = list_files,
   787           check_keywords = check_keywords,
   788           fresh_build = fresh_build,
   789           no_build = no_build,
   790           soft_build = soft_build,
   791           system_mode = system_mode,
   792           verbose = verbose,
   793           pide = pide,
   794           requirements = requirements,
   795           all_sessions = all_sessions,
   796           base_sessions = base_sessions,
   797           exclude_session_groups = exclude_session_groups,
   798           exclude_sessions = exclude_sessions,
   799           session_groups = session_groups,
   800           sessions = sessions)
   801       }
   802     val end_date = Date.now()
   803     val elapsed_time = end_date.time - start_date.time
   804 
   805     if (verbose) {
   806       progress.echo("\nFinished at " + Build_Log.print_date(end_date))
   807     }
   808 
   809     val total_timing =
   810       (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
   811         copy(elapsed = elapsed_time)
   812     progress.echo(total_timing.message_resources)
   813 
   814     sys.exit(results.rc)
   815   })
   816 }