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