src/Pure/Tools/build.scala
author wenzelm
Thu, 04 Mar 2021 16:23:34 +0100
changeset 73364 6bf6160a2c54
parent 73359 d8a0e996614b
child 73365 a78b5ffc0f46
permissions -rw-r--r--
proper scala.collection.immutable;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50686
d703e3aafa8c moved files;
wenzelm
parents: 50566
diff changeset
     1
/*  Title:      Pure/Tools/build.scala
48276
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
57923
cdae2467311d tuned comments;
wenzelm
parents: 56890
diff changeset
     3
    Options:    :folding=explicit:
48276
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
     4
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
     5
Build and manage Isabelle sessions.
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
     6
*/
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
     7
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
     8
package isabelle
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
     9
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    10
73364
6bf6160a2c54 proper scala.collection.immutable;
wenzelm
parents: 73359
diff changeset
    11
import scala.collection.immutable.SortedSet
48340
6f4fc030882a allow explicit specification of additional session directories;
wenzelm
parents: 48339
diff changeset
    12
import scala.annotation.tailrec
48337
9c7f8e5805b4 cumulate semantic Session_Info, based on syntactic Session_Entry;
wenzelm
parents: 48336
diff changeset
    13
48335
2f923e994056 more informative errors;
wenzelm
parents: 48334
diff changeset
    14
48276
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    15
object Build
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    16
{
62631
c39614ddb80b clarified modules;
wenzelm
parents: 62630
diff changeset
    17
  /** auxiliary **/
48424
wenzelm
parents: 48423
diff changeset
    18
65291
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    19
  /* persistent build info */
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    20
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    21
  sealed case class Session_Info(
66749
0445cfaf6132 more compact (second-order) digest for 10^2..10^3 source files, with slightly increased risk of collisions;
wenzelm
parents: 66747
diff changeset
    22
    sources: String,
65291
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    23
    input_heaps: List[String],
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    24
    output_heap: Option[String],
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    25
    return_code: Int)
66747
wenzelm
parents: 66746
diff changeset
    26
  {
wenzelm
parents: 66746
diff changeset
    27
    def ok: Boolean = return_code == 0
wenzelm
parents: 66746
diff changeset
    28
  }
65291
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    29
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    30
65289
86d93effc3df tuned signature;
wenzelm
parents: 65284
diff changeset
    31
  /* queue with scheduling information */
48676
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
    32
62631
c39614ddb80b clarified modules;
wenzelm
parents: 62630
diff changeset
    33
  private object Queue
48676
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
    34
  {
68086
9e1c670301b8 cleanup session output before starting build job;
wenzelm
parents: 67852
diff changeset
    35
    type Timings = (List[Properties.T], Double)
9e1c670301b8 cleanup session output before starting build job;
wenzelm
parents: 67852
diff changeset
    36
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
    37
    def load_timings(progress: Progress, store: Sessions.Store, session_name: String): Timings =
65289
86d93effc3df tuned signature;
wenzelm
parents: 65284
diff changeset
    38
    {
68086
9e1c670301b8 cleanup session output before starting build job;
wenzelm
parents: 67852
diff changeset
    39
      val no_timings: Timings = (Nil, 0.0)
65289
86d93effc3df tuned signature;
wenzelm
parents: 65284
diff changeset
    40
72634
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72624
diff changeset
    41
      store.try_open_database(session_name) match {
65291
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    42
        case None => no_timings
68214
b0e2a19df95b more abstract database access;
wenzelm
parents: 68213
diff changeset
    43
        case Some(db) =>
65291
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    44
          def ignore_error(msg: String) =
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    45
          {
68214
b0e2a19df95b more abstract database access;
wenzelm
parents: 68213
diff changeset
    46
            progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg))
65291
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    47
            no_timings
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    48
          }
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    49
          try {
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
    50
            val command_timings = store.read_command_timings(db, session_name)
68214
b0e2a19df95b more abstract database access;
wenzelm
parents: 68213
diff changeset
    51
            val session_timing =
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
    52
              store.read_session_timing(db, session_name) match {
68214
b0e2a19df95b more abstract database access;
wenzelm
parents: 68213
diff changeset
    53
                case Markup.Elapsed(t) => t
b0e2a19df95b more abstract database access;
wenzelm
parents: 68213
diff changeset
    54
                case _ => 0.0
b0e2a19df95b more abstract database access;
wenzelm
parents: 68213
diff changeset
    55
              }
b0e2a19df95b more abstract database access;
wenzelm
parents: 68213
diff changeset
    56
            (command_timings, session_timing)
65291
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    57
          }
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    58
          catch {
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    59
            case ERROR(msg) => ignore_error(msg)
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    60
            case exn: java.lang.Error => ignore_error(Exn.message(exn))
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    61
            case _: XML.Error => ignore_error("")
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
    62
          }
68214
b0e2a19df95b more abstract database access;
wenzelm
parents: 68213
diff changeset
    63
          finally { db.close }
65289
86d93effc3df tuned signature;
wenzelm
parents: 65284
diff changeset
    64
      }
86d93effc3df tuned signature;
wenzelm
parents: 65284
diff changeset
    65
    }
86d93effc3df tuned signature;
wenzelm
parents: 65284
diff changeset
    66
68731
c2dcb7f7a3ef tuned signature;
wenzelm
parents: 68487
diff changeset
    67
    def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double])
68486
6984a55f3cba clarified queue ordering: take session descendants into account, notably for "slow" AFP sessions;
wenzelm
parents: 68331
diff changeset
    68
      : Map[String, Double] =
6984a55f3cba clarified queue ordering: take session descendants into account, notably for "slow" AFP sessions;
wenzelm
parents: 68331
diff changeset
    69
    {
68731
c2dcb7f7a3ef tuned signature;
wenzelm
parents: 68487
diff changeset
    70
      val maximals = sessions_structure.build_graph.maximals.toSet
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
    71
      def desc_timing(session_name: String): Double =
68486
6984a55f3cba clarified queue ordering: take session descendants into account, notably for "slow" AFP sessions;
wenzelm
parents: 68331
diff changeset
    72
      {
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
    73
        if (maximals.contains(session_name)) timing(session_name)
68487
wenzelm
parents: 68486
diff changeset
    74
        else {
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
    75
          val descendants = sessions_structure.build_descendants(List(session_name)).toSet
68731
c2dcb7f7a3ef tuned signature;
wenzelm
parents: 68487
diff changeset
    76
          val g = sessions_structure.build_graph.restrict(descendants)
68487
wenzelm
parents: 68486
diff changeset
    77
          (0.0 :: g.maximals.flatMap(desc => {
wenzelm
parents: 68486
diff changeset
    78
            val ps = g.all_preds(List(desc))
71895
wenzelm
parents: 71894
diff changeset
    79
            if (ps.exists(p => !timing.isDefinedAt(p))) None
68487
wenzelm
parents: 68486
diff changeset
    80
            else Some(ps.map(timing(_)).sum)
wenzelm
parents: 68486
diff changeset
    81
          })).max
wenzelm
parents: 68486
diff changeset
    82
        }
68486
6984a55f3cba clarified queue ordering: take session descendants into account, notably for "slow" AFP sessions;
wenzelm
parents: 68331
diff changeset
    83
      }
6984a55f3cba clarified queue ordering: take session descendants into account, notably for "slow" AFP sessions;
wenzelm
parents: 68331
diff changeset
    84
      timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
6984a55f3cba clarified queue ordering: take session descendants into account, notably for "slow" AFP sessions;
wenzelm
parents: 68331
diff changeset
    85
    }
6984a55f3cba clarified queue ordering: take session descendants into account, notably for "slow" AFP sessions;
wenzelm
parents: 68331
diff changeset
    86
68731
c2dcb7f7a3ef tuned signature;
wenzelm
parents: 68487
diff changeset
    87
    def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store)
c2dcb7f7a3ef tuned signature;
wenzelm
parents: 68487
diff changeset
    88
      : Queue =
