Merge remote-tracking branch 'dk/main' into hollight.3.0

Deducteam · Dec 15, 2024 · 9ab8888 · 9ab8888
2 parents 77f2ec4 + 88aa1f6
commit 9ab8888
Show file tree

Hide file tree

Showing 7 changed files with 85 additions and 73 deletions.
diff --git a/README.md b/README.md
@@ -226,22 +226,22 @@ Remark: for the checking of generated Coq files to not fail because of lack of R
 Performance with the mapping of real numbers (master branch)
 ------------------------------------------------------------
 
-On a machine with 32 processors i9-13950HX and 64G RAM with OCaml 5.2.1, Camlp5 8.03.01, Coq 8.20.0:
+On a machine with 32 processors i9-13950HX and 64G RAM with HOL-Light 3.0.0, OCaml 5.2.1, Camlp5 8.03.01, Lambdapi c24b28e2 and Coq 8.20.0:
 
-| HOL-Light file | dump-simp | dump size | proof steps | nb theorems | make -j32 lp | make -j32 v | v files size | make -j32 vo |
-|----------------|-----------|-----------|-------------|-------------|--------------|-------------|--------------|--------------|
-| hol.ml         | 3m43s     | 3 Gb      | 5 M         | 5687        | 40s          | 1m29s       | 1 Gb         | 50m13s       |
+| HOL-Light file | dump  | size | steps | thms | lp  | v     | size | vo     |
+|----------------|-------|------|-------|------|-----|-------|------|--------|
+| hol.ml         | 3m43s | 3 Gb | 3 M   | 5687 | 40s | 1m29s | 1 Gb | 50m13s |
 
 Performance without the mapping of real numbers (hol2dk 2.0)
 ------------------------------------------------------------
 
-On a machine with 32 processors i9-13950HX and 64G RAM, with Hol2dk 2.0, OCaml 5.1.1, Camlp5 8.02.01, Lambdapi 2.5.0 and Coq 8.19.1, or (1) OCaml 4.14.2, Camlp5 8.02.01:
+On a machine with 32 processors i9-13950HX and 64G RAM, with HOL-Light ea45176, Hol2dk 2.0, OCaml 4.14.2, Camlp5 8.02.01, Lambdapi 2.5.0 and Coq 8.19.1:
 
-| HOL-Light file                     | dump-simp(1) | dump size | proof steps | nb theorems | make -j32 lp | make -j32 v | v files size | make -j32 vo |
-|------------------------------------|--------------|-----------|-------------|-------------|--------------|-------------|--------------|--------------|
-| hol.ml                             | 3m57s        | 3 Gb      | 5 M         | 5679        | 51s          | 55s         | 1 Gb         | 18m4s        |
-| Multivariate/make_upto_topology.ml | 48m          | 52 Gb     | 52 M        | 18866       | 22m22s       | 20m16s      | 68 Gb        | 8h (*)       |
-| Multivariate/make_complex.ml       | 2h48m        | 158 Gb    | 220 M       | 41883       | 52m26s       | 31m39s      | 240 Gb       |              |
+| HOL-Light file                     | simp  | size   | steps | thms  | lp     | v      | size   | vo     |
+|------------------------------------|-------|--------|-------|-------|--------|--------|--------|--------|
+| hol.ml                             | 3m57s | 3 Gb   | 3 M   | 5687  | 51s    | 55s    | 1 Gb   | 18m4s  |
+| Multivariate/make_upto_topology.ml | 48m   | 52 Gb  | 52 M  | 18866 | 22m22s | 20m16s | 68 Gb  | 8h (*) |
+| Multivariate/make_complex.ml       | 2h48m | 158 Gb | 220 M | 41883 | 52m26s | 31m39s | 240 Gb |        |
 
 (*) with `make -j32 vo; make -j8 vo`
 

diff --git a/fusion.ml b/fusion.ml
@@ -14,7 +14,7 @@ open Lib
 
 module type Hol_kernel =
   sig
-    type hol_type =
+      type hol_type =
       (*REMOVE
       private
       REMOVE*)
@@ -66,6 +66,10 @@ module type Hol_kernel =
 
       type proof = Proof of (thm * proof_content)
 
