# HG changeset patch # User wenzelm # Date 1737217328 -3600 # Node ID 02e107686442a5ad9d0a6c5b09a586c06276b791 # Parent b520eb5c82232059895c0fe94fd79c322431a419 move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version; diff -r b520eb5c8223 -r 02e107686442 src/HOL/Import/offline/offline.ml --- a/src/HOL/Import/offline/offline.ml Sat Jan 18 16:26:43 2025 +0100 +++ b/src/HOL/Import/offline/offline.ml Sat Jan 18 17:22:08 2025 +0100 @@ -80,12 +80,12 @@ | (c, l) -> failwith ((String.make 1 c) ^ (String.concat " " l)) ;; -let thth = Array.create 155097624 [];; -let tmth = Array.create 55000000 [];; -let tmtm = Array.create 55000000 [];; -let tyth = Array.create 200000 [];; -let tytm = Array.create 200000 [];; -let tyty = Array.create 200000 [];; +let thth = Array.make 155097624 [];; +let tmth = Array.make 55000000 [];; +let tmtm = Array.make 55000000 [];; +let tyth = Array.make 200000 [];; +let tytm = Array.make 200000 [];; +let tyty = Array.make 200000 [];; let needth no = not (IM.mem no !maps);; @@ -167,9 +167,9 @@ rev_tables ();; print_char 'C'; flush stdout;; -let othnth = Array.create 155300000 0;; -let otmntm = Array.create 55000000 0;; -let otynty = Array.create 200000 0;; +let othnth = Array.make 155300000 0;; +let otmntm = Array.make 55000000 0;; +let otynty = Array.make 200000 0;; let outl oc tag ss is = let ss = ss @ (List.map string_of_int is) in diff -r b520eb5c8223 -r 02e107686442 src/HOL/Import/patches/stage1.patch --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Import/patches/stage1.patch Sat Jan 18 17:22:08 2025 +0100 @@ -0,0 +1,25 @@ +--- hol-light/statements.ml 1970-01-01 01:00:00.000000000 +0100 ++++ hol-light-patched/statements.ml 2025-01-18 11:12:11.185279392 +0100 +@@ -0,0 +1,15 @@ ++let name2pairs acc (name, th) = ++ let acc = ++ if is_conj (concl th) then ++ let fold_fun (no, acc) th = (no + 1, (name ^ "_conjunct" ^ (string_of_int no), th) :: acc) in ++ snd (List.fold_left fold_fun (0, acc) (CONJUNCTS th)) ++ else acc ++ in (name, th) :: acc ++;; ++let dump_theorems () = ++ let oc = open_out "theorems" in ++ let all_thms = List.fold_left name2pairs [] !theorems in ++ output_value oc (map (fun (a,b) -> (a, dest_thm b)) all_thms); ++ close_out oc ++;; ++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 @@ ++#use "hol.ml";; ++#use "update_database.ml";; ++#use "statements.ml";; ++exit 0;; diff -r b520eb5c8223 -r 02e107686442 src/HOL/Import/patches/stage2.patch --- /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;; diff -r b520eb5c8223 -r 02e107686442 src/Pure/Admin/component_hol_light.scala --- 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) }) }