split opam statements into several files following HOL-Light filenames

.github/workflows/main.yml

@@ -42,7 +42,6 @@ jobs:
           dune install
       - name: Install dependencies
         run: |
-          #sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl
           opam install -y --deps-only hol_light.${{ matrix.hol-light-version }}
           opam install -y dedukti.${{ matrix.dedukti-version }}
       - name: Install lambdapi

CHANGES.md

@@ -7,17 +7,18 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 ### Added
 
-- Sig_mappings_N.v and Sig_With_N.v: axiomatizations of mappings_N.v and With_N.v
-- Makefile target check-spec generates Spec_mappings_N.v and Spec_With_N.v, standalone versions of Sig_mappings_N.v and Sig_With_N.v
-- The use of Spec_With_N.v instead of With_N.v allows to reduce the Coq checking time of Multivariate/make_complex.ml by 40% (21 hours instead of 35 hours)
-- alignment of the type of reals and basic functions on reals
-- command nbp
+- command nbp to print the number of (useful) proofs
+- command files to print theorem statements following the file structuration in HOL-Light
 - renamings to handle the Multivariate library
+- test/Sig_mappings_N.v and test/Sig_With_N.v: axiomatizations of mappings_N.v and With_N.v respectively
+
+- test/Makefile: generates Spec_mappings_N.v and Spec_With_N.v, standalone versions of Sig_mappings_N.v and Sig_With_N.v, and checks the correctness of mappings_N.v and With_N.v wrt to those specification files
+  the use of Spec_With_N.v instead of With_N.v allows to reduce the Coq checking time of Multivariate/make_complex.ml by 40% (21 hours instead of 35 hours)
 
 ### Changed
 
 - command link renamed into config and improved
-- update to work with HOL-Light 3.0
+- update to work with HOL-Light 3.1 and Rocq 9.0
 - minimize dependencies in spec files
 - theory_hol.lp: rename T into ⊤ and F into ⊥
 

Makefile

@@ -47,7 +47,7 @@ rm-use:
 
 .PHONY: rm-thp
 rm-thp:
-	rm -f $(BASE).thp
+	-rm -f $(BASE).thp
 
 BASE_FILES := $(BASE)_types $(BASE)_terms $(BASE)_axioms
 
@@ -77,7 +77,7 @@ $(BASE)_opam.lp:
 
 .PHONY: clean-opam
 clean-opam:
-	rm -f $(BASE)_opam.*
+	-rm -f $(BASE)_opam.*
 
 .PHONY: single
 single: $(BASE).lp
@@ -176,59 +176,59 @@ lp-abbrevs: $(MIN_FILES:%.min=%.lp)
 
 .PHONY: clean-lp
 clean-lp: rm-lp rm-lpo-mk rm-mk rm-min rm-max rm-idx rm-brv rm-brp rm-typ rm-sed rm-lpo rm-siz rm-rename-abbrevs clean-lpo clean-v
-	rm -f lpo.mk
+	-rm -f lpo.mk
 
 .PHONY: rm-lp
 rm-lp:
-	find . -maxdepth 1 -name '*.lp' -a ! -name theory_hol.lp -delete
+	-find . -maxdepth 1 -name '*.lp' -a ! -name theory_hol.lp -delete
 
 .PHONY: rm-lpo-mk
 rm-lpo-mk:
-	find . -maxdepth 1 -name '*.lpo.mk' -delete
+	-find . -maxdepth 1 -name '*.lpo.mk' -delete
 
 .PHONY: rm-mk
 rm-mk:
-	rm -f lpo.mk vo.mk
+	-rm -f lpo.mk vo.mk
 
 .PHONY: rm-max
 rm-max:
-	find . -maxdepth 1 -name '*.max' -delete
+	-find . -maxdepth 1 -name '*.max' -delete
 
 .PHONY: rm-idx
 rm-idx:
-	find . -maxdepth 1 -name '*.idx' -delete
+	-find . -maxdepth 1 -name '*.idx' -delete
 
 .PHONY: rm-brv
 rm-brv:
