wip

reproduce

@@ -5,80 +5,132 @@ set -e # to exit as soon as there is an error
 opam_version=2.2.1
 dune_version=3.7
 
-hol2dk_commit=58db5d9
+hol2dk_commit=f81cbca
 hollight_commit=ea45176
 lambdapi_version=2.5.1
-ocaml_version=4.14.1
+ocaml_version=4.14.2
 camlp5_version=8.02.01
-coq_version=8.20
-ssreflect_version=2.1.0
+coq_version=8.20.0
+mathcomp_ssreflect_version=2.2.0
+mathcomp_algebra_version=2.2.0
 
 hollight_file=hol_upto_realax
 dump_simp_option=-before-hol
 
 line() { echo '------------------------------------------------------------'; }
 
-line
-echo create opam switch reproduce ...
-opam switch create reproduce $ocaml_version || (echo 'you can remove the opam switch reproduce with:'; echo 'opam switch remove reproduce'; exit 1)
-
-line
-echo install HOL-Light dependencies ...
-opam install camlp5.$camlp5_version ocamlfind zarith
-
-line
-echo install lambdapi ...
-opam install lambdapi.$lambdapi_version
-
-line
-echo install coq and ssreflect ...
-opam install coq.$coq_version coq-mathcomp-ssreflect.$ssreflect_version
-
-mkdir tmp
+mkdir -p tmp
 cd tmp
 
-line
-echo install hol2dk ...
-git clone https://github.com/Deducteam/hol2dk.git
-cd hol2dk
-export HOL2DK_DIR=`pwd`
-git checkout $hol2dk_commit
-dune build && dune install
-cd ..
-
-line
-echo install and patch hol-light ...
-git clone https://github.com/jrh13/hol-light.git
-cd hol-light
-export HOLLIGHT_DIR=`pwd`
-git checkout $hollight_commit
-make
-hol2dk patch
-
-line
-echo extract hol-light proofs ...
-cp ../../$hollight_file.ml .
-hol2dk dump-simp$dump_simp_option $hollight_file.ml
-cd ..
-
-line
-echo translate HOL-Light proofs to lambdapi and coq ...
-mkdir output
-cd output
-hol2dk link $hollight_file
-make split
-make -j32 lp
-make -j32 v
-cp ../real*.v .
-sed -i -e 's/fourcolor\./HOLLight./' HOLLight.v
-coqc -R . HOLLight -no-glob HOLLight.v
-make -j32 vo
-make opam
-
-line
-echo create opam library ...
-mkdir ../opam
-../hol2dk/create-lib ../opam
+create_opam_switch() {
+    line
+    echo create opam switch reproduce ...
+    opam switch create reproduce $ocaml_version || (echo 'you can remove the opam switch reproduce with:'; echo 'opam switch remove reproduce'; exit 1)
+}
+
+install_hol_light_deps() {
+    line
+    echo install HOL-Light dependencies ...
+    opam install -y camlp5.$camlp5_version ocamlfind zarith
+}
+
+install_lambdapi() {
+    line
+    echo install lambdapi ...
+    opam install -y lambdapi.$lambdapi_version
+}
+
+install_coq_and_package_deps() {
+    line
+    echo install coq and package dependencies ...
+    opam repo add coq-released https://coq.inria.fr/opam/released
+    opam install -y coq.$coq_version coq-mathcomp-ssreflect.$mathcomp_ssreflect_version coq-mathcomp-algebra.$mathcomp_algebra_version
+}
+
+install_hol2dk() {
+    line
+    echo install hol2dk ...
+    git clone https://github.com/Deducteam/hol2dk.git
+    cd hol2dk
+    export HOL2DK_DIR=`pwd`
+    git checkout $hol2dk_commit
+    dune build && dune install
+    cd ..
+}
+
+install_and_patch_hol_light() {
+    line
+    echo install and patch hol-light ...
+    git clone https://github.com/jrh13/hol-light.git
+    cd hol-light
+    export HOLLIGHT_DIR=`pwd`
+    git checkout $hollight_commit
+    make
+    hol2dk patch
+    cd ..
+}
+
+dump_proofs() {
+    line
+    echo extract hol-light proofs ...
+    cd hol-light
+    cp ../../$hollight_file.ml .
+    hol2dk dump-simp$dump_simp_option $hollight_file.ml
+    cd ..
+}
+
+translate_proofs() {
+    line
+    echo translate HOL-Light proofs to lambdapi and coq ...
+    mkdir -p output
+    cd output
+    hol2dk link $hollight_file
+    make split
+    make -j32 lp
+    make -j32 v
+    cp ../../real*.v .
+    sed -i -e 's/HOLLight_Real/HOLLight/' real*.v
+    sed -e 's/HOLLight_Real/HOLLight/' ../../HOLLight_Real.v > HOLLight.v
+    cd ..
+}
+
+check_proofs() {
+    line
+    echo check proofs ...
+    cd output
+    coqc -R . HOLLight -no-glob real.v
+    coqc -R . HOLLight -no-glob realsyntax.v
+    coqc -R . HOLLight -no-glob realprop.v
+    coqc -R . HOLLight -no-glob realcategorical.v
+    make -j32 vo
+    make opam
+    cd ..
+}
+
+create_and_check_opam_library() {
+    line
+    echo create opam library ...
+    mkdir -p opam
+    cd output
+    ../hol2dk/create-lib ../opam
+    cd ../opam
+    mv HOLLight.v HOLLight_Real.v
+    sed -i -e 's/HOLLight/HOLLight_Real/g' *.v
+    cp ../../Makefile ../../real*.v .
+    make
+    cd ..
+}
+
+create_opam_switch
+install_hol_light_deps
+install_lambdapi
+install_coq_and_package_deps
+install_hol2dk
+install_and_patch_hol_light
+dump_proofs
+translate_proofs
+check_proofs
+create_and_check_opam_library
 
 line
 echo remove opam switch reproduce ...