author | wenzelm |
Fri, 06 Sep 2024 15:59:48 +0200 | |
changeset 80817 | e31ebb2be437 |
parent 80807 | b41c19523a2e |
child 80886 | 5d562dd387ae |
permissions | -rw-r--r-- |
79502 | 1 |
/* Title: Pure/Build/build.scala |
48276 | 2 |
Author: Makarius |
57923 | 3 |
Options: :folding=explicit: |
48276 | 4 |
|
77553 | 5 |
Command-line tools to build and manage Isabelle sessions. |
48276 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
77553 | 10 |
import scala.collection.mutable |
11 |
import scala.util.matching.Regex |
|
12 |
||
48276 | 13 |
|
75393 | 14 |
object Build { |
77553 | 15 |
/** "isabelle build" **/ |
16 |
||
78232 | 17 |
/* options */ |
18 |
||
19 |
def hostname(options: Options): String = |
|
20 |
Isabelle_System.hostname(options.string("build_hostname")) |
|
21 |
||
22 |
def engine_name(options: Options): String = options.string("build_engine") |
|
23 |
||
24 |
||
25 |
||
78421 | 26 |
/* context */ |
27 |
||
28 |
sealed case class Context( |
|
29 |
store: Store, |
|
79643 | 30 |
deps: isabelle.Sessions.Deps, |
79642 | 31 |
engine: Engine = Engine.Default, |
78421 | 32 |
afp_root: Option[Path] = None, |
33 |
build_hosts: List[Build_Cluster.Host] = Nil, |
|
34 |
ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"), |
|
35 |
hostname: String = Isabelle_System.hostname(), |
|
36 |
numa_shuffling: Boolean = false, |
|
80109
dbcd6dc7f70f
back to static numa_nodes (reverting part of c2c59de57df9);
wenzelm
parents:
80056
diff
changeset
|
37 |
numa_nodes: List[Int] = Nil, |
79710
32ca3d1283de
clarified signature: Build_Process tells how to clean sessions;
wenzelm
parents:
79709
diff
changeset
|
38 |
clean_sessions: List[String] = Nil, |
80118 | 39 |
store_heap: Boolean = false, |
78421 | 40 |
fresh_build: Boolean = false, |
41 |
no_build: Boolean = false, |
|
42 |
session_setup: (String, Session) => Unit = (_, _) => (), |
|
79717 | 43 |
build_uuid: String = UUID.random_string(), |
79811
d9fc2cc37694
more robust build_start for master and workers (via database);
wenzelm
parents:
79810
diff
changeset
|
44 |
build_start: Option[Date] = None, |
79644 | 45 |
jobs: Int = 0, |
78421 | 46 |
master: Boolean = false |
47 |
) { |
|
48 |
def build_options: Options = store.options |
|
49 |
||
79643 | 50 |
def sessions_structure: isabelle.Sessions.Structure = deps.sessions_structure |
78421 | 51 |
|
79645
7a1153c95bf9
clarifier worker vs. master, which may coincide for local build;
wenzelm
parents:
79644
diff
changeset
|
52 |
def worker: Boolean = jobs > 0 |
7a1153c95bf9
clarifier worker vs. master, which may coincide for local build;
wenzelm
parents:
79644
diff
changeset
|
53 |
|
7a1153c95bf9
clarifier worker vs. master, which may coincide for local build;
wenzelm
parents:
79644
diff
changeset
|
54 |
override def toString: String = |
7a1153c95bf9
clarifier worker vs. master, which may coincide for local build;
wenzelm
parents:
79644
diff
changeset
|
55 |
"Build.Context(build_uuid = " + quote(build_uuid) + |
7a1153c95bf9
clarifier worker vs. master, which may coincide for local build;
wenzelm
parents:
79644
diff
changeset
|
56 |
if_proper(worker, ", worker = true") + |
7a1153c95bf9
clarifier worker vs. master, which may coincide for local build;
wenzelm
parents:
79644
diff
changeset
|
57 |
if_proper(master, ", master = true") + ")" |
78421 | 58 |
} |
59 |
||
60 |
||
77330
47eb96592aa2
support alternative build engines, via system option "build_engine";
wenzelm
parents:
77326
diff
changeset
|
61 |
/* results */ |
48424 | 62 |
|
77311 | 63 |
object Results { |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78437
diff
changeset
|
64 |
def apply( |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78437
diff
changeset
|
65 |
context: Context, |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78437
diff
changeset
|
66 |
results: Map[String, Process_Result] = Map.empty, |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78437
diff
changeset
|
67 |
other_rc: Int = Process_Result.RC.ok |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78437
diff
changeset
|
68 |
): Results = { |
79643 | 69 |
new Results(context.store, context.deps, results, other_rc) |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78437
diff
changeset
|
70 |
} |
77311 | 71 |
} |
72 |
||
73 |
class Results private( |
|
78178 | 74 |
val store: Store, |
76209 | 75 |
val deps: Sessions.Deps, |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78437
diff
changeset
|
76 |
results: Map[String, Process_Result], |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78437
diff
changeset
|
77 |
other_rc: Int |
76198
fb4215da4919
clarified presentation_sessions: work with partial results;
wenzelm
parents:
76197
diff
changeset
|
78 |
) { |
76206
769a7cd5a16a
clarified signature: re-use store/cache from build results;
wenzelm
parents:
76202
diff
changeset
|
79 |
def cache: Term.Cache = store.cache |
769a7cd5a16a
clarified signature: re-use store/cache from build results;
wenzelm
parents:
76202
diff
changeset
|
80 |
|
77311 | 81 |
def sessions_ok: List[String] = |
80116 | 82 |
List.from( |
83 |
for { |
|
84 |
name <- deps.sessions_structure.build_topological_order.iterator |
|
85 |
result <- results.get(name) if result.ok |
|
86 |
} yield name) |
|
77311 | 87 |
|
77250
22016642d6af
clarified data structure: use static info from deps, not dynamic results;
wenzelm
parents:
77246
diff
changeset
|
88 |
def info(name: String): Sessions.Info = deps.sessions_structure(name) |
62403 | 89 |
def sessions: Set[String] = results.keySet |
77253
792dad9cb04f
clarified data structure: absorb Option[Process_Result] into Process_Result, e.g. to simplify database storage;
wenzelm
parents:
77252
diff
changeset
|
90 |
def cancelled(name: String): Boolean = !results(name).defined |
792dad9cb04f
clarified data structure: absorb Option[Process_Result] into Process_Result, e.g. to simplify database storage;
wenzelm
parents:
77252
diff
changeset
|
91 |
def apply(name: String): Process_Result = results(name).strict |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78437
diff
changeset
|
92 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78437
diff
changeset
|
93 |
val rc: Int = |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78437
diff
changeset
|
94 |
Process_Result.RC.merge(other_rc, |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78437
diff
changeset
|
95 |
Process_Result.RC.merge(results.valuesIterator.map(_.strict.rc))) |
74306 | 96 |
def ok: Boolean = rc == Process_Result.RC.ok |
62406 | 97 |
|
78566
a04277e3b313
tuned message: failure may stem from build_cluster init;
wenzelm
parents:
78562
diff
changeset
|
98 |
lazy val unfinished: List[String] = sessions.iterator.filterNot(apply(_).ok).toList.sorted |
76199 | 99 |
|
62406 | 100 |
override def toString: String = rc.toString |
62403 | 101 |
} |
102 |
||
77330
47eb96592aa2
support alternative build engines, via system option "build_engine";
wenzelm
parents:
77326
diff
changeset
|
103 |
|
47eb96592aa2
support alternative build engines, via system option "build_engine";
wenzelm
parents:
77326
diff
changeset
|
104 |
/* engine */ |
47eb96592aa2
support alternative build engines, via system option "build_engine";
wenzelm
parents:
77326
diff
changeset
|
105 |
|
78232 | 106 |
object Engine { |
107 |
lazy val services: List[Engine] = |
|
108 |
Isabelle_System.make_services(classOf[Engine]) |
|
109 |
||
110 |
def apply(name: String): Engine = |
|
111 |
services.find(_.name == name).getOrElse(error("Bad build engine " + quote(name))) |
|
79642 | 112 |
|
113 |
class Default extends Engine("") { override def toString: String = "<default>" } |
|
114 |
object Default extends Default |
|
78232 | 115 |
} |
116 |
||
77411
149cc77f7348
clafified signature: simplify object-oriented reuse;
wenzelm
parents:
77384
diff
changeset
|
117 |
class Engine(val name: String) extends Isabelle_System.Service { |
79705 | 118 |
engine => |
119 |
||
77330
47eb96592aa2
support alternative build engines, via system option "build_engine";
wenzelm
parents:
77326
diff
changeset
|
120 |
override def toString: String = name |
78232 | 121 |
|
79614 | 122 |
def build_options(options: Options, build_cluster: Boolean = false): Options = { |
78401 | 123 |
val options1 = options + "completion_limit=0" + "editor_tracing_messages=0" |
80160
ead20482da9c
build_cluster always uses build_database_server for now -- despite 1fa1b32b0379: its local/remote storage model often leads to incoherent state;
wenzelm
parents:
80128
diff
changeset
|
124 |
if (build_cluster) options1 + "build_database" + "build_database_server" + "build_log_verbose" else options1 // FIXME tmp: build_database_server |
78401 | 125 |
} |
78232 | 126 |
|
78412 | 127 |
final def build_store(options: Options, |
79614 | 128 |
build_cluster: Boolean = false, |
78412 | 129 |
cache: Term.Cache = Term.Cache.make() |
130 |
): Store = { |
|
79705 | 131 |
val build_options = engine.build_options(options, build_cluster = build_cluster) |
132 |
val store = Store(build_options, build_cluster = build_cluster, cache = cache) |
|
78412 | 133 |
Isabelle_System.make_directory(store.output_dir + Path.basic("log")) |
134 |
Isabelle_Fonts.init() |
|
135 |
store |
|
136 |
} |
|
137 |
||
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78435
diff
changeset
|
138 |
def open_build_process( |
78421 | 139 |
build_context: Context, |
78372 | 140 |
build_progress: Progress, |
141 |
server: SSH.Server |
|
142 |
): Build_Process = new Build_Process(build_context, build_progress, server) |
|
78232 | 143 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78435
diff
changeset
|
144 |
final def run_build_process( |
78421 | 145 |
context: Context, |
78372 | 146 |
progress: Progress, |
147 |
server: SSH.Server |
|
78412 | 148 |
): Results = { |
78232 | 149 |
Isabelle_Thread.uninterruptible { |
79710
32ca3d1283de
clarified signature: Build_Process tells how to clean sessions;
wenzelm
parents:
79709
diff
changeset
|
150 |
using(open_build_process(context, progress, server)) { build_process => |
32ca3d1283de
clarified signature: Build_Process tells how to clean sessions;
wenzelm
parents:
79709
diff
changeset
|
151 |
build_process.prepare() |
32ca3d1283de
clarified signature: Build_Process tells how to clean sessions;
wenzelm
parents:
79709
diff
changeset
|
152 |
build_process.run() |
32ca3d1283de
clarified signature: Build_Process tells how to clean sessions;
wenzelm
parents:
79709
diff
changeset
|
153 |
} |
78232 | 154 |
} |
78412 | 155 |
} |
77330
47eb96592aa2
support alternative build engines, via system option "build_engine";
wenzelm
parents:
77326
diff
changeset
|
156 |
} |
47eb96592aa2
support alternative build engines, via system option "build_engine";
wenzelm
parents:
77326
diff
changeset
|
157 |
|
47eb96592aa2
support alternative build engines, via system option "build_engine";
wenzelm
parents:
77326
diff
changeset
|
158 |
|
77558 | 159 |
|
160 |
/* build */ |
|
161 |
||
62641 | 162 |
def build( |
50404
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50367
diff
changeset
|
163 |
options: Options, |
78401 | 164 |
build_hosts: List[Build_Cluster.Host] = Nil, |
71981 | 165 |
selection: Sessions.Selection = Sessions.Selection.empty, |
75942
603852abed8f
clarified names: Browser_Info.Config vs. Browser_Info.Context;
wenzelm
parents:
75941
diff
changeset
|
166 |
browser_info: Browser_Info.Config = Browser_Info.Config.none, |
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71718
diff
changeset
|
167 |
progress: Progress = new Progress, |
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65831
diff
changeset
|
168 |
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
|
169 |
build_heap: Boolean = false, |
48595 | 170 |
clean_build: Boolean = false, |
78418
bc62be4144e6
added option -A for AFP root, following "isabelle sync";
wenzelm
parents:
78412
diff
changeset
|
171 |
afp_root: Option[Path] = None, |
56890 | 172 |
dirs: List[Path] = Nil, |
173 |
select_dirs: List[Path] = Nil, |
|
66968
9991671c98aa
allow to augment session context via explicit session infos;
wenzelm
parents:
66962
diff
changeset
|
174 |
infos: List[Sessions.Info] = Nil, |
64265 | 175 |
numa_shuffling: Boolean = false, |
79616 | 176 |
max_jobs: Option[Int] = None, |
48903 | 177 |
list_files: Boolean = false, |
59891
9ce697050455
added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents:
59811
diff
changeset
|
178 |
check_keywords: Set[String] = Set.empty, |
66841 | 179 |
fresh_build: Boolean = false, |
48509 | 180 |
no_build: Boolean = false, |
66745 | 181 |
soft_build: Boolean = false, |
73805
b73777a0c076
allow build session setup, e.g. for protocol handlers;
wenzelm
parents:
73804
diff
changeset
|
182 |
export_files: Boolean = false, |
76927
da13da82f6f9
treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
wenzelm
parents:
76919
diff
changeset
|
183 |
augment_options: String => List[Options.Spec] = _ => Nil, |
77559
4ad322ee6025
clarified signature: support all arguments of Sessions.store();
wenzelm
parents:
77558
diff
changeset
|
184 |
session_setup: (String, Session) => Unit = (_, _) => (), |
4ad322ee6025
clarified signature: support all arguments of Sessions.store();
wenzelm
parents:
77558
diff
changeset
|
185 |
cache: Term.Cache = Term.Cache.make() |
75393 | 186 |
): Results = { |
79707 | 187 |
val engine = Engine(engine_name(options)) |
188 |
val store = engine.build_store(options, build_cluster = build_hosts.nonEmpty, cache = cache) |
|
77557 | 189 |
val build_options = store.options |
69369
6ecc85955e04
prefer "Isabelle DejaVu Sans", even for headless batch-build (session_graph.pdf);
wenzelm
parents:
68957
diff
changeset
|
190 |
|
78372 | 191 |
using(store.open_server()) { server => |
66745 | 192 |
|
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
193 |
/* session selection and dependencies */ |
65422 | 194 |
|
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
195 |
val full_sessions = |
80056 | 196 |
Sessions.load_structure(build_options, dirs = AFP.main_dirs(afp_root) ::: dirs, |
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
197 |
select_dirs = select_dirs, infos = infos, augment_options = augment_options) |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
198 |
val full_sessions_selection = full_sessions.imports_selection(selection) |
73012
238ddf525da4
clarified HTML presentation, e.g. avoid bulky jobs like HOL or HOL-Analysis in applications;
wenzelm
parents:
72993
diff
changeset
|
199 |
|
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
200 |
val build_deps = { |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
201 |
val deps0 = |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
202 |
Sessions.deps(full_sessions.selection(selection), progress = progress, |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
203 |
inlined_files = true, list_files = list_files, check_keywords = check_keywords |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
204 |
).check_errors |
66745 | 205 |
|
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
206 |
if (soft_build && !fresh_build) { |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
207 |
val outdated = |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
208 |
deps0.sessions_structure.build_topological_order.flatMap(name => |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
209 |
store.try_open_database(name, server = server) match { |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
210 |
case Some(db) => |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
211 |
using(db)(store.read_build(_, name)) match { |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
212 |
case Some(build) if build.ok => |
80128 | 213 |
val sources_shasum = deps0.sources_shasum(name) |
214 |
val thorough = deps0.sessions_structure(name).build_thorough |
|
215 |
if (Sessions.eq_sources(thorough, build.sources, sources_shasum)) None |
|
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
216 |
else Some(name) |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
217 |
case _ => Some(name) |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
218 |
} |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
219 |
case None => Some(name) |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
220 |
}) |
68204 | 221 |
|
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
222 |
Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)), |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
223 |
progress = progress, inlined_files = true).check_errors |
78372 | 224 |
} |
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
225 |
else deps0 |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
226 |
} |
66745 | 227 |
|
228 |
||
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
229 |
/* check unknown files */ |
78372 | 230 |
|
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
231 |
if (check_unknown_files) { |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
232 |
val source_files = |
80116 | 233 |
List.from( |
234 |
for { |
|
235 |
(_, base) <- build_deps.session_bases.iterator |
|
236 |
(path, _) <- base.session_sources.iterator |
|
237 |
} yield path) |
|
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
238 |
Mercurial.check_files(source_files)._2 match { |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
239 |
case Nil => |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
240 |
case unknown_files => |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
241 |
progress.echo_warning( |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
242 |
"Unknown files (not part of the underlying Mercurial repository):" + |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
243 |
unknown_files.map(File.standard_path).sorted.mkString("\n ", "\n ", "")) |
78372 | 244 |
} |
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
245 |
} |
78372 | 246 |
|
247 |
||
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
248 |
/* build process and results */ |
78372 | 249 |
|
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
250 |
val clean_sessions = |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
251 |
if (clean_build) full_sessions.imports_descendants(full_sessions_selection) else Nil |
79710
32ca3d1283de
clarified signature: Build_Process tells how to clean sessions;
wenzelm
parents:
79709
diff
changeset
|
252 |
|
80109
dbcd6dc7f70f
back to static numa_nodes (reverting part of c2c59de57df9);
wenzelm
parents:
80056
diff
changeset
|
253 |
val numa_nodes = Host.numa_nodes(enabled = numa_shuffling) |
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
254 |
val build_context = |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
255 |
Context(store, build_deps, engine = engine, afp_root = afp_root, |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
256 |
build_hosts = build_hosts, hostname = hostname(build_options), |
80118 | 257 |
clean_sessions = clean_sessions, store_heap = build_heap, |
80109
dbcd6dc7f70f
back to static numa_nodes (reverting part of c2c59de57df9);
wenzelm
parents:
80056
diff
changeset
|
258 |
numa_shuffling = numa_shuffling, numa_nodes = numa_nodes, |
dbcd6dc7f70f
back to static numa_nodes (reverting part of c2c59de57df9);
wenzelm
parents:
80056
diff
changeset
|
259 |
fresh_build = fresh_build, no_build = no_build, session_setup = session_setup, |
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
260 |
jobs = max_jobs.getOrElse(if (build_hosts.nonEmpty) 0 else 1), master = true) |
48504
21dfd6c04482
actually check source vs. target stamps, based on information from log files;
wenzelm
parents:
48494
diff
changeset
|
261 |
|
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
262 |
val results = engine.run_build_process(build_context, progress, server) |
78372 | 263 |
|
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
264 |
if (export_files) { |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
265 |
for (name <- full_sessions_selection.iterator if results(name).ok) { |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
266 |
val info = results.info(name) |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
267 |
if (info.export_files.nonEmpty) { |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
268 |
progress.echo("Exporting " + info.name + " ...") |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
269 |
for ((dir, prune, pats) <- info.export_files) { |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
270 |
Export.export_files(store, name, info.dir + dir, |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
271 |
progress = if (progress.verbose) progress else new Progress, |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
272 |
export_prune = prune, |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
273 |
export_patterns = pats) |
78372 | 274 |
} |
275 |
} |
|
276 |
} |
|
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
277 |
} |
78372 | 278 |
|
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
279 |
val presentation_sessions = |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
280 |
results.sessions_ok.filter(name => browser_info.enabled(results.info(name))) |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
281 |
if (presentation_sessions.nonEmpty && !progress.stopped) { |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
282 |
Browser_Info.build(browser_info, results.store, results.deps, presentation_sessions, |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
283 |
progress = progress, server = server) |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
284 |
} |
78372 | 285 |
|
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
286 |
if (results.unfinished.nonEmpty && (progress.verbose || !no_build)) { |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
287 |
progress.echo("Unfinished session(s): " + commas(results.unfinished)) |
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
288 |
} |
78372 | 289 |
|
79715
e59d93da9109
removed unused database_server (amending 32ca3d1283de);
wenzelm
parents:
79710
diff
changeset
|
290 |
results |
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65831
diff
changeset
|
291 |
} |
48341 | 292 |
} |
293 |
||
294 |
||
77555 | 295 |
/* build logic image */ |
296 |
||
297 |
def build_logic(options: Options, logic: String, |
|
298 |
progress: Progress = new Progress, |
|
299 |
build_heap: Boolean = false, |
|
300 |
dirs: List[Path] = Nil, |
|
301 |
fresh: Boolean = false, |
|
302 |
strict: Boolean = false |
|
303 |
): Int = { |
|
304 |
val selection = Sessions.Selection.session(logic) |
|
305 |
val rc = |
|
306 |
if (!fresh && build(options, selection = selection, |
|
307 |
build_heap = build_heap, no_build = true, dirs = dirs).ok) Process_Result.RC.ok |
|
308 |
else { |
|
309 |
progress.echo("Build started for Isabelle/" + logic + " ...") |
|
310 |
build(options, selection = selection, progress = progress, |
|
311 |
build_heap = build_heap, fresh_build = fresh, dirs = dirs).rc |
|
312 |
} |
|
313 |
if (strict && rc != Process_Result.RC.ok) error("Failed to build Isabelle/" + logic) else rc |
|
314 |
} |
|
315 |
||
316 |
||
79629 | 317 |
/* Isabelle tool wrappers */ |
48341 | 318 |
|
77553 | 319 |
val isabelle_tool1 = Isabelle_Tool("build", "build and manage Isabelle sessions", |
75394 | 320 |
Scala_Project.here, |
321 |
{ args => |
|
78418
bc62be4144e6
added option -A for AFP root, following "isabelle sync";
wenzelm
parents:
78412
diff
changeset
|
322 |
var afp_root: Option[Path] = None |
78405 | 323 |
val base_sessions = new mutable.ListBuffer[String] |
324 |
val select_dirs = new mutable.ListBuffer[Path] |
|
78401 | 325 |
val build_hosts = new mutable.ListBuffer[Build_Cluster.Host] |
75394 | 326 |
var numa_shuffling = false |
75942
603852abed8f
clarified names: Browser_Info.Config vs. Browser_Info.Context;
wenzelm
parents:
75941
diff
changeset
|
327 |
var browser_info = Browser_Info.Config.none |
75394 | 328 |
var requirements = false |
329 |
var soft_build = false |
|
78405 | 330 |
val exclude_session_groups = new mutable.ListBuffer[String] |
75394 | 331 |
var all_sessions = false |
332 |
var build_heap = false |
|
333 |
var clean_build = false |
|
78405 | 334 |
val dirs = new mutable.ListBuffer[Path] |
75394 | 335 |
var export_files = false |
336 |
var fresh_build = false |
|
78405 | 337 |
val session_groups = new mutable.ListBuffer[String] |
79616 | 338 |
var max_jobs: Option[Int] = None |
75394 | 339 |
var check_keywords: Set[String] = Set.empty |
340 |
var list_files = false |
|
341 |
var no_build = false |
|
77628 | 342 |
var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS) |
75394 | 343 |
var verbose = false |
78405 | 344 |
val exclude_sessions = new mutable.ListBuffer[String] |
62590 | 345 |
|
75394 | 346 |
val getopts = Getopts(""" |
62590 | 347 |
Usage: isabelle build [OPTIONS] [SESSIONS ...] |
348 |
||
349 |
Options are: |
|
78418
bc62be4144e6
added option -A for AFP root, following "isabelle sync";
wenzelm
parents:
78412
diff
changeset
|
350 |
-A ROOT include AFP with given root directory (":" for """ + AFP.BASE.implode + """) |
66737
2edc0c42c883
option -B for "isabelle build" and "isabelle imports";
wenzelm
parents:
66736
diff
changeset
|
351 |
-B NAME include session NAME and all descendants |
62590 | 352 |
-D DIR include session directory and select its sessions |
79615 | 353 |
-H HOSTS additional cluster host specifications of the form |
354 |
NAMES:PARAMETERS (separated by commas) |
|
64265 | 355 |
-N cyclic shuffling of NUMA CPU nodes (performance tuning) |
72648 | 356 |
-P DIR enable HTML/PDF presentation in directory (":" for default) |
71807 | 357 |
-R refer to requirements of selected sessions |
66745 | 358 |
-S soft build: only observe changes of sources, not heap images |
62590 | 359 |
-X NAME exclude sessions from group NAME and all descendants |
360 |
-a select all sessions |
|
361 |
-b build heap images |
|
362 |
-c clean build |
|
363 |
-d DIR include session directory |
|
69811
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69777
diff
changeset
|
364 |
-e export files from session specification into file-system |
66841 | 365 |
-f fresh build |
62590 | 366 |
-g NAME select session group NAME |
79647 | 367 |
-j INT maximum number of parallel jobs |
368 |
(default: 1 for local build, 0 for build cluster) |
|
62590 | 369 |
-k KEYWORD check theory sources for conflicts with proposed keywords |
370 |
-l list session source files |
|
77554
4465d9dff448
clarified terminology of "session build database", while "build database" is the one underlying Build_Process;
wenzelm
parents:
77553
diff
changeset
|
371 |
-n no build -- take existing session build databases |
62590 | 372 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
373 |
-v verbose |
|
374 |
-x NAME exclude session NAME and all descendants |
|
375 |
||
77647 | 376 |
Build and manage Isabelle sessions: ML heaps, session databases, documents. |
62596 | 377 |
|
79615 | 378 |
Parameters for cluster host specifications (-H), apart from system options: |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78405
diff
changeset
|
379 |
""" + Library.indent_lines(4, Build_Cluster.Host.parameters.print()) + |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78405
diff
changeset
|
380 |
""" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78405
diff
changeset
|
381 |
|
77647 | 382 |
Notable system options: see "isabelle options -l -t build" |
383 |
||
384 |
Notable system settings: |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78405
diff
changeset
|
385 |
""" + Library.indent_lines(4, Build_Log.Settings.show()) + "\n", |
78418
bc62be4144e6
added option -A for AFP root, following "isabelle sync";
wenzelm
parents:
78412
diff
changeset
|
386 |
"A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))), |
78405 | 387 |
"B:" -> (arg => base_sessions += arg), |
388 |
"D:" -> (arg => select_dirs += Path.explode(arg)), |
|
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78916
diff
changeset
|
389 |
"H:" -> (arg => build_hosts ++= Build_Cluster.Host.parse(Registry.global, arg)), |
75394 | 390 |
"N" -> (_ => numa_shuffling = true), |
75942
603852abed8f
clarified names: Browser_Info.Config vs. Browser_Info.Context;
wenzelm
parents:
75941
diff
changeset
|
391 |
"P:" -> (arg => browser_info = Browser_Info.Config.make(arg)), |
75394 | 392 |
"R" -> (_ => requirements = true), |
393 |
"S" -> (_ => soft_build = true), |
|
78405 | 394 |
"X:" -> (arg => exclude_session_groups += arg), |
75394 | 395 |
"a" -> (_ => all_sessions = true), |
396 |
"b" -> (_ => build_heap = true), |
|
397 |
"c" -> (_ => clean_build = true), |
|
78405 | 398 |
"d:" -> (arg => dirs += Path.explode(arg)), |
75394 | 399 |
"e" -> (_ => export_files = true), |
400 |
"f" -> (_ => fresh_build = true), |
|
78405 | 401 |
"g:" -> (arg => session_groups += arg), |
79616 | 402 |
"j:" -> (arg => max_jobs = Some(Value.Nat.parse(arg))), |
75394 | 403 |
"k:" -> (arg => check_keywords = check_keywords + arg), |
404 |
"l" -> (_ => list_files = true), |
|
405 |
"n" -> (_ => no_build = true), |
|
406 |
"o:" -> (arg => options = options + arg), |
|
407 |
"v" -> (_ => verbose = true), |
|
78405 | 408 |
"x:" -> (arg => exclude_sessions += arg)) |
62590 | 409 |
|
75394 | 410 |
val sessions = getopts(args) |
62590 | 411 |
|
75394 | 412 |
val progress = new Console_Progress(verbose = verbose) |
62590 | 413 |
|
77521
5642de4d225d
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77505
diff
changeset
|
414 |
progress.echo( |
78895 | 415 |
"Started at " + Build_Log.print_date(progress.start) + |
77719 | 416 |
" (" + Isabelle_System.ml_identifier() + " on " + hostname(options) +")", |
77521
5642de4d225d
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77505
diff
changeset
|
417 |
verbose = true) |
5642de4d225d
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77505
diff
changeset
|
418 |
progress.echo(Build_Log.Settings.show() + "\n", verbose = true) |
62590 | 419 |
|
75394 | 420 |
val results = |
421 |
progress.interrupt_handler { |
|
422 |
build(options, |
|
423 |
selection = Sessions.Selection( |
|
424 |
requirements = requirements, |
|
425 |
all_sessions = all_sessions, |
|
78405 | 426 |
base_sessions = base_sessions.toList, |
427 |
exclude_session_groups = exclude_session_groups.toList, |
|
428 |
exclude_sessions = exclude_sessions.toList, |
|
429 |
session_groups = session_groups.toList, |
|
75394 | 430 |
sessions = sessions), |
75942
603852abed8f
clarified names: Browser_Info.Config vs. Browser_Info.Context;
wenzelm
parents:
75941
diff
changeset
|
431 |
browser_info = browser_info, |
75394 | 432 |
progress = progress, |
433 |
check_unknown_files = Mercurial.is_repository(Path.ISABELLE_HOME), |
|
434 |
build_heap = build_heap, |
|
435 |
clean_build = clean_build, |
|
78437 | 436 |
afp_root = afp_root, |
78405 | 437 |
dirs = dirs.toList, |
438 |
select_dirs = select_dirs.toList, |
|
77477 | 439 |
numa_shuffling = Host.numa_check(progress, numa_shuffling), |
75394 | 440 |
max_jobs = max_jobs, |
441 |
list_files = list_files, |
|
442 |
check_keywords = check_keywords, |
|
443 |
fresh_build = fresh_build, |
|
444 |
no_build = no_build, |
|
445 |
soft_build = soft_build, |
|
78401 | 446 |
export_files = export_files, |
447 |
build_hosts = build_hosts.toList) |
|
75394 | 448 |
} |
79810
4b23abde5d0b
more accurate progress.now(), notably for Database_Progress;
wenzelm
parents:
79717
diff
changeset
|
449 |
val stop_date = progress.now() |
79819 | 450 |
val elapsed_time = stop_date - progress.start |
75394 | 451 |
|
77545 | 452 |
progress.echo("\nFinished at " + Build_Log.print_date(stop_date), verbose = true) |
62590 | 453 |
|
75394 | 454 |
val total_timing = |
455 |
results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _). |
|
456 |
copy(elapsed = elapsed_time) |
|
457 |
progress.echo(total_timing.message_resources) |
|
62590 | 458 |
|
75394 | 459 |
sys.exit(results.rc) |
460 |
}) |
|
68305 | 461 |
|
462 |
||
77553 | 463 |
|
78562 | 464 |
/** build cluster management **/ |
77557 | 465 |
|
78219 | 466 |
/* identified builds */ |
467 |
||
78368
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
468 |
def read_builds(build_database: Option[SQL.Database]): List[Build_Process.Build] = |
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
469 |
build_database match { |
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
470 |
case None => Nil |
78634 | 471 |
case Some(db) => Build_Process.read_builds(db) |
78219 | 472 |
} |
473 |
||
78368
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
474 |
def print_builds(build_database: Option[SQL.Database], builds: List[Build_Process.Build]): String = |
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
475 |
{ |
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
476 |
val print_database = |
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
477 |
build_database match { |
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
478 |
case None => "" |
78634 | 479 |
case Some(db) => " (database " + db + ")" |
78368
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
480 |
} |
78640 | 481 |
if (builds.isEmpty) "No build processes" + print_database |
78641 | 482 |
else "Build processes" + print_database + builds.map(build => "\n " + build.print).mkString |
78368
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
483 |
} |
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
484 |
|
78410 | 485 |
def find_builds( |
78368
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
486 |
build_database: Option[SQL.Database], |
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
487 |
build_id: String, |
78221 | 488 |
builds: List[Build_Process.Build] |
78410 | 489 |
): Build_Process.Build = { |
78368
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
490 |
(build_id, builds.length) match { |
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
491 |
case (UUID(_), _) if builds.exists(_.build_uuid == build_id) => |
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
492 |
builds.find(_.build_uuid == build_id).get |
78410 | 493 |
case ("", 1) => builds.head |
78368
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
494 |
case ("", 0) => error(print_builds(build_database, builds)) |
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
495 |
case _ => |
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
496 |
cat_error("Cannot identify build process " + quote(build_id), |
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
497 |
print_builds(build_database, builds)) |
78219 | 498 |
} |
78410 | 499 |
} |
78219 | 500 |
|
501 |
||
78562 | 502 |
/* "isabelle build_process" */ |
503 |
||
504 |
def build_process( |
|
505 |
options: Options, |
|
79676
0cac7e3634d0
more explicit build_cluster flag to guard open_build_database server;
wenzelm
parents:
79647
diff
changeset
|
506 |
build_cluster: Boolean = false, |
78562 | 507 |
list_builds: Boolean = false, |
78636 | 508 |
remove_builds: Boolean = false, |
509 |
force: Boolean = false, |
|
78562 | 510 |
progress: Progress = new Progress |
511 |
): Unit = { |
|
79707 | 512 |
val engine = Engine(engine_name(options)) |
513 |
val store = engine.build_store(options, build_cluster = build_cluster) |
|
78562 | 514 |
|
515 |
using(store.open_server()) { server => |
|
516 |
using_optional(store.maybe_open_build_database(server = server)) { build_database => |
|
78636 | 517 |
def print(builds: List[Build_Process.Build]): Unit = |
518 |
if (list_builds) progress.echo(print_builds(build_database, builds)) |
|
78562 | 519 |
|
78636 | 520 |
build_database match { |
521 |
case None => print(Nil) |
|
79847 | 522 |
case Some(db) if remove_builds && force => |
523 |
db.transaction { |
|
524 |
val tables0 = |
|
525 |
ML_Heap.private_data.tables.list ::: |
|
526 |
Store.private_data.tables.list ::: |
|
79873 | 527 |
Database_Progress.private_data.tables.list ::: |
79847 | 528 |
Build_Process.private_data.tables.list |
529 |
val tables = tables0.filter(t => db.exists_table(t.name)).sortBy(_.name) |
|
530 |
if (tables.nonEmpty) { |
|
531 |
progress.echo("Removing tables " + commas_quote(tables.map(_.name)) + " ...") |
|
532 |
db.execute_statement(SQL.MULTI(tables.map(db.destroy))) |
|
533 |
} |
|
534 |
} |
|
78636 | 535 |
case Some(db) => |
536 |
Build_Process.private_data.transaction_lock(db, create = true, label = "build_process") { |
|
537 |
val builds = Build_Process.private_data.read_builds(db) |
|
538 |
print(builds) |
|
79847 | 539 |
if (remove_builds) { |
540 |
val remove = builds.flatMap(_.active_build_uuid) |
|
541 |
if (remove.nonEmpty) { |
|
78636 | 542 |
progress.echo("Removing " + commas(remove) + " ...") |
543 |
Build_Process.private_data.remove_builds(db, remove) |
|
544 |
print(Build_Process.private_data.read_builds(db)) |
|
545 |
} |
|
546 |
} |
|
547 |
} |
|
548 |
} |
|
78562 | 549 |
} |
550 |
} |
|
551 |
} |
|
552 |
||
553 |
val isabelle_tool2 = Isabelle_Tool("build_process", "manage session build process", |
|
554 |
Scala_Project.here, |
|
555 |
{ args => |
|
79676
0cac7e3634d0
more explicit build_cluster flag to guard open_build_database server;
wenzelm
parents:
79647
diff
changeset
|
556 |
var build_cluster = false |
78636 | 557 |
var force = false |
78562 | 558 |
var list_builds = false |
559 |
var options = |
|
79682
1fa1b32b0379
build local log_db, with store/restore via optional database server;
wenzelm
parents:
79679
diff
changeset
|
560 |
Options.init(specs = |
1fa1b32b0379
build local log_db, with store/restore via optional database server;
wenzelm
parents:
79679
diff
changeset
|
561 |
Options.Spec.ISABELLE_BUILD_OPTIONS ::: List(Options.Spec.make("build_database"))) |
78636 | 562 |
var remove_builds = false |
78562 | 563 |
|
564 |
val getopts = Getopts(""" |
|
565 |
Usage: isabelle build_process [OPTIONS] |
|
566 |
||
567 |
Options are: |
|
79676
0cac7e3634d0
more explicit build_cluster flag to guard open_build_database server;
wenzelm
parents:
79647
diff
changeset
|
568 |
-C build cluster mode (database server) |
78636 | 569 |
-f extra force for option -r |
78562 | 570 |
-l list build processes |
571 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
78636 | 572 |
-r remove data from build processes: inactive processes (default) |
573 |
or all processes (option -f) |
|
79700 | 574 |
|
575 |
Manage Isabelle build process, notably distributed build cluster (option -C). |
|
78562 | 576 |
""", |
79679
ba2c43592f35
proper treatment of "isabelle build_process -C" (amending 0cac7e3634d0);
wenzelm
parents:
79676
diff
changeset
|
577 |
"C" -> (_ => build_cluster = true), |
78636 | 578 |
"f" -> (_ => force = true), |
78562 | 579 |
"l" -> (_ => list_builds = true), |
78636 | 580 |
"o:" -> (arg => options = options + arg), |
581 |
"r" -> (_ => remove_builds = true)) |
|
78562 | 582 |
|
583 |
val more_args = getopts(args) |
|
584 |
if (more_args.nonEmpty) getopts.usage() |
|
585 |
||
586 |
val progress = new Console_Progress() |
|
587 |
||
79676
0cac7e3634d0
more explicit build_cluster flag to guard open_build_database server;
wenzelm
parents:
79647
diff
changeset
|
588 |
build_process(options, build_cluster = build_cluster, list_builds = list_builds, |
0cac7e3634d0
more explicit build_cluster flag to guard open_build_database server;
wenzelm
parents:
79647
diff
changeset
|
589 |
remove_builds = remove_builds, force = force, progress = progress) |
78562 | 590 |
}) |
591 |
||
592 |
||
593 |
||
594 |
/* "isabelle build_worker" */ |
|
77557 | 595 |
|
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78440
diff
changeset
|
596 |
def build_worker_command( |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78440
diff
changeset
|
597 |
host: Build_Cluster.Host, |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78440
diff
changeset
|
598 |
ssh: SSH.System = SSH.Local, |
78558 | 599 |
build_options: List[Options.Spec] = Nil, |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78440
diff
changeset
|
600 |
build_id: String = "", |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78440
diff
changeset
|
601 |
isabelle_home: Path = Path.current, |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78440
diff
changeset
|
602 |
dirs: List[Path] = Nil, |
78637 | 603 |
quiet: Boolean = false, |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78440
diff
changeset
|
604 |
verbose: Boolean = false |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78440
diff
changeset
|
605 |
): String = { |
78916 | 606 |
val options = build_options ::: Options.Spec.eq("build_hostname", host.name) :: host.options |
79624 | 607 |
ssh.bash_path(Isabelle_Tool.exe(isabelle_home)) + " build_worker" + |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78440
diff
changeset
|
608 |
if_proper(build_id, " -B " + Bash.string(build_id)) + |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78440
diff
changeset
|
609 |
dirs.map(dir => " -d " + ssh.bash_path(dir)).mkString + |
78560 | 610 |
if_proper(host.numa, " -N") + " -j" + host.jobs + |
78915
90756ad4d8d7
more accurate treatment of surrounding whitespace;
wenzelm
parents:
78908
diff
changeset
|
611 |
Options.Spec.bash_strings(options, bg = true) + |
78637 | 612 |
if_proper(quiet, " -q") + |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78440
diff
changeset
|
613 |
if_proper(verbose, " -v") |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78440
diff
changeset
|
614 |
} |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78440
diff
changeset
|
615 |
|
77557 | 616 |
def build_worker( |
617 |
options: Options, |
|
78410 | 618 |
build_id: String = "", |
77557 | 619 |
progress: Progress = new Progress, |
620 |
dirs: List[Path] = Nil, |
|
621 |
numa_shuffling: Boolean = false, |
|
79616 | 622 |
max_jobs: Option[Int] = None |
78568 | 623 |
): Results = { |
79707 | 624 |
val engine = Engine(engine_name(options)) |
625 |
val store = engine.build_store(options, build_cluster = true) |
|
77557 | 626 |
val build_options = store.options |
627 |
||
78372 | 628 |
using(store.open_server()) { server => |
629 |
using_optional(store.maybe_open_build_database(server = server)) { build_database => |
|
630 |
val builds = read_builds(build_database) |
|
78368
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
631 |
|
78634 | 632 |
val build_master = find_builds(build_database, build_id, builds.filter(_.active)) |
78368
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
633 |
|
80196 | 634 |
val more_dirs = List(Path.ISABELLE_HOME + Sync.DIRS).filter(Sessions.is_session_dir(_)) |
635 |
||
78562 | 636 |
val sessions_structure = |
80196 | 637 |
Sessions.load_structure(build_options, dirs = more_dirs ::: dirs). |
78562 | 638 |
selection(Sessions.Selection(sessions = build_master.sessions)) |
78219 | 639 |
|
78562 | 640 |
val build_deps = |
641 |
Sessions.deps(sessions_structure, progress = progress, inlined_files = true).check_errors |
|
78219 | 642 |
|
78562 | 643 |
val build_context = |
80196 | 644 |
Context(store, build_deps, engine = engine, hostname = hostname(build_options), |
645 |
numa_shuffling = numa_shuffling, build_uuid = build_master.build_uuid, |
|
646 |
build_start = Some(build_master.start), jobs = max_jobs.getOrElse(1)) |
|
78219 | 647 |
|
79707 | 648 |
engine.run_build_process(build_context, progress, server) |
78368
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
649 |
} |
6689b4c07bba
clarified signature: proper Scala function for command-line tool;
wenzelm
parents:
78280
diff
changeset
|
650 |
} |
77557 | 651 |
} |
652 |
||
78562 | 653 |
val isabelle_tool3 = Isabelle_Tool("build_worker", "start worker for session build process", |
77557 | 654 |
Scala_Project.here, |
655 |
{ args => |
|
78219 | 656 |
var build_id = "" |
77557 | 657 |
var numa_shuffling = false |
78405 | 658 |
val dirs = new mutable.ListBuffer[Path] |
79616 | 659 |
var max_jobs: Option[Int] = None |
78219 | 660 |
var options = |
79682
1fa1b32b0379
build local log_db, with store/restore via optional database server;
wenzelm
parents:
79679
diff
changeset
|
661 |
Options.init(specs = |
1fa1b32b0379
build local log_db, with store/restore via optional database server;
wenzelm
parents:
79679
diff
changeset
|
662 |
Options.Spec.ISABELLE_BUILD_OPTIONS ::: List(Options.Spec.make("build_database"))) |
78637 | 663 |
var quiet = false |
77557 | 664 |
var verbose = false |
665 |
||
666 |
val getopts = Getopts(""" |
|
78219 | 667 |
Usage: isabelle build_worker [OPTIONS] |
77557 | 668 |
|
669 |
Options are: |
|
78411 | 670 |
-B UUID existing UUID for build process (default: from database) |
77557 | 671 |
-N cyclic shuffling of NUMA CPU nodes (performance tuning) |
672 |
-d DIR include session directory |
|
673 |
-j INT maximum number of parallel jobs (default 1) |
|
674 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
78637 | 675 |
-q quiet mode: no progress |
77557 | 676 |
-v verbose |
77647 | 677 |
""", |
78410 | 678 |
"B:" -> (arg => build_id = arg), |
77557 | 679 |
"N" -> (_ => numa_shuffling = true), |
78405 | 680 |
"d:" -> (arg => dirs += Path.explode(arg)), |
79616 | 681 |
"j:" -> (arg => max_jobs = Some(Value.Nat.parse(arg))), |
77557 | 682 |
"o:" -> (arg => options = options + arg), |
78637 | 683 |
"q" -> (_ => quiet = true), |
77557 | 684 |
"v" -> (_ => verbose = true)) |
685 |
||
686 |
val more_args = getopts(args) |
|
687 |
if (more_args.nonEmpty) getopts.usage() |
|
688 |
||
78637 | 689 |
val progress = |
690 |
if (quiet && verbose) new Progress { override def verbose: Boolean = true } |
|
691 |
else if (quiet) new Progress |
|
692 |
else new Console_Progress(verbose = verbose) |
|
77557 | 693 |
|
80527
f6a9271cb177
ignore error code for "isabelle worker" (in contrast to eff08c3f89fe): avoid confusing "failed to work" messages via Build_Cluster.start;
wenzelm
parents:
80480
diff
changeset
|
694 |
progress.interrupt_handler { |
f6a9271cb177
ignore error code for "isabelle worker" (in contrast to eff08c3f89fe): avoid confusing "failed to work" messages via Build_Cluster.start;
wenzelm
parents:
80480
diff
changeset
|
695 |
build_worker(options, |
f6a9271cb177
ignore error code for "isabelle worker" (in contrast to eff08c3f89fe): avoid confusing "failed to work" messages via Build_Cluster.start;
wenzelm
parents:
80480
diff
changeset
|
696 |
build_id = build_id, |
f6a9271cb177
ignore error code for "isabelle worker" (in contrast to eff08c3f89fe): avoid confusing "failed to work" messages via Build_Cluster.start;
wenzelm
parents:
80480
diff
changeset
|
697 |
progress = progress, |
f6a9271cb177
ignore error code for "isabelle worker" (in contrast to eff08c3f89fe): avoid confusing "failed to work" messages via Build_Cluster.start;
wenzelm
parents:
80480
diff
changeset
|
698 |
dirs = dirs.toList, |
f6a9271cb177
ignore error code for "isabelle worker" (in contrast to eff08c3f89fe): avoid confusing "failed to work" messages via Build_Cluster.start;
wenzelm
parents:
80480
diff
changeset
|
699 |
numa_shuffling = Host.numa_check(progress, numa_shuffling), |
f6a9271cb177
ignore error code for "isabelle worker" (in contrast to eff08c3f89fe): avoid confusing "failed to work" messages via Build_Cluster.start;
wenzelm
parents:
80480
diff
changeset
|
700 |
max_jobs = max_jobs) |
f6a9271cb177
ignore error code for "isabelle worker" (in contrast to eff08c3f89fe): avoid confusing "failed to work" messages via Build_Cluster.start;
wenzelm
parents:
80480
diff
changeset
|
701 |
} |
77557 | 702 |
}) |
703 |
||
704 |
||
705 |
||
77563 | 706 |
/** "isabelle build_log" **/ |
77553 | 707 |
|
708 |
/* theory markup/messages from session database */ |
|
709 |
||
710 |
def read_theory( |
|
711 |
theory_context: Export.Theory_Context, |
|
712 |
unicode_symbols: Boolean = false |
|
713 |
): Option[Document.Snapshot] = { |
|
80447
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80350
diff
changeset
|
714 |
def decode(str: String): String = Symbol.output(unicode_symbols, str) |
77553 | 715 |
|
716 |
def read(name: String): Export.Entry = theory_context(name, permissive = true) |
|
717 |
||
718 |
def read_xml(name: String): XML.Body = |
|
80480
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
719 |
YXML.parse_body(read(name).bytes, recode = decode, cache = theory_context.cache) |
77553 | 720 |
|
78178 | 721 |
def read_source_file(name: String): Store.Source_File = |
77553 | 722 |
theory_context.session_context.source_file(name) |
723 |
||
724 |
for { |
|
725 |
id <- theory_context.document_id() |
|
726 |
(thy_file, blobs_files) <- theory_context.files(permissive = true) |
|
727 |
} |
|
728 |
yield { |
|
729 |
val master_dir = |
|
730 |
Path.explode(Url.strip_base_name(thy_file).getOrElse( |
|
731 |
error("Cannot determine theory master directory: " + quote(thy_file)))) |
|
732 |
||
733 |
val blobs = |
|
734 |
blobs_files.map { name => |
|
735 |
val path = Path.explode(name) |
|
736 |
val src_path = File.relative_path(master_dir, path).getOrElse(path) |
|
737 |
||
738 |
val file = read_source_file(name) |
|
739 |
val bytes = file.bytes |
|
80447
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80350
diff
changeset
|
740 |
val text = decode(bytes.text) |
77553 | 741 |
val chunk = Symbol.Text_Chunk(text) |
742 |
||
743 |
Command.Blob(Document.Node.Name(name), src_path, Some((file.digest, chunk))) -> |
|
744 |
Document.Blobs.Item(bytes, text, chunk, changed = false) |
|
745 |
} |
|
746 |
||
80447
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80350
diff
changeset
|
747 |
val thy_source = decode(read_source_file(thy_file).bytes.text) |
77553 | 748 |
val thy_xml = read_xml(Export.MARKUP) |
749 |
val blobs_xml = |
|
750 |
for (i <- (1 to blobs.length).toList) |
|
751 |
yield read_xml(Export.MARKUP + i) |
|
752 |
||
753 |
val markups_index = Command.Markup_Index.make(blobs.map(_._1)) |
|
754 |
val markups = |
|
755 |
Command.Markups.make( |
|
756 |
for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml)) |
|
757 |
yield index -> Markup_Tree.from_XML(xml)) |
|
758 |
||
759 |
val results = |
|
760 |
Command.Results.make( |
|
78592 | 761 |
for (case elem@XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES)) |
77553 | 762 |
yield i -> elem) |
763 |
||
764 |
val command = |
|
765 |
Command.unparsed(thy_source, theory = true, id = id, |
|
766 |
node_name = Document.Node.Name(thy_file, theory = theory_context.theory), |
|
767 |
blobs_info = Command.Blobs_Info.make(blobs), |
|
768 |
markups = markups, results = results) |
|
769 |
||
770 |
val doc_blobs = Document.Blobs.make(blobs) |
|
771 |
||
772 |
Document.State.init.snippet(command, doc_blobs) |
|
773 |
} |
|
774 |
} |
|
775 |
||
776 |
||
777 |
/* print messages */ |
|
778 |
||
779 |
def print_log( |
|
780 |
options: Options, |
|
781 |
sessions: List[String], |
|
782 |
theories: List[String] = Nil, |
|
783 |
message_head: List[Regex] = Nil, |
|
784 |
message_body: List[Regex] = Nil, |
|
785 |
progress: Progress = new Progress, |
|
786 |
margin: Double = Pretty.default_margin, |
|
787 |
breakgain: Double = Pretty.default_breakgain, |
|
788 |
metric: Pretty.Metric = Symbol.Metric, |
|
789 |
unicode_symbols: Boolean = false |
|
790 |
): Unit = { |
|
78178 | 791 |
val store = Store(options) |
77553 | 792 |
val session = new Session(options, Resources.bootstrap) |
793 |
||
794 |
def check(filter: List[Regex], make_string: => String): Boolean = |
|
795 |
filter.isEmpty || { |
|
80817 | 796 |
val s = Protocol_Message.clean_output(make_string) |
797 |
filter.forall(r => r.findFirstIn(Protocol_Message.clean_output(s)).nonEmpty) |
|
77553 | 798 |
} |
799 |
||
800 |
def print(session_name: String): Unit = { |
|
801 |
using(Export.open_session_context0(store, session_name)) { session_context => |
|
802 |
val result = |
|
803 |
for { |
|
804 |
db <- session_context.session_db() |
|
805 |
theories = store.read_theories(db, session_name) |
|
806 |
errors = store.read_errors(db, session_name) |
|
807 |
info <- store.read_build(db, session_name) |
|
808 |
} yield (theories, errors, info.return_code) |
|
809 |
result match { |
|
810 |
case None => store.error_database(session_name) |
|
811 |
case Some((used_theories, errors, rc)) => |
|
812 |
theories.filterNot(used_theories.toSet) match { |
|
813 |
case Nil => |
|
814 |
case bad => error("Unknown theories " + commas_quote(bad)) |
|
815 |
} |
|
816 |
val print_theories = |
|
817 |
if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet) |
|
818 |
||
819 |
for (thy <- print_theories) { |
|
820 |
val thy_heading = "\nTheory " + quote(thy) + " (in " + session_name + ")" + ":" |
|
821 |
||
78280 | 822 |
Build.read_theory(session_context.theory(thy), unicode_symbols = unicode_symbols) match { |
77553 | 823 |
case None => progress.echo(thy_heading + " MISSING") |
824 |
case Some(snapshot) => |
|
825 |
val rendering = new Rendering(snapshot, options, session) |
|
826 |
val messages = |
|
827 |
rendering.text_messages(Text.Range.full) |
|
828 |
.filter(message => progress.verbose || Protocol.is_exported(message.info)) |
|
829 |
if (messages.nonEmpty) { |
|
830 |
val line_document = Line.Document(snapshot.node.source) |
|
831 |
val buffer = new mutable.ListBuffer[String] |
|
832 |
for (Text.Info(range, elem) <- messages) { |
|
833 |
val line = line_document.position(range.start).line1 |
|
834 |
val pos = Position.Line_File(line, snapshot.node_name.node) |
|
835 |
def message_text: String = |
|
836 |
Protocol.message_text(elem, heading = true, pos = pos, |
|
837 |
margin = margin, breakgain = breakgain, metric = metric) |
|
838 |
val ok = |
|
839 |
check(message_head, Protocol.message_heading(elem, pos)) && |
|
80807 | 840 |
check(message_body, Pretty.unformatted_string_of(List(elem))) |
77553 | 841 |
if (ok) buffer += message_text |
842 |
} |
|
843 |
if (buffer.nonEmpty) { |
|
844 |
progress.echo(thy_heading) |
|
845 |
buffer.foreach(progress.echo(_)) |
|
846 |
} |
|
847 |
} |
|
848 |
} |
|
849 |
} |
|
850 |
||
851 |
if (errors.nonEmpty) { |
|
852 |
val msg = Symbol.output(unicode_symbols, cat_lines(errors)) |
|
853 |
progress.echo("\nBuild errors:\n" + Output.error_message_text(msg)) |
|
854 |
} |
|
855 |
if (rc != Process_Result.RC.ok) { |
|
856 |
progress.echo("\n" + Process_Result.RC.print_long(rc)) |
|
857 |
} |
|
858 |
} |
|
859 |
} |
|
860 |
} |
|
861 |
||
862 |
val errors = new mutable.ListBuffer[String] |
|
863 |
for (session_name <- sessions) { |
|
78705
fde0b195cb7d
clarified signature: avoid association with potentially dangerous Exn.capture;
wenzelm
parents:
78643
diff
changeset
|
864 |
Exn.result(print(session_name)) match { |
77553 | 865 |
case Exn.Res(_) => |
866 |
case Exn.Exn(exn) => errors += Exn.message(exn) |
|
867 |
} |
|
868 |
} |
|
869 |
if (errors.nonEmpty) error(cat_lines(errors.toList)) |
|
870 |
} |
|
871 |
||
872 |
||
79629 | 873 |
/* Isabelle tool wrapper */ |
77553 | 874 |
|
78562 | 875 |
val isabelle_tool4 = Isabelle_Tool("build_log", "print messages from session build database", |
77553 | 876 |
Scala_Project.here, |
877 |
{ args => |
|
878 |
/* arguments */ |
|
879 |
||
78405 | 880 |
val message_head = new mutable.ListBuffer[Regex] |
881 |
val message_body = new mutable.ListBuffer[Regex] |
|
77553 | 882 |
var unicode_symbols = false |
78405 | 883 |
val theories = new mutable.ListBuffer[String] |
77553 | 884 |
var margin = Pretty.default_margin |
885 |
var options = Options.init() |
|
886 |
var verbose = false |
|
887 |
||
888 |
val getopts = Getopts(""" |
|
77563 | 889 |
Usage: isabelle build_log [OPTIONS] [SESSIONS ...] |
77553 | 890 |
|
891 |
Options are: |
|
892 |
-H REGEX filter messages by matching against head |
|
893 |
-M REGEX filter messages by matching against body |
|
894 |
-T NAME restrict to given theories (multiple options possible) |
|
895 |
-U output Unicode symbols |
|
896 |
-m MARGIN margin for pretty printing (default: """ + margin + """) |
|
897 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
898 |
-v print all messages, including information etc. |
|
899 |
||
77554
4465d9dff448
clarified terminology of "session build database", while "build database" is the one underlying Build_Process;
wenzelm
parents:
77553
diff
changeset
|
900 |
Print messages from the session build database of the given sessions, |
4465d9dff448
clarified terminology of "session build database", while "build database" is the one underlying Build_Process;
wenzelm
parents:
77553
diff
changeset
|
901 |
without any checks against current sources nor session structure: results |
4465d9dff448
clarified terminology of "session build database", while "build database" is the one underlying Build_Process;
wenzelm
parents:
77553
diff
changeset
|
902 |
from old sessions or failed builds can be printed as well. |
77553 | 903 |
|
904 |
Multiple options -H and -M are conjunctive: all given patterns need to |
|
905 |
match. Patterns match any substring, but ^ or $ may be used to match the |
|
906 |
start or end explicitly. |
|
907 |
""", |
|
78405 | 908 |
"H:" -> (arg => message_head += arg.r), |
909 |
"M:" -> (arg => message_body += arg.r), |
|
910 |
"T:" -> (arg => theories += arg), |
|
77553 | 911 |
"U" -> (_ => unicode_symbols = true), |
912 |
"m:" -> (arg => margin = Value.Double.parse(arg)), |
|
913 |
"o:" -> (arg => options = options + arg), |
|
914 |
"v" -> (_ => verbose = true)) |
|
915 |
||
916 |
val sessions = getopts(args) |
|
917 |
||
918 |
val progress = new Console_Progress(verbose = verbose) |
|
919 |
||
920 |
if (sessions.isEmpty) progress.echo_warning("No sessions to print") |
|
921 |
else { |
|
78405 | 922 |
print_log(options, sessions, theories = theories.toList, message_head = message_head.toList, |
923 |
message_body = message_body.toList, margin = margin, progress = progress, |
|
77553 | 924 |
unicode_symbols = unicode_symbols) |
925 |
} |
|
926 |
}) |
|
48276 | 927 |
} |