-	find . -maxdepth 1 -name '*.brv' -delete
+	-find . -maxdepth 1 -name '*.brv' -delete
 
 .PHONY: rm-brp
 rm-brp:
-	find . -maxdepth 1 -name '*.brp' -delete
+	-find . -maxdepth 1 -name '*.brp' -delete
 
 .PHONY: rm-min
 rm-min:
-	find . -maxdepth 1 -name '*.min' -delete
+	-find . -maxdepth 1 -name '*.min' -delete
 
 .PHONY: rm-typ
 rm-typ:
-	find . -maxdepth 1 -name '*.typ' -delete
+	-find . -maxdepth 1 -name '*.typ' -delete
 
 .PHONY: rm-sed
 rm-sed:
-	find . -maxdepth 1 -name '*.sed' -delete
+	-find . -maxdepth 1 -name '*.sed' -delete
 
 .PHONY: rm-siz
 rm-siz:
-	find . -maxdepth 1 -name '*.siz' -delete
+	-find . -maxdepth 1 -name '*.siz' -delete
 
 ifeq ($(INCLUDE_LPO_MK),1)
 include lpo.mk
 
 LPO_MK_FILES := theory_hol.lpo.mk $(wildcard *.lpo.mk)
 
 lpo.mk: $(LPO_MK_FILES)
-	find . -maxdepth 1 -name '*.lpo.mk' | xargs cat > $@
+	-find . -maxdepth 1 -name '*.lpo.mk' | xargs cat > $@
 
 theory_hol.lpo.mk: theory_hol.lp
 	echo 'theory_hol.lpo:' > $@
@@ -248,7 +248,7 @@ clean-lpo: rm-lpo
 
 .PHONY: rm-lpo
 rm-lpo:
-	find . -maxdepth 1 -name '*.lpo' -delete
+	-find . -maxdepth 1 -name '*.lpo' -delete
 
 .PHONY: v
 v: $(LP_FILES:%.lp=%.v)
@@ -262,11 +262,11 @@ endif
 
 .PHONY: clean-v
 clean-v: rm-v clean-vo
-	rm -f vo.mk
+	-rm -f vo.mk
 
 .PHONY: rm-v
 rm-v:
-	find . -maxdepth 1 -name '*.v' -a -type f -delete
+	-find . -maxdepth 1 -name '*.v' -a -type f -delete
 
 .PHONY: rm-empty-deps
 rm-empty-deps: $(V_FILES:%=%.rm)
@@ -276,7 +276,7 @@ else
 	sed -e "s/ theory_hol.vo/ $(VOFILES)/" -e "s/ $(BASE)_types.vo//" -e "s/ $(BASE)_axioms.vo//" vo.mk > new-vo.mk
 	touch -r vo.mk new-vo.mk
 	cp -p new-vo.mk vo.mk
-	rm -f new-vo.mk
+	-rm -f new-vo.mk
 endif
 
 %.v.rm: %.v
@@ -303,7 +303,7 @@ endif
 .PHONY: vo
 vo: $(V_FILES:%.v=%.vo)
 ifeq ($(PROGRESS),1)
-	rm -f .finished
+	-rm -f .finished
 	$(HOL2DK_DIR)/progress &
 endif
 ifneq ($(INCLUDE_VO_MK),1)
@@ -321,19 +321,19 @@ clean-vo: rm-vo rm-glob rm-aux rm-cache
 
 .PHONY: rm-vo
 rm-vo:
-	find . -maxdepth 1 -name '*.vo*' -delete
+	-find . -maxdepth 1 -name '*.vo*' -delete
 
 .PHONY: rm-glob
 rm-glob:
-	find . -maxdepth 1 -name '*.glob' -delete
+	-find . -maxdepth 1 -name '*.glob' -delete
 
 .PHONY: rm-aux
 rm-aux:
-	find . -maxdepth 1 -name '.*.aux' -delete
+	-find . -maxdepth 1 -name '.*.aux' -delete
 
 .PHONY: rm-cache
 rm-cache:
