add-links/Makefile: add ROOT_PATH and ERASING arguments/variables (#141)

- main, xlp: add option --root-path to customize the lambdapi root_path, and allow more arguments for link - add-links: can now take two additional arguments: a coq root_path file and an erasing.lp file - Makefile: rename REQUIRE into ROOT_PATH to set the value of the ho2dk --root-path option - Makefile: add variables ERASING to set the value of the lambdapi export --erasing option - Makefile: remove sed after lambdapi export by using the same root_path for both lambdapi and coq - Makefile: variables MAX_PROOF and MAX_ABBREV are integers now - lambdapi.pkg: change variables to HOLLight as in coq - reproduce: update according to above changes - update README.md
Deducteam · Nov 25, 2024 · b0f222b · b0f222b
1 parent 0a35ddd
commit b0f222b
Show file tree

Hide file tree

Showing 9 changed files with 153 additions and 92 deletions.
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -12,8 +12,8 @@ jobs:
         ocaml-version: [4.14.2]
         camlp5-version: [8.02.01]
         dedukti-version: [2.7]
-        lambdapi-version: [master, 2.5.1]
-        dune-version: [3.15.0]
+        lambdapi-version: [master] # >= 31aef37c > 2.5.1
+        dune-version: [3.16.1]
     runs-on: ubuntu-latest
     steps:
     # actions/checkout must be done BEFORE avsm/setup-ocaml

diff --git a/CHANGES.md b/CHANGES.md
@@ -3,6 +3,12 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/),
 and this project adheres to [Semantic Versioning](https://semver.org/).
 
+## Unrelease
+
+### Added
+
+- alignment of the type of reals and basic functions on reals
+
 ## 2.0.0 (2024-04-23)
 
 Big improvements in Lambdapi and Coq file generation time, and Coq checking time.

diff --git a/Makefile b/Makefile
@@ -1,14 +1,19 @@
 .SUFFIXES:
 
 BASE = $(shell if test -f BASE; then cat BASE; fi)
+ROOT_PATH = $(shell if test -f ROOT_PATH; then cat ROOT_PATH; else echo HOLLight; fi)
+ERASING = $(shell if test -f ERASING; then cat ERASING; fi)
+
+MAX_PROOF = 500_000
+MAX_ABBREV = 2_000_000
 
 .PHONY: default
 default:
+	@echo "usage: make TARGET [VAR=VAL ...]"
 	@echo "targets: split lp lpo v vo opam clean-<target> clean-all"
 	@echo "variables:"
-	@echo "  REQUIRE: Coq module required in generated Coq files"
-	@echo "  MAX_PROOF: hol2dk max proof size option"
-	@echo "  MAX_ABBREV: hol2dk max abbrev size option"
+	@echo "  MAX_PROOF: hol2dk max proof size (default is $(MAX_PROOF))"
+	@echo "  MAX_ABBREV: hol2dk max abbrev size (default is $(MAX_ABBREV))"
 
 .PHONY: split
 split:
@@ -40,7 +45,7 @@ rm-thp:
 BASE_FILES := $(BASE)_types $(BASE)_type_abbrevs $(BASE)_terms $(BASE)_axioms
 
 $(BASE_FILES:%=%.lp) &:
-	hol2dk sig $(BASE).lp
+	hol2dk --root-path $(ROOT_PATH) sig $(BASE).lp
 
 ifeq ($(INCLUDE_VO_MK),1)
 INCLUDE_LPO_MK=1
@@ -86,7 +91,7 @@ find-big-files:
 lp: $(BASE_FILES:%=%.lp) $(BIG_FILES:%=%.max)
 	$(MAKE) SET_STI_FILES=1 SET_IDX_FILES=1 lp-proofs
 	$(MAKE) SET_MIN_FILES=1 lp-abbrevs
-	hol2dk type_abbrevs $(BASE)
+	hol2dk --root-path $(ROOT_PATH) type_abbrevs $(BASE)
 	$(MAKE) SET_SED_FILES=1 rename-abbrevs
 
 .PHONY: rename-abbrevs
@@ -98,29 +103,25 @@ rename-abbrevs: $(SED_FILES:%.sed=%.lp.rename-abbrevs)
 .PHONY: lp-proofs
 lp-proofs: $(STI_FILES:%.sti=%.lp) $(IDX_FILES:%.idx=%.lp)
 
-MAX_PROOF = --max-proof-size 500_000
-
 %.max: %.siz
-	hol2dk $(MAX_PROOF) thmsplit $(BASE) $*.lp
+	hol2dk --root-path $(ROOT_PATH) --max-proof-size $(MAX_PROOF) thmsplit $(BASE) $*.lp
 
 %.siz: %.sti
 	hol2dk thmsize $(BASE) $*
 
 .PRECIOUS: $(BIG_FILES:%=%.siz)
 
-MAX_ABBREV = --max-abbrev-size 2_000_000
-
 %.lp: %.idx
-	hol2dk $(MAX_ABBREV) thmpart $(BASE) $*.lp
+	hol2dk --root-path $(ROOT_PATH) --max-abbrev-size $(MAX_ABBREV) thmpart $(BASE) $*.lp
 
 %.lp: %.sti
-	hol2dk theorem $(BASE) $*.lp
+	hol2dk --root-path $(ROOT_PATH) theorem $(BASE) $*.lp
 
 .PHONY: lp-abbrevs
 lp-abbrevs: $(MIN_FILES:%.min=%.lp)
 
 %.lp: %.min
-	hol2dk abbrev $(BASE) $*.lp
+	hol2dk --root-path $(ROOT_PATH) abbrev $(BASE) $*.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 clean-lpo clean-v
@@ -203,24 +204,26 @@ ifneq ($(SET_LP_FILES),1)
 	$(MAKE) SET_LP_FILES=1 $@
 endif
 
-REQUIRE = HOLLight
+.PHONY: echo-require
+echo-require:
+	@echo $(ROOT_PATH)
 
 %.v: %.lp
 	@echo lambdapi export -o stt_coq $<
-	@lambdapi export -o stt_coq --encoding $(HOL2DK_DIR)/encoding.lp --renaming $(HOL2DK_DIR)/renaming.lp --erasing $(HOL2DK_DIR)/erasing.lp --use-notations --requiring $(REQUIRE).v $< | sed -e 's/^Require Import hol-light\./Require Import /g' > $@
+	@lambdapi export -o stt_coq --encoding $(HOL2DK_DIR)/encoding.lp --renaming $(HOL2DK_DIR)/renaming.lp --erasing $(ERASING) --use-notations --requiring $(ROOT_PATH) $< > $@
 
 .PHONY: clean-v
 clean-v: rm-v clean-vo
 
 .PHONY: rm-v
 rm-v:
-	find . -maxdepth 1 -name '*.v' -a ! -name $(REQUIRE).v -delete
+	find . -maxdepth 1 -name '*.v' -a ! -name $(ROOT_PATH).v -delete
 
 ifeq ($(INCLUDE_VO_MK),1)
 include vo.mk
 
 vo.mk: lpo.mk
-	sed -e 's/\.lp/.v/g' -e "s/: theory_hol.vo/: $(REQUIRE).vo theory_hol.vo/" -e "s/theory_hol.vo:/theory_hol.vo: $(REQUIRE).vo/" lpo.mk > $@
+	sed -e 's/\.lp/.v/g' -e "s/: theory_hol.vo/: $(ROOT_PATH).vo theory_hol.vo/" -e "s/theory_hol.vo:/theory_hol.vo: $(ROOT_PATH).vo/" lpo.mk > $@
 endif
 
 .PHONY: dep
@@ -244,7 +247,7 @@ endif
 COQC_OPTIONS = -no-glob # -w -coercions
 %.vo: %.v
 	@echo coqc $<
-	@coqc $(COQC_OPTIONS) -R . $(REQUIRE) $<
+	@coqc $(COQC_OPTIONS) -R . $(ROOT_PATH) $<
 
 .PHONY: clean-vo
 clean-vo: rm-vo rm-glob rm-aux rm-cache
@@ -271,7 +274,7 @@ opam: $(BASE)_opam.vo
 .PRECIOUS: $(BASE)_opam.v
 
 $(BASE)_opam.lp:
-	hol2dk axm $(BASE).lp
+	hol2dk --root-path $(ROOT_PATH) axm $(BASE).lp
 
 .PHONY: clean-opam
 clean-opam:

diff --git a/README.md b/README.md
@@ -203,7 +203,7 @@ The command `simp` is the sequential composition of `rewrite` and `purge`.
 Translating HOL-Light proofs to Lambdapi and Coq in parallel
 ------------------------------------------------------------
 
-**Requirement:** lambdapi >= 2.5.0
+**Requirements:** lambdapi commit >= 31aef37c (25/11/24) > 2.5.1
 
 For not cluttering HOL-Light sources with the many generated files, we suggest to proceed as follows. For instance, for generating the proofs of the `Logic` library, do:
 ```
@@ -213,17 +213,18 @@ mkdir -p ~/output-hol2dk/Logic
 cd ~/output-hol2dk/Logic
 hol2dk link Logic/make
 ```
-This will add links to files needed to generate, translate and check proofs.
+This will create files and add links to files needed to generate, translate and check proofs.
 
 You can then do in order:
+- `make` to get the list of targets and variables
 - `make split` to generate a file for each theorem
 - `make -j$jobs lp` to translate HOL-Light proofs to Lambdapi
 - `make -j$jobs lpo` to check Lambdapi files (optional)
 - `make -j$jobs v` to translate Lambdapi files to Coq files
 - `make -j$jobs vo` to check Coq files
 
 To speed up lp file generation for some theorems with very big proofs, you can write in a file called `BIG_FILES` a list of theorem names (lines starting with `#` are ignored). See for instance [BIG_FILES](https://github.com/Deducteam/hol2dk/blob/main/BIG_FILES). You can also change the default values of the options `--max-proof-size` and `--max-abbrev-size` as follows:
-- `make -j$jobs MAX_PROOF='--max-proof-size 500_000' MAX_ABBREV='--max-max-abbrev 2_000_000' lp`
+- `make -j$jobs MAX_PROOF=500_000 MAX_ABBREV=2_000_000 lp`
 
 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}`. 
 
@@ -234,9 +235,9 @@ On a machine with 32 processors i9-13950HX and 64G RAM, with OCaml 5.1.1, Camlp5
 
 | 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                             | 3m57s     | 3 Go      | 5 M         | 5679        | 51s          | 55s         | 1 Gb         | 18m4s        |
-| Multivariate/make_upto_topology.ml | 48m       | 52 Go     | 52 M        | 18866       | 22m22s       | 20m16s      | 68 Gb        | 8h (*)       |
-| Multivariate/make_complex.ml       | 2h48m     | 158 Go    | 220 M       | 20200       | 52m26s       | 31m39s      | 240 Gb       |              |
+| 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       | 20200       | 52m26s       | 31m39s      | 240 Gb       |              |
 
 (*) with `make -j32 vo; make -j8 vo`
 
@@ -279,6 +280,8 @@ functions have been aligned with those of Coq:
 - option type constructor
 - type of lists
 - functions on lists
+- type of reals
+- basic functions and predicates on reals
 
 The part of HOL-Light that is aligned with Coq is gathered in the package
 [coq-hol-light](https://github.com/Deducteam/coq-hol-light) available

diff --git a/add-links b/add-links
@@ -12,24 +12,56 @@ then
     exit 1
 fi
 
-if test $# -ne 1
+if test $# -ne 1 -a $# -ne 3
 then
-    echo "usage: `basename $0` FILE"
-    echo 'create BASE and add links to files in $HOL2DK_DIR and $HOLLIGHT_DIR for translating and checking the proofs of FILE'
+    echo "usage: `basename $0` hollight_file.ml [coq_file.v erasing.lp]"
+    echo '  hollight_file.ml: path to an ml file relative to $HOLLIGHT_DIR'
+    echo '  coq_file.v: coq file imported in all generated coq files'
+    echo '  erasing.lp: mappings between lambdapi and coq'
+    echo 'in the current directory:'
+    echo '- create a file BASE'
+    echo '- create a file ROOT_PATH'
+    echo '- create a file lambdapi.pkg'
+    echo '- create a file _CoqProject'
+    echo '- create a file ERASING'
+    echo '- add links to coq_file.v and other files in $HOL2DK_DIR and $HOLLIGHT_DIR for translating and checking the proofs of hollight_file'
     exit 1
 fi
 
+base=`basename $1 .ml`
+
 echo create BASE ...
-echo `basename $1` > BASE
+echo $base > BASE
 
-for ext in prf nbp sig thm pos use
-do
-    echo ln -f -s $HOLLIGHT_DIR/$1.$ext
-    ln -f -s $HOLLIGHT_DIR/$1.$ext
-done
+root_path=`basename ${2:-HOLLight} .v`
+if test $# -gt 1
+then
+    echo create ROOT_PATH ...
+    echo $root_path > ROOT_PATH
+fi
+
+echo create lambdapi.pkg ...
+echo "package_name = $root_path" > lambdapi.pkg
+echo "root_path = $root_path" >> lambdapi.pkg
 
-for f in theory_hol.dk theory_hol.lp lambdapi.pkg HOLLight.v _CoqProject Makefile BIG_FILES
+echo create _CoqProject ...
+echo "-R . $root_path ." > _CoqProject
+
+echo create ERASING ...
+echo ${3:-$HOL2DK_DIR/erasing.lp} > ERASING
+
+coq_file=${2:-$HOL2DK_DIR/HOLLight.v}
+echo ln -f -s $coq_file
+ln -f -s $coq_file
+
+for f in theory_hol.dk theory_hol.lp Makefile BIG_FILES
 do
     echo ln -f -s $HOL2DK_DIR/$f
     ln -f -s $HOL2DK_DIR/$f
 done
+
+for ext in prf nbp sig thm pos use
+do
+    echo ln -f -s $HOLLIGHT_DIR/$base.$ext
+    ln -f -s $HOLLIGHT_DIR/$base.$ext
+done
diff --git a/lambdapi.pkg b/lambdapi.pkg
@@ -1,2 +1,2 @@
-package_name = hol-light
-root_path = hol-light
+package_name = HOLLight
+root_path = HOLLight
diff --git a/main.ml b/main.ml
@@ -20,9 +20,11 @@ hol2dk options command arguments
 Options
 -------
 
---max-proof-size INT: maximum size of proof files
+--root-path MODNAME: set lambdapi and coq's root_path (default is HOLLight)
 
---max-abbrev-size INT: maximum size of term abbreviation files
+--max-proof-size INT: maximum size of proof files (default is 500_000)
+
+--max-abbrev-size INT: maximum size of term abbreviation files (default is 2_000_000)
 
 --use-sharing: define term abbreviations using let's
 
@@ -79,11 +81,12 @@ hol2dk $base.(dk|lp) $thm_id
 Multi-threaded lp file generation by having a file for each named theorem
 -------------------------------------------------------------------------
 
-hol2dk link [$path/]$base
-  add links to the files generated by dump in $HOLLIGHT_DIR[/$path/]
-  and to hol2dk files needed to translate $base.prf to Dedukti, Lambdapi
-  and Coq, and check the obtained files
-
+hol2dk link hollight_file.ml [coq_file.v erasing.lp]
+  create files and links to the files generated by hol2dk dump
+  in $HOLLIGHT_DIR and to the hol2dk files needed to translate
+  $base.prf to Dedukti, Lambdapi and Coq, and check the obtained files
+  do hol2dk link without arguments to get more explanations
+ 
 hol2dk split $base
   generate $base.thp and the files $thm.sti, $thm.pos and $thm.use
   for each theorem $thm
@@ -436,6 +439,8 @@ and command = function
   | "--max-proof-size"::k::args ->
      Xlp.max_proof_part_size := integer k; command args
 
+  | "--root-path"::arg::args -> Xlp.root_path := arg; command args
+
   | s::_ when String.starts_with ~prefix:"--" s ->
      err "unknown option \"%s\"\n" s; 1
 
@@ -478,8 +483,7 @@ and command = function
   | ["unpatch" as s] -> call_script s []
   | "unpatch"::_ -> wrong_nb_args()
 
-  | ["link";arg] -> call_script "add-links" [arg]
-  | "link"::_ -> wrong_nb_args()
+  | "link"::args -> call_script "add-links" args
 
   | ["dump";f] -> dump true f (basename_ml f)
   | "dump"::_ -> wrong_nb_args()