author | wenzelm |
Sun, 26 Feb 2023 11:55:24 +0100 | |
changeset 77372 | 44fe9fe96130 |
parent 77371 | 84ca5e036897 |
child 77396 | f184fbac99bc |
permissions | -rw-r--r-- |
72662 | 1 |
/* Title: Pure/Tools/build_job.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Build job running prover process, with rudimentary PIDE session. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
import scala.collection.mutable |
|
76087 | 11 |
import scala.util.matching.Regex |
72662 | 12 |
|
13 |
||
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
14 |
trait Build_Job { |
77349
5a84de89170d
more operations to support management of jobs, e.g. from external database;
wenzelm
parents:
77298
diff
changeset
|
15 |
def job_name: String |
77372 | 16 |
def node_info: Build_Job.Node_Info |
77298 | 17 |
def start(): Unit = () |
18 |
def terminate(): Unit = () |
|
19 |
def is_finished: Boolean = false |
|
20 |
def join: Process_Result = Process_Result.undefined |
|
77372 | 21 |
def make_abstract: Build_Job.Abstract = Build_Job.Abstract(job_name, node_info) |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
22 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
23 |
|
75393 | 24 |
object Build_Job { |
77372 | 25 |
object Node_Info { def none: Node_Info = Node_Info("", None) } |
26 |
sealed case class Node_Info(hostname: String, numa_node: Option[Int]) |
|
27 |
||
28 |
sealed case class Result(node_info: Node_Info, process_result: Process_Result) { |
|
29 |
def ok: Boolean = process_result.ok |
|
30 |
} |
|
31 |
||
77371 | 32 |
sealed case class Abstract( |
77349
5a84de89170d
more operations to support management of jobs, e.g. from external database;
wenzelm
parents:
77298
diff
changeset
|
33 |
override val job_name: String, |
77372 | 34 |
override val node_info: Node_Info |
77349
5a84de89170d
more operations to support management of jobs, e.g. from external database;
wenzelm
parents:
77298
diff
changeset
|
35 |
) extends Build_Job { |
5a84de89170d
more operations to support management of jobs, e.g. from external database;
wenzelm
parents:
77298
diff
changeset
|
36 |
override def make_abstract: Abstract = this |
5a84de89170d
more operations to support management of jobs, e.g. from external database;
wenzelm
parents:
77298
diff
changeset
|
37 |
} |
5a84de89170d
more operations to support management of jobs, e.g. from external database;
wenzelm
parents:
77298
diff
changeset
|
38 |
|
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
39 |
class Build_Session(progress: Progress, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
40 |
session_background: Sessions.Background, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
41 |
store: Sessions.Store, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
42 |
val do_store: Boolean, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
43 |
resources: Resources, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
44 |
session_setup: (String, Session) => Unit, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
45 |
val input_heaps: SHA1.Shasum, |
77372 | 46 |
override val node_info: Node_Info |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
47 |
) extends Build_Job { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
48 |
def session_name: String = session_background.session_name |
77349
5a84de89170d
more operations to support management of jobs, e.g. from external database;
wenzelm
parents:
77298
diff
changeset
|
49 |
def job_name: String = session_name |
5a84de89170d
more operations to support management of jobs, e.g. from external database;
wenzelm
parents:
77298
diff
changeset
|
50 |
|
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
51 |
val info: Sessions.Info = session_background.sessions_structure(session_name) |
77372 | 52 |
val options: Options = NUMA.policy_options(info.options, node_info.numa_node) |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
53 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
54 |
val session_sources: Sessions.Sources = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
55 |
Sessions.Sources.load(session_background.base, cache = store.cache.compress) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
56 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
57 |
private lazy val future_result: Future[Process_Result] = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
58 |
Future.thread("build", uninterruptible = true) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
59 |
val parent = info.parent.getOrElse("") |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
60 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
61 |
val env = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
62 |
Isabelle_System.settings( |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
63 |
List("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
64 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
65 |
val is_pure = Sessions.is_pure(session_name) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
66 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
67 |
val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
68 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
69 |
val eval_store = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
70 |
if (do_store) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
71 |
(if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) ::: |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
72 |
List("ML_Heap.save_child " + |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
73 |
ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name)))) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
74 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
75 |
else Nil |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
76 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
77 |
def session_blobs(node_name: Document.Node.Name): List[(Command.Blob, Document.Blobs.Item)] = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
78 |
session_background.base.theory_load_commands.get(node_name.theory) match { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
79 |
case None => Nil |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
80 |
case Some(spans) => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
81 |
val syntax = session_background.base.theory_syntax(node_name) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
82 |
val master_dir = Path.explode(node_name.master_dir) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
83 |
for (span <- spans; file <- span.loaded_files(syntax).files) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
84 |
yield { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
85 |
val src_path = Path.explode(file) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
86 |
val blob_name = Document.Node.Name(File.symbolic_path(master_dir + src_path)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
87 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
88 |
val bytes = session_sources(blob_name.node).bytes |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
89 |
val text = bytes.text |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
90 |
val chunk = Symbol.Text_Chunk(text) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
91 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
92 |
Command.Blob(blob_name, src_path, Some((SHA1.digest(bytes), chunk))) -> |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
93 |
Document.Blobs.Item(bytes, text, chunk, changed = false) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
94 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
95 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
96 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
97 |
val session = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
98 |
new Session(options, resources) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
99 |
override val cache: Term.Cache = store.cache |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
100 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
101 |
override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
102 |
Command.Blobs_Info.make(session_blobs(node_name)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
103 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
104 |
override def build_blobs(node_name: Document.Node.Name): Document.Blobs = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
105 |
Document.Blobs.make(session_blobs(node_name)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
106 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
107 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
108 |
object Build_Session_Errors { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
109 |
private val promise: Promise[List[String]] = Future.promise |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
110 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
111 |
def result: Exn.Result[List[String]] = promise.join_result |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
112 |
def cancel(): Unit = promise.cancel() |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
113 |
def apply(errs: List[String]): Unit = { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
114 |
try { promise.fulfill(errs) } |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
115 |
catch { case _: IllegalStateException => } |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
116 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
117 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
118 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
119 |
val export_consumer = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
120 |
Export.consumer(store.open_database(session_name, output = true), store.cache, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
121 |
progress = progress) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
122 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
123 |
val stdout = new StringBuilder(1000) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
124 |
val stderr = new StringBuilder(1000) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
125 |
val command_timings = new mutable.ListBuffer[Properties.T] |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
126 |
val theory_timings = new mutable.ListBuffer[Properties.T] |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
127 |
val session_timings = new mutable.ListBuffer[Properties.T] |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
128 |
val runtime_statistics = new mutable.ListBuffer[Properties.T] |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
129 |
val task_statistics = new mutable.ListBuffer[Properties.T] |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
130 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
131 |
def fun( |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
132 |
name: String, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
133 |
acc: mutable.ListBuffer[Properties.T], |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
134 |
unapply: Properties.T => Option[Properties.T] |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
135 |
): (String, Session.Protocol_Function) = { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
136 |
name -> ((msg: Prover.Protocol_Output) => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
137 |
unapply(msg.properties) match { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
138 |
case Some(props) => acc += props; true |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
139 |
case _ => false |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
140 |
}) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
141 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
142 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
143 |
session.init_protocol_handler(new Session.Protocol_Handler { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
144 |
override def exit(): Unit = Build_Session_Errors.cancel() |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
145 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
146 |
private def build_session_finished(msg: Prover.Protocol_Output): Boolean = { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
147 |
val (rc, errors) = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
148 |
try { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
149 |
val (rc, errs) = { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
150 |
import XML.Decode._ |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
151 |
pair(int, list(x => x))(Symbol.decode_yxml(msg.text)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
152 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
153 |
val errors = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
154 |
for (err <- errs) yield { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
155 |
val prt = Protocol_Message.expose_no_reports(err) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
156 |
Pretty.string_of(prt, metric = Symbol.Metric) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
157 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
158 |
(rc, errors) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
159 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
160 |
catch { case ERROR(err) => (Process_Result.RC.failure, List(err)) } |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
161 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
162 |
session.protocol_command("Prover.stop", rc.toString) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
163 |
Build_Session_Errors(errors) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
164 |
true |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
165 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
166 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
167 |
private def loading_theory(msg: Prover.Protocol_Output): Boolean = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
168 |
msg.properties match { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
169 |
case Markup.Loading_Theory(Markup.Name(name)) => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
170 |
progress.theory(Progress.Theory(name, session = session_name)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
171 |
false |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
172 |
case _ => false |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
173 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
174 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
175 |
private def export_(msg: Prover.Protocol_Output): Boolean = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
176 |
msg.properties match { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
177 |
case Protocol.Export(args) => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
178 |
export_consumer.make_entry(session_name, args, msg.chunk) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
179 |
true |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
180 |
case _ => false |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
181 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
182 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
183 |
override val functions: Session.Protocol_Functions = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
184 |
List( |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
185 |
Markup.Build_Session_Finished.name -> build_session_finished, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
186 |
Markup.Loading_Theory.name -> loading_theory, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
187 |
Markup.EXPORT -> export_, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
188 |
fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply), |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
189 |
fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply), |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
190 |
fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
191 |
}) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
192 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
193 |
session.command_timings += Session.Consumer("command_timings") { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
194 |
case Session.Command_Timing(props) => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
195 |
for { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
196 |
elapsed <- Markup.Elapsed.unapply(props) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
197 |
elapsed_time = Time.seconds(elapsed) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
198 |
if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold") |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
199 |
} command_timings += props.filter(Markup.command_timing_property) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
200 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
201 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
202 |
session.runtime_statistics += Session.Consumer("ML_statistics") { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
203 |
case Session.Runtime_Statistics(props) => runtime_statistics += props |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
204 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
205 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
206 |
session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories") { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
207 |
case snapshot => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
208 |
if (!progress.stopped) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
209 |
def export_(name: String, xml: XML.Body, compress: Boolean = true): Unit = { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
210 |
if (!progress.stopped) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
211 |
val theory_name = snapshot.node_name.theory |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
212 |
val args = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
213 |
Protocol.Export.Args(theory_name = theory_name, name = name, compress = compress) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
214 |
val body = Bytes(Symbol.encode(YXML.string_of_body(xml))) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
215 |
export_consumer.make_entry(session_name, args, body) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
216 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
217 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
218 |
def export_text(name: String, text: String, compress: Boolean = true): Unit = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
219 |
export_(name, List(XML.Text(text)), compress = compress) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
220 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
221 |
for (command <- snapshot.snippet_command) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
222 |
export_text(Export.DOCUMENT_ID, command.id.toString, compress = false) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
223 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
224 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
225 |
export_text(Export.FILES, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
226 |
cat_lines(snapshot.node_files.map(name => File.symbolic_path(name.path))), |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
227 |
compress = false) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
228 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
229 |
for ((blob_name, i) <- snapshot.node_files.tail.zipWithIndex) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
230 |
val xml = snapshot.switch(blob_name).xml_markup() |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
231 |
export_(Export.MARKUP + (i + 1), xml) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
232 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
233 |
export_(Export.MARKUP, snapshot.xml_markup()) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
234 |
export_(Export.MESSAGES, snapshot.messages.map(_._1)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
235 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
236 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
237 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
238 |
session.all_messages += Session.Consumer[Any]("build_session_output") { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
239 |
case msg: Prover.Output => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
240 |
val message = msg.message |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
241 |
if (msg.is_system) resources.log(Protocol.message_text(message)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
242 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
243 |
if (msg.is_stdout) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
244 |
stdout ++= Symbol.encode(XML.content(message)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
245 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
246 |
else if (msg.is_stderr) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
247 |
stderr ++= Symbol.encode(XML.content(message)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
248 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
249 |
else if (msg.is_exit) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
250 |
val err = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
251 |
"Prover terminated" + |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
252 |
(msg.properties match { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
253 |
case Markup.Process_Result(result) => ": " + result.print_rc |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
254 |
case _ => "" |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
255 |
}) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
256 |
Build_Session_Errors(List(err)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
257 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
258 |
case _ => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
259 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
260 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
261 |
session_setup(session_name, session) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
262 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
263 |
val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
264 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
265 |
val process = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
266 |
Isabelle_Process.start(store, options, session, session_background, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
267 |
logic = parent, raw_ml_system = is_pure, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
268 |
use_prelude = use_prelude, eval_main = eval_main, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
269 |
cwd = info.dir.file, env = env) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
270 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
271 |
val build_errors = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
272 |
Isabelle_Thread.interrupt_handler(_ => process.terminate()) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
273 |
Exn.capture { process.await_startup() } match { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
274 |
case Exn.Res(_) => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
275 |
val resources_yxml = resources.init_session_yxml |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
276 |
val encode_options: XML.Encode.T[Options] = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
277 |
options => session.prover_options(options).encode |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
278 |
val args_yxml = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
279 |
YXML.string_of_body( |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
280 |
{ |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
281 |
import XML.Encode._ |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
282 |
pair(string, list(pair(encode_options, list(pair(string, properties)))))( |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
283 |
(session_name, info.theories)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
284 |
}) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
285 |
session.protocol_command("build_session", resources_yxml, args_yxml) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
286 |
Build_Session_Errors.result |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
287 |
case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn))) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
288 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
289 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
290 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
291 |
val process_result = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
292 |
Isabelle_Thread.interrupt_handler(_ => process.terminate()) { process.await_shutdown() } |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
293 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
294 |
session.stop() |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
295 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
296 |
val export_errors = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
297 |
export_consumer.shutdown(close = true).map(Output.error_message_text) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
298 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
299 |
val (document_output, document_errors) = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
300 |
try { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
301 |
if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
302 |
using(Export.open_database_context(store)) { database_context => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
303 |
val documents = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
304 |
using(database_context.open_session(session_background)) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
305 |
session_context => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
306 |
Document_Build.build_documents( |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
307 |
Document_Build.context(session_context, progress = progress), |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
308 |
output_sources = info.document_output, |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
309 |
output_pdf = info.document_output) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
310 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
311 |
using(database_context.open_database(session_name, output = true))(session_database => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
312 |
documents.foreach(_.write(session_database.db, session_name))) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
313 |
(documents.flatMap(_.log_lines), Nil) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
314 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
315 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
316 |
else (Nil, Nil) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
317 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
318 |
catch { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
319 |
case exn: Document_Build.Build_Error => (exn.log_lines, exn.log_errors) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
320 |
case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
321 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
322 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
323 |
val result = { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
324 |
val theory_timing = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
325 |
theory_timings.iterator.flatMap( |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
326 |
{ |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
327 |
case props @ Markup.Name(name) => Some(name -> props) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
328 |
case _ => None |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
329 |
}).toMap |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
330 |
val used_theory_timings = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
331 |
for { (name, _) <- session_background.base.used_theories } |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
332 |
yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
333 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
334 |
val more_output = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
335 |
Library.trim_line(stdout.toString) :: |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
336 |
command_timings.toList.map(Protocol.Command_Timing_Marker.apply) ::: |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
337 |
used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) ::: |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
338 |
session_timings.toList.map(Protocol.Session_Timing_Marker.apply) ::: |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
339 |
runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) ::: |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
340 |
task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) ::: |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
341 |
document_output |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
342 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
343 |
process_result.output(more_output) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
344 |
.error(Library.trim_line(stderr.toString)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
345 |
.errors_rc(export_errors ::: document_errors) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
346 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
347 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
348 |
build_errors match { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
349 |
case Exn.Res(build_errs) => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
350 |
val errs = build_errs ::: document_errors |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
351 |
if (errs.nonEmpty) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
352 |
result.error_rc.output( |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
353 |
errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
354 |
errs.map(Protocol.Error_Message_Marker.apply)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
355 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
356 |
else if (progress.stopped && result.ok) result.copy(rc = Process_Result.RC.interrupt) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
357 |
else result |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
358 |
case Exn.Exn(Exn.Interrupt()) => |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
359 |
if (result.ok) result.copy(rc = Process_Result.RC.interrupt) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
360 |
else result |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
361 |
case Exn.Exn(exn) => throw exn |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
362 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
363 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
364 |
|
77298 | 365 |
override def start(): Unit = future_result |
366 |
override def terminate(): Unit = future_result.cancel() |
|
367 |
override def is_finished: Boolean = future_result.is_finished |
|
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
368 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
369 |
private val timeout_request: Option[Event_Timer.Request] = { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
370 |
if (info.timeout_ignored) None |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
371 |
else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() }) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
372 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
373 |
|
77298 | 374 |
override def join: Process_Result = { |
77297
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
375 |
val result = future_result.join |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
376 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
377 |
val was_timeout = |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
378 |
timeout_request match { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
379 |
case None => false |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
380 |
case Some(request) => !request.cancel() |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
381 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
382 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
383 |
if (result.ok) result |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
384 |
else if (was_timeout) result.error(Output.error_message_text("Timeout")).timeout_rc |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
385 |
else if (result.interrupted) result.error(Output.error_message_text("Interrupt")) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
386 |
else result |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
387 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
388 |
|
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
389 |
lazy val finish: SHA1.Shasum = { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
390 |
require(is_finished, "Build job not finished: " + quote(session_name)) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
391 |
if (join.ok && do_store && store.output_heap(session_name).is_file) { |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
392 |
SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name) |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
393 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
394 |
else SHA1.no_shasum |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
395 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
396 |
} |
226a880d0423
clarified types: support a variety of Build_Job instances;
wenzelm
parents:
77294
diff
changeset
|
397 |
|
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75762
diff
changeset
|
398 |
/* theory markup/messages from session database */ |
72854 | 399 |
|
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75762
diff
changeset
|
400 |
def read_theory( |
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75762
diff
changeset
|
401 |
theory_context: Export.Theory_Context, |
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75762
diff
changeset
|
402 |
unicode_symbols: Boolean = false |
76205 | 403 |
): Option[Document.Snapshot] = { |
76936 | 404 |
def decode_bytes(bytes: Bytes): String = |
405 |
Symbol.output(unicode_symbols, UTF8.decode_permissive(bytes)) |
|
406 |
||
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75762
diff
changeset
|
407 |
def read(name: String): Export.Entry = theory_context(name, permissive = true) |
72848
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
408 |
|
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
409 |
def read_xml(name: String): XML.Body = |
76936 | 410 |
YXML.parse_body(decode_bytes(read(name).bytes), cache = theory_context.cache) |
72848
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
411 |
|
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
412 |
def read_source_file(name: String): Sessions.Source_File = |
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
413 |
theory_context.session_context.source_file(name) |
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
414 |
|
75733 | 415 |
for { |
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75762
diff
changeset
|
416 |
id <- theory_context.document_id() |
75903 | 417 |
(thy_file, blobs_files) <- theory_context.files(permissive = true) |
75733 | 418 |
} |
419 |
yield { |
|
76881
b59118d11a46
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents:
76879
diff
changeset
|
420 |
val master_dir = |
b59118d11a46
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents:
76879
diff
changeset
|
421 |
Path.explode(Url.strip_base_name(thy_file).getOrElse( |
b59118d11a46
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents:
76879
diff
changeset
|
422 |
error("Cannot determine theory master directory: " + quote(thy_file)))) |
b59118d11a46
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents:
76879
diff
changeset
|
423 |
|
75733 | 424 |
val blobs = |
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
425 |
blobs_files.map { name => |
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
426 |
val path = Path.explode(name) |
76881
b59118d11a46
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents:
76879
diff
changeset
|
427 |
val src_path = File.relative_path(master_dir, path).getOrElse(path) |
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
428 |
|
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
429 |
val file = read_source_file(name) |
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
430 |
val bytes = file.bytes |
76936 | 431 |
val text = decode_bytes(bytes) |
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
432 |
val chunk = Symbol.Text_Chunk(text) |
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
433 |
|
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
434 |
Command.Blob(Document.Node.Name(name), src_path, Some((file.digest, chunk))) -> |
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
435 |
Document.Blobs.Item(bytes, text, chunk, changed = false) |
75733 | 436 |
} |
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
437 |
|
76936 | 438 |
val thy_source = decode_bytes(read_source_file(thy_file).bytes) |
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
439 |
val thy_xml = read_xml(Export.MARKUP) |
75733 | 440 |
val blobs_xml = |
441 |
for (i <- (1 to blobs.length).toList) |
|
442 |
yield read_xml(Export.MARKUP + i) |
|
72865
ebf72a3b8daa
clarified file sources: take from build database instead of file-system;
wenzelm
parents:
72864
diff
changeset
|
443 |
|
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
444 |
val markups_index = Command.Markup_Index.make(blobs.map(_._1)) |
75733 | 445 |
val markups = |
446 |
Command.Markups.make( |
|
447 |
for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml)) |
|
448 |
yield index -> Markup_Tree.from_XML(xml)) |
|
449 |
||
76911 | 450 |
val results = |
451 |
Command.Results.make( |
|
452 |
for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES)) |
|
453 |
yield i -> elem) |
|
454 |
||
76205 | 455 |
val command = |
76881
b59118d11a46
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents:
76879
diff
changeset
|
456 |
Command.unparsed(thy_source, theory = true, id = id, |
b59118d11a46
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents:
76879
diff
changeset
|
457 |
node_name = Document.Node.Name(thy_file, theory = theory_context.theory), |
76913 | 458 |
blobs_info = Command.Blobs_Info.make(blobs), |
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
459 |
markups = markups, results = results) |
76205 | 460 |
|
76913 | 461 |
val doc_blobs = Document.Blobs.make(blobs) |
76912
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
462 |
|
ca872f20cf5b
clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents:
76911
diff
changeset
|
463 |
Document.State.init.snippet(command, doc_blobs) |
72848
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
464 |
} |
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
465 |
} |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
466 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
467 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
468 |
/* print messages */ |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
469 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
470 |
def print_log( |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
471 |
options: Options, |
76088
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
472 |
sessions: List[String], |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
473 |
theories: List[String] = Nil, |
76087 | 474 |
message_head: List[Regex] = Nil, |
475 |
message_body: List[Regex] = Nil, |
|
72878 | 476 |
verbose: Boolean = false, |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
477 |
progress: Progress = new Progress, |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
478 |
margin: Double = Pretty.default_margin, |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
479 |
breakgain: Double = Pretty.default_breakgain, |
72873 | 480 |
metric: Pretty.Metric = Symbol.Metric, |
75393 | 481 |
unicode_symbols: Boolean = false |
482 |
): Unit = { |
|
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
483 |
val store = Sessions.store(options) |
76654 | 484 |
val session = new Session(options, Resources.bootstrap) |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
485 |
|
76087 | 486 |
def check(filter: List[Regex], make_string: => String): Boolean = |
487 |
filter.isEmpty || { |
|
488 |
val s = Output.clean_yxml(make_string) |
|
489 |
filter.forall(r => r.findFirstIn(Output.clean_yxml(s)).nonEmpty) |
|
490 |
} |
|
491 |
||
76088
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
492 |
def print(session_name: String): Unit = { |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
493 |
using(Export.open_session_context0(store, session_name)) { session_context => |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
494 |
val result = |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
495 |
for { |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
496 |
db <- session_context.session_db() |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
497 |
theories = store.read_theories(db, session_name) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
498 |
errors = store.read_errors(db, session_name) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
499 |
info <- store.read_build(db, session_name) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
500 |
} yield (theories, errors, info.return_code) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
501 |
result match { |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
502 |
case None => store.error_database(session_name) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
503 |
case Some((used_theories, errors, rc)) => |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
504 |
theories.filterNot(used_theories.toSet) match { |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
505 |
case Nil => |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
506 |
case bad => error("Unknown theories " + commas_quote(bad)) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
507 |
} |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
508 |
val print_theories = |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
509 |
if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet) |
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75762
diff
changeset
|
510 |
|
76088
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
511 |
for (thy <- print_theories) { |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
512 |
val thy_heading = "\nTheory " + quote(thy) + " (in " + session_name + ")" + ":" |
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75762
diff
changeset
|
513 |
|
76088
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
514 |
read_theory(session_context.theory(thy), unicode_symbols = unicode_symbols) match { |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
515 |
case None => progress.echo(thy_heading + " MISSING") |
76205 | 516 |
case Some(snapshot) => |
76088
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
517 |
val rendering = new Rendering(snapshot, options, session) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
518 |
val messages = |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
519 |
rendering.text_messages(Text.Range.full) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
520 |
.filter(message => verbose || Protocol.is_exported(message.info)) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
521 |
if (messages.nonEmpty) { |
76933 | 522 |
val line_document = Line.Document(snapshot.node.source) |
76088
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
523 |
val buffer = new mutable.ListBuffer[String] |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
524 |
for (Text.Info(range, elem) <- messages) { |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
525 |
val line = line_document.position(range.start).line1 |
76205 | 526 |
val pos = Position.Line_File(line, snapshot.node_name.node) |
76088
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
527 |
def message_text: String = |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
528 |
Protocol.message_text(elem, heading = true, pos = pos, |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
529 |
margin = margin, breakgain = breakgain, metric = metric) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
530 |
val ok = |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
531 |
check(message_head, Protocol.message_heading(elem, pos)) && |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
532 |
check(message_body, XML.content(Pretty.unformatted(List(elem)))) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
533 |
if (ok) buffer += message_text |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
534 |
} |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
535 |
if (buffer.nonEmpty) { |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
536 |
progress.echo(thy_heading) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
537 |
buffer.foreach(progress.echo) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
538 |
} |
76087 | 539 |
} |
76088
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
540 |
} |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
541 |
} |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
542 |
|
76088
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
543 |
if (errors.nonEmpty) { |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
544 |
val msg = Symbol.output(unicode_symbols, cat_lines(errors)) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
545 |
progress.echo("\nBuild errors:\n" + Output.error_message_text(msg)) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
546 |
} |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
547 |
if (rc != Process_Result.RC.ok) { |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
548 |
progress.echo("\n" + Process_Result.RC.print_long(rc)) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
549 |
} |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
550 |
} |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
551 |
} |
75394 | 552 |
} |
76088
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
553 |
|
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
554 |
val errors = new mutable.ListBuffer[String] |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
555 |
for (session_name <- sessions) { |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
556 |
Exn.interruptible_capture(print(session_name)) match { |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
557 |
case Exn.Res(_) => |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
558 |
case Exn.Exn(exn) => errors += Exn.message(exn) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
559 |
} |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
560 |
} |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
561 |
if (errors.nonEmpty) error(cat_lines(errors.toList)) |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
562 |
} |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
563 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
564 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
565 |
/* Isabelle tool wrapper */ |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
566 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
567 |
val isabelle_tool = Isabelle_Tool("log", "print messages from build database", |
75394 | 568 |
Scala_Project.here, |
569 |
{ args => |
|
570 |
/* arguments */ |
|
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
571 |
|
76087 | 572 |
var message_head = List.empty[Regex] |
573 |
var message_body = List.empty[Regex] |
|
75394 | 574 |
var unicode_symbols = false |
575 |
var theories: List[String] = Nil |
|
576 |
var margin = Pretty.default_margin |
|
577 |
var options = Options.init() |
|
578 |
var verbose = false |
|
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
579 |
|
75394 | 580 |
val getopts = Getopts(""" |
76088
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
581 |
Usage: isabelle log [OPTIONS] [SESSIONS ...] |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
582 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
583 |
Options are: |
76087 | 584 |
-H REGEX filter messages by matching against head |
585 |
-M REGEX filter messages by matching against body |
|
72876 | 586 |
-T NAME restrict to given theories (multiple options possible) |
72867 | 587 |
-U output Unicode symbols |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
588 |
-m MARGIN margin for pretty printing (default: """ + margin + """) |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
589 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
73837
f72335f6a9ed
clarified documentation: tracing messages are not shown here;
wenzelm
parents:
73835
diff
changeset
|
590 |
-v print all messages, including information etc. |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
591 |
|
76088
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
592 |
Print messages from the build database of the given sessions, without any |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
593 |
checks against current sources nor session structure: results from old |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
594 |
sessions or failed builds can be printed as well. |
76087 | 595 |
|
596 |
Multiple options -H and -M are conjunctive: all given patterns need to |
|
76088
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
597 |
match. Patterns match any substring, but ^ or $ may be used to match the |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
598 |
start or end explicitly. |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
599 |
""", |
76087 | 600 |
"H:" -> (arg => message_head = message_head ::: List(arg.r)), |
601 |
"M:" -> (arg => message_body = message_body ::: List(arg.r)), |
|
75394 | 602 |
"T:" -> (arg => theories = theories ::: List(arg)), |
603 |
"U" -> (_ => unicode_symbols = true), |
|
604 |
"m:" -> (arg => margin = Value.Double.parse(arg)), |
|
605 |
"o:" -> (arg => options = options + arg), |
|
606 |
"v" -> (_ => verbose = true)) |
|
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
607 |
|
76088
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
608 |
val sessions = getopts(args) |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
609 |
|
75394 | 610 |
val progress = new Console_Progress() |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
611 |
|
76088
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
612 |
if (sessions.isEmpty) progress.echo_warning("No sessions to print") |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
613 |
else { |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
614 |
print_log(options, sessions, theories = theories, message_head = message_head, |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
615 |
message_body = message_body, verbose = verbose, margin = margin, progress = progress, |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
616 |
unicode_symbols = unicode_symbols) |
bec8677d0e5b
support multiple sessions, with cumulative errors;
wenzelm
parents:
76087
diff
changeset
|
617 |
} |
75394 | 618 |
}) |
72848
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
619 |
} |