48676
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
    89
    {
68731
c2dcb7f7a3ef tuned signature;
wenzelm
parents: 68487
diff changeset
    90
      val graph = sessions_structure.build_graph
65415
8cd54b18b68b clarified signature: tree structure is not essential;
wenzelm
parents: 65406
diff changeset
    91
      val names = graph.keys
51220
e140c8fa485a recover timing information from old log files;
wenzelm
parents: 51218
diff changeset
    92
65831
3b197547c1d4 prefer explicit progress channel;
wenzelm
parents: 65828
diff changeset
    93
      val timings = names.map(name => (name, load_timings(progress, store, name)))
51220
e140c8fa485a recover timing information from old log files;
wenzelm
parents: 51218
diff changeset
    94
      val command_timings =
68486
6984a55f3cba clarified queue ordering: take session descendants into account, notably for "slow" AFP sessions;
wenzelm
parents: 68331
diff changeset
    95
        timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
51220
e140c8fa485a recover timing information from old log files;
wenzelm
parents: 51218
diff changeset
    96
      val session_timing =
68731
c2dcb7f7a3ef tuned signature;
wenzelm
parents: 68487
diff changeset
    97
        make_session_timing(sessions_structure,
c2dcb7f7a3ef tuned signature;
wenzelm
parents: 68487
diff changeset
    98
          timings.map({ case (name, (_, t)) => (name, t) }).toMap)
48678
ff27af15530c queue ordering by descending outdegree and timeout;
wenzelm
parents: 48676
diff changeset
    99
ff27af15530c queue ordering by descending outdegree and timeout;
wenzelm
parents: 48676
diff changeset
   100
      object Ordering extends scala.math.Ordering[String]
ff27af15530c queue ordering by descending outdegree and timeout;
wenzelm
parents: 48676
diff changeset
   101
      {
51227
88c96e836ed6 prefer comparison of session timing, if this is known already;
wenzelm
parents: 51223
diff changeset
   102
        def compare_timing(name1: String, name2: String): Int =
88c96e836ed6 prefer comparison of session timing, if this is known already;
wenzelm
parents: 51223
diff changeset
   103
        {
88c96e836ed6 prefer comparison of session timing, if this is known already;
wenzelm
parents: 51223
diff changeset
   104
          val t1 = session_timing(name1)
88c96e836ed6 prefer comparison of session timing, if this is known already;
wenzelm
parents: 51223
diff changeset
   105
          val t2 = session_timing(name2)
88c96e836ed6 prefer comparison of session timing, if this is known already;
wenzelm
parents: 51223
diff changeset
   106
          if (t1 == 0.0 || t2 == 0.0) 0
88c96e836ed6 prefer comparison of session timing, if this is known already;
wenzelm
parents: 51223
diff changeset
   107
          else t1 compare t2
88c96e836ed6 prefer comparison of session timing, if this is known already;
wenzelm
parents: 51223
diff changeset
   108
        }
88c96e836ed6 prefer comparison of session timing, if this is known already;
wenzelm
parents: 51223
diff changeset
   109
48678
ff27af15530c queue ordering by descending outdegree and timeout;
wenzelm
parents: 48676
diff changeset
   110
        def compare(name1: String, name2: String): Int =
68486
6984a55f3cba clarified queue ordering: take session descendants into account, notably for "slow" AFP sessions;
wenzelm
parents: 68331
diff changeset
   111
          compare_timing(name2, name1) match {
48678
ff27af15530c queue ordering by descending outdegree and timeout;
wenzelm
parents: 48676
diff changeset
   112
            case 0 =>
68731
c2dcb7f7a3ef tuned signature;
wenzelm
parents: 68487
diff changeset
   113
              sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
68486
6984a55f3cba clarified queue ordering: take session descendants into account, notably for "slow" AFP sessions;
wenzelm
parents: 68331
diff changeset
   114
                case 0 => name1 compare name2
48678
ff27af15530c queue ordering by descending outdegree and timeout;
wenzelm
parents: 48676
diff changeset
   115
                case ord => ord
ff27af15530c queue ordering by descending outdegree and timeout;
wenzelm
parents: 48676
diff changeset
   116
              }
ff27af15530c queue ordering by descending outdegree and timeout;
wenzelm
parents: 48676
diff changeset
   117
            case ord => ord
ff27af15530c queue ordering by descending outdegree and timeout;
wenzelm
parents: 48676
diff changeset
   118
          }
ff27af15530c queue ordering by descending outdegree and timeout;
wenzelm
parents: 48676
diff changeset
   119
      }
ff27af15530c queue ordering by descending outdegree and timeout;
wenzelm
parents: 48676
diff changeset
   120
65415
8cd54b18b68b clarified signature: tree structure is not essential;
wenzelm
parents: 65406
diff changeset
   121
      new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
48676
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
   122
    }
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
   123
  }
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
   124
65314
wenzelm
parents: 65313
diff changeset
   125
  private class Queue(
62631
c39614ddb80b clarified modules;
wenzelm
parents: 62630
diff changeset
   126
    graph: Graph[String, Sessions.Info],
51220
e140c8fa485a recover timing information from old log files;
wenzelm
parents: 51218
diff changeset
   127
    order: SortedSet[String],
e140c8fa485a recover timing information from old log files;
wenzelm
parents: 51218
diff changeset
   128
    val command_timings: String => List[Properties.T])
48676
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
   129
  {
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
   130
    def is_inner(name: String): Boolean = !graph.is_maximal(name)
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
   131
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
   132
    def is_empty: Boolean = graph.is_empty
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
   133
51227
88c96e836ed6 prefer comparison of session timing, if this is known already;
wenzelm
parents: 51223
diff changeset
   134
    def - (name: String): Queue =
88c96e836ed6 prefer comparison of session timing, if this is known already;
wenzelm
parents: 51223
diff changeset
   135
      new Queue(graph.del_node(name),
67011
bab3208d8d37 updated comments;
wenzelm
parents: 66972
diff changeset
   136
        order - name,  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
51227
88c96e836ed6 prefer comparison of session timing, if this is known already;
wenzelm
parents: 51223
diff changeset
   137
        command_timings)
48676
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
   138
62631
c39614ddb80b clarified modules;
wenzelm
parents: 62630
diff changeset
   139
    def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
48676
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
   140
    {
51227
88c96e836ed6 prefer comparison of session timing, if this is known already;
wenzelm
parents: 51223
diff changeset
   141
      val it = order.iterator.dropWhile(name =>
88c96e836ed6 prefer comparison of session timing, if this is known already;
wenzelm
parents: 51223
diff changeset
   142
        skip(name)
67011
bab3208d8d37 updated comments;
wenzelm
parents: 66972
diff changeset
   143
          || !graph.defined(name)  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
51227
88c96e836ed6 prefer comparison of session timing, if this is known already;
wenzelm
parents: 51223
diff changeset
   144
          || !graph.is_minimal(name))
73344
f5c147654661 tuned --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   145
      if (it.hasNext) { val name = it.next(); Some((name, graph.get_node(name))) }
48676
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
   146
      else None
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
   147
    }
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
   148
  }
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
   149
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
   150
62631
c39614ddb80b clarified modules;
wenzelm
parents: 62630
diff changeset
   151
62641
0b1b7465f2ef always build with full results;
wenzelm
parents: 62638
diff changeset
   152
  /** build with results **/
48424
wenzelm
parents: 48423
diff changeset
   153
63996
3f47fec9edfc tuned whitespace;
wenzelm
parents: 63865
diff changeset
   154
  class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)])
62403
1d7aba20a332 explicit class Build_Results;
wenzelm
parents: 62402
diff changeset
   155
  {
1d7aba20a332 explicit class Build_Results;
wenzelm
parents: 62402
diff changeset
   156
    def sessions: Set[String] = results.keySet
72673
8ff7a0e394f9 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents: 72662
diff changeset
   157
    def infos: List[Sessions.Info] = results.values.map(_._2).toList
63082
6af03422535a expose Sessions.Info in Build.Results
Lars Hupel <lars.hupel@mytum.de>
parents: 62946
diff changeset
   158
    def cancelled(name: String): Boolean = results(name)._1.isEmpty
6af03422535a expose Sessions.Info in Build.Results
Lars Hupel <lars.hupel@mytum.de>
parents: 62946
diff changeset
   159
    def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
6af03422535a expose Sessions.Info in Build.Results
Lars Hupel <lars.hupel@mytum.de>
parents: 62946
diff changeset
   160
    def info(name: String): Sessions.Info = results(name)._2
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71598
diff changeset
   161
    val rc: Int =
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73344
diff changeset
   162
      results.iterator.map({ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }).
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73344
diff changeset
   163
        foldLeft(0)(_ max _)
62641
0b1b7465f2ef always build with full results;
wenzelm
parents: 62638
diff changeset
   164
    def ok: Boolean = rc == 0
62406
b5b8fb87447a tuned signature;
wenzelm
parents: 62405
diff changeset
   165
b5b8fb87447a tuned signature;
wenzelm
parents: 62405
diff changeset
   166
    override def toString: String = rc.toString
62403
1d7aba20a332 explicit class Build_Results;
wenzelm
parents: 62402
diff changeset
   167
  }
1d7aba20a332 explicit class Build_Results;
wenzelm
parents: 62402
diff changeset
   168
72021
664e90313a54 clarified signature;
wenzelm
parents: 72019
diff changeset
   169
  def session_finished(session_name: String, process_result: Process_Result): String =
664e90313a54 clarified signature;
wenzelm
parents: 72019
diff changeset
   170
    "Finished " + session_name + " (" + process_result.timing.message_resources + ")"
