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