-	rm -f .lia.cache .nia.cache
+	-rm -f .lia.cache .nia.cache
 
 .PHONY: clean-all
 clean-all: clean-split clean-lp clean-opam

README.md

@@ -18,10 +18,10 @@ Dedukti proofs.
 [Rocq](https://rocq-prover.org/) is a proof assistant based on the
 Calculus of Inductive Constructions.
 
-Examples:
----------
+Examples
+--------
 
-hol2dk has been used to translate to Rocq the
+hol2dk is used to translate to Rocq the
 [Multivariate](https://github.com/jrh13/hol-light/blob/master/Multivariate/make_complex.ml)
 library of HOL-Light which contains more than 20,000 theorems on
 arithmetic, wellfounded relations, lists, real numbers, integers,

main.ml

@@ -98,7 +98,7 @@ hol2dk thmsplit $base $thm.lp
   split the proof of $thm in various pieces according to --max-proof-size
 
 hol2dk thmpart $base ${thm}_part_$k.lp
-  generate ${thm}_part_$k.lp and its term abbreviations
+  generate ${thm}_part_$k.lp and record its term abbreviations
   according to --max-abbrev-size
 
 hol2dk abbrev $base ${thm}_term_abbrevs_part_$k.lp
@@ -122,14 +122,19 @@ hol2dk sig $base
   generate dk/lp signature files from $base.sig
 
 hol2dk thm $base.(dk|lp)
-  generate $base.(dk|lp) from $base.thm
-
-hol2dk axm $base.(dk|lp)
-  generate ${base}_opam.(dk|lp) from $base.thm (same as thm but without proofs)
+  generate $base.(dk|lp)
 
 Other commands
 --------------
 
+hol2dk axm $base.(dk|lp)
+  generate ${base}_opam.(dk|lp) with all the statements of all the theorems
+  but without proofs
+
+hol2dk files [$path/]$base.(dk|lp)
+  for each HOL-Light file required by $HOLLIGHT_DIR/$path/$base.ml, generate
+  a (dk|lp) file with the statements of the theorems proved in that file
+
 hol2dk env
   print the values of $HOL2DK_DIR and $HOLLIGHT_DIR
 
@@ -245,7 +250,7 @@ let dump after_hol f b =
     if after_hol then out oc "#use \"hol.ml\";;\nneeds \"%s\";;" f
     else out oc "#use \"%s\";;" f
   in
-  let dg = dep_graph (files()) in
+  let dg = dep_graph "" (files ".") in
   let deps = trans_file_deps dg (if after_hol then ["hol.ml";f] else [f]) in
   let cmd oc after_hol =
     if after_hol then out oc " dump" else out oc " dump-before-hol" in
@@ -344,14 +349,14 @@ and command = function
 
   (* Print dependencies of the ml file f. *)
   | ["dep";f] ->
-     let dg = dep_graph (files()) in
+     let dg = dep_graph "" (files ".") in
      log "%a\n" (list_sep " " string) (trans_file_deps dg [f]);
      0
 
   (* Print dependencies of all ml files in the current directory and
      its subdirectories recursively. *)
   | ["dep"] ->
-     out_dep_graph stdout (dep_graph (files()));
+     out_dep_graph stdout (dep_graph "" (files "."));
      0
 
   | "dep"::_ -> wrong_nb_args()
@@ -363,18 +368,18 @@ and command = function
 
   (* Print the names of theorems proved in f and all its dependencies. *)
   | ["name";"upto";f] ->
-     let dg = dep_graph (files()) in
+     let dg = dep_graph "" (files ".") in
      List.iter
        (fun d -> List.iter (log "%s %s\n" d) (thms_of_file d))
        (trans_file_deps dg [f]);
      0
 
   (* Print the names of theorems proved in all files in the current
-     directort and its subdirectories recursively. *)
+     directory and its subdirectories recursively. *)
   | ["name"] ->
      List.iter
        (fun f -> List.iter (log "%s %s\n" f) (thms_of_file f))
-       (files());
+       (files ".");
      0
 
   | "name"::_ -> wrong_nb_args()
@@ -818,7 +823,8 @@ and command = function
      read_pos b;
      init_proof_reading b;
      begin
-       if dk then Xdk.export_theorems b map_thid_name
+       if dk then Xdk.export_theorems (b^"_theorems")
+                    map_thid_name (fun _ _ -> true) true
        else let nb_parts = read_val (b^".dg") in
             Xlp.export_theorems_part nb_parts b map_thid_name
      end;
@@ -863,23 +869,57 @@ and command = function
   | "part"::_ -> wrong_nb_args()
 
   (* Called in Makefile to generate b_opam.lp with, for each named
-     theorem name, a declaration "symbol thm_name : type". *)
+     theorem, a declaration "symbol thm_name : type". *)
   | ["axm";f] ->
      let dk = is_dk f in
      let b = Filename.chop_extension f in
      read_sig b;
      let map_thid_name = read_val (b^".thm") in
      read_pos b;
      init_proof_reading b;