72013
6a24ecc4ff1b clarified signature;
wenzelm
parents: 72012
diff changeset
   171
72021
664e90313a54 clarified signature;
wenzelm
parents: 72019
diff changeset
   172
  def session_timing(session_name: String, build_log: Build_Log.Session_Info): String =
664e90313a54 clarified signature;
wenzelm
parents: 72019
diff changeset
   173
  {
664e90313a54 clarified signature;
wenzelm
parents: 72019
diff changeset
   174
    val props = build_log.session_timing
664e90313a54 clarified signature;
wenzelm
parents: 72019
diff changeset
   175
    val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
664e90313a54 clarified signature;
wenzelm
parents: 72019
diff changeset
   176
    val timing = Markup.Timing_Properties.parse(props)
72015
6c6609fd898c more accurate message;
wenzelm
parents: 72013
diff changeset
   177
    "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
72021
664e90313a54 clarified signature;
wenzelm
parents: 72019
diff changeset
   178
  }
72018
5c9984820caa clarified signature;
wenzelm
parents: 72017
diff changeset
   179
62641
0b1b7465f2ef always build with full results;
wenzelm
parents: 62638
diff changeset
   180
  def build(
50404
898cac1dad5e avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents: 50367
diff changeset
   181
    options: Options,
71981
0be06f99b210 clarified signature;
wenzelm
parents: 71978
diff changeset
   182
    selection: Sessions.Selection = Sessions.Selection.empty,
72652
07edf1952ab1 clarified modules;
wenzelm
parents: 72648
diff changeset
   183
    presentation: Presentation.Context = Presentation.Context.none,
71726
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 71718
diff changeset
   184
    progress: Progress = new Progress,
65832
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65831
diff changeset
   185
    check_unknown_files: Boolean = false,
48511
37999ee01156 remove old output heaps, to ensure that result is valid wrt. check_stamps;
wenzelm
parents: 48509
diff changeset
   186
    build_heap: Boolean = false,
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   187
    clean_build: Boolean = false,
56890
7f120d227ca5 tuned signature;
wenzelm
parents: 56873
diff changeset
   188
    dirs: List[Path] = Nil,
7f120d227ca5 tuned signature;
wenzelm
parents: 56873
diff changeset
   189
    select_dirs: List[Path] = Nil,
66968
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66962
diff changeset
   190
    infos: List[Sessions.Info] = Nil,
64265
8eb6365f5916 isabelle build -N;
wenzelm
parents: 64173
diff changeset
   191
    numa_shuffling: Boolean = false,
48509
4854ced3e9d7 support session groups;
wenzelm
parents: 48508
diff changeset
   192
    max_jobs: Int = 1,
48903
1621b3f26095 added build option -l (list files);
wenzelm
parents: 48883
diff changeset
   193
    list_files: Boolean = false,
59891
9ce697050455 added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents: 59811
diff changeset
   194
    check_keywords: Set[String] = Set.empty,
66841
5c32a072ca8b added isablle build option -f;
wenzelm
parents: 66822
diff changeset
   195
    fresh_build: Boolean = false,
48509
4854ced3e9d7 support session groups;
wenzelm
parents: 48508
diff changeset
   196
    no_build: Boolean = false,
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   197
    soft_build: Boolean = false,
48509
4854ced3e9d7 support session groups;
wenzelm
parents: 48508
diff changeset
   198
    verbose: Boolean = false,
71896
ce06d6456cc8 clarified signature --- fit within limit of 22 arguments;
wenzelm
parents: 71895
diff changeset
   199
    export_files: Boolean = false): Results =
63224
78e93610a3c8 more flexible build_selection;
wenzelm
parents: 63082
diff changeset
   200
  {
71677
ff2c26b8ffb1 clarified build_options vs. job options;
wenzelm
parents: 71676
diff changeset
   201
    val build_options =
71679
eeaa4021f080 proper "editor_tracing_messages=0" as in "isabelle dump";
wenzelm
parents: 71677
diff changeset
   202
      options +
eeaa4021f080 proper "editor_tracing_messages=0" as in "isabelle dump";
wenzelm
parents: 71677
diff changeset
   203
        "completion_limit=0" +
eeaa4021f080 proper "editor_tracing_messages=0" as in "isabelle dump";
wenzelm
parents: 71677
diff changeset
   204
        "editor_tracing_messages=0" +
72993
6ead333e450d more robust defaults: spurious problems with parallel invocations and interrupts;
wenzelm
parents: 72992
diff changeset
   205
        "kodkod_scala=false" +
72728
caa182bdab7a clarified options: batch-build has pide_reports disabled by default (requires significant resources);
wenzelm
parents: 72693
diff changeset
   206
        ("pide_reports=" + options.bool("build_pide_reports"))
51220
e140c8fa485a recover timing information from old log files;
wenzelm
parents: 51218
diff changeset
   207
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69811
diff changeset
   208
    val store = Sessions.store(build_options)
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   209
69369
6ecc85955e04 prefer "Isabelle DejaVu Sans", even for headless batch-build (session_graph.pdf);
wenzelm
parents: 68957
diff changeset
   210
    Isabelle_Fonts.init()
6ecc85955e04 prefer "Isabelle DejaVu Sans", even for headless batch-build (session_graph.pdf);
wenzelm
parents: 68957
diff changeset
   211
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   212
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   213
    /* session selection and dependencies */
65422
b606c98e6d10 tuned signature;
wenzelm
parents: 65420
diff changeset
   214
66961
wenzelm
parents: 66944
diff changeset
   215
    val full_sessions =
67026
687c822ee5e3 tuned signature;
wenzelm
parents: 67025
diff changeset
   216
      Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
65422
b606c98e6d10 tuned signature;
wenzelm
parents: 65420
diff changeset
   217
73012
238ddf525da4 clarified HTML presentation, e.g. avoid bulky jobs like HOL or HOL-Analysis in applications;
wenzelm
parents: 72993
diff changeset
   218
    val full_sessions_selection = full_sessions.imports_selection(selection)
238ddf525da4 clarified HTML presentation, e.g. avoid bulky jobs like HOL or HOL-Analysis in applications;
wenzelm
parents: 72993
diff changeset
   219
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   220
    def sources_stamp(deps: Sessions.Deps, session_name: String): String =
66749
0445cfaf6132 more compact (second-order) digest for 10^2..10^3 source files, with slightly increased risk of collisions;
wenzelm
parents: 66747
diff changeset
   221
    {
0445cfaf6132 more compact (second-order) digest for 10^2..10^3 source files, with slightly increased risk of collisions;
wenzelm
parents: 66747
diff changeset
   222
      val digests =
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   223
        full_sessions(session_name).meta_digest ::
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   224
        deps.sources(session_name) :::
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   225
        deps.imported_sources(session_name)
72654
99a6bcd1e8e4 tuned signature;
wenzelm
parents: 72653
diff changeset
   226
      SHA1.digest_set(digests).toString
66749
0445cfaf6132 more compact (second-order) digest for 10^2..10^3 source files, with slightly increased risk of collisions;
wenzelm
parents: 66747
diff changeset
   227
    }
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   228
68204
a554da2811f2 clarified signature;
wenzelm
parents: 68198
diff changeset
   229
    val deps =
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   230
    {
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   231
      val deps0 =
71896
ce06d6456cc8 clarified signature --- fit within limit of 22 arguments;
wenzelm
parents: 71895
diff changeset
   232
        Sessions.deps(full_sessions.selection(selection),
66962
e1bde71bace6 clarified signature: global_theories is always required;
wenzelm
parents: 66961
diff changeset
   233
          progress = progress, inlined_files = true, verbose = verbose,
e1bde71bace6 clarified signature: global_theories is always required;
wenzelm
parents: 66961
diff changeset
   234
          list_files = list_files, check_keywords = check_keywords).check_errors
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   235
66841
5c32a072ca8b added isablle build option -f;
wenzelm
parents: 66822
diff changeset
   236
      if (soft_build && !fresh_build) {
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   237
        val outdated =
68204
a554da2811f2 clarified signature;
wenzelm
parents: 68198
diff changeset
   238
          deps0.sessions_structure.build_topological_order.flatMap(name =>
72634
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72624
diff changeset
   239
            store.try_open_database(name) match {
68214
b0e2a19df95b more abstract database access;
wenzelm
parents: 68213
diff changeset
   240
              case Some(db) =>
68216
wenzelm
parents: 68214
diff changeset
   241
                using(db)(store.read_build(_, name)) match {
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   242
                  case Some(build)
66747
wenzelm
parents: 66746
diff changeset
   243
                  if build.ok && build.sources == sources_stamp(deps0, name) => None
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   244
                  case _ => Some(name)
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   245
                }
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   246
              case None => Some(name)
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   247
            })
68204
a554da2811f2 clarified signature;
wenzelm
parents: 68198
diff changeset
   248
a554da2811f2 clarified signature;
wenzelm
parents: 68198
diff changeset
   249
        Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)),
70671
cb1776c8e216 clarified signature: retain global session information, unaffected by later restriction;
wenzelm
parents: 70509
diff changeset
   250
          progress = progress, inlined_files = true).check_errors
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   251
      }
