# HG changeset patch # User wenzelm # Date 1737292993 -3600 # Node ID 61b7111220616c3a6f507a54a18d48b4e984cfae # Parent 02b4ae06974d66a09314fba87e1ef6c4efbc3ecb allow to load additional HOL Light files, after "hol.ml"; diff -r 02b4ae06974d -r 61b711122061 src/HOL/Import/patches/patch1 --- a/src/HOL/Import/patches/patch1 Sat Jan 18 23:46:46 2025 +0100 +++ b/src/HOL/Import/patches/patch1 Sun Jan 19 14:23:13 2025 +0100 @@ -18,14 +18,16 @@ +dump_theorems ();; --- hol-light/stage1.ml 1970-01-01 01:00:00.000000000 +0100 +++ hol-light-patched/stage1.ml 2025-01-18 11:12:11.185279392 +0100 -@@ -0,0 +1,4 @@ +@@ -0,0 +1,5 @@ +#use "hol.ml";; ++(*LOAD MORE*) +#use "update_database.ml";; +#use "statements.ml";; +exit 0;; --- hol-light/stage2.ml 1970-01-01 01:00:00.000000000 +0100 +++ hol-light-patched/stage2.ml 2025-01-18 11:12:11.384276293 +0100 -@@ -0,0 +1,3 @@ +@@ -0,0 +1,4 @@ +#use "hol.ml";; ++(*LOAD MORE*) +stop_recording ();; +exit 0;; diff -r 02b4ae06974d -r 61b711122061 src/Pure/Admin/component_hol_light.scala --- a/src/Pure/Admin/component_hol_light.scala Sat Jan 18 23:46:46 2025 +0100 +++ b/src/Pure/Admin/component_hol_light.scala Sun Jan 19 14:23:13 2025 +0100 @@ -20,6 +20,7 @@ only_offline: Boolean = false, progress: Progress = new Progress, target_dir: Path = Path.current, + load_more: List[Path] = Nil, hol_light_url: String = default_hol_light_url, hol_light_rev: String = default_hol_light_rev ): Unit = { @@ -118,6 +119,7 @@ /* clone repository */ 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) @@ -131,6 +133,15 @@ for (n <- List(1, 2)) Isabelle_System.copy_file(patch(n, source = true), patch(n)) + if (load_more.nonEmpty) { + val bad = load_more.filter(path => !(hol_light_dir + path).is_file) + if (bad.nonEmpty) error("Bad HOL Light files: " + bad.mkString(", ")) + + val more = load_more.map(path => "needs " + path + ";; ").mkString("+", "", "") + File.change_lines(patch(1), strict = true)(_.map(line => + if (line == "+(*LOAD MORE*)") more else line)) + } + /* export stages */ @@ -176,6 +187,7 @@ Scala_Project.here, { args => var target_dir = Path.current + var load_more = List.empty[Path] var only_offline = false var hol_light_url = default_hol_light_url var hol_light_rev = default_hol_light_rev @@ -186,6 +198,7 @@ Options are: -D DIR target directory (default ".") + -L PATH load additional HOL Light files, after "hol.ml" -O only build the "offline" tool -U URL git URL for original HOL Light repository, default: """ + default_hol_light_url + """ @@ -193,9 +206,13 @@ default_hol_light_rev + """) -v verbose - Build Isabelle component for HOL Light import. + Build Isabelle component for HOL Light import. For example: + + isabelle component_hol_light_import -L Logic/make.ml + isabelle component_hol_light_import -L 100/thales.ml -L 100/ceva.ml """, "D:" -> (arg => target_dir = Path.explode(arg)), + "L:" -> (arg => load_more = load_more ::: List(Path.explode(arg))), "O" -> (_ => only_offline = true), "U:" -> (arg => hol_light_url = arg), "r:" -> (arg => hol_light_rev = arg), @@ -208,6 +225,6 @@ build_hol_light_import( only_offline = only_offline, progress = progress, target_dir = target_dir, - hol_light_url = hol_light_url, hol_light_rev = hol_light_rev) + load_more = load_more, hol_light_url = hol_light_url, hol_light_rev = hol_light_rev) }) }