reproduce

#!/bin/sh

set -e # to exit as soon as there is an error

hollight_version=3.0.0 # for dependencies
hollight_commit=28e4aed
hol2dk_commit=7eb6a02
lambdapi_commit=21ee7f3d

opam_version=2.2.1
dune_version=3.17.1
ocaml_version=5.2.1
camlp5_version=8.03.01
coq_version=8.20.1

hollight_file=Multivariate/make_complex.ml
base=`basename $hollight_file .ml`
root_path=HOLLight
jobs='-j32'

line() { echo '------------------------------------------------------------'; }

mkdir -p tmp
cd tmp

#usage: checkout_commit url commit
checkout_commit() {
    line
    d=`basename $1 .git`
    echo install $d ...
    git clone $1
    cd $d
    git checkout $2
    cd ..
}

create_opam_switch() {
    line
    echo create opam switch ...
    opam switch create . $ocaml_version
}

install_hol_light_deps() {
    line
    echo install HOL-Light dependencies ...
    opam install -y --deps-only hol_light.$hollight_version
}

install_lambdapi() {
    checkout_commit https://github.com/Deducteam/lambdapi.git $lambdapi_commit
    cd lambdapi
    git checkout -b reproduce
    opam install -y .
    cd ..
}

install_coq() {
    line
    echo install coq ...
    opam repo add coq-released https://coq.inria.fr/opam/released
    opam install -y coq.$coq_version
}

install_coq_deps() {
    line
    echo install coq dependencies ...
    opam install -y --deps-only .
}

install_hol2dk() {
    checkout_commit https://github.com/Deducteam/hol2dk.git $hol2dk_commit
    cd hol2dk
    dune build && dune install
    cd ..
}

install_hol_light() {
    checkout_commit https://github.com/jrh13/hol-light.git $hollight_commit
    cd hol-light
    make
    cd ..
}

patch_hol_light() {
    line
    echo patch hol-light ...
    hol2dk patch
}

dump_proofs() {
    line
    echo dump hol-light proofs ...
    cd hol-light
    hol2dk dump-simp $hollight_file
    cd ..
}

config_output_dir() {
    line
    echo configure output directory ...
    mkdir -p output
    cd output
    if test -f Makefile; then make $jobs clean-all; fi
    hol2dk config $hollight_file $root_path HOLLight_Real_With_N.mappings ../../With_N.v Coq.NArith.BinNat Coq.Reals.Rbase Coq.Reals.Rdefinitions Coq.Reals.Rbasic_fun ../../With_N.lp ../../With_N.mk
    cd ..
}
    
translate_proofs() {
    line
    echo translate HOL-Light proofs to lambdapi and coq ...
    cd output
    make split
    make $jobs lp
    make $jobs v
    cd ..
}

check_proofs() {
    line
    echo check proofs ...
    cd output
    make $jobs -k vo
    cd ..
}

create_and_check_opam_library() {
    line
    echo create opam library ...
    cd output
    make opam
    cd ..
    mkdir -p opam
    cd opam
    cp ../../Makefile ../../With_N.v ../output/theory_hol.v .
    sed -e "s/${base}_//g" -e "/^Require Import ${root_path}.types.$/d" ../output/${base}_terms.v > terms.v
    sed -e "s/${base}_//g" -e "/^Require Import ${root_path}.types.$/d" -e '/^Require Import ${root_path}.axioms.$/d' -e "/^Axiom thm_HAS_INTEGRAL_TWIZZLE_INTERVAL /d" ../output/${base}_opam.v > theorems.v
    make
    cd ..
}

compare_opam_file() {
    line
    echo compare $1 ...
    diff ../$1 opam/$1
}

compare_opam_files() {
    for f in theory_hol.v terms.v theorems.v
    do
        compare_opam_file $f
    done
}

export HOLLIGHT_DIR=`pwd`/hol-light
export HOL2DK_DIR=`pwd`/hol2dk

stage() {
    if test -f STAGE
    then
        i=`head -n1 STAGE`
        i=`expr $i + 1`
    else
        i=1
    fi
    if test $i -eq $1
    then
        $2
        echo $1 > STAGE
    fi
}

if test -n "$1"
then
    expr $1 - 1 > STAGE
fi

stage 1 create_opam_switch
eval `opam env`
stage 2 install_hol_light_deps
stage 3 install_lambdapi
stage 4 install_coq
stage 5 install_hol2dk
stage 6 install_hol_light
stage 7 patch_hol_light
stage 8 dump_proofs
stage 9 config_output_dir
stage 10 translate_proofs
stage 11 install_coq_deps
stage 12 check_proofs
stage 13 create_and_check_opam_library
stage 14 compare_opam_files