reproduce

#!/bin/sh

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

#opam_version=2.2.1
#dune_version=3.20.2
#make_version=4.3

hollight_version=3.1.0
hollight_commit=Release-3.1.0
hol2dk_commit=2.1.0
lambdapi_commit=3.0.0
camlp5_version=8.03.06
ocaml_version=5.3.0
rocq_version=9.0.0

hollight_file=hol_upto_real.ml
base=`basename $hollight_file .ml`
dump_simp_option=-before-hol
lpfile=mappings.lp
vfiles='type.v mappings.v'
mkfile=mappings.mk
require=Stdlib.NArith.BinNat
root_path=`awk -F'[":]' '/logpath/{print $3}' opam`
jobs='-j32'

# we prefix $lpfile, $vfiles and $mkfile with "../../"
lpfile=../../$lpfile
if test -n "$mkfile"; then mkfile=../../$mkfile; fi
for f in $vfiles; do files="$files ../../$f"; done
vfiles=$files

mkdir -p tmp
cd tmp

if test -n "$1"
then
    stage=$1
else
    if test -f STAGE
    then
        stage=`head -n1 STAGE` # last completed stage
        stage=`expr $stage + 1`
    else
        stage=1
    fi
fi

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

start() {
    line
    echo STAGE $stage: $* ...
}

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

#usage: install package_name version
install() {
    start install $1
    opam install -y $1.$2
}

create_opam_switch() {
    start create opam switch
    opam update
    opam switch create . $ocaml_version
}

install_hollight_deps() {
    start install HOL-Light dependencies
    opam pin -y camlp5 $camlp5_version
    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_deps() {
    start install dependencies
    opam repo add rocq-released https://rocq-prover.org/opam/released
    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_hollight() {
    checkout_commit https://github.com/jrh13/hol-light.git $hollight_commit
    cd hol-light
    make
    cd ..
}

patch_hollight() {
    start patch hol-light
    hol2dk patch
}

gen_hollight_file() {
    awk "/^loads \"$1.ml\"/{print;RM=1;next}/^loads /{if(RM)next}{print}" hol_lib.ml > hol_lib_upto_$1.ml
    sed -e "s/hol_lib.ml/hol_lib_upto_$1.ml/" hol.ml > $hollight_file
}

dump_proofs() {
    start dump hol-light proofs
    cd hol-light
    gen_hollight_file real
    hol2dk dump-simp$dump_simp_option $hollight_file
    cd ..
}

config_output_dir() {
    start configure output directory
    mkdir -p output
    cd output
    if test -f Makefile; then make $jobs clean-all; fi
    hol2dk config $hollight_file $root_path $require $vfiles $mkfile $lpfile
    cd ..
}

translate_proofs() {
    start translate HOL-Light proofs to lambdapi and rocq
    cd output
    make split
    make $jobs lp
    make $jobs v
    make $jobs merge-spec-files
    make $jobs rm-empty-deps
    cd ..
}

check_proofs() {
    start check proofs
    cd output
    make $jobs vo
    cd ..
}

remove_empty_modules() {
    sed -e "s/${base}_//g" \
        -e "/^Require \(Im\|Ex\)port ${root_path}\.theory_hol\.$/d" \
        -e "/^Require \(Im\|Ex\)port ${root_path}\.types\.$/d" \
        -e "/^Require \(Im\|Ex\)port ${root_path}\.axioms\.$/d" \
        $1
}

create_and_check_opam_library() {
    start create opam library
    cd output
    make $jobs opam
    cd ..
    mkdir -p opam
    cd opam
    if test -f Makefile; then make $jobs clean; fi
    cp ../../opam ../../Makefile $vfiles $mkfile .
    remove_empty_modules ../output/${base}_terms.v > terms.v
    remove_empty_modules ../output/${base}_opam.v > theorems.v
    sed -i -e 's/NUMERAL //g' -e 's/(N0)/N0/g' terms.v theorems.v
    make $jobs
    cd ..
}

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

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

stage() {
    if test $1 -eq $stage
    then
        shift
        $*
        echo $stage > STAGE
        stage=`expr $stage + 1`
    fi
}

stage 1 create_opam_switch
eval `opam env`
stage 2 install_hollight_deps
stage 3 install lambdapi $lambdapi_commit
stage 4 install rocq-prover $rocq_version
stage 5 install_deps
stage 6 install hol2dk $hol2dk_commit
#export HOL2DK_DIR=`pwd`/hol2dk
export HOL2DK_DIR=$OPAM_SWITCH_PREFIX/share/hol2dk
stage 7 install_hollight
export HOLLIGHT_DIR=`pwd`/hol-light
stage 8 patch_hollight
stage 9 dump_proofs
stage 10 config_output_dir
stage 11 create_and_check_opam_library
stage 12 compare_opam_files
stage 13 translate_proofs
stage 14 check_proofs