From bbc4d527a57eaf1a6bda1e60b344f04c03ee7e39 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sat, 11 Jan 2025 13:47:54 +0100 Subject: [PATCH 1/5] modify link command --- Makefile | 8 +++- add-links | 112 ++++++++++++++++++++++++++++++---------------------- renaming.lp | 4 ++ 3 files changed, 75 insertions(+), 49 deletions(-) diff --git a/Makefile b/Makefile index 450a05ad..5a835000 100644 --- a/Makefile +++ b/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 diff --git a/add-links b/add-links index 010ecc4f..cfff2d19 100755 --- a/add-links +++ b/add-links @@ -14,23 +14,25 @@ fi usage() { cat <<__EOF__ -usage: `basename $0` hollight_file.ml [coq_mod] ... [--root-path coq_file.v] [--erasing erasing.lp] [coq_mod] ... +usage: `basename $0` [--erasing $erasing.lp] $hollight_file.ml $file.mk $root_path [coq_file_or_module] ... arguments: - hollight_file.ml: path to an ml file relative to $HOLLIGHT_DIR - coq_file.v: coq file imported in all generated coq files (mandatory if coq modules are given) - erasing.lp: mappings between lambdapi and coq - coq_mod: coq module that needs to be imported in generated files + $erasing.lp: mappings between lambdapi and coq + $hollight_file.ml: path to an ml file relative to $HOLLIGHT_DIR + $file.mk: dependencies of vo files given in arguments ($file must be different from "lpo" or "vo") + $root_path: name of the generated library + coq_file_or_module: coq modules that needs to be imported in generated files effect in the current directory: -- create a file COMMAND containing the command used to create links -- create a file BASE containing the base name of hollight_file.ml -- create a file ROOT_PATH containing the base name of coq_file.v -- create a file REQUIRING containing the coq modules and root path in the order they are given +- create a file CONFIG containing the command used to create links +- create a file BASE containing the base name of $hollight_file.ml +- create a file ROOT_PATH containing $root_path - create a file lambdapi.pkg - create a file _CoqProject -- create a file ERASING containing the name of erasing.lp -- add links to coq_file.v and other files in $HOL2DK_DIR and $HOLLIGHT_DIR for translating and checking the proofs of hollight_file +- create a file ERASING containing $erasing.lp +- create a file REQUIRING containing the list of Coq module names that need to be imported (in the same order as they are given in the command) +- create a file VOFILES containing the list of Coq module names corresponding to the Coq files given in arguments with file extension ".vo" +- add links to $file.mk, the Coq files given in argument and other files in $HOL2DK_DIR and $HOLLIGHT_DIR for translating and checking the proofs of $hollight_file.ml __EOF__ } @@ -44,66 +46,78 @@ error() { parse_args() { if test $# -ne 0; then case $1 in - --root-path) - if test -z "$root_path_arg" - then - if test $# -eq 1 - then - error 'missing --root-path argument' - else - root_path_arg=$2 - requiring="$requiring `basename $2 .v`" - shift 2 - parse_args $* - fi - else - error 'too many --root-path options' - fi;; --erasing) - if test -z "$erasing_arg" + if test -z "$erasing" then if test $# -eq 1 then error 'missing --erasing argument' else - erasing_arg=$2 + erasing=$2 shift 2 parse_args $* fi else error 'too many --erasing options' fi;; - *) + *.ml) if test -z "$hollight_file" then hollight_file=$1 shift parse_args $* else - requiring="$requiring $1" + error 'too many ml files' + fi;; + lpo.mk|vo.mk) + error 'lpo.mk and vo.mk are reserved filenames';; + *.mk) + if test -z "$mk_file" + then + mk_file=$1 shift parse_args $* + else + error 'too many make files' fi;; + *.v) + if test -z "$root_path" + then + error 'the root_path must be given before Coq files' + else + coq_files="$coq_files $1" + vo_files="$vo_files `basename $1`o" + requiring="$requiring $root_path.`basename $1 .v`" + shift + parse_args $* + fi;; + *) + if test -z "$root_path" + then + root_path=$1 + else + requiring="$requiring $1" + fi + shift + parse_args $*;; esac fi } -echo create COMMAND ... -echo '#!/bin/sh' > COMMAND -echo $0 $* >> COMMAND -chmod a+x COMMAND +echo create CONFIG ... +echo '#!/bin/sh' > CONFIG +echo $0 $* >> CONFIG +chmod a+x CONFIG parse_args $* -if test -n "$requiring" -a -z "$root_path_arg" +if test -z "$root_path" then - error "the --root-path option is mandatory when coq modules are given" + error 'missing root_path' fi -base=`basename $hollight_file .ml` echo create BASE ... -echo $base > BASE +echo `basename $hollight_file .ml` > BASE -root_path=`basename ${root_path_arg:-HOLLight} .v` echo create ROOT_PATH ... echo $root_path > ROOT_PATH @@ -115,18 +129,22 @@ echo create _CoqProject ... echo "-R . $root_path ." > _CoqProject echo create ERASING ... -echo ${erasing_arg:-$HOL2DK_DIR/erasing.lp} > ERASING +echo ${erasing:-$HOL2DK_DIR/erasing.lp} > ERASING -if test -z "$requiring" -then - requiring=${root_path}.${root_path} -fi echo create REQUIRING ... echo $requiring > REQUIRING -coq_file=${root_path_arg:-$HOL2DK_DIR/HOLLight.v} -echo ln -f -s $coq_file -ln -f -s $coq_file +echo create VOFILES ... +echo $vo_files > VOFILES + +echo ln -f -s $mk_file deps.mk +ln -f -s $mk_file deps.mk + +for f in $coq_files +do + echo ln -f -s $f + ln -f -s $f +done for f in theory_hol.dk theory_hol.lp Makefile BIG_FILES do diff --git a/renaming.lp b/renaming.lp index bf9cb2d0..d13a6f11 100644 --- a/renaming.lp +++ b/renaming.lp @@ -95,6 +95,10 @@ builtin "dollardollar_def" ≔ ﹩﹩_def; builtin "longarrow" ≔ ⭬; builtin "longarrow_def" ≔ ⭬_def; +builtin "N'" ≔ N; +builtin "N''" ≔ N'; +builtin "N'''" ≔ N''; + builtin "R'" ≔ R; builtin "R''" ≔ R'; From 4f242908c227ac0ac3e37cea8b048eb06bb2573e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sat, 11 Jan 2025 14:06:52 +0100 Subject: [PATCH 2/5] rename link into config --- README.md | 36 ++++++++++++++++++++---------------- add-links => config | 0 main.ml | 2 +- 3 files changed, 21 insertions(+), 17 deletions(-) rename add-links => config (100%) diff --git a/README.md b/README.md index 20ecd5b9..7f03ed98 100644 --- a/README.md +++ b/README.md @@ -200,25 +200,29 @@ 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 data: ``` -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 $file.mk $root_path [coq_file_or_module] ... ``` -This will create files and add links to files needed to generate, translate and check proofs. +Do `hol2dk config` for 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}`. @@ -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: diff --git a/add-links b/config similarity index 100% rename from add-links rename to config diff --git a/main.ml b/main.ml index 6910b5ec..5e3513ea 100644 --- a/main.ml +++ b/main.ml @@ -492,7 +492,7 @@ and command = function | ["unpatch" as s] -> call_script s [] | "unpatch"::_ -> wrong_nb_args() - | "link"::args -> call_script "add-links" args + | "config"::args -> call_script "config" args | ["dump";f] -> dump true f (basename_ml f) | "dump"::_ -> wrong_nb_args() From 82e371a023312bdfd48947714837c17ef5833245 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sat, 11 Jan 2025 14:13:16 +0100 Subject: [PATCH 3/5] wip --- .github/workflows/main.yml | 2 +- README.md | 2 +- config | 15 +++++++++------ 3 files changed, 11 insertions(+), 8 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 0f13bb18..4cbe795a 100644 --- a/.github/workflows/main.yml +++ b/.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 diff --git a/README.md b/README.md index 7f03ed98..0885d622 100644 --- a/README.md +++ b/README.md @@ -210,7 +210,7 @@ mkdir output - setup the directory with all the required data: ``` cd output -hol2dk config $hollight_file.ml $file.mk $root_path [coq_file_or_module] ... +hol2dk config $hollight_file.ml $root_path [coq_file_or_module] ... [$file.mk] ``` Do `hol2dk config` for more details. diff --git a/config b/config index cfff2d19..fc735739 100755 --- a/config +++ b/config @@ -14,14 +14,14 @@ fi usage() { cat <<__EOF__ -usage: `basename $0` [--erasing $erasing.lp] $hollight_file.ml $file.mk $root_path [coq_file_or_module] ... +usage: `basename $0` [--erasing $erasing.lp] $hollight_file.ml $root_path [coq_file_or_module] ... [$file.mk] arguments: $erasing.lp: mappings between lambdapi and coq $hollight_file.ml: path to an ml file relative to $HOLLIGHT_DIR - $file.mk: dependencies of vo files given in arguments ($file must be different from "lpo" or "vo") $root_path: name of the generated library coq_file_or_module: coq modules that needs to be imported in generated files + $file.mk: dependencies of vo files given in arguments effect in the current directory: - create a file CONFIG containing the command used to create links @@ -69,8 +69,6 @@ parse_args() { else error 'too many ml files' fi;; - lpo.mk|vo.mk) - error 'lpo.mk and vo.mk are reserved filenames';; *.mk) if test -z "$mk_file" then @@ -137,8 +135,13 @@ echo $requiring > REQUIRING echo create VOFILES ... echo $vo_files > VOFILES -echo ln -f -s $mk_file deps.mk -ln -f -s $mk_file deps.mk +if test -z "$mk_file" +then + touch deps.mk +else + echo ln -f -s $mk_file deps.mk + ln -f -s $mk_file deps.mk +fi for f in $coq_files do From 3daad5f0523d53325cc705176c212ca3bfe24b4f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sat, 11 Jan 2025 14:25:43 +0100 Subject: [PATCH 4/5] wip --- CHANGES.md | 15 ++++++++++++++- dune | 2 +- 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index be1d8382..160083c5 100644 --- a/CHANGES.md +++ b/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) diff --git a/dune b/dune index 59d0f32c..5543ad11 100644 --- a/dune +++ b/dune @@ -5,7 +5,7 @@ ) (install - (files HOLLight.v _CoqProject lambdapi.pkg theory_hol.dk theory_hol.lp encoding.lp renaming.lp erasing.lp fusion.ml bool.ml equal.ml xnames.ml patch unpatch add-links Makefile dep-lpo dep-vo progress README.md) + (files HOLLight.v _CoqProject lambdapi.pkg theory_hol.dk theory_hol.lp encoding.lp renaming.lp erasing.lp fusion.ml bool.ml equal.ml xnames.ml patch unpatch config Makefile dep-lpo dep-vo progress README.md) (section share) (package hol2dk) ) From 27c445eceb559d08d3e4b5502dd1f10ce4780e3e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sat, 11 Jan 2025 14:55:40 +0100 Subject: [PATCH 5/5] wip --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 0885d622..6e7c75f8 100644 --- a/README.md +++ b/README.md @@ -207,12 +207,12 @@ Translating HOL-Light proofs to Lambdapi and Coq mkdir output ``` -- setup the directory with all the required data: +- setup the directory with all the required files: ``` cd output hol2dk config $hollight_file.ml $root_path [coq_file_or_module] ... [$file.mk] ``` -Do `hol2dk config` for more details. +Do `hol2dk config` to get more details. - you can then do in order: * `make` to get the list of targets and variables @@ -225,7 +225,7 @@ Do `hol2dk config` for more details. 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 ------------