7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 object Update { |
10 object Update { |
11 def update(options: Options, |
11 def update(options: Options, |
|
12 selection: Sessions.Selection = Sessions.Selection.empty, |
12 base_logics: List[String] = Nil, |
13 base_logics: List[String] = Nil, |
13 progress: Progress = new Progress, |
14 progress: Progress = new Progress, |
14 dirs: List[Path] = Nil, |
15 dirs: List[Path] = Nil, |
15 select_dirs: List[Path] = Nil, |
16 select_dirs: List[Path] = Nil, |
16 selection: Sessions.Selection = Sessions.Selection.empty |
17 numa_shuffling: Boolean = false, |
|
18 max_jobs: Int = 1, |
|
19 no_build: Boolean = false, |
|
20 verbose: Boolean = false |
17 ): Build.Results = { |
21 ): Build.Results = { |
18 /* excluded sessions */ |
22 /* excluded sessions */ |
19 |
23 |
20 val exclude: Set[String] = |
24 val exclude: Set[String] = |
21 if (base_logics.isEmpty) Set.empty |
25 if (base_logics.isEmpty) Set.empty |
34 |
38 |
35 /* build */ |
39 /* build */ |
36 |
40 |
37 val build_results = |
41 val build_results = |
38 Build.build(options, progress = progress, dirs = dirs, select_dirs = select_dirs, |
42 Build.build(options, progress = progress, dirs = dirs, select_dirs = select_dirs, |
39 selection = selection) |
43 selection = selection, numa_shuffling = numa_shuffling, max_jobs = max_jobs, |
40 |
44 no_build = no_build, verbose = verbose) |
41 if (!build_results.ok) error("Build failed") |
|
42 |
45 |
43 val store = build_results.store |
46 val store = build_results.store |
44 val sessions_structure = build_results.deps.sessions_structure |
47 val sessions_structure = build_results.deps.sessions_structure |
45 |
48 |
46 |
49 |
63 } |
66 } |
64 |
67 |
65 var seen_theory = Set.empty[String] |
68 var seen_theory = Set.empty[String] |
66 |
69 |
67 using(Export.open_database_context(store)) { database_context => |
70 using(Export.open_database_context(store)) { database_context => |
68 for (session <- sessions_structure.build_topological_order if !exclude(session)) { |
71 for { |
|
72 session <- sessions_structure.build_topological_order |
|
73 if build_results(session).ok && !exclude(session) |
|
74 } { |
|
75 progress.echo("Session " + session + " ...") |
69 using(database_context.open_session0(session)) { session_context => |
76 using(database_context.open_session0(session)) { session_context => |
70 for { |
77 for { |
71 db <- session_context.session_db() |
78 db <- session_context.session_db() |
72 theory <- store.read_theories(db, session) |
79 theory <- store.read_theories(db, session) |
73 if !seen_theory(theory) |
80 if !seen_theory(theory) |
104 val isabelle_tool = |
111 val isabelle_tool = |
105 Isabelle_Tool("update", "update theory sources based on PIDE markup", Scala_Project.here, |
112 Isabelle_Tool("update", "update theory sources based on PIDE markup", Scala_Project.here, |
106 { args => |
113 { args => |
107 var base_sessions: List[String] = Nil |
114 var base_sessions: List[String] = Nil |
108 var select_dirs: List[Path] = Nil |
115 var select_dirs: List[Path] = Nil |
|
116 var numa_shuffling = false |
109 var requirements = false |
117 var requirements = false |
110 var exclude_session_groups: List[String] = Nil |
118 var exclude_session_groups: List[String] = Nil |
111 var all_sessions = false |
119 var all_sessions = false |
112 var dirs: List[Path] = Nil |
120 var dirs: List[Path] = Nil |
113 var session_groups: List[String] = Nil |
121 var session_groups: List[String] = Nil |
114 var base_logics: List[String] = Nil |
122 var base_logics: List[String] = Nil |
|
123 var max_jobs = 1 |
|
124 var no_build = false |
115 var options = Options.init() |
125 var options = Options.init() |
116 var verbose = false |
126 var verbose = false |
117 var exclude_sessions: List[String] = Nil |
127 var exclude_sessions: List[String] = Nil |
118 |
128 |
119 val getopts = Getopts(""" |
129 val getopts = Getopts(""" |
126 -X NAME exclude sessions from group NAME and all descendants |
136 -X NAME exclude sessions from group NAME and all descendants |
127 -a select all sessions |
137 -a select all sessions |
128 -b NAME additional base logic |
138 -b NAME additional base logic |
129 -d DIR include session directory |
139 -d DIR include session directory |
130 -g NAME select session group NAME |
140 -g NAME select session group NAME |
|
141 -j INT maximum number of parallel jobs (default 1) |
|
142 -n no build -- take existing build databases |
131 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
143 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
132 -u OPT override "update" option: shortcut for "-o update_OPT" |
144 -u OPT override "update" option: shortcut for "-o update_OPT" |
133 -v verbose |
145 -v verbose |
134 -x NAME exclude session NAME and all descendants |
146 -x NAME exclude session NAME and all descendants |
135 |
147 |
136 Update theory sources based on PIDE markup. |
148 Update theory sources based on PIDE markup. |
137 """, |
149 """, |
138 "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), |
150 "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), |
139 "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), |
151 "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), |
|
152 "N" -> (_ => numa_shuffling = true), |
140 "R" -> (_ => requirements = true), |
153 "R" -> (_ => requirements = true), |
141 "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), |
154 "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), |
142 "a" -> (_ => all_sessions = true), |
155 "a" -> (_ => all_sessions = true), |
143 "b:" -> (arg => base_logics ::= arg), |
156 "b:" -> (arg => base_logics ::= arg), |
144 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
157 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
145 "g:" -> (arg => session_groups = session_groups ::: List(arg)), |
158 "g:" -> (arg => session_groups = session_groups ::: List(arg)), |
|
159 "j:" -> (arg => max_jobs = Value.Int.parse(arg)), |
|
160 "n" -> (_ => no_build = true), |
146 "o:" -> (arg => options = options + arg), |
161 "o:" -> (arg => options = options + arg), |
147 "u:" -> (arg => options = options + ("update_" + arg)), |
162 "u:" -> (arg => options = options + ("update_" + arg)), |
148 "v" -> (_ => verbose = true), |
163 "v" -> (_ => verbose = true), |
149 "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) |
164 "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) |
150 |
165 |
153 val progress = new Console_Progress(verbose = verbose) |
168 val progress = new Console_Progress(verbose = verbose) |
154 |
169 |
155 val results = |
170 val results = |
156 progress.interrupt_handler { |
171 progress.interrupt_handler { |
157 update(options, |
172 update(options, |
158 base_logics = base_logics, |
|
159 progress = progress, |
|
160 dirs = dirs, |
|
161 select_dirs = select_dirs, |
|
162 selection = Sessions.Selection( |
173 selection = Sessions.Selection( |
163 requirements = requirements, |
174 requirements = requirements, |
164 all_sessions = all_sessions, |
175 all_sessions = all_sessions, |
165 base_sessions = base_sessions, |
176 base_sessions = base_sessions, |
166 exclude_session_groups = exclude_session_groups, |
177 exclude_session_groups = exclude_session_groups, |
167 exclude_sessions = exclude_sessions, |
178 exclude_sessions = exclude_sessions, |
168 session_groups = session_groups, |
179 session_groups = session_groups, |
169 sessions = sessions)) |
180 sessions = sessions), |
|
181 base_logics = base_logics, |
|
182 progress = progress, |
|
183 dirs = dirs, |
|
184 select_dirs = select_dirs, |
|
185 numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling), |
|
186 max_jobs = max_jobs, |
|
187 no_build = no_build, |
|
188 verbose = verbose) |
170 } |
189 } |
171 |
190 |
172 sys.exit(results.rc) |
191 sys.exit(results.rc) |
173 }) |
192 }) |
174 } |
193 } |