summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2021-12-17 16:07:04 -0600
committerGitHub <noreply@github.com>2021-12-17 22:07:04 +0000
commit63892729113274410dd974f1d2541aa96d3788d3 (patch)
tree4aa87fe3830a22a4aefd9bd409abefa512650737
parent2df0cc4257391daf6daf175826d69a735517ad19 (diff)
Simplify contrib/get-lfsc-checker and use cvc5 repo for LFSC signatures (#7835)
-rwxr-xr-xcontrib/get-lfsc-checker12
1 files changed, 4 insertions, 8 deletions
diff --git a/contrib/get-lfsc-checker b/contrib/get-lfsc-checker
index 9a7292fc7..889455917 100755
--- a/contrib/get-lfsc-checker
+++ b/contrib/get-lfsc-checker
@@ -25,7 +25,7 @@ mkdir -p $LFSC_DIR
# download and unpack LFSC
version="15f53d6feb84e4ddb41deaf2b5630f5c1303b06d"
-download "https://github.com/CVC4/LFSC/archive/$version.tar.gz" $BASE_DIR/tmp/lfsc.tgz
+download "https://github.com/cvc5/LFSC/archive/$version.tar.gz" $BASE_DIR/tmp/lfsc.tgz
tar --strip 1 -xzf $BASE_DIR/tmp/lfsc.tgz -C $LFSC_DIR
# build and install LFSC
@@ -36,17 +36,13 @@ make install
popd
##### signatures
-SIG_DIR="$BASE_DIR/lfsc-signatures"
-mkdir -p $SIG_DIR
-# download and unpack signatures
-sig_version="5d72dafd48aded21fd717ef77321e1c88f732d28"
-download "https://github.com/CVC4/signatures/archive/$sig_version.tar.gz" $BASE_DIR/tmp/signatures.tgz
-tar --strip 1 -xzf $BASE_DIR/tmp/signatures.tgz -C $SIG_DIR
+# The LFSC signatures live in the main cvc5 repository
+SIG_DIR="$BASE_DIR/../proofs/lfsc/signatures"
# install signatures and scripts
mkdir -p $BASE_DIR/share/lfsc
-cp -r $SIG_DIR/lfsc/new/signatures $BASE_DIR/share/lfsc
+cp -r $SIG_DIR $BASE_DIR/share/lfsc
# based on https://github.com/CVC4/signatures/blob/master/lfsc/new/scripts/cvc4_gen_and_check.sh
cat << EOF > $BASE_DIR/bin/cvc5-lfsc-check.sh
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback