author | wenzelm |
Sat, 14 Jan 2023 19:29:14 +0100 | |
changeset 76969 | d1fbd04a976e |
parent 76968 | fd4195298eff |
child 76970 | 7d23555fda83 |
permissions | -rw-r--r-- |
69557 | 1 |
/* Title: Pure/Tools/update.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Update theory sources based on PIDE markup. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
75393 | 10 |
object Update { |
76969 | 11 |
val update_elements: Markup.Elements = |
12 |
Markup.Elements(Markup.UPDATE, Markup.LANGUAGE) |
|
13 |
||
14 |
def update_xml(options: Options, xml: XML.Body): XML.Body = { |
|
15 |
val path_cartouches = options.bool("update_path_cartouches") |
|
16 |
||
17 |
def upd(lang: Markup.Language, ts: XML.Body): XML.Body = |
|
18 |
ts flatMap { |
|
19 |
case XML.Wrapped_Elem(markup, body1, body2) => |
|
20 |
val body = if (markup.name == Markup.UPDATE) body1 else body2 |
|
21 |
upd(lang, body) |
|
22 |
case XML.Elem(Markup.Language(lang1), body) => |
|
23 |
if (lang1.is_path && path_cartouches) { |
|
24 |
Token.read_embedded(Keyword.Keywords.empty, XML.content(body)) match { |
|
25 |
case Some(tok) => List(XML.Text(Symbol.cartouche(tok.content))) |
|
26 |
case None => upd(lang1, body) |
|
27 |
} |
|
28 |
} |
|
29 |
else upd(lang1, body) |
|
30 |
case XML.Elem(_, body) => upd(lang, body) |
|
31 |
case t => List(t) |
|
32 |
} |
|
33 |
upd(Markup.Language.outer, xml) |
|
34 |
} |
|
35 |
||
76918
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
36 |
def update(options: Options, |
76927
da13da82f6f9
treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
wenzelm
parents:
76926
diff
changeset
|
37 |
update_options: List[Options.Spec], |
76920 | 38 |
selection: Sessions.Selection = Sessions.Selection.empty, |
76918
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
39 |
base_logics: List[String] = Nil, |
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71573
diff
changeset
|
40 |
progress: Progress = new Progress, |
76926 | 41 |
build_heap: Boolean = false, |
42 |
clean_build: Boolean = false, |
|
69557 | 43 |
dirs: List[Path] = Nil, |
44 |
select_dirs: List[Path] = Nil, |
|
76920 | 45 |
numa_shuffling: Boolean = false, |
46 |
max_jobs: Int = 1, |
|
76926 | 47 |
fresh_build: Boolean = false, |
76920 | 48 |
no_build: Boolean = false, |
49 |
verbose: Boolean = false |
|
76918
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
50 |
): Build.Results = { |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
51 |
/* excluded sessions */ |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
52 |
|
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
53 |
val exclude: Set[String] = |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
54 |
if (base_logics.isEmpty) Set.empty |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
55 |
else { |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
56 |
val sessions = |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
57 |
Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs) |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
58 |
.selection(selection) |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
59 |
|
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
60 |
for (name <- base_logics if !sessions.defined(name)) { |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
61 |
error("Base logic " + quote(name) + " outside of session selection") |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
62 |
} |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
63 |
|
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
64 |
sessions.build_requirements(base_logics).toSet |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
65 |
} |
69557 | 66 |
|
76927
da13da82f6f9
treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
wenzelm
parents:
76926
diff
changeset
|
67 |
// test |
da13da82f6f9
treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
wenzelm
parents:
76926
diff
changeset
|
68 |
options ++ update_options |
da13da82f6f9
treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
wenzelm
parents:
76926
diff
changeset
|
69 |
|
da13da82f6f9
treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
wenzelm
parents:
76926
diff
changeset
|
70 |
def augment_options(name: String): List[Options.Spec] = |
da13da82f6f9
treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
wenzelm
parents:
76926
diff
changeset
|
71 |
if (exclude(name)) Nil else update_options |
da13da82f6f9
treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
wenzelm
parents:
76926
diff
changeset
|
72 |
|
76918
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
73 |
|
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
74 |
/* build */ |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
75 |
|
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
76 |
val build_results = |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
77 |
Build.build(options, progress = progress, dirs = dirs, select_dirs = select_dirs, |
76928 | 78 |
selection = selection, build_heap = build_heap, clean_build = clean_build, |
79 |
numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build, |
|
76927
da13da82f6f9
treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
wenzelm
parents:
76926
diff
changeset
|
80 |
no_build = no_build, verbose = verbose, augment_options = augment_options) |
76918
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
81 |
|
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
82 |
val store = build_results.store |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
83 |
val sessions_structure = build_results.deps.sessions_structure |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
84 |
|
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
85 |
|
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
86 |
/* update */ |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
87 |
|
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
88 |
var seen_theory = Set.empty[String] |
69571 | 89 |
|
76918
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
90 |
using(Export.open_database_context(store)) { database_context => |
76920 | 91 |
for { |
92 |
session <- sessions_structure.build_topological_order |
|
93 |
if build_results(session).ok && !exclude(session) |
|
94 |
} { |
|
95 |
progress.echo("Session " + session + " ...") |
|
76929 | 96 |
val proper_session_theory = |
97 |
build_results.deps(session).proper_session_theories.map(_.theory).toSet |
|
76918
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
98 |
using(database_context.open_session0(session)) { session_context => |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
99 |
for { |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
100 |
db <- session_context.session_db() |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
101 |
theory <- store.read_theories(db, session) |
76929 | 102 |
if proper_session_theory(theory) && !seen_theory(theory) |
76918
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
103 |
} { |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
104 |
seen_theory += theory |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
105 |
val theory_context = session_context.theory(theory) |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
106 |
for { |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
107 |
theory_snapshot <- Build_Job.read_theory(theory_context) |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
108 |
node_name <- theory_snapshot.node_files |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
109 |
snapshot = theory_snapshot.switch(node_name) |
76924 | 110 |
if snapshot.node.source_wellformed |
76918
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
111 |
} { |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
112 |
progress.expose_interrupt() |
76969 | 113 |
val xml = snapshot.xml_markup(elements = update_elements) |
114 |
val source1 = XML.content(update_xml(options, xml)) |
|
76918
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
115 |
if (source1 != snapshot.node.source) { |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
116 |
val path = Path.explode(node_name.node) |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
117 |
progress.echo("Updating " + quote(File.standard_path(path))) |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
118 |
File.write(path, source1) |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
119 |
} |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
120 |
} |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
121 |
} |
70640
5f4b8a505090
more explicit type Dump.Session, with context information;
wenzelm
parents:
69896
diff
changeset
|
122 |
} |
75393 | 123 |
} |
76918
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
124 |
} |
70876 | 125 |
|
76918
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
126 |
build_results |
69557 | 127 |
} |
128 |
||
129 |
||
130 |
/* Isabelle tool wrapper */ |
|
131 |
||
132 |
val isabelle_tool = |
|
72763 | 133 |
Isabelle_Tool("update", "update theory sources based on PIDE markup", Scala_Project.here, |
75394 | 134 |
{ args => |
135 |
var base_sessions: List[String] = Nil |
|
136 |
var select_dirs: List[Path] = Nil |
|
76920 | 137 |
var numa_shuffling = false |
75394 | 138 |
var requirements = false |
139 |
var exclude_session_groups: List[String] = Nil |
|
140 |
var all_sessions = false |
|
76926 | 141 |
var build_heap = false |
142 |
var clean_build = false |
|
75394 | 143 |
var dirs: List[Path] = Nil |
76926 | 144 |
var fresh_build = false |
75394 | 145 |
var session_groups: List[String] = Nil |
76925
47f1b099497c
tuned options --- avoid confusion with "isabelle build -b";
wenzelm
parents:
76924
diff
changeset
|
146 |
var max_jobs = 1 |
76918
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
147 |
var base_logics: List[String] = Nil |
76920 | 148 |
var no_build = false |
75394 | 149 |
var options = Options.init() |
76927
da13da82f6f9
treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
wenzelm
parents:
76926
diff
changeset
|
150 |
var update_options: List[Options.Spec] = Nil |
75394 | 151 |
var verbose = false |
152 |
var exclude_sessions: List[String] = Nil |
|
69557 | 153 |
|
75394 | 154 |
val getopts = Getopts(""" |
69557 | 155 |
Usage: isabelle update [OPTIONS] [SESSIONS ...] |
156 |
||
157 |
Options are: |
|
158 |
-B NAME include session NAME and all descendants |
|
159 |
-D DIR include session directory and select its sessions |
|
71807 | 160 |
-R refer to requirements of selected sessions |
69557 | 161 |
-X NAME exclude sessions from group NAME and all descendants |
162 |
-a select all sessions |
|
76926 | 163 |
-b build heap images |
164 |
-c clean build |
|
69557 | 165 |
-d DIR include session directory |
76926 | 166 |
-f fresh build |
69557 | 167 |
-g NAME select session group NAME |
76920 | 168 |
-j INT maximum number of parallel jobs (default 1) |
76925
47f1b099497c
tuned options --- avoid confusion with "isabelle build -b";
wenzelm
parents:
76924
diff
changeset
|
169 |
-l NAME additional base logic |
76920 | 170 |
-n no build -- take existing build databases |
69557 | 171 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
76927
da13da82f6f9
treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
wenzelm
parents:
76926
diff
changeset
|
172 |
-u OPT override "update" option for selected sessions |
69557 | 173 |
-v verbose |
174 |
-x NAME exclude session NAME and all descendants |
|
175 |
||
76926 | 176 |
Update theory sources based on PIDE markup produced by "isabelle build". |
69557 | 177 |
""", |
75394 | 178 |
"B:" -> (arg => base_sessions = base_sessions ::: List(arg)), |
179 |
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), |
|
76920 | 180 |
"N" -> (_ => numa_shuffling = true), |
75394 | 181 |
"R" -> (_ => requirements = true), |
182 |
"X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), |
|
183 |
"a" -> (_ => all_sessions = true), |
|
76926 | 184 |
"b" -> (_ => build_heap = true), |
185 |
"c" -> (_ => clean_build = true), |
|
75394 | 186 |
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
76926 | 187 |
"f" -> (_ => fresh_build = true), |
75394 | 188 |
"g:" -> (arg => session_groups = session_groups ::: List(arg)), |
76920 | 189 |
"j:" -> (arg => max_jobs = Value.Int.parse(arg)), |
76925
47f1b099497c
tuned options --- avoid confusion with "isabelle build -b";
wenzelm
parents:
76924
diff
changeset
|
190 |
"l:" -> (arg => base_logics ::= arg), |
76920 | 191 |
"n" -> (_ => no_build = true), |
75394 | 192 |
"o:" -> (arg => options = options + arg), |
76927
da13da82f6f9
treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
wenzelm
parents:
76926
diff
changeset
|
193 |
"u:" -> (arg => update_options = update_options ::: List(("update_" + arg, None))), |
75394 | 194 |
"v" -> (_ => verbose = true), |
195 |
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) |
|
69557 | 196 |
|
75394 | 197 |
val sessions = getopts(args) |
69557 | 198 |
|
75394 | 199 |
val progress = new Console_Progress(verbose = verbose) |
69557 | 200 |
|
76918
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
201 |
val results = |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
202 |
progress.interrupt_handler { |
76927
da13da82f6f9
treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
wenzelm
parents:
76926
diff
changeset
|
203 |
update(options, update_options, |
76918
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
204 |
selection = Sessions.Selection( |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
205 |
requirements = requirements, |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
206 |
all_sessions = all_sessions, |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
207 |
base_sessions = base_sessions, |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
208 |
exclude_session_groups = exclude_session_groups, |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
209 |
exclude_sessions = exclude_sessions, |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
210 |
session_groups = session_groups, |
76920 | 211 |
sessions = sessions), |
212 |
base_logics = base_logics, |
|
213 |
progress = progress, |
|
76926 | 214 |
build_heap, |
215 |
clean_build, |
|
76920 | 216 |
dirs = dirs, |
217 |
select_dirs = select_dirs, |
|
218 |
numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling), |
|
219 |
max_jobs = max_jobs, |
|
76926 | 220 |
fresh_build, |
76920 | 221 |
no_build = no_build, |
222 |
verbose = verbose) |
|
76918
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
223 |
} |
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
224 |
|
19be7d89bf03
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
wenzelm
parents:
75394
diff
changeset
|
225 |
sys.exit(results.rc) |
75394 | 226 |
}) |
69557 | 227 |
} |