--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/patches/stage2.patch Sat Jan 18 17:22:08 2025 +0100
@@ -0,0 +1,374 @@
+--- hol-light/fusion.ml 2025-01-18 11:11:28.417955236 +0100
++++ hol-light-patched/fusion.ml 2025-01-18 11:12:11.384276293 +0100
+@@ -9,6 +9,18 @@
+
+ needs "lib.ml";;
+
++#load "unix.cma";;
++let poutc = Unix.open_process_out "buffer | gzip -c > proofs.gz";;
++let foutc = open_out "facts.lst";;
++let stop_recording () = close_out poutc; close_out foutc;;
++
++let rec outl = function
++ [] -> ()
++| (h :: t) -> try
++ output_string poutc h; List.fold_left
++ (fun () e -> output_char poutc ' '; output_string poutc e) () t
++ with Sys_error _ -> ();;
++
+ module type Hol_kernel =
+ sig
+ type hol_type = private
+@@ -101,7 +113,165 @@
+ | Comb of term * term
+ | Abs of term * term
+
+- type thm = Sequent of (term list * term)
++ type thm = Sequent of (term list * term * int)
++(* PROOFRECORDING BEGIN *)
++let thms = Hashtbl.create 20000;;
++
++let inc = open_in "theorems";;
++let l = ((input_value inc) : ((string * (term list * term)) list));;
++close_in inc;;
++List.iter (fun (n,t) -> Hashtbl.replace thms t (n, 0)) l;;
++print_endline ("Read in: " ^ string_of_int (Hashtbl.length thms));;
++
++module Fm = Map.Make(struct type t = float let compare = compare end);;
++module Tys = Map.Make(struct type t = hol_type let compare = compare end);;
++module Tms = Map.Make(struct type t = term let compare = compare end);;
++module Ps = Map.Make(struct type t = (term list * term) let compare = compare end);;
++
++let ty_no = ref 0;;
++let tys = ref Tys.empty;;
++
++let rec out_type ty =
++ try
++ Tys.find ty !tys
++ with Not_found ->
++ match ty with
++ Tyvar t ->
++ incr ty_no; tys := Tys.add ty !ty_no !tys;
++ output_char poutc 't'; output_string poutc t; output_char poutc '\n';
++ !ty_no
++ | Tyapp (id, tl) ->
++ let tln = map out_type tl in
++ incr ty_no; tys := Tys.add ty !ty_no !tys;
++ output_char poutc 'a'; output_string poutc id; output_char poutc ' ';
++ outl (map string_of_int tln); output_char poutc '\n';
++ !ty_no;;
++
++let tm_no = ref 0;;
++let tms = ref Tms.empty;;
++let tms_prio = ref Fm.empty;;
++let tms_size = ref 0;;
++let tms_maxsize = ref (int_of_string (Sys.getenv "MAXTMS"));;
++let tm_lookup tm =
++ let (ret, oldtime) = Tms.find tm !tms in
++ let newtime = Unix.gettimeofday () in
++ tms := Tms.add tm (ret, newtime) !tms;
++ tms_prio := Fm.add newtime tm (Fm.remove oldtime !tms_prio);
++ ret;;
++
++let tm_delete () =
++ let (time, tm) = Fm.min_binding !tms_prio in
++ tms := Tms.remove tm !tms;
++ tms_prio := Fm.remove time !tms_prio;
++ decr tms_size; ();;
++
++let tm_add tm no =
++ while (!tms_size > !tms_maxsize) do tm_delete (); done;
++ let newtime = Unix.gettimeofday () in
++ tms := Tms.add tm (no, newtime) (!tms);
++ tms_prio := Fm.add newtime tm (!tms_prio);
++ incr tms_size; ();;
++
++let rec out_term tm =
++ try
++ tm_lookup tm
++ with Not_found ->
++ let outc = output_char poutc and out = output_string poutc in
++ match tm with
++ Var (name, ty) ->
++ let ty = out_type ty in
++ incr tm_no; tm_add tm !tm_no;
++ outc 'v'; out name; outc ' '; out (string_of_int ty); outc '\n';
++ !tm_no
++ | Const (name, ty) ->
++ let ty = out_type ty in
++ incr tm_no; tm_add tm !tm_no;
++ outc 'c'; out name; outc ' '; out (string_of_int ty); outc '\n';
++ !tm_no
++ | Comb (f, a) ->
++ let f = out_term f and a = out_term a in
++ incr tm_no; tm_add tm !tm_no;
++ outc 'f'; out (string_of_int f); outc ' '; out (string_of_int a); outc '\n';
++ !tm_no
++ | Abs (x, a) ->
++ let x = out_term x and a = out_term a in
++ incr tm_no; tm_add tm !tm_no;
++ outc 'l'; out (string_of_int x); outc ' '; out (string_of_int a); outc '\n';
++ !tm_no
++;;
++
++let prf_no = ref 0;;
++let outt tag ss tys tms pfs =
++ let tys = map out_type tys and
++ tms = map out_term tms in
++ try
++ output_char poutc tag;
++ outl (ss @ (map string_of_int tys)
++ @ (map string_of_int tms)
++ @ (map string_of_int pfs));
++ output_char poutc '\n'
++ with Sys_error _ -> ()
++;;
++
++let ps = ref Ps.empty;;
++
++let p_lookup p = Ps.find p !ps;;
++let p_add p no = ps := Ps.singleton p no;;
++
++let mk_prff f = incr prf_no; f (); !prf_no;;
++
++let chk_mk_prff f th =
++ try p_lookup th
++ with Not_found ->
++ try
++ let (name, i) = Hashtbl.find thms th in
++ if i > 0 then i else
++ let i = mk_prff f in
++ (ps := Ps.empty;
++ Hashtbl.replace thms th (name, i);
++ (try output_string foutc (name ^ " " ^ string_of_int i ^ "\n"); flush foutc with Sys_error _ -> ());
++ i)
++ with Not_found ->
++ mk_prff (fun () -> f (); p_add th !prf_no);;
++
++
++let mk_prf t l1 l2 l3 l4 _ = mk_prff (fun () -> outt t l1 l2 l3 l4);;
++let chk_mk_prf t l1 l2 l3 l4 th = chk_mk_prff (fun () -> outt t l1 l2 l3 l4) th;;
++let proof_REFL t th = chk_mk_prf 'R' [] [] [t] [] th;;
++let proof_TRANS (p, q) th = chk_mk_prf 'T' [] [] [] [p; q] th;;
++let proof_MK_COMB (p, q) th = chk_mk_prf 'C' [] [] [] [p; q] th;;
++let proof_ABS x p th = chk_mk_prf 'L' [] [] [x] [p] th;;
++let proof_BETA t th = chk_mk_prf 'B' [] [] [t] [] th;;
++let proof_ASSUME t th = chk_mk_prf 'H' [] [] [t] [] th;;
++let proof_EQ_MP p q th = chk_mk_prf 'E' [] [] [] [p; q] th;;
++let proof_DEDUCT_ANTISYM_RULE (p1,t1) (p2,t2) th =
++ chk_mk_prf 'D' [] [] [] [p1; p2] th;;
++let rec explode_subst = function
++ [] -> []
++| ((y,x)::rest) -> x::y::(explode_subst rest);;
++let proof_INST_TYPE s p th = chk_mk_prf 'Q' [] (explode_subst s) [] [p] th;;
++let proof_INST s p th = chk_mk_prf 'S' [] [] (explode_subst s) [p] th;;
++
++let global_ax_counter = ref 0;;
++let new_axiom_name n = incr global_ax_counter; ("ax_" ^ n ^ "_" ^ string_of_int(!global_ax_counter));;
++let proof_new_axiom axname t th = chk_mk_prf 'A' [axname] [] [t] [] th;;
++let proof_new_definition cname t th =
++ chk_mk_prf 'F' [cname] [] [t] [] th;;
++let proof_new_basic_type_definition tyname (absname, repname) (pt,tt) p th =
++ chk_mk_prf 'Y' [tyname; absname; repname] [] [pt; tt] [p] th;;
++let proof_CONJUNCT1 p th = chk_mk_prf '1' [] [] [] [p] th;;
++let proof_CONJUNCT2 p th = chk_mk_prf '2' [] [] [] [p] th;;
++
++let clean_ts_at_saved = ((try Sys.getenv "CLEANTMS" with _ -> "") = "YES");;
++
++let save_proof name p th =
++ Hashtbl.replace thms th (name, p);
++ ps := Ps.empty;
++ if clean_ts_at_saved then (
++ tms := Tms.empty; tms_prio := Fm.empty; tms_size := 0;
++ );
++ (try output_string foutc (name ^ " " ^ string_of_int p ^ "\n"); flush foutc with Sys_error _ -> ());;
++(* PROOFRECORDING END *)
+
+ (* ------------------------------------------------------------------------- *)
+ (* List of current type constants with their arities. *)
+@@ -485,43 +655,48 @@
+ (* Basic theorem destructors. *)
+ (* ------------------------------------------------------------------------- *)
+
+- let dest_thm (Sequent(asl,c)) = (asl,c)
++ let dest_thm (Sequent(asl,c,_)) = (asl,c)
+
+- let hyp (Sequent(asl,c)) = asl
++ let hyp (Sequent(asl,c,_)) = asl
+
+- let concl (Sequent(asl,c)) = c
++ let concl (Sequent(asl,c,_)) = c
+
+ (* ------------------------------------------------------------------------- *)
+ (* Basic equality properties; TRANS is derivable but included for efficiency *)
+ (* ------------------------------------------------------------------------- *)
+
+ let REFL tm =
+- Sequent([],safe_mk_eq tm tm)
++ let eq = safe_mk_eq tm tm in
++ Sequent([],eq,proof_REFL tm ([], eq))
+
+- let TRANS (Sequent(asl1,c1)) (Sequent(asl2,c2)) =
++ let TRANS (Sequent(asl1,c1,p1)) (Sequent(asl2,c2,p2)) =
+ match (c1,c2) with
+ Comb((Comb(Const("=",_),_) as eql),m1),Comb(Comb(Const("=",_),m2),r)
+- when alphaorder m1 m2 = 0 -> Sequent(term_union asl1 asl2,Comb(eql,r))
++ when alphaorder m1 m2 = 0 ->
++ let (a, g) = (term_union asl1 asl2,Comb(eql,r)) in
++ Sequent (a, g, proof_TRANS (p1, p2) (a, g))
+ | _ -> failwith "TRANS"
+
+ (* ------------------------------------------------------------------------- *)
+ (* Congruence properties of equality. *)
+ (* ------------------------------------------------------------------------- *)
+
+- let MK_COMB(Sequent(asl1,c1),Sequent(asl2,c2)) =
++ let MK_COMB(Sequent(asl1,c1,p1),Sequent(asl2,c2,p2)) =
+ match (c1,c2) with
+ Comb(Comb(Const("=",_),l1),r1),Comb(Comb(Const("=",_),l2),r2) ->
+ (match type_of r1 with
+ Tyapp("fun",[ty;_]) when compare ty (type_of r2) = 0
+- -> Sequent(term_union asl1 asl2,
+- safe_mk_eq (Comb(l1,l2)) (Comb(r1,r2)))
++ -> let (a, g) = (term_union asl1 asl2,
++ safe_mk_eq (Comb(l1,l2)) (Comb(r1,r2))) in
++ Sequent (a, g, proof_MK_COMB (p1, p2) (a,g))
+ | _ -> failwith "MK_COMB: types do not agree")
+ | _ -> failwith "MK_COMB: not both equations"
+
+- let ABS v (Sequent(asl,c)) =
++ let ABS v (Sequent(asl,c,p)) =
+ match (v,c) with
+ Var(_,_),Comb(Comb(Const("=",_),l),r) when not(exists (vfree_in v) asl)
+- -> Sequent(asl,safe_mk_eq (Abs(v,l)) (Abs(v,r)))
++ -> let eq = safe_mk_eq (Abs(v,l)) (Abs(v,r)) in
++ Sequent (asl,eq,proof_ABS v p (asl,eq))
+ | _ -> failwith "ABS";;
+
+ (* ------------------------------------------------------------------------- *)
+@@ -531,7 +706,8 @@
+ let BETA tm =
+ match tm with
+ Comb(Abs(v,bod),arg) when compare arg v = 0
+- -> Sequent([],safe_mk_eq tm bod)
++ -> let eq = safe_mk_eq tm bod in
++ Sequent([],eq,proof_BETA tm ([], eq))
+ | _ -> failwith "BETA: not a trivial beta-redex"
+
+ (* ------------------------------------------------------------------------- *)
+@@ -539,30 +715,35 @@
+ (* ------------------------------------------------------------------------- *)
+
+ let ASSUME tm =
+- if compare (type_of tm) bool_ty = 0 then Sequent([tm],tm)
++ if compare (type_of tm) bool_ty = 0 then
++ Sequent([tm],tm,proof_ASSUME tm ([tm], tm))
+ else failwith "ASSUME: not a proposition"
+
+- let EQ_MP (Sequent(asl1,eq)) (Sequent(asl2,c)) =
++ let EQ_MP (Sequent(asl1,eq,p1)) (Sequent(asl2,c,p2)) =
+ match eq with
+ Comb(Comb(Const("=",_),l),r) when alphaorder l c = 0
+- -> Sequent(term_union asl1 asl2,r)
++ -> let t = term_union asl1 asl2 in
++ Sequent(t,r,proof_EQ_MP p1 p2 (t,r))
+ | _ -> failwith "EQ_MP"
+
+- let DEDUCT_ANTISYM_RULE (Sequent(asl1,c1)) (Sequent(asl2,c2)) =
++ let DEDUCT_ANTISYM_RULE (Sequent(asl1,c1,p1)) (Sequent(asl2,c2,p2)) =
+ let asl1' = term_remove c2 asl1 and asl2' = term_remove c1 asl2 in
+- Sequent(term_union asl1' asl2',safe_mk_eq c1 c2)
++ let (a,g) = (term_union asl1' asl2',safe_mk_eq c1 c2) in
++ Sequent (a, g, proof_DEDUCT_ANTISYM_RULE (p1,c1) (p2,c2) (a, g))
+
+ (* ------------------------------------------------------------------------- *)
+ (* Type and term instantiation. *)
+ (* ------------------------------------------------------------------------- *)
+
+- let INST_TYPE theta (Sequent(asl,c)) =
++ let INST_TYPE theta (Sequent(asl,c,p)) =
+ let inst_fn = inst theta in
+- Sequent(term_image inst_fn asl,inst_fn c)
++ let (a, g) = (term_image inst_fn asl,inst_fn c) in
++ Sequent(a,g, proof_INST_TYPE theta p (a,g))
+
+- let INST theta (Sequent(asl,c)) =
++ let INST theta (Sequent(asl,c,p)) =
+ let inst_fun = vsubst theta in
+- Sequent(term_image inst_fun asl,inst_fun c)
++ let (a, g) = (term_image inst_fun asl,inst_fun c) in
++ Sequent(a, g, proof_INST theta p (a,g))
+
+ (* ------------------------------------------------------------------------- *)
+ (* Handling of axioms. *)
+@@ -574,8 +755,11 @@
+
+ let new_axiom tm =
+ if compare (type_of tm) bool_ty = 0 then
+- let th = Sequent([],tm) in
+- (the_axioms := th::(!the_axioms); th)
++ let axname = new_axiom_name "" in
++ let p = proof_new_axiom axname tm ([], tm) in
++ let th = Sequent([],tm,p) in
++ (the_axioms := th::(!the_axioms);
++ save_proof axname p ([], tm); th)
+ else failwith "new_axiom: Not a proposition"
+
+ (* ------------------------------------------------------------------------- *)
+@@ -595,7 +779,10 @@
+ else if not (subset (type_vars_in_term r) (tyvars ty))
+ then failwith "new_definition: Type variables not reflected in constant"
+ else let c = new_constant(cname,ty); Const(cname,ty) in
+- let dth = Sequent([],safe_mk_eq c r) in
++ let concl = safe_mk_eq c r in
++ let p = proof_new_definition cname r ([], concl) in
++ let dth = Sequent([],concl, p) in
++ save_proof ("DEF_"^cname) p ([], concl);
+ the_definitions := dth::(!the_definitions); dth
+ | Comb(Comb(Const("=",_),Const(cname,ty)),r) ->
+ failwith ("new_basic_definition: '" ^ cname ^ "' is already defined")
+@@ -614,7 +801,7 @@
+ (* Where "abs" and "rep" are new constants with the nominated names. *)
+ (* ------------------------------------------------------------------------- *)
+
+- let new_basic_type_definition tyname (absname,repname) (Sequent(asl,c)) =
++ let new_basic_type_definition tyname (absname,repname) (Sequent(asl,c,p)) =
+ if exists (can get_const_type) [absname; repname] then
+ failwith "new_basic_type_definition: Constant(s) already in use" else
+ if not (asl = []) then
+@@ -634,9 +821,19 @@
+ let abs = (new_constant(absname,absty); Const(absname,absty))
+ and rep = (new_constant(repname,repty); Const(repname,repty)) in
+ let a = Var("a",aty) and r = Var("r",rty) in
+- Sequent([],safe_mk_eq (Comb(abs,mk_comb(rep,a))) a),
+- Sequent([],safe_mk_eq (Comb(P,r))
+- (safe_mk_eq (mk_comb(rep,mk_comb(abs,r))) r))
++ let ax1 = safe_mk_eq (Comb(abs,mk_comb(rep,a))) a
++ and ax2 = safe_mk_eq (Comb(P,r)) (safe_mk_eq (mk_comb(rep,mk_comb(abs,r))) r) in
++ let mk_binary s =
++ let c = mk_const(s,[]) in
++ fun (l,r) -> try mk_comb(mk_comb(c,l),r)
++ with Failure _ -> failwith "tydef_mk_binary"
++ in
++ let axc = mk_binary "/\\" (ax1, ax2) in
++ let tp = proof_new_basic_type_definition tyname (absname, repname) (P,x) p ([], axc) in
++ let p1 = proof_CONJUNCT1 tp ([], ax1) in
++ let p2 = proof_CONJUNCT2 tp ([], ax2) in
++ save_proof ("TYDEF_" ^ tyname) tp ([], axc);
++ (Sequent([],ax1,p1), Sequent([],ax2,p2));;
+
+ end;;
+
+--- hol-light/stage1.ml 2025-01-18 11:12:11.373276465 +0100
++++ hol-light-patched/stage1.ml 1970-01-01 01:00:00.000000000 +0100
+@@ -1,4 +0,0 @@
+-#use "hol.ml";;
+-#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 @@
++#use "hol.ml";;
++stop_recording ();;
++exit 0;;
--- a/src/Pure/Admin/component_hol_light.scala Sat Jan 18 16:26:43 2025 +0100
+++ b/src/Pure/Admin/component_hol_light.scala Sat Jan 18 17:22:08 2025 +0100
@@ -14,40 +14,16 @@
val default_hol_light_url = "https://github.com/jrh13/hol-light.git"
val default_hol_light_rev = "Release-3.0.0"
- val default_hol_light_patched_url = "https://gitlab.inria.fr/hol-light-isabelle/hol-light.git"
- val default_hol_light_patched_rev = "master"
-
- val default_import_url = "https://gitlab.inria.fr/hol-light-isabelle/import.git"
- val default_import_rev = "master"
-
- def hol_light_dirs(base_dir: Path): (Path, Path) =
- (base_dir + Path.basic("hol-light"), base_dir + Path.basic("hol-light-patched"))
-
- val patched_files: List[Path] =
- List("fusion.ml", "statements.ml", "stage1.ml", "stage2.ml").map(Path.explode)
-
- def make_patch(base_dir: Path): String = {
- val (dir1, dir2) = hol_light_dirs(Path.current)
- (for (path <- patched_files) yield {
- val path1 = dir1 + path
- val path2 = dir2 + path
- if ((base_dir + path1).is_file || (base_dir + path2).is_file) {
- Isabelle_System.make_patch(base_dir, path1, path2)
- }
- else ""
- }).mkString
- }
+ 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,
progress: Progress = new Progress,
target_dir: Path = Path.current,
hol_light_url: String = default_hol_light_url,
- hol_light_rev: String = default_hol_light_rev,
- hol_light_patched_url: String = default_hol_light_patched_url,
- hol_light_patched_rev: String = default_hol_light_patched_rev,
- import_url: String = default_import_url,
- import_rev: String = default_import_rev
+ hol_light_rev: String = default_hol_light_rev
): Unit = {
/* system */
@@ -92,18 +68,19 @@
The original repository """ + hol_light_url + """
has been patched in 2 stages. The overall export process works like this:
+ cd hol-light
make
- patch -p1 < patches/stage1.patch
+ patch -p1 < """ + patch1 + """
./ocaml-hol -I +compiler-libs stage1.ml
- patch -p1 < patches/stage2.patch
+ patch -p1 < """ + patch2 + """
export MAXTMS=10000
./ocaml-hol -I +compiler-libs stage2.ml
gzip -d proofs.gz
> maps.lst
- x86_64-linux/offline
+ "$HOL_LIGHT_IMPORT/x86_64-linux/offline"
Makarius
@@ -124,22 +101,15 @@
val opam_env = Isabelle_System.bash("isabelle ocaml_opam env").check.out
- /* repository clones */
+ /* repository clone */
- val (hol_light_dir, hol_light_patched_dir) = hol_light_dirs(tmp_dir)
- val import_dir = tmp_dir + Path.basic("import")
+ val hol_light_dir = tmp_dir + Path.basic("hol-light")
if (!only_offline) {
Isabelle_System.git_clone(hol_light_url, hol_light_dir, checkout = hol_light_rev,
progress = progress)
-
- Isabelle_System.git_clone(
- hol_light_patched_url, hol_light_patched_dir, checkout = hol_light_patched_rev,
- progress = progress)
}
- Isabelle_System.git_clone(import_url, import_dir, checkout = import_rev, progress = progress)
-
/* "offline" tool */
@@ -147,45 +117,24 @@
val offline_path = Path.explode("offline")
val offline_exe = offline_path.platform_exe
- val import_offline_dir = import_dir + offline_path
+ val offline_dir = Isabelle_System.make_directory(tmp_dir + offline_path)
+
+ Isabelle_System.copy_dir(hol_import_dir + offline_path, offline_dir, direct = true)
- Isabelle_System.copy_dir(import_offline_dir, component_dir.path)
- (component_dir.path + Path.explode("offline/.gitignore")).file.delete
-
- progress.bash("make", cwd = import_offline_dir, echo = progress.verbose).check
- Isabelle_System.copy_file(import_offline_dir + offline_exe, platform_dir + offline_exe)
+ progress.bash("ocamlopt offline.ml -o offline",
+ cwd = offline_dir, echo = progress.verbose).check
+ Isabelle_System.copy_file(offline_dir + offline_exe, platform_dir + offline_exe)
File.set_executable(platform_dir + offline_exe)
- if (!only_offline) {
-
- /* patches */
-
- progress.echo("Preparing patches ...")
-
- val patches_dir = Isabelle_System.make_directory(component_dir.path + Path.basic("patches"))
- val patch1 = patches_dir + Path.basic("stage1.patch")
- val patch2 = patches_dir + Path.basic("stage2.patch")
-
- Isabelle_System.bash("git reset --hard origin/stdlib/isabelle-export-base",
- cwd = hol_light_patched_dir).check
+ /* export */
- File.write(patch1, make_patch(tmp_dir))
-
- Isabelle_System.bash("patch -p1 < " + File.bash_path(patch1), cwd = hol_light_dir).check
-
- Isabelle_System.bash("git reset --hard origin/stdlib/isabelle-export",
- cwd = hol_light_patched_dir).check
-
- File.write(patch2, make_patch(tmp_dir))
-
-
- /* export */
-
+ if (!only_offline) {
progress.echo("Exporting proofs ...")
progress.bash(
Library.make_lines("set -e", opam_env,
"make",
+ "patch -p1 < " + File.bash_path(patch1),
"./ocaml-hol -I +compiler-libs stage1.ml",
"patch -p1 < " + File.bash_path(patch2),
"export MAXTMS=10000",
@@ -212,11 +161,7 @@
var target_dir = Path.current
var only_offline = false
var hol_light_url = default_hol_light_url
- var hol_light_patched_url = default_hol_light_patched_url
var hol_light_rev = default_hol_light_rev
- var hol_light_patched_rev = default_hol_light_patched_rev
- var import_url = default_import_url
- var import_rev = default_import_rev
var verbose = false
val getopts = Getopts("""
@@ -227,16 +172,8 @@
-O only build the "offline" tool
-U URL git URL for original HOL Light repository, default:
""" + default_hol_light_url + """
- -V URL git URL for patched HOL Light repository, default:
- """ + default_hol_light_patched_url + """
- -W URL git URL for import repository, default:
- """ + default_import_url + """
-r REV revision or branch to checkout HOL Light (default: """ +
default_hol_light_rev + """)
- -s REV revision or branch to checkout HOL-Light-to-Isabelle (default: """ +
- default_hol_light_patched_rev + """)
- -t REV revision or branch to checkout import (default: """ +
- default_import_rev + """)
-v verbose
Build Isabelle component for HOL Light import.
@@ -244,11 +181,7 @@
"D:" -> (arg => target_dir = Path.explode(arg)),
"O" -> (_ => only_offline = true),
"U:" -> (arg => hol_light_url = arg),
- "V:" -> (arg => hol_light_patched_url = arg),
- "W:" -> (arg => import_url = arg),
"r:" -> (arg => hol_light_rev = arg),
- "s:" -> (arg => hol_light_patched_rev = arg),
- "t:" -> (arg => import_rev = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
@@ -258,11 +191,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,
- hol_light_patched_url = hol_light_patched_url,
- hol_light_patched_rev = hol_light_patched_rev,
- import_url = import_url,
- import_rev = import_rev)
+ hol_light_url = hol_light_url, hol_light_rev = hol_light_rev)
})
}