--- a/src/Pure/Admin/component_hol_light.scala Sat Jan 18 22:25:47 2025 +0100
+++ b/src/Pure/Admin/component_hol_light.scala Sat Jan 18 22:29:47 2025 +0100
@@ -15,8 +15,6 @@
val default_hol_light_rev = "Release-3.0.0"
val hol_import_dir: Path = Path.explode("~~/src/HOL/Import")
- def patch1: Path = hol_import_dir + Path.explode("patches/stage1.patch")
- def patch2: Path = hol_import_dir + Path.explode("patches/stage2.patch")
def build_hol_light_import(
only_offline: Boolean = false,
@@ -66,15 +64,15 @@
This is an export of primitive proofs from HOL Light """ + hol_light_rev + """.
The original repository """ + hol_light_url + """
-has been patched in 2 stages. The overall export process works like this:
+has been patched in 2 phases. The overall export process works like this:
cd hol-light
make
- patch -p1 < """ + patch1 + """
+ patch -p1 < "$HOL_LIGHT_IMPORT/patches/patch1"
./ocaml-hol -I +compiler-libs stage1.ml
- patch -p1 < """ + patch2 + """
+ patch -p1 < "$HOL_LIGHT_IMPORT/patches/patch2"
export MAXTMS=10000
./ocaml-hol -I +compiler-libs stage2.ml
@@ -116,20 +114,33 @@
File.set_executable(platform_dir + offline_exe)
- /* export */
+ if (!only_offline) {
+ /* clone repository */
- if (!only_offline) {
val hol_light_dir = tmp_dir + Path.basic("hol-light")
Isabelle_System.git_clone(hol_light_url, hol_light_dir, checkout = hol_light_rev,
progress = progress)
+
+ /* patches */
+
+ Isabelle_System.make_directory(component_dir.path + Path.basic("patches"))
+
+ def patch(n: Int, source: Boolean = false): Path =
+ (if (source) hol_import_dir else component_dir.path) + Path.explode("patches/patch" + n)
+
+ for (n <- List(1, 2)) Isabelle_System.copy_file(patch(n, source = true), patch(n))
+
+
+ /* export stages */
+
def run(n: Int, lines: String*): Unit = {
val title = "stage " + n
if (n > 0) progress.echo("Running " + title + " ...")
val start = Time.now()
progress.bash(cat_lines("set -e" :: opam_env :: lines.toList),
- cwd = hol_light_dir, echo = progress.verbose).check
+ cwd = hol_light_dir, echo = progress.verbose).check.timing
val elapsed = Time.now() - start
if (n > 0) {
@@ -139,10 +150,10 @@
run(0, "make")
run(1,
- "patch -p1 < " + File.bash_path(patch1),
+ "patch -p1 < " + File.bash_path(patch(1)),
"./ocaml-hol -I +compiler-libs stage1.ml")
run(2,
- "patch -p1 < " + File.bash_path(patch2),
+ "patch -p1 < " + File.bash_path(patch(2)),
"export MAXTMS=10000",
"./ocaml-hol -I +compiler-libs stage2.ml")
run(3,