68204
a554da2811f2 clarified signature;
wenzelm
parents: 68198
diff changeset
   252
      else deps0
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   253
    }
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   254
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   255
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   256
    /* check unknown files */
48504
21dfd6c04482 actually check source vs. target stamps, based on information from log files;
wenzelm
parents: 48494
diff changeset
   257
65832
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65831
diff changeset
   258
    if (check_unknown_files) {
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65831
diff changeset
   259
      val source_files =
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65831
diff changeset
   260
        (for {
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65831
diff changeset
   261
          (_, base) <- deps.session_bases.iterator
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65831
diff changeset
   262
          (path, _) <- base.sources.iterator
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65831
diff changeset
   263
        } yield path).toList
67098
0f750a6dc754 suppress warning;
wenzelm
parents: 67052
diff changeset
   264
      val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
0f750a6dc754 suppress warning;
wenzelm
parents: 67052
diff changeset
   265
      val unknown_files =
67782
7e223a05e6d8 clarified notion of unknown files: ignore files outside of a Mercurial repository;
wenzelm
parents: 67493
diff changeset
   266
        Mercurial.check_files(source_files)._2.
67098
0f750a6dc754 suppress warning;
wenzelm
parents: 67052
diff changeset
   267
          filterNot(path => exclude_files.contains(path.canonical_file))
65832
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65831
diff changeset
   268
      if (unknown_files.nonEmpty) {
67782
7e223a05e6d8 clarified notion of unknown files: ignore files outside of a Mercurial repository;
wenzelm
parents: 67493
diff changeset
   269
        progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
65832
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65831
diff changeset
   270
          unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65831
diff changeset
   271
      }
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65831
diff changeset
   272
    }
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65831
diff changeset
   273
51220
e140c8fa485a recover timing information from old log files;
wenzelm
parents: 51218
diff changeset
   274
e140c8fa485a recover timing information from old log files;
wenzelm
parents: 51218
diff changeset
   275
    /* main build process */
e140c8fa485a recover timing information from old log files;
wenzelm
parents: 51218
diff changeset
   276
68204
a554da2811f2 clarified signature;
wenzelm
parents: 68198
diff changeset
   277
    val queue = Queue(progress, deps.sessions_structure, store)
65289
86d93effc3df tuned signature;
wenzelm
parents: 65284
diff changeset
   278
68219
c0341c0080e2 clarified store directories;
wenzelm
parents: 68217
diff changeset
   279
    store.prepare_output_dir()
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48370
diff changeset
   280
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   281
    if (clean_build) {
73012
238ddf525da4 clarified HTML presentation, e.g. avoid bulky jobs like HOL or HOL-Analysis in applications;
wenzelm
parents: 72993
diff changeset
   282
      for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
68220
8fc4e3d1df86 clarified store.clean_output: cleanup user_output_dir even in system_mode;
wenzelm
parents: 68219
diff changeset
   283
        val (relevant, ok) = store.clean_output(name)
8fc4e3d1df86 clarified store.clean_output: cleanup user_output_dir even in system_mode;
wenzelm
parents: 68219
diff changeset
   284
        if (relevant) {
8fc4e3d1df86 clarified store.clean_output: cleanup user_output_dir even in system_mode;
wenzelm
parents: 68219
diff changeset
   285
          if (ok) progress.echo("Cleaned " + name)
8fc4e3d1df86 clarified store.clean_output: cleanup user_output_dir even in system_mode;
wenzelm
parents: 68219
diff changeset
   286
          else progress.echo(name + " FAILED to clean")
8fc4e3d1df86 clarified store.clean_output: cleanup user_output_dir even in system_mode;
wenzelm
parents: 68219
diff changeset
   287
        }
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   288
      }
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   289
    }
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
   290
48425
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48424
diff changeset
   291
    // scheduler loop
63082
6af03422535a expose Sessions.Info in Build.Results
Lars Hupel <lars.hupel@mytum.de>
parents: 62946
diff changeset
   292
    case class Result(
66594
c16ed3250de0 tuned whitespace;
wenzelm
parents: 66571
diff changeset
   293
      current: Boolean,
68213
wenzelm
parents: 68212
diff changeset
   294
      heap_digest: Option[String],
66594
c16ed3250de0 tuned whitespace;
wenzelm
parents: 66571
diff changeset
   295
      process: Option[Process_Result],
c16ed3250de0 tuned whitespace;
wenzelm
parents: 66571
diff changeset
   296
      info: Sessions.Info)
62402
bff56eae3ec5 more informative Build.build_results;
wenzelm
parents: 62401
diff changeset
   297
    {
bff56eae3ec5 more informative Build.build_results;
wenzelm
parents: 62401
diff changeset
   298
      def ok: Boolean =
bff56eae3ec5 more informative Build.build_results;
wenzelm
parents: 62401
diff changeset
   299
        process match {
bff56eae3ec5 more informative Build.build_results;
wenzelm
parents: 62401
diff changeset
   300
          case None => false
bff56eae3ec5 more informative Build.build_results;
wenzelm
parents: 62401
diff changeset
   301
          case Some(res) => res.rc == 0
bff56eae3ec5 more informative Build.build_results;
wenzelm
parents: 62401
diff changeset
   302
        }
bff56eae3ec5 more informative Build.build_results;
wenzelm
parents: 62401
diff changeset
   303
    }
48639
675988e64bf9 store parent heap stamp as well -- needs to be propagated through the build hierarchy;
wenzelm
parents: 48626
diff changeset
   304
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73055
diff changeset
   305
    def sleep(): Unit =
71727
0cb14b7455ee more careful handling of interrupts, notably for Isabelle/jEdit Scala Console;
wenzelm
parents: 71726
diff changeset
   306
      Isabelle_Thread.interrupt_handler(_ => progress.stop) { Time.seconds(0.5).sleep }
50366
b1dd455593a9 more formal progress context;
wenzelm
parents: 50207
diff changeset
   307
64265
8eb6365f5916 isabelle build -N;
wenzelm
parents: 64173
diff changeset
   308
    val numa_nodes = new NUMA.Nodes(numa_shuffling)
8eb6365f5916 isabelle build -N;
wenzelm
parents: 64173
diff changeset
   309
48425
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48424
diff changeset
   310
    @tailrec def loop(
48676
3ef82491cdd6 clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
wenzelm
parents: 48675
diff changeset
   311
      pending: Queue,
72662
5c08ad7adf77 clarified modules;
wenzelm
parents: 72654
diff changeset
   312
      running: Map[String, (List[String], Build_Job)],
48639
675988e64bf9 store parent heap stamp as well -- needs to be propagated through the build hierarchy;
wenzelm
parents: 48626
diff changeset
   313
      results: Map[String, Result]): Map[String, Result] =
