minimize dependencies in spec files (#157)

README.md

@@ -243,15 +243,15 @@ To speed up lp file generation for some theorems with very big proofs, you can w
 
 Remark: for the checking of generated Coq files to not fail because of lack of RAM, we generate for each theorem `${thm}.lp` one or several files for its proof, and a file `${thm}_spec.lp` declaring this theorem as an axiom. Moreover, each other theorem proof using `${thm}` requires `${thm}_spec` instead of `${thm}`. 
 
-Performance
------------
+Performances
+------------
 
 On a machine with 32 processors i9-13950HX, 128 Gb RAM, HOL-Light ea45176, Hol2dk master, OCaml 4.14.2, Camlp5 8.02.01, Lambdapi c24b28e2 and Coq 8.20.0:
 
 | HOL-Light file               | dump  | size   | steps | thms  | lp     | v      | size  | vo     |
 |------------------------------|-------|--------|-------|-------|--------|--------|-------|--------|
-| hol.ml                       | 3m57s | 3 Gb   | 3 M   | 5687  | 39s    | 34s    | 1 Gb  | 56m23s |
-| Multivariate/make_complex.ml | 2h48m | 158 Gb | 90 M  | 41883 | 52m26s | 31m39s | 94 Gb | >63h   |
+| hol.ml                       | 3m57s | 3 Gb   | 3 M   | 5687  | 40s    | 34s    | 1 Gb  | 48m36s |
+| Multivariate/make_complex.ml | 2h48m | 158 Gb | 90 M  | 41883 | 54m58s | 25m17s | 84 Gb | >63h   |
 
 Translating HOL-Light proofs to Dedukti
 ---------------------------------------

xlp.ml

@@ -1001,7 +1001,7 @@ 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
-  create_file (p^"_proofs.lp")
+  create_file (p^"_body.lp")
     (fun oc ->
       create_file (p^"_spec_body.lp")
         (fun oc_spec ->
@@ -1034,11 +1034,19 @@ 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 _ -> ());
-  create_file_with_deps (p^"_deps") (p^"_spec") iter_deps (fun _ -> ());
+  (* generate [n^part(k)^"_spec_deps.lp"] *)
+  let iter_deps f =
+    f (b^"_types");
+    f (b^"_terms");
+    f (b^"_type_abbrevs");
+    if !use_sharing then f (p^"_subterm_abbrevs");
+    for j = 1 to nb_parts do f (p^"_term_abbrevs"^part j) done
+  in
+  create_file_with_deps (p^"_spec_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")
+  concat (p^"_deps.lp") (p^"_body.lp") (p^".lp");
+  concat (p^"_spec_deps.lp") (p^"_spec_body.lp") (p^"_spec.lp");
+  remove (p^"_deps.lp "^p^"_body.lp "^p^"_spec_deps.lp "^p^"_spec_body.lp")
 ;;
 
 (****************************************************************************)