Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

use abbreviations in spec files #152

Merged
merged 3 commits into from
Dec 15, 2024
+52 −42
Merged

use abbreviations in spec files #152

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
58d035b
use abbreviations in spec files
fblanqui Dec 15, 2024
fef7d52
wip
fblanqui Dec 15, 2024
e3cfe14
wip
fblanqui Dec 15, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 10 additions & 10 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -246,22 +246,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.02.01, Coq 8.20.0, 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 master, OCaml 4.14.2, Camlp5 8.02.01, Lambdapi c24b28e2 and Coq 8.20.0:

| 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 | 5682 | 39s | 1m29s | 1 Gb | 50m13s |
| HOL-Light file | dump | size | steps | thms | lp | v | size | vo |
|----------------|-------|------|-------|------|-----|-----|------|--------|
| hol.ml | 3m57s | 3 Gb | 3 M | 5687 | 39s | 37s | 1 Gb | 56m23s |

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`

Expand Down
2 changes: 1 addition & 1 deletion main.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
9 changes: 6 additions & 3 deletions xlib.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
61 changes: 34 additions & 27 deletions xlp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -622,10 +622,10 @@ let decl_axioms oc ths =
(****************************************************************************)

type decl =
| Unnamed_thm (* lemXXX : abbrev_type := proof *)
| Axiom (* lemXXX : unabbrev_type *)
| Named_thm of string (* name : unabbrev_type := lemXXX *)
| Named_axm of string (* name : unabbrev_type *)
| DefThmIdProof (* lemXXX : abbrev_type := proof *)
| DeclThmId of (*abbrev:*)bool (* lemXXX : [un]abbrev_type *)
| DefThmNameAsThmId of string (* name : unabbrev_type := lemXXX *)
| DeclThmName of string (* name : unabbrev_type *)
;;

(* [!proof_part_max_idx] indicates the maximal index of the current part. *)
Expand All @@ -645,38 +645,38 @@ let decl_theorem oc k p d =
in
let decl_hyps term = List.iteri (decl_hyp term) in
match d with
| Unnamed_thm ->
| DefThmIdProof ->
let term = term rmap in
let prv = let l = get_use k in l > 0 && l <= !proof_part_max_idx in
string oc (if prv then "private" else "opaque");
string oc " symbol lem"; int oc k; typ_vars oc tvs;
list (decl_param rmap) oc xs; decl_hyps term ts; string oc " : Prf ";
term oc t; string oc " ≔ "; proof tvs rmap oc p; string oc ";\n";
| Axiom ->
let term = unabbrev_term rmap in
| DeclThmId abbrev ->
let term = if abbrev then term rmap else unabbrev_term rmap in
string oc "symbol lem"; int oc k; typ_vars oc tvs;
list (unabbrev_decl_param rmap) oc xs; decl_hyps term ts;
string oc " : Prf "; term oc t; string oc ";\n"
| Named_thm n ->
| DefThmNameAsThmId n ->
let term = unabbrev_term rmap in
string oc "opaque symbol "; string oc n; typ_vars oc tvs;
list (unabbrev_decl_param rmap) oc xs; decl_hyps term ts;
string oc " ≔ @lem"; int oc k; list_prefix " " raw_typ oc tvs;
list_prefix " " (var rmap) oc xs;
List.iteri (fun i _ -> string oc " h"; int oc (i+1)) ts; string oc ";\n"
| Named_axm n ->
| DeclThmName n ->
let term = unabbrev_term rmap in
string oc "symbol thm_"; string oc n; typ_vars oc tvs;
list (unabbrev_decl_param rmap) oc xs; decl_hyps term ts;
string oc " : Prf "; term oc t; string oc ";\n"
;;

(* [theorem oc k p] outputs on [oc] the proof [p] of index [k]. *)
let theorem oc k p = decl_theorem oc k p Unnamed_thm;;
let theorem oc k p = decl_theorem oc k p DefThmIdProof;;

(* [theorem_as_axiom oc k p] outputs on [oc] the proof [p] of index
[k] as an axiom. *)
let theorem_as_axiom oc k p = decl_theorem oc k p Axiom;;
(* [theorem_as_axiom abbrev oc k p] outputs on [oc] the proof [p] of index
[k] as an axiom, with abbreviated terms if [abbrev]. *)
let theorem_as_axiom abbrev oc k p = decl_theorem oc k p (DeclThmId abbrev);;

(* [proofs_in_interval oc x y] outputs on [oc] the proofs in interval
[x] .. [y]. *)
Expand All @@ -691,7 +691,7 @@ let proofs_in_interval oc x y =
let proofs_in_range oc = function
| Only x ->
let p = proof_at x in
List.iter (fun k -> theorem_as_axiom oc k (proof_at k)) (deps p);
List.iter (fun k -> theorem_as_axiom false oc k (proof_at k)) (deps p);
theorem oc x p(*;
out oc
"flag \"print_implicits\" on;
Expand Down Expand Up @@ -762,7 +762,8 @@ let export_theorem_term_abbrevs_part b n k =
in
create_file_with_deps (p^"_head") p iter_deps (fun _ -> ());
(* generate [p^".lp"] *)
concat (p^"_head.lp") (p^"_tail.lp") (p^".lp")
concat (p^"_head.lp") (p^"_tail.lp") (p^".lp");
remove (p^"_head.lp "^p^"_tail.lp")
;;

(****************************************************************************)
Expand Down Expand Up @@ -856,7 +857,7 @@ let export_theorem_proof b n =
Xlib.rename (n^part !proof_part^"_proofs.lp") (n^"_proofs.lp");
write_val (n^".typ") !map_typ_abbrev;
export (n^"_spec") [b^"_types";b^"_terms"]
(fun oc -> theorem_as_axiom oc thid (proof_at thid))
(fun oc -> theorem_as_axiom false oc thid (proof_at thid))
;;

(* 3rd step in command "theorem" when n is not in BIG_FILES.
Expand All @@ -879,7 +880,8 @@ let export_theorem_deps b n =
SetStr.iter (spec f) (Hashtbl.find htbl_thm_deps i);
in
create_file_with_deps (p^"_deps") p iter_deps (fun _ -> ());
concat (p^"_deps.lp") (p^"_proofs.lp") (p^".lp")
concat (p^"_deps.lp") (p^"_proofs.lp") (p^".lp");
remove (p^"_deps.lp "^p^"_proofs.lp")
done
;;

Expand Down Expand Up @@ -915,19 +917,21 @@ let split_theorem_proof b n =
let max_of =
Array.init (Hashtbl.length ht_part_max) (Hashtbl.find ht_part_max) in
write_val (n^".max") max_of;
(* generate [n^".lp"] and [n^"_spec.lp"]. *)
(* generate [n^".lp"] and [n^"_spec.lp"].
Remark: these two files are identical. *)
let iter_deps f =
f (b^"_types");
f (b^"_terms");
spec f (n^part !proof_part);
in
let p = proof_at max in
let t = Named_thm ("lem"^string_of_int max) in
let t = DefThmNameAsThmId ("lem"^string_of_int max) in
export_iter n iter_deps (fun oc -> decl_theorem oc max p t);
export_iter (n^"_spec") iter_deps (fun oc -> decl_theorem oc max p t)
;;

(* Called in [export_theorem_proof_part].
(* Called in [export_theorem_proof_part] which is
called by command "thmpart" in Makefile when n is in BIG_FILES.
[split_theorem_abbrevs n] generates the files [n^".brv"],
[n^".brp"] and [n^"_term_abbrevs"^part(k)^".min"]. *)
let split_theorem_abbrevs n =
Expand Down Expand Up @@ -995,9 +999,9 @@ let export_theorem_proof_part b n k =
let p = part_of d in
if p <> !proof_part then part_deps := SetInt.add p !part_deps
in
export (p^"_proofs") []
create_file (p^"_proofs.lp")
(fun oc ->
export (p^"_spec") [b^"_types";b^"_terms"]
create_file (p^"_spec_body.lp")
(fun oc_spec ->
proof_part_max_idx := max - 1;
for k = min to max do
Expand All @@ -1007,7 +1011,7 @@ let export_theorem_proof_part b n k =
let p = proof_at k in
List.iter add_dep (deps p);
theorem oc k p;
if l = 0 || l >= max then theorem_as_axiom oc_spec k p
if l = 0 || l >= max then theorem_as_axiom true oc_spec k p
end
done));
(* dump term abbreviations *)
Expand All @@ -1028,8 +1032,11 @@ let export_theorem_proof_part b n k =
for j = 1 to nb_parts do f (p^"_term_abbrevs"^part j) done
in
create_file_with_deps (p^"_deps") p iter_deps (fun _ -> ());
(* generate [n^part(k)^".lp"] *)
concat (p^"_deps.lp") (p^"_proofs.lp") (p^".lp")
create_file_with_deps (p^"_deps") (p^"_spec") iter_deps (fun _ -> ());
(* generate [n^part(k)^".lp"] and [n^part(k)^"_spec.lp"] *)
concat (p^"_deps.lp") (p^"_proofs.lp") (p^".lp");
concat (p^"_deps.lp") (p^"_spec_body.lp") (p^"_spec.lp");
remove (p^"_deps.lp "^p^"_proofs.lp "^p^"_spec_body.lp")
;;

(****************************************************************************)
Expand Down Expand Up @@ -1079,14 +1086,14 @@ let export_proofs b r =
(* Generate a declaration of the form "thm_name : type" for each named
theorem. *)
let out_map_thid_name_as_axioms map_thid_name oc =
MapInt.iter (fun k n -> decl_theorem oc k (proof_at k) (Named_axm n))
MapInt.iter (fun k n -> decl_theorem oc k (proof_at k) (DeclThmName n))
map_thid_name
;;

(* Generate a declaration of the form "name : type := lemXXX" for each
named theorem. *)
let out_map_thid_name map_thid_name oc =
MapInt.iter (fun k n -> decl_theorem oc k (proof_at k) (Named_thm n))
MapInt.iter (fun k n -> decl_theorem oc k (proof_at k) (DefThmNameAsThmId n))
map_thid_name
;;

Expand Down
2 changes: 1 addition & 1 deletion xnames.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ let idx = Stdlib.ref (-1);;
index. *)
let map_thid_name =
(* OCaml code for setting [idx] to the index of theorem [name]. *)
let cmd_set_idx = Printf.sprintf "idx := index_of %s;;" in
let cmd_set_idx s = "idx := index_of "^s^";;" in
List.fold_left
(fun map tname ->
(*if tname = "_" then map
Expand Down
Loading