wip

README.md

@@ -5,7 +5,7 @@ This library provides a translation in Coq of the definition of real numbers in
 
 It has been automatically generated from HOL-Light using [hol2dk](https://github.com/Deducteam/hol2dk) and [lambdapi](https://github.com/Deducteam/lambdapi).
 
-Proofs are not included but can be regenerated and rechecked by running [reproduce](https://github.com/Deducteam/coq-hol-light-real/blob/main/reproduce) (it takes around 5 minutes on a machine with 32 processors Intel Core i9-13950HX and 64 Gb RAM).
+Proofs are not included but can be regenerated and rechecked by running [reproduce](https://github.com/Deducteam/coq-hol-light-real/blob/main/reproduce) (it takes around 10 minutes on a machine with 32 processors Intel Core i9-13950HX and 64 Gb RAM).
 
 As HOL-Light is based on higher-order logic, this library assumes classical logic, Hilbert's ε operator, functional and propositional extensionnality (see [HOLLight.v](https://github.com/Deducteam/coq-hol-light-real/blob/main/HOLLight.v) for more details):
 

reproduce

@@ -4,7 +4,7 @@ set -e # to exit as soon as there is an error
 
 hollight_version=3.0.0 # for dependencies
 hollight_commit=28e4aed
-hol2dk_commit=123cf68
+hol2dk_commit=86bdfb0
 lambdapi_commit=ccfa0e77
 
 opam_version=2.2.1
@@ -96,7 +96,7 @@ translate_proofs() {
     mkdir -p output
     cd output
     make $jobs clean-all || true
-    hol2dk config $base.ml --erasing ../../erasing.lp HOLLight_Real ../../Logic.v ../With_N.v ../../deps.mk
+    hol2dk config $base.ml $root_path ../../Logic.v ../../With_N.v BinNat ../../deps.mk ../../erasing.lp
     make split
     make $jobs lp
     make $jobs v
@@ -121,7 +121,7 @@ create_and_check_opam_library() {
     sed -e "s/${base}_//g" -e "/^Require Import ${root_path}.types.$/d" ${base}_terms.v > ../opam/terms.v
     sed -e "s/${base}_//g" -e "/^Require Import ${root_path}.types.$/d" -e '/^Require Import ${root_path}.axioms.$/d' ${base}_opam.v > ../opam/theorems.v
     cd ../opam
-    cp ../../Logic.v ../../With_N.v ../../deps.mk ../../Makefile .
+    cp ../../*.v ../../deps.mk ../../Makefile .
     make
     cd ..
 }