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