+     let cond _ _ = true in
      begin
-       if dk then Xdk.export_theorems_as_axioms b map_thid_name
-       else Xlp.export_theorems_as_axioms b map_thid_name
+       if dk then Xdk.export_theorems (b^"_opam") map_thid_name cond false
+       else Xlp.export_theorems (b^"_opam") b map_thid_name cond
      end;
      close_in !Xproof.ic_prf;
      0
 
   | "axm"::_ -> wrong_nb_args()
 
+  (* Called in Makefile to generate a file f.lp with, for each named
+     theorem in f.ml, a declaration "symbol thm_name : type". *)
+  | ["files";f] ->
+     let dk = is_dk f in
+     let f = Filename.chop_extension f in
+     let b = Filename.basename f in
+     read_sig b;
+     let map_thid_name = read_val (b^".thm") in
+     read_pos b;
+     init_proof_reading b;
+     begin
+       try
+         let d = Sys.getenv "HOLLIGHT_DIR" in
+         let dg = dep_graph d (files d) in
+         let files = trans_file_deps dg [f^".ml"] in
+         let gen file =
+           let thm_names = thms_of_file (Filename.concat d file) in
+           let cond _ n = List.mem n thm_names in
+           let f = Filename.chop_extension file in
+           if dk then Xdk.export_theorems f map_thid_name cond false
+           else Xlp.export_theorems f b map_thid_name cond
+         in
+         List.iter gen files;
+         close_in !Xproof.ic_prf;
+         0
+       with Not_found ->
+         close_in !Xproof.ic_prf;
+         err "set $HOLLIGHT_DIR first\n";
+         1
+     end
+
+  | "files"::_ -> wrong_nb_args()
+
   (* Called in Makefile when n is in BIG_FILES to create the file
      n.siz which contains an array mapping every proof step index used
      in the proof of n to an estimation of the size of its Dedukti
@@ -912,7 +952,6 @@ and command = function
   | ["split";b] ->
      read_pos b;
      read_use b;
-     (*init_proof_reading b;*)
      let map_thid_name = read_val (b^".thm") in
      let map = ref MapInt.empty in
      let create_segment start_index end_index =
@@ -1101,7 +1140,9 @@ and command = function
      if dk then
        begin
          Xdk.export_proofs b r;
-         if r = All then Xdk.export_theorems b (read_val (b^".thm"));
+         if r = All then
+           Xdk.export_theorems (b^"_theorems")
+             (read_val (b^".thm")) (fun _ _ -> true) true;
          Xdk.export_term_abbrevs b;
          Xdk.export_type_abbrevs b;
          log_gen f;
@@ -1118,7 +1159,7 @@ and command = function
      else
        begin
          Xlp.export_proofs b r;
-         if r = All then Xlp.export_theorems b (read_val (b^".thm"));
+         if r = All then Xlp.single_export_theorems b b (read_val (b^".thm"));
          Xlp.export_term_abbrevs_in_one_file b b;
          Xlp.export_type_abbrevs b b
        end;