Rename link into config + change its interface

.github/workflows/main.yml

@@ -102,7 +102,7 @@ jobs:
           export HOLLIGHT_DIR=`pwd`/hol-light
           mkdir -p output/hol_upto_arith
           cd output/hol_upto_arith
-          hol2dk link hol_upto_arith
+          hol2dk config hol_upto_arith.ml HOLLight
           make split
           make -j3 lp
           make -j3 v

CHANGES.md

@@ -3,11 +3,24 @@ 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
+## Unreleased
 
 ### Added
 
 - alignment of the type of reals and basic functions on reals
+- command nbp
+- renamings to handle Multivariate
+
+### Changed
+
+- command link renamed into config and improved
+- update to work with HOL-Light 3.0
+- minimize dependencies in spec files
+- theory_hol.lp: rename T into ⊤ and F into ⊥
+
+### Fixed
+
+- handling of type variables occurring in a proof but not in a statement
 
 ## 2.0.0 (2024-04-23)
 

Makefile

@@ -3,7 +3,8 @@
 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)
-REQUIRING := $(shell if test -f REQUIRING; then cat REQUIRING; else echo $(ROOT_PATH); fi)
+REQUIRING := $(shell if test -f REQUIRING; then cat REQUIRING; fi)
+VOFILES := $(shell if test -f VOFILES; then cat VOFILES; fi)
 
 MAX_PROOF = 500_000
 MAX_ABBREV = 2_000_000
@@ -137,6 +138,7 @@ 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 clean-lpo clean-v
+	rm -f lpo.mk
 
 .PHONY: rm-lp
 rm-lp:
@@ -222,6 +224,7 @@ endif
 
 .PHONY: clean-v
 clean-v: rm-v clean-vo
+	rm -f vo.mk
 
 .PHONY: rm-v
 rm-v:
@@ -231,7 +234,8 @@ ifeq ($(INCLUDE_VO_MK),1)
 include vo.mk
 
 vo.mk: 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 > $@
+	cp deps.mk $@
+	sed -e 's/\.lp/.v/g' -e "s/^theory_hol.vo:/theory_hol.vo: $(VOFILES) /" lpo.mk >> $@
 endif
 
 .PHONY: dep

README.md

@@ -200,28 +200,32 @@ Translating HOL-Light proofs to Lambdapi and Coq
 - [coq-hol-light-real](https://github.com/Deducteam/coq-hol-light-real)
 - [coq-fourcolor-reals](https://github.com/coq-community/fourcolor/blob/master/coq-fourcolor-reals.opam)
 
-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:
+**Procedure after dumping:**
+
+- create a directory where all files will be generated:
+```
+mkdir output
+```
+
+- setup the directory with all the required files:
 ```
-cd $HOLLIGHT_DIR/Logic
-hol2dk dump-simp make.ml
-mkdir -p ~/output-hol2dk/Logic
-cd ~/output-hol2dk/Logic
-hol2dk link Logic/make.ml HOLLight_Real.HOLLight_Real --root-path $HOL2DK_DIR/HOLLight.v Rdefinitions Rbasic_fun Raxioms
+cd output
+hol2dk config $hollight_file.ml $root_path [coq_file_or_module] ... [$file.mk]
 ```
-This will create files and add links to files needed to generate, translate and check proofs.
+Do `hol2dk config` to get more details.
 
-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
+- 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:
+To speed up lp file generation for some theorems with very big proofs, you can write in a file named `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=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}`. 
+**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}`.
 
 Performances
 ------------
@@ -236,7 +240,7 @@ On a machine with 32 processors i9-13950HX, 64 Gb RAM, Hol2dk master, HOL-Light
 Translating HOL-Light proofs to Dedukti
 ---------------------------------------
 
-Requirement: dedukti 2.7
+**Requirement:** dedukti 2.7
 
 The Makefile commands above are not implemented for Dedukti yet. It is however possible to translate HOL-Light proofs to Dedukti in parallel by using the following older and less efficient commands: