19 private val default_threads = 1 |
19 private val default_threads = 1 |
20 private val default_heap = 1000 |
20 private val default_heap = 1000 |
21 private val default_isabelle_identifier = "build_history" |
21 private val default_isabelle_identifier = "build_history" |
22 |
22 |
23 def build_history( |
23 def build_history( |
|
24 progress: Progress, |
24 hg: Mercurial.Repository, |
25 hg: Mercurial.Repository, |
25 rev: String = default_rev, |
26 rev: String = default_rev, |
26 isabelle_identifier: String = default_isabelle_identifier, |
27 isabelle_identifier: String = default_isabelle_identifier, |
27 components_base: String = "", |
28 components_base: String = "", |
28 fresh: Boolean = false, |
29 fresh: Boolean = false, |
33 max_heap: Option[Int] = None, |
34 max_heap: Option[Int] = None, |
34 more_settings: List[String] = Nil, |
35 more_settings: List[String] = Nil, |
35 verbose: Boolean = false, |
36 verbose: Boolean = false, |
36 build_args: List[String] = Nil): Process_Result = |
37 build_args: List[String] = Nil): Process_Result = |
37 { |
38 { |
|
39 /* output */ |
|
40 |
|
41 def output(msg: String) { progress.echo(msg) } |
|
42 def output_if(b: Boolean, msg: String) { if (b) output(msg) } |
|
43 |
|
44 |
38 /* sanity checks */ |
45 /* sanity checks */ |
39 |
46 |
40 if (threads < 1) error("Bad threads value < 1: " + threads) |
47 if (threads < 1) error("Bad threads value < 1: " + threads) |
41 |
48 |
42 if (heap < 100) error("Bad heap value < 100: " + heap) |
49 if (heap < 100) error("Bad heap value < 100: " + heap) |
51 |
58 |
52 |
59 |
53 /* purge repository */ |
60 /* purge repository */ |
54 |
61 |
55 hg.update(rev = rev, clean = true) |
62 hg.update(rev = rev, clean = true) |
56 if (verbose) Output.writeln(hg.log(rev, options = "-l1")) |
63 output_if(verbose, hg.log(rev, options = "-l1")) |
57 |
64 |
58 |
65 |
59 /* invoke isabelle tools */ |
66 /* invoke isabelle tools */ |
60 |
67 |
61 def bash(script: String, redirect: Boolean = false): Process_Result = |
68 def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = |
62 Isabelle_System.bash("env ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + |
69 Isabelle_System.bash("env ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + |
63 " " + script, cwd = hg.root.file, env = null, redirect = redirect) |
70 " " + script, cwd = hg.root.file, env = null, redirect = redirect, |
64 |
71 progress_stdout = output_if(echo, _), progress_stderr = output_if(echo, _)) |
65 def isabelle(cmdline: String, redirect: Boolean = false): Process_Result = |
72 |
66 bash("bin/isabelle " + cmdline, redirect) |
73 def isabelle(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = |
67 |
74 bash("bin/isabelle " + cmdline, redirect, echo) |
68 val isabelle_home_user: Path = Path.explode(isabelle("getenv -b ISABELLE_HOME_USER").check.out) |
75 |
|
76 val isabelle_home_user = Path.explode(isabelle("getenv -b ISABELLE_HOME_USER").check.out) |
69 |
77 |
70 |
78 |
71 /* reset settings */ |
79 /* reset settings */ |
72 |
80 |
73 val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings") |
81 val etc_settings = isabelle_home_user + Path.explode("etc/settings") |
74 |
82 |
75 if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle")) |
83 if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle")) |
76 error("Cannot proceed with existing user settings file: " + etc_settings) |
84 error("Cannot proceed with existing user settings file: " + etc_settings) |
77 |
85 |
78 Isabelle_System.mkdirs(etc_settings.dir) |
86 Isabelle_System.mkdirs(etc_settings.dir) |
158 File.append(etc_settings, "\n" + Library.terminate_lines(more_settings)) |
166 File.append(etc_settings, "\n" + Library.terminate_lines(more_settings)) |
159 |
167 |
160 |
168 |
161 /* build */ |
169 /* build */ |
162 |
170 |
163 isabelle("components -a", redirect = true).check.print_if(verbose) |
171 isabelle("components -a", redirect = true, echo = verbose).check |
164 isabelle("jedit -b" + (if (fresh) " -f" else ""), redirect = true).check.print_if(verbose) |
172 isabelle("jedit -b" + (if (fresh) " -f" else ""), redirect = true, echo = verbose).check |
165 |
173 |
166 isabelle("build " + File.bash_args(build_args), redirect = true) |
174 isabelle("build " + File.bash_args(build_args), redirect = true, echo = verbose) |
167 } |
175 } |
168 |
176 |
169 |
177 |
170 /* command line entry point */ |
178 /* command line entry point */ |
171 |
179 |
234 { |
242 { |
235 if (!allow) |
243 if (!allow) |
236 error("Repository " + hg + " will be cleaned thoroughly!\n" + |
244 error("Repository " + hg + " will be cleaned thoroughly!\n" + |
237 "Provide option -A to allow this explicitly.") |
245 "Provide option -A to allow this explicitly.") |
238 |
246 |
|
247 val progress = new Console_Progress(false) |
239 val res = |
248 val res = |
240 build_history(hg, rev = rev, isabelle_identifier = isabelle_identifier, |
249 build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier, |
241 components_base = components_base, fresh = fresh, nonfree = nonfree, |
250 components_base = components_base, fresh = fresh, nonfree = nonfree, |
242 threads = threads, arch_64 = arch_64, |
251 threads = threads, arch_64 = arch_64, |
243 heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap), |
252 heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap), |
244 max_heap = max_heap, more_settings = more_settings, verbose = verbose, |
253 max_heap = max_heap, more_settings = more_settings, verbose = verbose, |
245 build_args = build_args) |
254 build_args = build_args) |
246 res.print |
|
247 if (!res.ok) sys.exit(res.rc) |
255 if (!res.ok) sys.exit(res.rc) |
248 }) |
256 }) |
249 } |
257 } |
250 } |
258 } |
251 } |
259 } |