src/Pure/Tools/build.scala
author wenzelm
Thu Jan 31 21:33:24 2019 +0100 (9 months ago)
changeset 69777 1df241e340c8
parent 69744 bb0a354f6b46
child 69811 18f61ce86425
permissions -rw-r--r--
removed left-over test material (amending bb0a354f6b46);
     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, prune, pats) <- info.export_files) {
   339           Export.export_files(store, name, info.dir + dir,
   340             progress = if (verbose) progress else No_Progress,
   341             export_prune = prune,
   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     Isabelle_Fonts.init()
   423 
   424 
   425     /* session selection and dependencies */
   426 
   427     val full_sessions =
   428       Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
   429 
   430     def sources_stamp(deps: Sessions.Deps, name: String): String =
   431     {
   432       val digests =
   433         full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name)
   434       SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
   435     }
   436 
   437     val selection1 =
   438       Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
   439         exclude_sessions, session_groups, sessions) ++ selection
   440 
   441     val deps =
   442     {
   443       val deps0 =
   444         Sessions.deps(full_sessions.selection(selection1), full_sessions.global_theories,
   445           progress = progress, inlined_files = true, verbose = verbose,
   446           list_files = list_files, check_keywords = check_keywords).check_errors
   447 
   448       if (soft_build && !fresh_build) {
   449         val outdated =
   450           deps0.sessions_structure.build_topological_order.flatMap(name =>
   451             store.access_database(name) match {
   452               case Some(db) =>
   453                 using(db)(store.read_build(_, name)) match {
   454                   case Some(build)
   455                   if build.ok && build.sources == sources_stamp(deps0, name) => None
   456                   case _ => Some(name)
   457                 }
   458               case None => Some(name)
   459             })
   460 
   461         Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)),
   462           full_sessions.global_theories, progress = progress, inlined_files = true).check_errors
   463       }
   464       else deps0
   465     }
   466 
   467 
   468     /* check unknown files */
   469 
   470     if (check_unknown_files) {
   471       val source_files =
   472         (for {
   473           (_, base) <- deps.session_bases.iterator
   474           (path, _) <- base.sources.iterator
   475         } yield path).toList
   476       val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
   477       val unknown_files =
   478         Mercurial.check_files(source_files)._2.
   479           filterNot(path => exclude_files.contains(path.canonical_file))
   480       if (unknown_files.nonEmpty) {
   481         progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
   482           unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
   483       }
   484     }
   485 
   486 
   487     /* main build process */
   488 
   489     val queue = Queue(progress, deps.sessions_structure, store)
   490 
   491     store.prepare_output_dir()
   492 
   493     if (clean_build) {
   494       for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection1))) {
   495         val (relevant, ok) = store.clean_output(name)
   496         if (relevant) {
   497           if (ok) progress.echo("Cleaned " + name)
   498           else progress.echo(name + " FAILED to clean")
   499         }
   500       }
   501     }
   502 
   503     // scheduler loop
   504     case class Result(
   505       current: Boolean,
   506       heap_digest: Option[String],
   507       process: Option[Process_Result],
   508       info: Sessions.Info)
   509     {
   510       def ok: Boolean =
   511         process match {
   512           case None => false
   513           case Some(res) => res.rc == 0
   514         }
   515     }
   516 
   517     def sleep()
   518     {
   519       try { Thread.sleep(500) }
   520       catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
   521     }
   522 
   523     val numa_nodes = new NUMA.Nodes(numa_shuffling)
   524 
   525     @tailrec def loop(
   526       pending: Queue,
   527       running: Map[String, (List[String], Job)],
   528       results: Map[String, Result]): Map[String, Result] =
   529     {
   530       def used_node(i: Int): Boolean =
   531         running.iterator.exists(
   532           { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
   533 
   534       if (pending.is_empty) results
   535       else {
   536         if (progress.stopped)
   537           for ((_, (_, job)) <- running) job.terminate
   538 
   539         running.find({ case (_, (_, job)) => job.is_finished }) match {
   540           case Some((name, (input_heaps, job))) =>
   541             //{{{ finish job
   542 
   543             val (process_result, heap_digest) = job.join
   544 
   545             val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
   546             val process_result_tail =
   547             {
   548               val tail = job.info.options.int("process_output_tail")
   549               process_result.copy(
   550                 out_lines =
   551                   "(see also " + store.output_log(name).file.toString + ")" ::
   552                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
   553             }
   554 
   555 
   556             // write log file
   557             if (process_result.ok) {
   558               File.write_gzip(store.output_log_gz(name), terminate_lines(log_lines))
   559             }
   560             else File.write(store.output_log(name), terminate_lines(log_lines))
   561 
   562             // write database
   563             {
   564               val build_log =
   565                 Build_Log.Log_File(name, process_result.out_lines).
   566                   parse_session_info(
   567                     command_timings = true,
   568                     theory_timings = true,
   569                     ml_statistics = true,
   570                     task_statistics = true)
   571 
   572               using(store.open_database(name, output = true))(db =>
   573                 store.write_session_info(db, name,
   574                   build_log =
   575                     if (process_result.timeout) build_log.error("Timeout") else build_log,
   576                   build =
   577                     Session_Info(sources_stamp(deps, name), input_heaps, heap_digest,
   578                       process_result.rc)))
   579             }
   580 
   581             // messages
   582             process_result.err_lines.foreach(progress.echo(_))
   583 
   584             if (process_result.ok)
   585               progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
   586             else {
   587               progress.echo(name + " FAILED")
   588               if (!process_result.interrupted) progress.echo(process_result_tail.out)
   589             }
   590 
   591             loop(pending - name, running - name,
   592               results + (name -> Result(false, heap_digest, Some(process_result_tail), job.info)))
   593             //}}}
   594           case None if running.size < (max_jobs max 1) =>
   595             //{{{ check/start next job
   596             pending.dequeue(running.isDefinedAt(_)) match {
   597               case Some((name, info)) =>
   598                 val ancestor_results =
   599                   deps.sessions_structure.build_requirements(List(name)).filterNot(_ == name).
   600                     map(results(_))
   601                 val ancestor_heaps = ancestor_results.flatMap(_.heap_digest)
   602 
   603                 val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
   604 
   605                 val (current, heap_digest) =
   606                 {
   607                   store.access_database(name) match {
   608                     case Some(db) =>
   609                       using(db)(store.read_build(_, name)) match {
   610                         case Some(build) =>
   611                           val heap_digest = store.find_heap_digest(name)
   612                           val current =
   613                             !fresh_build &&
   614                             build.ok &&
   615                             build.sources == sources_stamp(deps, name) &&
   616                             build.input_heaps == ancestor_heaps &&
   617                             build.output_heap == heap_digest &&
   618                             !(do_output && heap_digest.isEmpty)
   619                           (current, heap_digest)
   620                         case None => (false, None)
   621                       }
   622                     case None => (false, None)
   623                   }
   624                 }
   625                 val all_current = current && ancestor_results.forall(_.current)
   626 
   627                 if (all_current)
   628                   loop(pending - name, running,
   629                     results + (name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
   630                 else if (no_build) {
   631                   if (verbose) progress.echo("Skipping " + name + " ...")
   632                   loop(pending - name, running,
   633                     results + (name -> Result(false, heap_digest, Some(Process_Result(1)), info)))
   634                 }
   635                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
   636                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   637 
   638                   store.clean_output(name)
   639                   using(store.open_database(name, output = true))(store.init_session_info(_, name))
   640 
   641                   val numa_node = numa_nodes.next(used_node(_))
   642                   val job =
   643                     new Job(progress, name, info, deps, store, do_output,
   644                       verbose, pide, numa_node, queue.command_timings(name))
   645                   loop(pending, running + (name -> (ancestor_heaps, job)), results)
   646                 }
   647                 else {
   648                   progress.echo(name + " CANCELLED")
   649                   loop(pending - name, running,
   650                     results + (name -> Result(false, heap_digest, None, info)))
   651                 }
   652               case None => sleep(); loop(pending, running, results)
   653             }
   654             ///}}}
   655           case None => sleep(); loop(pending, running, results)
   656         }
   657       }
   658     }
   659 
   660 
   661     /* build results */
   662 
   663     val results0 =
   664       if (deps.is_empty) {
   665         progress.echo_warning("Nothing to build")
   666         Map.empty[String, Result]
   667       }
   668       else loop(queue, Map.empty, Map.empty)
   669 
   670     val results =
   671       new Results(
   672         (for ((name, result) <- results0.iterator)
   673           yield (name, (result.process, result.info))).toMap)
   674 
   675     if (results.rc != 0 && (verbose || !no_build)) {
   676       val unfinished =
   677         (for {
   678           name <- results.sessions.iterator
   679           if !results(name).ok
   680          } yield name).toList.sorted
   681       progress.echo("Unfinished session(s): " + commas(unfinished))
   682     }
   683 
   684 
   685     /* global browser info */
   686 
   687     if (!no_build) {
   688       val browser_chapters =
   689         (for {
   690           (name, result) <- results0.iterator
   691           if result.ok
   692           info = full_sessions(name)
   693           if info.options.bool("browser_info")
   694         } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
   695             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
   696 
   697       for ((chapter, entries) <- browser_chapters)
   698         Present.update_chapter_index(store.browser_info, chapter, entries)
   699 
   700       if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info)
   701     }
   702 
   703     results
   704   }
   705 
   706 
   707   /* Isabelle tool wrapper */
   708 
   709   val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
   710   {
   711     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
   712 
   713     var base_sessions: List[String] = Nil
   714     var select_dirs: List[Path] = Nil
   715     var numa_shuffling = false
   716     var pide = false
   717     var requirements = false
   718     var soft_build = false
   719     var exclude_session_groups: List[String] = Nil
   720     var all_sessions = false
   721     var build_heap = false
   722     var clean_build = false
   723     var dirs: List[Path] = Nil
   724     var fresh_build = false
   725     var session_groups: List[String] = Nil
   726     var max_jobs = 1
   727     var check_keywords: Set[String] = Set.empty
   728     var list_files = false
   729     var no_build = false
   730     var options = Options.init(opts = build_options)
   731     var system_mode = false
   732     var verbose = false
   733     var exclude_sessions: List[String] = Nil
   734 
   735     val getopts = Getopts("""
   736 Usage: isabelle build [OPTIONS] [SESSIONS ...]
   737 
   738   Options are:
   739     -B NAME      include session NAME and all descendants
   740     -D DIR       include session directory and select its sessions
   741     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
   742     -P           build via PIDE protocol
   743     -R           operate on requirements of selected sessions
   744     -S           soft build: only observe changes of sources, not heap images
   745     -X NAME      exclude sessions from group NAME and all descendants
   746     -a           select all sessions
   747     -b           build heap images
   748     -c           clean build
   749     -d DIR       include session directory
   750     -f           fresh build
   751     -g NAME      select session group NAME
   752     -j INT       maximum number of parallel jobs (default 1)
   753     -k KEYWORD   check theory sources for conflicts with proposed keywords
   754     -l           list session source files
   755     -n           no build -- test dependencies only
   756     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   757     -s           system build mode: produce output in ISABELLE_HOME
   758     -v           verbose
   759     -x NAME      exclude session NAME and all descendants
   760 
   761   Build and manage Isabelle sessions, depending on implicit settings:
   762 
   763 """ + Library.prefix_lines("  ", Build_Log.Settings.show()) + "\n",
   764       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
   765       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   766       "N" -> (_ => numa_shuffling = true),
   767       "P" -> (_ => pide = true),
   768       "R" -> (_ => requirements = true),
   769       "S" -> (_ => soft_build = true),
   770       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   771       "a" -> (_ => all_sessions = true),
   772       "b" -> (_ => build_heap = true),
   773       "c" -> (_ => clean_build = true),
   774       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   775       "f" -> (_ => fresh_build = true),
   776       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   777       "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
   778       "k:" -> (arg => check_keywords = check_keywords + arg),
   779       "l" -> (_ => list_files = true),
   780       "n" -> (_ => no_build = true),
   781       "o:" -> (arg => options = options + arg),
   782       "s" -> (_ => system_mode = true),
   783       "v" -> (_ => verbose = true),
   784       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   785 
   786     val sessions = getopts(args)
   787 
   788     val progress = new Console_Progress(verbose = verbose)
   789 
   790     val start_date = Date.now()
   791 
   792     if (verbose) {
   793       progress.echo(
   794         "Started at " + Build_Log.print_date(start_date) +
   795           " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
   796       progress.echo(Build_Log.Settings.show() + "\n")
   797     }
   798 
   799     val results =
   800       progress.interrupt_handler {
   801         build(options,
   802           progress = progress,
   803           check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
   804           build_heap = build_heap,
   805           clean_build = clean_build,
   806           dirs = dirs,
   807           select_dirs = select_dirs,
   808           numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
   809           max_jobs = max_jobs,
   810           list_files = list_files,
   811           check_keywords = check_keywords,
   812           fresh_build = fresh_build,
   813           no_build = no_build,
   814           soft_build = soft_build,
   815           system_mode = system_mode,
   816           verbose = verbose,
   817           pide = pide,
   818           requirements = requirements,
   819           all_sessions = all_sessions,
   820           base_sessions = base_sessions,
   821           exclude_session_groups = exclude_session_groups,
   822           exclude_sessions = exclude_sessions,
   823           session_groups = session_groups,
   824           sessions = sessions)
   825       }
   826     val end_date = Date.now()
   827     val elapsed_time = end_date.time - start_date.time
   828 
   829     if (verbose) {
   830       progress.echo("\nFinished at " + Build_Log.print_date(end_date))
   831     }
   832 
   833     val total_timing =
   834       (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
   835         copy(elapsed = elapsed_time)
   836     progress.echo(total_timing.message_resources)
   837 
   838     sys.exit(results.rc)
   839   })
   840 
   841 
   842   /* build logic image */
   843 
   844   def build_logic(options: Options, logic: String,
   845     progress: Progress = No_Progress,
   846     build_heap: Boolean = false,
   847     dirs: List[Path] = Nil,
   848     system_mode: Boolean = false,
   849     strict: Boolean = false): Int =
   850   {
   851     val rc =
   852       if (build(options, build_heap = build_heap, no_build = true, dirs = dirs,
   853           system_mode = system_mode, sessions = List(logic)).ok) 0
   854       else {
   855         progress.echo("Build started for Isabelle/" + logic + " ...")
   856         Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
   857           system_mode = system_mode, sessions = List(logic)).rc
   858       }
   859 
   860     if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc
   861   }
   862 }