-
Notifications
You must be signed in to change notification settings - Fork 1
/
reproduce
executable file
·148 lines (126 loc) · 3.02 KB
/
reproduce
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
#!/bin/sh
set -e # to exit as soon as there is an error
hollight_commit=ea45176
hol2dk_commit=9fa1374
lambdapi_commit=c24b28e2
opam_version=2.2.1
dune_version=3.7
ocaml_version=4.14.2
camlp5_version=8.02.01
coq_version=8.20.0
base=hol_upto_real
dump_simp_option=-before-hol
root_path=HOLLight_Real
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 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() {
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 and package dependencies ...
opam repo add coq-released https://coq.inria.fr/opam/released
opam install -y coq.$coq_version
}
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
cp ../../$base.ml .
hol2dk dump-simp$dump_simp_option $base.ml
cd ..
}
translate_proofs() {
line
echo translate HOL-Light proofs to lambdapi and coq ...
mkdir -p output
cd output
hol2dk link $base --root-path ../../$root_path.v --erasing ../../erasing.lp
make split
make $jobs lp
make $jobs v
cd ..
}
check_proofs() {
line
echo check proofs ...
cd output
make $jobs vo
make opam
cd ..
}
create_and_check_opam_library() {
line
echo create opam library ...
mkdir -p opam
cd output
cp theory_hol.v ../opam
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 ../../$root_path.v ../../Makefile .
make
cd ..
}
export HOLLIGHT_DIR=`pwd`/hol-light
export HOL2DK_DIR=`pwd`/hol2dk
setup_env() {
create_opam_switch
install_hol_light_deps
install_lambdapi
install_coq
install_hol2dk
install_hol_light
patch_hol_light
}
setup_env
dump_proofs
translate_proofs
check_proofs
create_and_check_opam_library
line
echo remove opam switch reproduce ...
opam switch remove reproduce