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