From 04e5f3660ac9174618c5e47d473798628b10e31c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Sun, 25 Feb 2024 10:01:56 +0100
Subject: [PATCH] wip

---
 reproduce.sh | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)
 mode change 100644 => 100755 reproduce.sh

diff --git a/reproduce.sh b/reproduce.sh
old mode 100644
new mode 100755
index 620ec6c..70ae12b
--- a/reproduce.sh
+++ b/reproduce.sh
@@ -1,5 +1,7 @@
 #!/bin/sh
 
+set -e # to exit as soon as there is an error
+
 mkdir reproduce
 cd reproduce
 
@@ -19,13 +21,19 @@ git checkout 3d231f3
 make
 hol2dk patch
 
-echo extract hol-light proofs
-#cp hol.ml hol_upto_lists.ml
-#emacs hol_upto_lists.ml # remove every thing after ``loads "lists.ml";;''
-cp ../hol-light.ml .
+echo extract hol-light proofs ...
+cp ../../coq_hol_light.ml .
 hol2dk dump-simp-use coq_hol_light.ml # 39s
 cd ..
 
+echo install lambdapi ...
+git clone https://github.com/Deducteam/lambdapi.git
+cd lambdapi
+git checkout 1bb724cf
+opam install -y .
+cd ..
+
+echo translate HOL-Light proofs to lambdapi and coq ...
 mkdir output
 cd output
 hol2dk link coq_hol_light
@@ -38,6 +46,7 @@ make -j32 vo # 4m
 make opam
 cd ..
 
+echo create opam library ...
 mkdir opam
 cd opam
 ../../create-lib.sh ../output