+      val index_of : thm -> int
+      val content_of : proof -> proof_content
+      val change_content : proof -> proof_content -> proof
+
       val types: unit -> (string * int)list
       val get_type_arity : string -> int
       (*REMOVE
@@ -116,9 +120,6 @@ module type Hol_kernel =
       val dest_thm : thm -> term list * term
       val hyp : thm -> term list
       val concl : thm -> term
-      val index_of : thm -> int
-      val content_of : proof -> proof_content
-      val change_content : proof -> proof_content -> proof
       (*REMOVE
       val REFL : term -> thm
       val TRANS : thm -> thm -> thm
@@ -130,6 +131,12 @@ module type Hol_kernel =
       val DEDUCT_ANTISYM_RULE : thm -> thm -> thm
       val INST_TYPE : (hol_type * hol_type) list -> thm -> thm
       val INST : (term * term) list -> thm -> thm
+      val axioms : unit -> thm list
+      val new_axiom : term -> thm
+      val definitions : unit -> thm list
+      val new_basic_definition : term -> thm
+      val new_basic_type_definition :
+              string -> string * string -> thm -> thm * thm
 
       (*START_ND*)
       val TRUTH : thm
@@ -153,14 +160,8 @@ module type Hol_kernel =
       val new_theorem : term list -> term -> proof_content -> thm
       val dump_nb_proofs : string -> unit
       val dump_signature : string -> unit
-      REMOVE*)
-      val axioms : unit -> thm list
-      val new_axiom : term -> thm
-      val definitions : unit -> thm list
-      val new_basic_definition : term -> thm
-      val new_basic_type_definition :
-              string -> string * string -> thm -> thm * thm
       val oc_dump : out_channel
+      REMOVE*)
       (*REMOVE*)val the_type_constants : (string * int) list ref
       (*REMOVE*)val the_term_constants : (string * hol_type) list ref
       (*REMOVE*)val the_axioms : thm list ref
@@ -183,6 +184,7 @@ module Hol : Hol_kernel = struct
 
 
   type thm = Sequent of (term list * term * int)
+  (*REMOVE*)let dummy_thm = Sequent([],Var("x",Tyvar("a")),0)
 
 (*---------------------------------------------------------------------------*)
 (* Proof dumping.                                                            *)
@@ -223,8 +225,7 @@ module Hol : Hol_kernel = struct
   let change_content p c = let Proof(th,_) = p in Proof(th,c)
 
   let thm_index = ref (-1)
-
-  (*REMOVE*)let dump_filename = "/tmp/dump.prf"
+  (*REMOVE
   let oc_dump = open_out_bin dump_filename
 
   let new_theorem hyps concl proof_content =
@@ -234,7 +235,7 @@ module Hol : Hol_kernel = struct
     output_value oc_dump (Proof(thm,proof_content));
     thm
   ;;
-
+  REMOVE*)
 (* ------------------------------------------------------------------------- *)
 (* List of current type constants with their arities.                        *)
 (*                                                                           *)
@@ -625,10 +626,11 @@ module Hol : Hol_kernel = struct
 
   let index_of (Sequent(_,_,k)) = k
 
+(*REMOVE
 (* ------------------------------------------------------------------------- *)
 (* Basic equality properties; TRANS is derivable but included for efficiency *)
 (* ------------------------------------------------------------------------- *)
-(*REMOVE
+
   let REFL tm = new_theorem [] (safe_mk_eq tm tm) (Prefl tm)
 
   let TRANS (Sequent(asl1,c1,k1)) (Sequent(asl2,c2,k2)) =
@@ -820,21 +822,21 @@ REMOVE*)
 (* ------------------------------------------------------------------------- *)
 
   let the_axioms = ref ([]:thm list)
-
+(*REMOVE
   let axioms() = !the_axioms
 
   let new_axiom tm =
     if Stdlib.compare (type_of tm) bool_ty = 0 then
       let th = new_theorem [] tm (Paxiom tm) in
       (the_axioms := th::(!the_axioms); th)
     else failwith "new_axiom: Not a proposition"
-
+REMOVE*)
 (* ------------------------------------------------------------------------- *)
 (* Handling of (term) definitions.                                           *)
 (* ------------------------------------------------------------------------- *)
 
   let the_definitions = ref ([]:thm list)
-
+(*REMOVE
   let definitions() = !the_definitions
 
   let new_basic_definition tm =
@@ -852,7 +854,7 @@ REMOVE*)
     | Comb(Comb(Const("=",_),Const(cname,ty)),r) ->
       failwith ("new_basic_definition: '" ^ cname ^ "' is already defined")
     | _ -> failwith "new_basic_definition"
-
+REMOVE*)
 (* ------------------------------------------------------------------------- *)
 (* Handling of type definitions.                                             *)
 (*                                                                           *)
