|
1 /* Title: Pure/Tools/update_tool.scala |
|
2 Author: Makarius |
|
3 |
|
4 Update theory sources based on PIDE markup. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object Update_Tool { |
|
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 update_path_cartouches = options.bool("update_path_cartouches") |
|
16 val update_cite = options.bool("update_cite") |
|
17 val cite_commands = Bibtex.cite_commands(options) |
|
18 |
|
19 def upd(lang: Markup.Language, ts: XML.Body): XML.Body = |
|
20 ts flatMap { |
|
21 case XML.Wrapped_Elem(markup, body1, body2) => |
|
22 val body = if (markup.name == Markup.UPDATE) body1 else body2 |
|
23 upd(lang, body) |
|
24 case XML.Elem(Markup.Language(lang1), body) => |
|
25 if (update_path_cartouches && lang1.is_path) { |
|
26 Token.read_embedded(Keyword.Keywords.empty, XML.content(body)) match { |
|
27 case Some(tok) => List(XML.Text(Symbol.cartouche(tok.content))) |
|
28 case None => upd(lang1, body) |
|
29 } |
|
30 } |
|
31 else if (update_cite && lang1.is_antiquotation) { |
|
32 List(XML.Text(Bibtex.update_cite_antiquotation(cite_commands, XML.content(body)))) |
|
33 } |
|
34 else upd(lang1, body) |
|
35 case XML.Elem(_, body) => upd(lang, body) |
|
36 case XML.Text(s) if update_cite && lang.is_document => |
|
37 List(XML.Text(Bibtex.update_cite_commands(s))) |
|
38 case t => List(t) |
|
39 } |
|
40 upd(Markup.Language.outer, xml) |
|
41 } |
|
42 |
|
43 def default_base_logic: String = Isabelle_System.getenv("ISABELLE_LOGIC") |
|
44 |
|
45 def update(options: Options, |
|
46 update_options: List[Options.Spec], |
|
47 selection: Sessions.Selection = Sessions.Selection.empty, |
|
48 base_logics: List[String] = Nil, |
|
49 progress: Progress = new Progress, |
|
50 build_heap: Boolean = false, |
|
51 clean_build: Boolean = false, |
|
52 dirs: List[Path] = Nil, |
|
53 select_dirs: List[Path] = Nil, |
|
54 numa_shuffling: Boolean = false, |
|
55 max_jobs: Option[Int] = None, |
|
56 fresh_build: Boolean = false, |
|
57 no_build: Boolean = false |
|
58 ): Build.Results = { |
|
59 /* excluded sessions */ |
|
60 |
|
61 val exclude: Set[String] = |
|
62 if (base_logics.isEmpty) Set.empty |
|
63 else { |
|
64 Sessions.load_structure(options, dirs = dirs ::: select_dirs) |
|
65 .selection(Sessions.Selection(sessions = base_logics)) |
|
66 .build_graph.domain |
|
67 } |
|
68 |
|
69 // test |
|
70 options ++ update_options |
|
71 |
|
72 def augment_options(name: String): List[Options.Spec] = |
|
73 if (exclude(name)) Nil else update_options |
|
74 |
|
75 |
|
76 /* build */ |
|
77 |
|
78 val build_options = options + "build_thorough" |
|
79 |
|
80 val build_results = |
|
81 Build.build(build_options, progress = progress, dirs = dirs, select_dirs = select_dirs, |
|
82 selection = selection, build_heap = build_heap, clean_build = clean_build, |
|
83 numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build, |
|
84 no_build = no_build, augment_options = augment_options) |
|
85 |
|
86 val store = build_results.store |
|
87 val sessions_structure = build_results.deps.sessions_structure |
|
88 |
|
89 |
|
90 /* update */ |
|
91 |
|
92 var seen_theory = Set.empty[String] |
|
93 |
|
94 using(Export.open_database_context(store)) { database_context => |
|
95 for { |
|
96 session <- sessions_structure.build_topological_order |
|
97 if build_results(session).ok && !exclude(session) |
|
98 } { |
|
99 progress.echo("Updating " + session + " ...") |
|
100 val session_options = sessions_structure(session).options |
|
101 val proper_session_theory = |
|
102 build_results.deps(session).proper_session_theories.map(_.theory).toSet |
|
103 using(database_context.open_session0(session)) { session_context => |
|
104 for { |
|
105 db <- session_context.session_db() |
|
106 theory <- store.read_theories(db, session) |
|
107 if proper_session_theory(theory) && !seen_theory(theory) |
|
108 } { |
|
109 seen_theory += theory |
|
110 val theory_context = session_context.theory(theory) |
|
111 for { |
|
112 theory_snapshot <- Build.read_theory(theory_context) |
|
113 node_name <- theory_snapshot.node_files |
|
114 snapshot = theory_snapshot.switch(node_name) |
|
115 if snapshot.node.source_wellformed |
|
116 } { |
|
117 progress.expose_interrupt() |
|
118 val xml = YXML.parse_body(YXML.string_of_body(snapshot.xml_markup(elements = update_elements))) |
|
119 val source1 = XML.content(update_xml(session_options, xml)) |
|
120 if (source1 != snapshot.node.source) { |
|
121 val path = Path.explode(node_name.node) |
|
122 progress.echo("File " + quote(File.standard_path(path))) |
|
123 File.write(path, source1) |
|
124 } |
|
125 } |
|
126 } |
|
127 } |
|
128 } |
|
129 } |
|
130 |
|
131 build_results |
|
132 } |
|
133 |
|
134 |
|
135 /* Isabelle tool wrapper */ |
|
136 |
|
137 val isabelle_tool = |
|
138 Isabelle_Tool("update", "update theory sources based on PIDE markup", Scala_Project.here, |
|
139 { args => |
|
140 var base_sessions: List[String] = Nil |
|
141 var select_dirs: List[Path] = Nil |
|
142 var numa_shuffling = false |
|
143 var requirements = false |
|
144 var exclude_session_groups: List[String] = Nil |
|
145 var all_sessions = false |
|
146 var build_heap = false |
|
147 var clean_build = false |
|
148 var dirs: List[Path] = Nil |
|
149 var fresh_build = false |
|
150 var session_groups: List[String] = Nil |
|
151 var max_jobs: Option[Int] = None |
|
152 var base_logics: List[String] = List(default_base_logic) |
|
153 var no_build = false |
|
154 var options = Options.init() |
|
155 var update_options: List[Options.Spec] = Nil |
|
156 var verbose = false |
|
157 var exclude_sessions: List[String] = Nil |
|
158 |
|
159 val getopts = Getopts(""" |
|
160 Usage: isabelle update [OPTIONS] [SESSIONS ...] |
|
161 |
|
162 Options are: |
|
163 -B NAME include session NAME and all descendants |
|
164 -D DIR include session directory and select its sessions |
|
165 -R refer to requirements of selected sessions |
|
166 -X NAME exclude sessions from group NAME and all descendants |
|
167 -a select all sessions |
|
168 -b build heap images |
|
169 -c clean build |
|
170 -d DIR include session directory |
|
171 -f fresh build |
|
172 -g NAME select session group NAME |
|
173 -j INT maximum number of parallel jobs (default 1) |
|
174 -l NAMES comma-separated list of base logics, to remain unchanged |
|
175 (default: """ + quote(default_base_logic) + """) |
|
176 -n no build -- take existing session build databases |
|
177 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
178 -u OPT override "update" option for selected sessions |
|
179 -v verbose |
|
180 -x NAME exclude session NAME and all descendants |
|
181 |
|
182 Update theory sources based on PIDE markup produced by "isabelle build". |
|
183 """, |
|
184 "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), |
|
185 "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), |
|
186 "N" -> (_ => numa_shuffling = true), |
|
187 "R" -> (_ => requirements = true), |
|
188 "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), |
|
189 "a" -> (_ => all_sessions = true), |
|
190 "b" -> (_ => build_heap = true), |
|
191 "c" -> (_ => clean_build = true), |
|
192 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
|
193 "f" -> (_ => fresh_build = true), |
|
194 "g:" -> (arg => session_groups = session_groups ::: List(arg)), |
|
195 "j:" -> (arg => max_jobs = Some(Value.Nat.parse(arg))), |
|
196 "l:" -> (arg => base_logics = space_explode(',', arg)), |
|
197 "n" -> (_ => no_build = true), |
|
198 "o:" -> (arg => options = options + arg), |
|
199 "u:" -> (arg => update_options = update_options ::: List(Options.Spec("update_" + arg))), |
|
200 "v" -> (_ => verbose = true), |
|
201 "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) |
|
202 |
|
203 val sessions = getopts(args) |
|
204 |
|
205 val progress = new Console_Progress(verbose = verbose) |
|
206 |
|
207 val results = |
|
208 progress.interrupt_handler { |
|
209 update(options, update_options, |
|
210 selection = Sessions.Selection( |
|
211 requirements = requirements, |
|
212 all_sessions = all_sessions, |
|
213 base_sessions = base_sessions, |
|
214 exclude_session_groups = exclude_session_groups, |
|
215 exclude_sessions = exclude_sessions, |
|
216 session_groups = session_groups, |
|
217 sessions = sessions), |
|
218 base_logics = base_logics, |
|
219 progress = progress, |
|
220 build_heap = build_heap, |
|
221 clean_build = clean_build, |
|
222 dirs = dirs, |
|
223 select_dirs = select_dirs, |
|
224 numa_shuffling = Host.numa_check(progress, numa_shuffling), |
|
225 max_jobs = max_jobs, |
|
226 fresh_build = fresh_build, |
|
227 no_build = no_build) |
|
228 } |
|
229 |
|
230 sys.exit(results.rc) |
|
231 }) |
|
232 } |