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