@@ -865,7 +867,7 @@ REMOVE*)
 (*                                                                           *)
 (* Where "abs" and "rep" are new constants with the nominated names.         *)
 (* ------------------------------------------------------------------------- *)
-
+(*REMOVE
   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
@@ -917,7 +919,7 @@ REMOVE*)
     output_value oc (definitions());
     close_out oc
   ;;
-
+REMOVE*)
 end;;
 
 include Hol;;

diff --git a/main.ml b/main.ml
@@ -719,7 +719,7 @@ and command = function
      (* replace file.prf by file-simp.prf, and recompute file.pos and
         file.use *)
      log "replace %s.prf by %s-simp.prf ...\n" b b;
-     begin match Sys.command (Printf.sprintf "mv %s-simp.prf %s.prf" b b) with
+     begin match Sys.command ("mv "^b^"-simp.prf "^b^".prf") with
      | 0 ->
         begin match log_command ["pos";b] with
         | 0 -> log_command ["use";b]

diff --git a/xdk.ml b/xdk.ml
@@ -475,15 +475,15 @@ let proof tvs rmap =
        end
     | Paxiom(t) ->
        let k =
-         try pos_first (fun th -> concl th = t) (axioms())
+         try pos_first (fun th -> concl th = t) !the_axioms
          with Not_found -> assert false
        in
        string oc "axiom_"; int oc k;
        list_prefix " " typ oc (type_vars_in_term t);
        list_prefix " " term oc (frees t)
     | Pdeft(_,t,_,_) ->
        let k =
-         try pos_first (fun th -> concl th = t) (axioms())
+         try pos_first (fun th -> concl th = t) !the_axioms
          with Not_found -> assert false
        in
        string oc "axiom_"; int oc k;
@@ -787,9 +787,9 @@ let export_axioms b =
   export (b^"_axioms")
     (fun oc ->
       string oc "\n(; axioms ;)\n";
-      decl_axioms oc (axioms());
+      decl_axioms oc !the_axioms;
       string oc "\n(; definitional axioms ;)\n";
-      list decl_def oc (definitions()))
+      list decl_def oc !the_definitions)
 ;;
 
 let export_proofs b r =
@@ -848,9 +848,9 @@ eq : a : Set -> El a -> El a -> El bool.\n";
   string oc "\n(; constants ;)\n";
   list decl_sym oc constants;
   string oc "\n(; axioms ;)\n";
-  decl_axioms oc (axioms());
+  decl_axioms oc !the_axioms;
   string oc "\n(; definitions ;)\n";
-  list decl_def oc (definitions());
+  list decl_def oc !the_definitions;
   string oc "\n"
 ;;
 

diff --git a/xlib.ml b/xlib.ml
@@ -62,11 +62,14 @@ let create_file_bin n f = let oc = log_open_out_bin n in f oc; close_out oc;;
 let read_file_bin n f = let ic = log_open_in_bin n in f ic; close_in ic;;
 
 let concat f1 f2 f3 =
-  log "generate %s ...\n%!" f3;
-  command (Printf.sprintf "cat %s %s > %s && rm -f %s %s" f1 f2 f3 f1 f2)
+  log "generate %s ...\n%!" f3; command ("cat "^f1^" "^f2^" > "^f3)
 ;;
 
-let rename f1 f2 = log "rename %s into %s ...\n%!" f1 f2; Sys.rename f1 f2;;
+let remove f = command ("rm -f "^f);;
+
+let copy f1 f2 = log "generate %s ...\n%!" f2; command ("cp -f "^f1^" "^f2);;
+
+let rename f1 f2 = log "generate %s ...\n%!" f2; command ("mv -f "^f1^" "^f2);;
 
 (* [string_of_file f] puts the contents of file [f] in a string. *)
 let string_of_file f =