48425
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48424
diff changeset
   314
    {
64265
8eb6365f5916 isabelle build -N;
wenzelm
parents: 64173
diff changeset
   315
      def used_node(i: Int): Boolean =
8eb6365f5916 isabelle build -N;
wenzelm
parents: 64173
diff changeset
   316
        running.iterator.exists(
8eb6365f5916 isabelle build -N;
wenzelm
parents: 64173
diff changeset
   317
          { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
8eb6365f5916 isabelle build -N;
wenzelm
parents: 64173
diff changeset
   318
48425
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48424
diff changeset
   319
      if (pending.is_empty) results
51253
ab4c296a1e60 clarified Progress.stopped: rising edge only;
wenzelm
parents: 51252
diff changeset
   320
      else {
71726
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 71718
diff changeset
   321
        if (progress.stopped) {
51253
ab4c296a1e60 clarified Progress.stopped: rising edge only;
wenzelm
parents: 51252
diff changeset
   322
          for ((_, (_, job)) <- running) job.terminate
71726
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 71718
diff changeset
   323
        }
51253
ab4c296a1e60 clarified Progress.stopped: rising edge only;
wenzelm
parents: 51252
diff changeset
   324
48674
03e88e4619a2 simplified class Job;
wenzelm
parents: 48671
diff changeset
   325
        running.find({ case (_, (_, job)) => job.is_finished }) match {
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   326
          case Some((session_name, (input_heaps, job))) =>
50367
69efe72886e3 allow to terminate jobs via Progress;
wenzelm
parents: 50366
diff changeset
   327
            //{{{ finish job
48424
wenzelm
parents: 48423
diff changeset
   328
68217
3e90b88b0fc2 clarified handling of output heap;
wenzelm
parents: 68216
diff changeset
   329
            val (process_result, heap_digest) = job.join
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48370
diff changeset
   330
71623
b3bddebe44ca clarified signature: more explicit type Protocol_Message.Marker;
wenzelm
parents: 71614
diff changeset
   331
            val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
62404
13a0f537e232 retain tail out_lines as printed, but not the whole log content;
wenzelm
parents: 62403
diff changeset
   332
            val process_result_tail =
13a0f537e232 retain tail out_lines as printed, but not the whole log content;
wenzelm
parents: 62403
diff changeset
   333
            {
62409
e391528eff3b proper option process_output_tail, more generous default;
wenzelm
parents: 62406
diff changeset
   334
              val tail = job.info.options.int("process_output_tail")
62632
cd991ba01ffd clarified modules;
wenzelm
parents: 62631
diff changeset
   335
              process_result.copy(
cd991ba01ffd clarified modules;
wenzelm
parents: 62631
diff changeset
   336
                out_lines =
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   337
                  "(see also " + store.output_log(session_name).file.toString + ")" ::
65294
69100bf4ead4 suppress inlined properties from log output;
wenzelm
parents: 65291
diff changeset
   338
                  (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
62404
13a0f537e232 retain tail out_lines as printed, but not the whole log content;
wenzelm
parents: 62403
diff changeset
   339
            }
13a0f537e232 retain tail out_lines as printed, but not the whole log content;
wenzelm
parents: 62403
diff changeset
   340
72017
wenzelm
parents: 72016
diff changeset
   341
            val build_log =
wenzelm
parents: 72016
diff changeset
   342
              Build_Log.Log_File(session_name, process_result.out_lines).
wenzelm
parents: 72016
diff changeset
   343
                parse_session_info(
wenzelm
parents: 72016
diff changeset
   344
                  command_timings = true,
wenzelm
parents: 72016
diff changeset
   345
                  theory_timings = true,
wenzelm
parents: 72016
diff changeset
   346
                  ml_statistics = true,
wenzelm
parents: 72016
diff changeset
   347
                  task_statistics = true)
66666
1a620647285c clarified messages: after writing all files (see also 27f90319a499 and 57c85c83c11b);
wenzelm
parents: 66595
diff changeset
   348
1a620647285c clarified messages: after writing all files (see also 27f90319a499 and 57c85c83c11b);
wenzelm
parents: 66595
diff changeset
   349
            // write log file
68217
3e90b88b0fc2 clarified handling of output heap;
wenzelm
parents: 68216
diff changeset
   350
            if (process_result.ok) {
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   351
              File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines))
68217
3e90b88b0fc2 clarified handling of output heap;
wenzelm
parents: 68216
diff changeset
   352
            }
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   353
            else File.write(store.output_log(session_name), terminate_lines(log_lines))
65291
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
   354
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
   355
            // write database
72017
wenzelm
parents: 72016
diff changeset
   356
            using(store.open_database(session_name, output = true))(db =>
wenzelm
parents: 72016
diff changeset
   357
              store.write_session_info(db, session_name,
wenzelm
parents: 72016
diff changeset
   358
                build_log =
wenzelm
parents: 72016
diff changeset
   359
                  if (process_result.timeout) build_log.error("Timeout") else build_log,
wenzelm
parents: 72016
diff changeset
   360
                build =
wenzelm
parents: 72016
diff changeset
   361
                  Session_Info(sources_stamp(deps, session_name), input_heaps, heap_digest,
wenzelm
parents: 72016
diff changeset
   362
                    process_result.rc)))
65291
57c85c83c11b maintain persistent session info in SQLite database instead of log file;
wenzelm
parents: 65289
diff changeset
   363
66666
1a620647285c clarified messages: after writing all files (see also 27f90319a499 and 57c85c83c11b);
wenzelm
parents: 66595
diff changeset
   364
            // messages
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71598
diff changeset
   365
            process_result.err_lines.foreach(progress.echo)
66666
1a620647285c clarified messages: after writing all files (see also 27f90319a499 and 57c85c83c11b);
wenzelm
parents: 66595
diff changeset
   366
72013
6a24ecc4ff1b clarified signature;
wenzelm
parents: 72012
diff changeset
   367
            if (process_result.ok) {
72022
45865bb06182 clarified message --- as in former ML version (see 940195fbb282);
wenzelm
parents: 72021
diff changeset
   368
              if (verbose) progress.echo(session_timing(session_name, build_log))
72021
664e90313a54 clarified signature;
wenzelm
parents: 72019
diff changeset
   369
              progress.echo(session_finished(session_name, process_result))
72013
6a24ecc4ff1b clarified signature;
wenzelm
parents: 72012
diff changeset
   370
            }
66666
1a620647285c clarified messages: after writing all files (see also 27f90319a499 and 57c85c83c11b);
wenzelm
parents: 66595
diff changeset
   371
            else {
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   372
              progress.echo(session_name + " FAILED")
66666
1a620647285c clarified messages: after writing all files (see also 27f90319a499 and 57c85c83c11b);
wenzelm
parents: 66595
diff changeset
   373
              if (!process_result.interrupted) progress.echo(process_result_tail.out)
1a620647285c clarified messages: after writing all files (see also 27f90319a499 and 57c85c83c11b);
wenzelm
parents: 66595
diff changeset
   374
            }
1a620647285c clarified messages: after writing all files (see also 27f90319a499 and 57c85c83c11b);
wenzelm
parents: 66595
diff changeset
   375
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   376
            loop(pending - session_name, running - session_name,
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   377
              results +
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   378
                (session_name -> Result(false, heap_digest, Some(process_result_tail), job.info)))
50367
69efe72886e3 allow to terminate jobs via Progress;
wenzelm
parents: 50366
diff changeset
   379
            //}}}
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 60106
diff changeset
   380
          case None if running.size < (max_jobs max 1) =>
50367
69efe72886e3 allow to terminate jobs via Progress;
wenzelm
parents: 50366
diff changeset
   381
            //{{{ check/start next job
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71598
diff changeset
   382
            pending.dequeue(running.isDefinedAt) match {
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   383
              case Some((session_name, info)) =>
66848
982baed14542 clarified signature;
wenzelm
parents: 66841
diff changeset
   384
                val ancestor_results =
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   385
                  deps.sessions_structure.build_requirements(List(session_name)).
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   386
                    filterNot(_ == session_name).map(results(_))
68213
wenzelm
parents: 68212
diff changeset
   387
                val ancestor_heaps = ancestor_results.flatMap(_.heap_digest)
62628
6031191a8d9c record stamps of cumulative input heaps;
wenzelm
parents: 62610
diff changeset
   388
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   389
                val do_store =
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   390
                  build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name)
48547
wenzelm
parents: 48546
diff changeset
   391
68213
wenzelm
parents: 68212
diff changeset
   392
                val (current, heap_digest) =
48547
wenzelm
parents: 48546
diff changeset
   393
                {
72634
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72624
diff changeset
   394
                  store.try_open_database(session_name) match {
68212
5a59fded83c7 clarified heap vs. database operations: discontinued correlation of directory;
wenzelm
parents: 68209
diff changeset
   395
                    case Some(db) =>
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   396
                      using(db)(store.read_build(_, session_name)) match {
68216
wenzelm
parents: 68214
diff changeset
   397
                        case Some(build) =>
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   398
                          val heap_digest = store.find_heap_digest(session_name)
68216
wenzelm
parents: 68214
diff changeset
   399
                          val current =
wenzelm
parents: 68214
diff changeset
   400
                            !fresh_build &&
wenzelm
parents: 68214
diff changeset
   401
                            build.ok &&
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   402
                            build.sources == sources_stamp(deps, session_name) &&
68216
wenzelm
parents: 68214
diff changeset
   403
                            build.input_heaps == ancestor_heaps &&
wenzelm
parents: 68214
diff changeset
   404
                            build.output_heap == heap_digest &&
71614
wenzelm
parents: 71613
diff changeset
   405
                            !(do_store && heap_digest.isEmpty)
68216
wenzelm
parents: 68214
diff changeset
   406
                          (current, heap_digest)
wenzelm
parents: 68214
diff changeset
   407
                        case None => (false, None)
wenzelm
parents: 68214
diff changeset
   408
                      }
62636
e676ae9f1bf6 clarified signature;
wenzelm
parents: 62635
diff changeset
   409
                    case None => (false, None)
48504
21dfd6c04482 actually check source vs. target stamps, based on information from log files;
wenzelm
parents: 48494
diff changeset
   410
                  }
48547
wenzelm
parents: 48546
diff changeset
   411
                }
62628
6031191a8d9c record stamps of cumulative input heaps;
wenzelm
parents: 62610
diff changeset
   412
                val all_current = current && ancestor_results.forall(_.current)
48528
784c6f63d79c proper all_current, which regards parent status as well;
wenzelm
parents: 48511
diff changeset
   413
48547
wenzelm
parents: 48546
diff changeset
   414
                if (all_current)
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   415
                  loop(pending - session_name, running,
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   416
                    results +
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   417
                      (session_name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
48678
ff27af15530c queue ordering by descending outdegree and timeout;
wenzelm
parents: 48676
diff changeset
   418
                else if (no_build) {
71894
wenzelm
parents: 71879
diff changeset
   419
                  progress.echo_if(verbose, "Skipping " + session_name + " ...")
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   420
                  loop(pending - session_name, running,
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   421
                    results +
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   422
                      (session_name -> Result(false, heap_digest, Some(Process_Result(1)), info)))
48678
ff27af15530c queue ordering by descending outdegree and timeout;
wenzelm
parents: 48676
diff changeset
   423
                }
62628
6031191a8d9c record stamps of cumulative input heaps;
wenzelm
parents: 62610
diff changeset
   424
                else if (ancestor_results.forall(_.ok) && !progress.stopped) {
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   425
                  progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
68086
9e1c670301b8 cleanup session output before starting build job;
wenzelm
parents: 67852
diff changeset
   426
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   427
                  store.clean_output(session_name)
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   428
                  using(store.open_database(session_name, output = true))(
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   429
                    store.init_session_info(_, session_name))
68086
9e1c670301b8 cleanup session output before starting build job;
wenzelm
parents: 67852
diff changeset
   430
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71598
diff changeset
   431
                  val numa_node = numa_nodes.next(used_node)
51220
e140c8fa485a recover timing information from old log files;
wenzelm
parents: 51218
diff changeset
   432
                  val job =
72693
0201ae367518 unused;
wenzelm
parents: 72692
diff changeset
   433
                    new Build_Job(progress, session_name, info, deps, store, do_store,
72648
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72640
diff changeset
   434
                      verbose, numa_node, queue.command_timings(session_name))
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   435
                  loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
48547
wenzelm
parents: 48546
diff changeset
   436
                }
wenzelm
parents: 48546
diff changeset
   437
                else {
71669
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   438
                  progress.echo(session_name + " CANCELLED")
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   439
                  loop(pending - session_name, running,
12ebd8d0deee tuned signature;
wenzelm
parents: 71668
diff changeset
   440
                    results + (session_name -> Result(false, heap_digest, None, info)))
48547
wenzelm
parents: 48546
diff changeset
   441
                }
wenzelm
parents: 48546
diff changeset
   442
              case None => sleep(); loop(pending, running, results)
48425
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48424
diff changeset
   443
            }
50367
69efe72886e3 allow to terminate jobs via Progress;
wenzelm
parents: 50366
diff changeset
   444
            ///}}}
48425
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48424
diff changeset
   445
          case None => sleep(); loop(pending, running, results)
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48370
diff changeset
   446
        }
51253
ab4c296a1e60 clarified Progress.stopped: rising edge only;
wenzelm
parents: 51252
diff changeset
   447
      }
48425
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48424
diff changeset
   448
    }
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48424
diff changeset
   449
51220
e140c8fa485a recover timing information from old log files;
wenzelm
parents: 51218
diff changeset
   450
e140c8fa485a recover timing information from old log files;
wenzelm
parents: 51218
diff changeset
   451
    /* build results */
e140c8fa485a recover timing information from old log files;
wenzelm
parents: 51218
diff changeset
   452
72673
8ff7a0e394f9 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents: 72662
diff changeset
   453
    val results =
8ff7a0e394f9 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents: 72662
diff changeset
   454
    {
8ff7a0e394f9 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents: 72662
diff changeset
   455
      val results0 =
8ff7a0e394f9 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents: 72662
diff changeset
   456
        if (deps.is_empty) {
8ff7a0e394f9 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents: 72662
diff changeset
   457
          progress.echo_warning("Nothing to build")
8ff7a0e394f9 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents: 72662
diff changeset
   458
          Map.empty[String, Result]
8ff7a0e394f9 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents: 72662
diff changeset
   459
        }
8ff7a0e394f9 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents: 72662
diff changeset
   460
        else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) }
48583
ed975dbb16ca tuned messages;
wenzelm
parents: 48579
diff changeset
   461
64265
8eb6365f5916 isabelle build -N;
wenzelm
parents: 64173
diff changeset
   462
      new Results(
8eb6365f5916 isabelle build -N;
wenzelm
parents: 64173
diff changeset
   463
        (for ((name, result) <- results0.iterator)
8eb6365f5916 isabelle build -N;
wenzelm
parents: 64173
diff changeset
   464
          yield (name, (result.process, result.info))).toMap)
72673
8ff7a0e394f9 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents: 72662
diff changeset
   465
    }
62641
0b1b7465f2ef always build with full results;
wenzelm
parents: 62638
diff changeset
   466
69811
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69777
diff changeset
   467
    if (export_files) {
71896
ce06d6456cc8 clarified signature --- fit within limit of 22 arguments;
wenzelm
parents: 71895
diff changeset
   468
      for (name <- full_sessions.imports_selection(selection).iterator if results(name).ok) {
69811
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69777
diff changeset
   469
        val info = results.info(name)
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69777
diff changeset
   470
        if (info.export_files.nonEmpty) {
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69777
diff changeset
   471
          progress.echo("Exporting " + info.name + " ...")
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69777
diff changeset
   472
          for ((dir, prune, pats) <- info.export_files) {
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69777
diff changeset
   473
            Export.export_files(store, name, info.dir + dir,
71726
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 71718
diff changeset
   474
              progress = if (verbose) progress else new Progress,
69811
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69777
diff changeset
   475
              export_prune = prune,
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69777
diff changeset
   476
              export_patterns = pats)
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69777
diff changeset
   477
          }
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69777
diff changeset
   478
        }
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69777
diff changeset
   479
      }
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69777
diff changeset
   480
    }
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69777
diff changeset
   481
62641
0b1b7465f2ef always build with full results;
wenzelm
parents: 62638
diff changeset
   482
    if (results.rc != 0 && (verbose || !no_build)) {
0b1b7465f2ef always build with full results;
wenzelm
parents: 62638
diff changeset
   483
      val unfinished =
0b1b7465f2ef always build with full results;
wenzelm
parents: 62638
diff changeset
   484
        (for {
0b1b7465f2ef always build with full results;
wenzelm
parents: 62638
diff changeset
   485
          name <- results.sessions.iterator
0b1b7465f2ef always build with full results;
wenzelm
parents: 62638
diff changeset
   486
          if !results(name).ok
0b1b7465f2ef always build with full results;
wenzelm
parents: 62638
diff changeset
   487
         } yield name).toList.sorted
0b1b7465f2ef always build with full results;
wenzelm
parents: 62638
diff changeset
   488
      progress.echo("Unfinished session(s): " + commas(unfinished))
0b1b7465f2ef always build with full results;
wenzelm
parents: 62638
diff changeset
   489
    }
0b1b7465f2ef always build with full results;
wenzelm
parents: 62638
diff changeset
   490
51418
7b8ce8403340 more accurate handling of global browser info at the very end (without races), subject to no_build and info.browser_info;
wenzelm
parents: 51402
diff changeset
   491
72673
8ff7a0e394f9 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents: 72662
diff changeset
   492
    /* PDF/HTML presentation */
51418
7b8ce8403340 more accurate handling of global browser info at the very end (without races), subject to no_build and info.browser_info;
wenzelm
parents: 51402
diff changeset
   493
72677
86fac52c2795 more interrupts;
wenzelm
parents: 72676
diff changeset
   494
    if (!no_build && !progress.stopped && results.ok) {
73012
238ddf525da4 clarified HTML presentation, e.g. avoid bulky jobs like HOL or HOL-Analysis in applications;
wenzelm
parents: 72993
diff changeset
   495
      val selected = full_sessions_selection.toSet
72673
8ff7a0e394f9 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents: 72662
diff changeset
   496
      val presentation_chapters =
72674
a9fea3f11cc0 clarified messages;
wenzelm
parents: 72673
diff changeset
   497
        (for {
a9fea3f11cc0 clarified messages;
wenzelm
parents: 72673
diff changeset
   498
          session_name <- deps.sessions_structure.build_topological_order.iterator
a9fea3f11cc0 clarified messages;
wenzelm
parents: 72673
diff changeset
   499
          info = results.info(session_name)
73012
238ddf525da4 clarified HTML presentation, e.g. avoid bulky jobs like HOL or HOL-Analysis in applications;
wenzelm
parents: 72993
diff changeset
   500
          if selected(session_name) && presentation.enabled(info) && results(session_name).ok }
72676
1cbf36ac4d0b clarified messages;
wenzelm
parents: 72674
diff changeset
   501
        yield (info.chapter, (session_name, info.description))).toList
1cbf36ac4d0b clarified messages;
wenzelm
parents: 72674
diff changeset
   502
1cbf36ac4d0b clarified messages;
wenzelm
parents: 72674
diff changeset
   503
      if (presentation_chapters.nonEmpty) {
1cbf36ac4d0b clarified messages;
wenzelm
parents: 72674
diff changeset
   504
        val presentation_dir = presentation.dir(store)
1cbf36ac4d0b clarified messages;
wenzelm
parents: 72674
diff changeset
   505
        progress.echo("Presentation in " + presentation_dir.absolute)
1cbf36ac4d0b clarified messages;
wenzelm
parents: 72674
diff changeset
   506
72962
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72854
diff changeset
   507
        val resources = Resources.empty
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72854
diff changeset
   508
        val html_context = Presentation.html_context()
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72854
diff changeset
   509
72854
6c660f05f70c clarified signature;
wenzelm
parents: 72763
diff changeset
   510
        using(store.open_database_context())(db_context =>
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72677
diff changeset
   511
          for ((_, (session_name, _)) <- presentation_chapters) {
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72677
diff changeset
   512
            progress.expose_interrupt()
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72677
diff changeset
   513
            progress.echo("Presenting " + session_name + " ...")
72962
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72854
diff changeset
   514
            Presentation.session_html(
73022
38528017e4c8 more verbosity for potentially bulky presentation;
wenzelm
parents: 73012
diff changeset
   515
              resources, session_name, deps, db_context, progress = progress,
73036
b028e8d22d8d clarified HTML presentation elements;
wenzelm
parents: 73022
diff changeset
   516
              verbose = verbose, html_context = html_context,
73055
3e4df2e689ff clarified signature;
wenzelm
parents: 73036
diff changeset
   517
              elements = Presentation.elements1, presentation = presentation)
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72677
diff changeset
   518
          })
72676
1cbf36ac4d0b clarified messages;
wenzelm
parents: 72674
diff changeset
   519
1cbf36ac4d0b clarified messages;
wenzelm
parents: 72674
diff changeset
   520
        val browser_chapters =
1cbf36ac4d0b clarified messages;
wenzelm
parents: 72674
diff changeset
   521
          presentation_chapters.groupBy(_._1).
1cbf36ac4d0b clarified messages;
wenzelm
parents: 72674
diff changeset
   522
            map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
72673
8ff7a0e394f9 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents: 72662
diff changeset
   523
72676
1cbf36ac4d0b clarified messages;
wenzelm
parents: 72674
diff changeset
   524
        for ((chapter, entries) <- browser_chapters)
1cbf36ac4d0b clarified messages;
wenzelm
parents: 72674
diff changeset
   525
          Presentation.update_chapter_index(presentation_dir, chapter, entries)
72648
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72640
diff changeset
   526
72676
1cbf36ac4d0b clarified messages;
wenzelm
parents: 72674
diff changeset
   527
        if (browser_chapters.nonEmpty) Presentation.make_global_index(presentation_dir)
1cbf36ac4d0b clarified messages;
wenzelm
parents: 72674
diff changeset
   528
      }
51418
7b8ce8403340 more accurate handling of global browser info at the very end (without races), subject to no_build and info.browser_info;
wenzelm
parents: 51402
diff changeset
   529
    }
7b8ce8403340 more accurate handling of global browser info at the very end (without races), subject to no_build and info.browser_info;
wenzelm
parents: 51402
diff changeset
   530
62641
0b1b7465f2ef always build with full results;
wenzelm
parents: 62638
diff changeset
   531
    results
48341
752de4e10162 tuned source structure;
wenzelm
parents: 48340
diff changeset
   532
  }
