src/Pure/Tools/build.scala
author wenzelm
Sat Dec 16 21:53:07 2017 +0100 (17 months ago)
changeset 67219 81e9804b2014
parent 67098 0f750a6dc754
child 67297 86a099f896fc
permissions -rw-r--r--
added document antiquotation @{session name};
renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation;
     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                 list(pair(string, 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, (base.loaded_theories.keys,
   222                 base.dest_known_theories))))))))))))))))
   223             })
   224 
   225         val env =
   226           Isabelle_System.settings() +
   227             ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
   228 
   229         def save_heap: String =
   230           (if (info.theories.isEmpty) "" else "ML_Heap.share_common_data (); ") +
   231             "ML_Heap.save_child " + ML_Syntax.print_string_bytes(File.platform_path(output))
   232 
   233         if (pide && !Sessions.is_pure(name)) {
   234           val resources = new Resources(deps(parent))
   235           val session = new Session(options, resources)
   236           val handler = new Handler(progress, session, name)
   237           session.init_protocol_handler(handler)
   238 
   239           val session_result = Future.promise[Process_Result]
   240 
   241           Isabelle_Process.start(session, options, logic = parent,
   242             cwd = info.dir.file, env = env, sessions = Some(sessions), store = store,
   243             phase_changed =
   244             {
   245               case Session.Ready => session.protocol_command("build_session", args_yxml)
   246               case Session.Terminated(result) => session_result.fulfill(result)
   247               case _ =>
   248             })
   249 
   250           val result = session_result.join
   251           handler.result_error.join match {
   252             case "" => result
   253             case msg =>
   254               result.copy(
   255                 rc = result.rc max 1,
   256                 out_lines = result.out_lines ::: split_lines(Output.error_message_text(msg)))
   257           }
   258         }
   259         else {
   260           val args_file = Isabelle_System.tmp_file("build")
   261           File.write(args_file, args_yxml)
   262 
   263           val eval =
   264             "Command_Line.tool0 (fn () => (" +
   265             "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) +
   266             (if (do_output) "; " + save_heap else "") + "));"
   267 
   268           val process =
   269             if (Sessions.is_pure(name)) {
   270               ML_Process(options, raw_ml_system = true, cwd = info.dir.file,
   271                 args =
   272                   (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
   273                   List("--eval", eval),
   274                 env = env, sessions = Some(sessions), store = store,
   275                 cleanup = () => args_file.delete)
   276             }
   277             else {
   278               ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
   279                 env = env, sessions = Some(sessions), store = store,
   280                 cleanup = () => args_file.delete)
   281             }
   282 
   283           process.result(
   284             progress_stdout = (line: String) =>
   285               Library.try_unprefix("\floading_theory = ", line) match {
   286                 case Some(theory) => progress.theory(name, theory)
   287                 case None =>
   288               },
   289             progress_limit =
   290               options.int("process_output_limit") match {
   291                 case 0 => None
   292                 case m => Some(m * 1000000L)
   293               },
   294             strict = false)
   295         }
   296       }
   297 
   298     def terminate: Unit = future_result.cancel
   299     def is_finished: Boolean = future_result.is_finished
   300 
   301     private val timeout_request: Option[Event_Timer.Request] =
   302     {
   303       if (info.timeout > Time.zero)
   304         Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
   305       else None
   306     }
   307 
   308     def join: Process_Result =
   309     {
   310       val result = future_result.join
   311 
   312       if (result.ok)
   313         Present.finish(progress, store.browser_info, graph_file, info, name)
   314 
   315       graph_file.delete
   316 
   317       val was_timeout =
   318         timeout_request match {
   319           case None => false
   320           case Some(request) => !request.cancel
   321         }
   322 
   323       if (result.interrupted) {
   324         if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout
   325         else result.error(Output.error_message_text("Interrupt"))
   326       }
   327       else result
   328     }
   329   }
   330 
   331 
   332 
   333   /** build with results **/
   334 
   335   class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)])
   336   {
   337     def sessions: Set[String] = results.keySet
   338     def cancelled(name: String): Boolean = results(name)._1.isEmpty
   339     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
   340     def info(name: String): Sessions.Info = results(name)._2
   341     val rc =
   342       (0 /: results.iterator.map(
   343         { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
   344     def ok: Boolean = rc == 0
   345 
   346     override def toString: String = rc.toString
   347   }
   348 
   349   def build(
   350     options: Options,
   351     progress: Progress = No_Progress,
   352     check_unknown_files: Boolean = false,
   353     build_heap: Boolean = false,
   354     clean_build: Boolean = false,
   355     dirs: List[Path] = Nil,
   356     select_dirs: List[Path] = Nil,
   357     infos: List[Sessions.Info] = Nil,
   358     numa_shuffling: Boolean = false,
   359     max_jobs: Int = 1,
   360     list_files: Boolean = false,
   361     check_keywords: Set[String] = Set.empty,
   362     fresh_build: Boolean = false,
   363     no_build: Boolean = false,
   364     soft_build: Boolean = false,
   365     system_mode: Boolean = false,
   366     verbose: Boolean = false,
   367     pide: Boolean = false,
   368     requirements: Boolean = false,
   369     all_sessions: Boolean = false,
   370     base_sessions: List[String] = Nil,
   371     exclude_session_groups: List[String] = Nil,
   372     exclude_sessions: List[String] = Nil,
   373     session_groups: List[String] = Nil,
   374     sessions: List[String] = Nil,
   375     selection: Sessions.Selection = Sessions.Selection.empty): Results =
   376   {
   377     val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
   378 
   379     val store = Sessions.store(system_mode)
   380 
   381 
   382     /* session selection and dependencies */
   383 
   384     val full_sessions =
   385       Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
   386 
   387     def sources_stamp(deps: Sessions.Deps, name: String): String =
   388     {
   389       val digests =
   390         full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name)
   391       SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
   392     }
   393 
   394     val selection1 =
   395       Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
   396         exclude_sessions, session_groups, sessions) ++ selection
   397 
   398     val (selected_sessions, deps) =
   399     {
   400       val selected_sessions0 = full_sessions.selection(selection1)
   401       val deps0 =
   402         Sessions.deps(selected_sessions0, full_sessions.global_theories,
   403           progress = progress, inlined_files = true, verbose = verbose,
   404           list_files = list_files, check_keywords = check_keywords).check_errors
   405 
   406       if (soft_build && !fresh_build) {
   407         val outdated =
   408           selected_sessions0.build_topological_order.flatMap(name =>
   409             store.find_database(name) match {
   410               case Some(database) =>
   411                 using(SQLite.open_database(database))(store.read_build(_, name)) match {
   412                   case Some(build)
   413                   if build.ok && build.sources == sources_stamp(deps0, name) => None
   414                   case _ => Some(name)
   415                 }
   416               case None => Some(name)
   417             })
   418         val selected_sessions =
   419           full_sessions.selection(Sessions.Selection(sessions = outdated))
   420         val deps =
   421           Sessions.deps(selected_sessions, full_sessions.global_theories, inlined_files = true)
   422             .check_errors
   423         (selected_sessions, deps)
   424       }
   425       else (selected_sessions0, deps0)
   426     }
   427 
   428 
   429     /* check unknown files */
   430 
   431     if (check_unknown_files) {
   432       val source_files =
   433         (for {
   434           (_, base) <- deps.session_bases.iterator
   435           (path, _) <- base.sources.iterator
   436         } yield path).toList
   437       val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
   438       val unknown_files =
   439         Mercurial.unknown_files(source_files).
   440           filterNot(path => exclude_files.contains(path.canonical_file))
   441       if (unknown_files.nonEmpty) {
   442         progress.echo_warning("Unknown files (not part of a Mercurial repository):" +
   443           unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
   444       }
   445     }
   446 
   447 
   448     /* main build process */
   449 
   450     val queue = Queue(progress, selected_sessions, store)
   451 
   452     store.prepare_output()
   453 
   454     // optional cleanup
   455     if (clean_build) {
   456       for (name <- full_sessions.build_descendants(full_sessions.build_selection(selection1))) {
   457         val files =
   458           List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
   459             map(store.output_dir + _).filter(_.is_file)
   460         if (files.nonEmpty) progress.echo("Cleaning " + name + " ...")
   461         if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
   462       }
   463     }
   464 
   465     // scheduler loop
   466     case class Result(
   467       current: Boolean,
   468       heap_stamp: Option[String],
   469       process: Option[Process_Result],
   470       info: Sessions.Info)
   471     {
   472       def ok: Boolean =
   473         process match {
   474           case None => false
   475           case Some(res) => res.rc == 0
   476         }
   477     }
   478 
   479     def sleep()
   480     {
   481       try { Thread.sleep(500) }
   482       catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
   483     }
   484 
   485     val numa_nodes = new NUMA.Nodes(numa_shuffling)
   486 
   487     @tailrec def loop(
   488       pending: Queue,
   489       running: Map[String, (List[String], Job)],
   490       results: Map[String, Result]): Map[String, Result] =
   491     {
   492       def used_node(i: Int): Boolean =
   493         running.iterator.exists(
   494           { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
   495 
   496       if (pending.is_empty) results
   497       else {
   498         if (progress.stopped)
   499           for ((_, (_, job)) <- running) job.terminate
   500 
   501         running.find({ case (_, (_, job)) => job.is_finished }) match {
   502           case Some((name, (input_heaps, job))) =>
   503             //{{{ finish job
   504 
   505             val process_result = job.join
   506 
   507             val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
   508             val process_result_tail =
   509             {
   510               val tail = job.info.options.int("process_output_tail")
   511               process_result.copy(
   512                 out_lines =
   513                   "(see also " + (store.output_dir + store.log(name)).file.toString + ")" ::
   514                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
   515             }
   516 
   517 
   518             // write log file
   519             val heap_stamp =
   520               if (process_result.ok) {
   521                 (store.output_dir + store.log(name)).file.delete
   522                 val heap_stamp =
   523                   for (path <- job.output_path if path.is_file)
   524                     yield Sessions.write_heap_digest(path)
   525 
   526                 File.write_gzip(store.output_dir + store.log_gz(name), terminate_lines(log_lines))
   527 
   528                 heap_stamp
   529               }
   530               else {
   531                 (store.output_dir + Path.basic(name)).file.delete
   532                 (store.output_dir + store.log_gz(name)).file.delete
   533 
   534                 File.write(store.output_dir + store.log(name), terminate_lines(log_lines))
   535 
   536                 None
   537               }
   538 
   539             // write database
   540             {
   541               val database = store.output_dir + store.database(name)
   542               database.file.delete
   543 
   544               val build_log =
   545                 Build_Log.Log_File(name, process_result.out_lines).
   546                   parse_session_info(
   547                     command_timings = true,
   548                     theory_timings = true,
   549                     ml_statistics = true,
   550                     task_statistics = true)
   551 
   552               using(SQLite.open_database(database))(db =>
   553                 store.write_session_info(db, name,
   554                   build_log =
   555                     if (process_result.timeout) build_log.error("Timeout") else build_log,
   556                   build =
   557                     Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
   558                       process_result.rc)))
   559             }
   560 
   561             // messages
   562             process_result.err_lines.foreach(progress.echo(_))
   563 
   564             if (process_result.ok)
   565               progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
   566             else {
   567               progress.echo(name + " FAILED")
   568               if (!process_result.interrupted) progress.echo(process_result_tail.out)
   569             }
   570 
   571             loop(pending - name, running - name,
   572               results + (name -> Result(false, heap_stamp, Some(process_result_tail), job.info)))
   573             //}}}
   574           case None if running.size < (max_jobs max 1) =>
   575             //{{{ check/start next job
   576             pending.dequeue(running.isDefinedAt(_)) match {
   577               case Some((name, info)) =>
   578                 val ancestor_results =
   579                   selected_sessions.build_requirements(List(name)).filterNot(_ == name).
   580                     map(results(_))
   581                 val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
   582 
   583                 val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
   584 
   585                 val (current, heap_stamp) =
   586                 {
   587                   store.find_database_heap(name) match {
   588                     case Some((database, heap_stamp)) =>
   589                       using(SQLite.open_database(database))(store.read_build(_, name)) match {
   590                         case Some(build) =>
   591                           val current =
   592                             !fresh_build &&
   593                             build.ok &&
   594                             build.sources == sources_stamp(deps, name) &&
   595                             build.input_heaps == ancestor_heaps &&
   596                             build.output_heap == heap_stamp &&
   597                             !(do_output && heap_stamp.isEmpty)
   598                           (current, heap_stamp)
   599                         case None => (false, None)
   600                       }
   601                     case None => (false, None)
   602                   }
   603                 }
   604                 val all_current = current && ancestor_results.forall(_.current)
   605 
   606                 if (all_current)
   607                   loop(pending - name, running,
   608                     results + (name -> Result(true, heap_stamp, Some(Process_Result(0)), info)))
   609                 else if (no_build) {
   610                   if (verbose) progress.echo("Skipping " + name + " ...")
   611                   loop(pending - name, running,
   612                     results + (name -> Result(false, heap_stamp, Some(Process_Result(1)), info)))
   613                 }
   614                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
   615                   val numa_node = numa_nodes.next(used_node(_))
   616                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   617                   val job =
   618                     new Job(progress, name, info, selected_sessions, deps, store, do_output,
   619                       verbose, pide, numa_node, queue.command_timings(name))
   620                   loop(pending, running + (name -> (ancestor_heaps, job)), results)
   621                 }
   622                 else {
   623                   progress.echo(name + " CANCELLED")
   624                   loop(pending - name, running,
   625                     results + (name -> Result(false, heap_stamp, None, info)))
   626                 }
   627               case None => sleep(); loop(pending, running, results)
   628             }
   629             ///}}}
   630           case None => sleep(); loop(pending, running, results)
   631         }
   632       }
   633     }
   634 
   635 
   636     /* build results */
   637 
   638     val results0 =
   639       if (deps.is_empty) {
   640         progress.echo_warning("Nothing to build")
   641         Map.empty[String, Result]
   642       }
   643       else loop(queue, Map.empty, Map.empty)
   644 
   645     val results =
   646       new Results(
   647         (for ((name, result) <- results0.iterator)
   648           yield (name, (result.process, result.info))).toMap)
   649 
   650     if (results.rc != 0 && (verbose || !no_build)) {
   651       val unfinished =
   652         (for {
   653           name <- results.sessions.iterator
   654           if !results(name).ok
   655          } yield name).toList.sorted
   656       progress.echo("Unfinished session(s): " + commas(unfinished))
   657     }
   658 
   659 
   660     /* global browser info */
   661 
   662     if (!no_build) {
   663       val browser_chapters =
   664         (for {
   665           (name, result) <- results0.iterator
   666           if result.ok
   667           info = full_sessions(name)
   668           if info.options.bool("browser_info")
   669         } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
   670             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
   671 
   672       for ((chapter, entries) <- browser_chapters)
   673         Present.update_chapter_index(store.browser_info, chapter, entries)
   674 
   675       if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info)
   676     }
   677 
   678     results
   679   }
   680 
   681 
   682   /* Isabelle tool wrapper */
   683 
   684   val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
   685   {
   686     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
   687 
   688     var base_sessions: List[String] = Nil
   689     var select_dirs: List[Path] = Nil
   690     var numa_shuffling = false
   691     var pide = false
   692     var requirements = false
   693     var soft_build = false
   694     var exclude_session_groups: List[String] = Nil
   695     var all_sessions = false
   696     var build_heap = false
   697     var clean_build = false
   698     var dirs: List[Path] = Nil
   699     var fresh_build = false
   700     var session_groups: List[String] = Nil
   701     var max_jobs = 1
   702     var check_keywords: Set[String] = Set.empty
   703     var list_files = false
   704     var no_build = false
   705     var options = (Options.init() /: build_options)(_ + _)
   706     var system_mode = false
   707     var verbose = false
   708     var exclude_sessions: List[String] = Nil
   709 
   710     val getopts = Getopts("""
   711 Usage: isabelle build [OPTIONS] [SESSIONS ...]
   712 
   713   Options are:
   714     -B NAME      include session NAME and all descendants
   715     -D DIR       include session directory and select its sessions
   716     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
   717     -P           build via PIDE protocol
   718     -R           operate on requirements of selected sessions
   719     -S           soft build: only observe changes of sources, not heap images
   720     -X NAME      exclude sessions from group NAME and all descendants
   721     -a           select all sessions
   722     -b           build heap images
   723     -c           clean build
   724     -d DIR       include session directory
   725     -f           fresh build
   726     -g NAME      select session group NAME
   727     -j INT       maximum number of parallel jobs (default 1)
   728     -k KEYWORD   check theory sources for conflicts with proposed keywords
   729     -l           list session source files
   730     -n           no build -- test dependencies only
   731     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   732     -s           system build mode: produce output in ISABELLE_HOME
   733     -v           verbose
   734     -x NAME      exclude session NAME and all descendants
   735 
   736   Build and manage Isabelle sessions, depending on implicit settings:
   737 
   738 """ + Library.prefix_lines("  ", Build_Log.Settings.show()) + "\n",
   739       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
   740       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   741       "N" -> (_ => numa_shuffling = true),
   742       "P" -> (_ => pide = true),
   743       "R" -> (_ => requirements = true),
   744       "S" -> (_ => soft_build = true),
   745       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   746       "a" -> (_ => all_sessions = true),
   747       "b" -> (_ => build_heap = true),
   748       "c" -> (_ => clean_build = true),
   749       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   750       "f" -> (_ => fresh_build = true),
   751       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   752       "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
   753       "k:" -> (arg => check_keywords = check_keywords + arg),
   754       "l" -> (_ => list_files = true),
   755       "n" -> (_ => no_build = true),
   756       "o:" -> (arg => options = options + arg),
   757       "s" -> (_ => system_mode = true),
   758       "v" -> (_ => verbose = true),
   759       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   760 
   761     val sessions = getopts(args)
   762 
   763     val progress = new Console_Progress(verbose = verbose)
   764 
   765     val start_date = Date.now()
   766 
   767     if (verbose) {
   768       progress.echo(
   769         "Started at " + Build_Log.print_date(start_date) +
   770           " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
   771       progress.echo(Build_Log.Settings.show() + "\n")
   772     }
   773 
   774     val results =
   775       progress.interrupt_handler {
   776         build(options, progress,
   777           check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
   778           build_heap = build_heap,
   779           clean_build = clean_build,
   780           dirs = dirs,
   781           select_dirs = select_dirs,
   782           numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
   783           max_jobs = max_jobs,
   784           list_files = list_files,
   785           check_keywords = check_keywords,
   786           fresh_build = fresh_build,
   787           no_build = no_build,
   788           soft_build = soft_build,
   789           system_mode = system_mode,
   790           verbose = verbose,
   791           pide = pide,
   792           requirements = requirements,
   793           all_sessions = all_sessions,
   794           base_sessions = base_sessions,
   795           exclude_session_groups = exclude_session_groups,
   796           exclude_sessions = exclude_sessions,
   797           session_groups = session_groups,
   798           sessions = sessions)
   799       }
   800     val end_date = Date.now()
   801     val elapsed_time = end_date.time - start_date.time
   802 
   803     if (verbose) {
   804       progress.echo("\nFinished at " + Build_Log.print_date(end_date))
   805     }
   806 
   807     val total_timing =
   808       (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
   809         copy(elapsed = elapsed_time)
   810     progress.echo(total_timing.message_resources)
   811 
   812     sys.exit(results.rc)
   813   })
   814 }