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