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