752de4e10162 tuned source structure;
wenzelm
parents: 48340
diff changeset
   533
752de4e10162 tuned source structure;
wenzelm
parents: 48340
diff changeset
   534
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   535
  /* Isabelle tool wrapper */
48341
752de4e10162 tuned source structure;
wenzelm
parents: 48340
diff changeset
   536
72763
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72728
diff changeset
   537
  val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions",
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72728
diff changeset
   538
    Scala_Project.here, args =>
48341
752de4e10162 tuned source structure;
wenzelm
parents: 48340
diff changeset
   539
  {
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   540
    val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
62590
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   541
66737
2edc0c42c883 option -B for "isabelle build" and "isabelle imports";
wenzelm
parents: 66736
diff changeset
   542
    var base_sessions: List[String] = Nil
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   543
    var select_dirs: List[Path] = Nil
64265
8eb6365f5916 isabelle build -N;
wenzelm
parents: 64173
diff changeset
   544
    var numa_shuffling = false
72652
07edf1952ab1 clarified modules;
wenzelm
parents: 72648
diff changeset
   545
    var presentation = Presentation.Context.none
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   546
    var requirements = false
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   547
    var soft_build = false
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   548
    var exclude_session_groups: List[String] = Nil
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   549
    var all_sessions = false
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   550
    var build_heap = false
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   551
    var clean_build = false
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   552
    var dirs: List[Path] = Nil
69811
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69777
diff changeset
   553
    var export_files = false
66841
5c32a072ca8b added isablle build option -f;
wenzelm
parents: 66822
diff changeset
   554
    var fresh_build = false
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   555
    var session_groups: List[String] = Nil
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   556
    var max_jobs = 1
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   557
    var check_keywords: Set[String] = Set.empty
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   558
    var list_files = false
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   559
    var no_build = false
67847
c61acb4855b6 tuned signature;
wenzelm
parents: 67846
diff changeset
   560
    var options = Options.init(opts = build_options)
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   561
    var verbose = false
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   562
    var exclude_sessions: List[String] = Nil
62590
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   563
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   564
    val getopts = Getopts("""
62590
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   565
Usage: isabelle build [OPTIONS] [SESSIONS ...]
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   566
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   567
  Options are:
66737
2edc0c42c883 option -B for "isabelle build" and "isabelle imports";
wenzelm
parents: 66736
diff changeset
   568
    -B NAME      include session NAME and all descendants
62590
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   569
    -D DIR       include session directory and select its sessions
64265
8eb6365f5916 isabelle build -N;
wenzelm
parents: 64173
diff changeset
   570
    -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
72648
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72640
diff changeset
   571
    -P DIR       enable HTML/PDF presentation in directory (":" for default)
71807
cdfa8f027bb9 tuned messages;
wenzelm
parents: 71727
diff changeset
   572
    -R           refer to requirements of selected sessions
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   573
    -S           soft build: only observe changes of sources, not heap images
62590
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   574
    -X NAME      exclude sessions from group NAME and all descendants
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   575
    -a           select all sessions
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   576
    -b           build heap images
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   577
    -c           clean build
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   578
    -d DIR       include session directory
69811
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69777
diff changeset
   579
    -e           export files from session specification into file-system
66841
5c32a072ca8b added isablle build option -f;
wenzelm
parents: 66822
diff changeset
   580
    -f           fresh build
62590
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   581
    -g NAME      select session group NAME
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   582
    -j INT       maximum number of parallel jobs (default 1)
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   583
    -k KEYWORD   check theory sources for conflicts with proposed keywords
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   584
    -l           list session source files
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   585
    -n           no build -- test dependencies only
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   586
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   587
    -v           verbose
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   588
    -x NAME      exclude session NAME and all descendants
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   589
62596
cf79f8866bc3 tuned messages;
wenzelm
parents: 62595
diff changeset
   590
  Build and manage Isabelle sessions, depending on implicit settings:
cf79f8866bc3 tuned messages;
wenzelm
parents: 62595
diff changeset
   591
71992
c8c3f4f0f68b clarified log message (more uniform);
wenzelm
parents: 71982
diff changeset
   592
""" + Library.prefix_lines("  ",  Build_Log.Settings.show()) + "\n",
66737
2edc0c42c883 option -B for "isabelle build" and "isabelle imports";
wenzelm
parents: 66736
diff changeset
   593
      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   594
      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
64265
8eb6365f5916 isabelle build -N;
wenzelm
parents: 64173
diff changeset
   595
      "N" -> (_ => numa_shuffling = true),
72652
07edf1952ab1 clarified modules;
wenzelm
parents: 72648
diff changeset
   596
      "P:" -> (arg => presentation = Presentation.Context.make(arg)),
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   597
      "R" -> (_ => requirements = true),
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   598
      "S" -> (_ => soft_build = true),
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   599
      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   600
      "a" -> (_ => all_sessions = true),
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   601
      "b" -> (_ => build_heap = true),
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   602
      "c" -> (_ => clean_build = true),
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   603
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
69811
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69777
diff changeset
   604
      "e" -> (_ => export_files = true),
66841
5c32a072ca8b added isablle build option -f;
wenzelm
parents: 66822
diff changeset
   605
      "f" -> (_ => fresh_build = true),
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   606
      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
63805
c272680df665 clarified modules;
wenzelm
parents: 63685
diff changeset
   607
      "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   608
      "k:" -> (arg => check_keywords = check_keywords + arg),
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   609
      "l" -> (_ => list_files = true),
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   610
      "n" -> (_ => no_build = true),
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   611
      "o:" -> (arg => options = options + arg),
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   612
      "v" -> (_ => verbose = true),
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   613
      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
62590
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   614
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   615
    val sessions = getopts(args)
62590
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   616
64115
wenzelm
parents: 64082
diff changeset
   617
    val progress = new Console_Progress(verbose = verbose)
62590
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   618
64140
96d398871124 modernized date format;
wenzelm
parents: 64115
diff changeset
   619
    val start_date = Date.now()
96d398871124 modernized date format;
wenzelm
parents: 64115
diff changeset
   620
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   621
    if (verbose) {
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   622
      progress.echo(
64155
646c4d6a6a02 tuned signature;
wenzelm
parents: 64140
diff changeset
   623
        "Started at " + Build_Log.print_date(start_date) +
64140
96d398871124 modernized date format;
wenzelm
parents: 64115
diff changeset
   624
          " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
64081
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
   625
      progress.echo(Build_Log.Settings.show() + "\n")
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   626
    }
62590
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   627
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   628
    val results =
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   629
      progress.interrupt_handler {
67846
wenzelm
parents: 67835
diff changeset
   630
        build(options,
71981
0be06f99b210 clarified signature;
wenzelm
parents: 71978
diff changeset
   631
          selection = Sessions.Selection(
71896
ce06d6456cc8 clarified signature --- fit within limit of 22 arguments;
wenzelm
parents: 71895
diff changeset
   632
            requirements = requirements,
ce06d6456cc8 clarified signature --- fit within limit of 22 arguments;
wenzelm
parents: 71895
diff changeset
   633
            all_sessions = all_sessions,
ce06d6456cc8 clarified signature --- fit within limit of 22 arguments;
wenzelm
parents: 71895
diff changeset
   634
            base_sessions = base_sessions,
ce06d6456cc8 clarified signature --- fit within limit of 22 arguments;
wenzelm
parents: 71895
diff changeset
   635
            exclude_session_groups = exclude_session_groups,
ce06d6456cc8 clarified signature --- fit within limit of 22 arguments;
wenzelm
parents: 71895
diff changeset
   636
            exclude_sessions = exclude_sessions,
ce06d6456cc8 clarified signature --- fit within limit of 22 arguments;
wenzelm
parents: 71895
diff changeset
   637
            session_groups = session_groups,
ce06d6456cc8 clarified signature --- fit within limit of 22 arguments;
wenzelm
parents: 71895
diff changeset
   638
            sessions = sessions),
72648
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72640
diff changeset
   639
          presentation = presentation,
67846
wenzelm
parents: 67835
diff changeset
   640
          progress = progress,
65832
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65831
diff changeset
   641
          check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
63224
78e93610a3c8 more flexible build_selection;
wenzelm
parents: 63082
diff changeset
   642
          build_heap = build_heap,
78e93610a3c8 more flexible build_selection;
wenzelm
parents: 63082
diff changeset
   643
          clean_build = clean_build,
78e93610a3c8 more flexible build_selection;
wenzelm
parents: 63082
diff changeset
   644
          dirs = dirs,
78e93610a3c8 more flexible build_selection;
wenzelm
parents: 63082
diff changeset
   645
          select_dirs = select_dirs,
65831
3b197547c1d4 prefer explicit progress channel;
wenzelm
parents: 65828
diff changeset
   646
          numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
63224
78e93610a3c8 more flexible build_selection;
wenzelm
parents: 63082
diff changeset
   647
          max_jobs = max_jobs,
78e93610a3c8 more flexible build_selection;
wenzelm
parents: 63082
diff changeset
   648
          list_files = list_files,
78e93610a3c8 more flexible build_selection;
wenzelm
parents: 63082
diff changeset
   649
          check_keywords = check_keywords,
66841
5c32a072ca8b added isablle build option -f;
wenzelm
parents: 66822
diff changeset
   650
          fresh_build = fresh_build,
63224
78e93610a3c8 more flexible build_selection;
wenzelm
parents: 63082
diff changeset
   651
          no_build = no_build,
66745
e7ac579b883c option -S for "isabelle build";
wenzelm
parents: 66744
diff changeset
   652
          soft_build = soft_build,
63224
78e93610a3c8 more flexible build_selection;
wenzelm
parents: 63082
diff changeset
   653
          verbose = verbose,
71896
ce06d6456cc8 clarified signature --- fit within limit of 22 arguments;
wenzelm
parents: 71895
diff changeset
   654
          export_files = export_files)
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   655
      }
64140
96d398871124 modernized date format;
wenzelm
parents: 64115
diff changeset
   656
    val end_date = Date.now()
96d398871124 modernized date format;
wenzelm
parents: 64115
diff changeset
   657
    val elapsed_time = end_date.time - start_date.time
62590
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   658
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   659
    if (verbose) {
64155
646c4d6a6a02 tuned signature;
wenzelm
parents: 64140
diff changeset
   660
      progress.echo("\nFinished at " + Build_Log.print_date(end_date))
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   661
    }
62590
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   662
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   663
    val total_timing =
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73344
diff changeset
   664
      results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   665
        copy(elapsed = elapsed_time)
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   666
    progress.echo(total_timing.message_resources)
62590
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62573
diff changeset
   667
62833
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   668
    sys.exit(results.rc)
29dfa2ed9343 prefer internal tool;
wenzelm
parents: 62825
diff changeset
   669
  })
68305
5321218147d3 clarified signature;
wenzelm
parents: 68292
diff changeset
   670
5321218147d3 clarified signature;
wenzelm
parents: 68292
diff changeset
   671
5321218147d3 clarified signature;
wenzelm
parents: 68292
diff changeset
   672
  /* build logic image */
5321218147d3 clarified signature;
wenzelm
parents: 68292
diff changeset
   673
5321218147d3 clarified signature;
wenzelm
parents: 68292
diff changeset
   674
  def build_logic(options: Options, logic: String,
71726
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 71718
diff changeset
   675
    progress: Progress = new Progress,
68305
5321218147d3 clarified signature;
wenzelm
parents: 68292
diff changeset
   676
    build_heap: Boolean = false,
5321218147d3 clarified signature;
wenzelm
parents: 68292
diff changeset
   677
    dirs: List[Path] = Nil,
70791
02edce6f0c71 clarified signature: more options;
wenzelm
parents: 70712
diff changeset
   678
    fresh: Boolean = false,
69540
a1e8bcda8cec tuned signature;
wenzelm
parents: 69369
diff changeset
   679
    strict: Boolean = false): Int =
68305
5321218147d3 clarified signature;
wenzelm
parents: 68292
diff changeset
   680
  {
71896
ce06d6456cc8 clarified signature --- fit within limit of 22 arguments;
wenzelm
parents: 71895
diff changeset
   681
    val selection = Sessions.Selection.session(logic)
69540
a1e8bcda8cec tuned signature;
wenzelm
parents: 69369
diff changeset
   682
    val rc =
71981
0be06f99b210 clarified signature;
wenzelm
parents: 71978
diff changeset
   683
      if (!fresh && build(options, selection = selection,
0be06f99b210 clarified signature;
wenzelm
parents: 71978
diff changeset
   684
            build_heap = build_heap, no_build = true, dirs = dirs).ok) 0
69540
a1e8bcda8cec tuned signature;
wenzelm
parents: 69369
diff changeset
   685
      else {
a1e8bcda8cec tuned signature;
wenzelm
parents: 69369
diff changeset
   686
        progress.echo("Build started for Isabelle/" + logic + " ...")
71981
0be06f99b210 clarified signature;
wenzelm
parents: 71978
diff changeset
   687
        Build.build(options, selection = selection, progress = progress,
0be06f99b210 clarified signature;
wenzelm
parents: 71978
diff changeset
   688
          build_heap = build_heap, fresh_build = fresh, dirs = dirs).rc
69540
a1e8bcda8cec tuned signature;
wenzelm
parents: 69369
diff changeset
   689
      }
a1e8bcda8cec tuned signature;
wenzelm
parents: 69369
diff changeset
   690
    if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc
68305
5321218147d3 clarified signature;
wenzelm
parents: 68292
diff changeset
   691
  }
48276
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   692
}