From b06f158f67638348d4b896bf6c88512d31df9c8a Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 22 Jan 2025 18:53:08 -0500 Subject: [PATCH 1/3] Two updates to the SAW integration: 1. Update the SAW download to use the latest release instead of an ancient nightly that's no longer available. 2. Skip the downloads of both SAW and Cryptol if IN_SAW_CI is set to "yes". These are motivated by the use of this tree in the SAW CI tests, which has been blowing up, first because we tried to delete the ancient nightlies, then because the website reorg broke the downloads. However, at least point (1) seems to be of general value. --- scripts/install.sh | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/scripts/install.sh b/scripts/install.sh index 4c7bf7b7..b55b433d 100755 --- a/scripts/install.sh +++ b/scripts/install.sh @@ -8,6 +8,7 @@ ABC_URL='https://saw.galois.com/builds/abc/abc-c78ee311-Linux.tar.gz' if [ $# -ne 0 ] && [ "$1" = "--latest" ]; then # Determine the URL of the latest SAW and Cryptol nightly + # XXX: this will not work any more ######################################################### SAW_DATE=$(curl -s https://saw.galois.com/builds/nightly/ | grep saw | grep -o "[0-9]\{4\}-[0-9]\{2\}-[0-9]\{2\}" | sort | tail -n 1) # `grep -o` says print only the matched substring SAW_NIGHTLY=$(curl -s https://saw.galois.com/builds/nightly/ | grep -oP "saw.*?${SAW_DATE}-Linux.*?\.tar\.gz" | head -n 1) # `curl -s` means silent; `grep -o` says print only the matched substring; `grep -P` says Perl syntax, which we use to get a lazy match (shortest) with .*? @@ -17,7 +18,8 @@ if [ $# -ne 0 ] && [ "$1" = "--latest" ]; then CRYPTOL_NIGHTLY=$(curl -s https://cryptol.net/builds/nightly/ | grep -oP "cryptol.*?${CRYPTOL_DATE}-Ubuntu.*?\.tar\.gz" | head -n 1) # `curl -s` means silent; `grep -o` says print only the matched substring; `grep -P` says Perl syntax, which we use to get a lazy match (shortest) with .*? CRYPTOL_URL="https://cryptol.net/builds/nightly/${CRYPTOL_NIGHTLY}" else - SAW_URL="https://saw.galois.com/builds/nightly/saw-0.8.0.99-2021-12-06-Linux-x86_64.tar.gz" + #SAW_URL="https://saw.galois.com/builds/nightly/saw-0.8.0.99-2021-12-06-Linux-x86_64.tar.gz" + SAW_URL='https://github.com/GaloisInc/saw-script/releases/download/v1.2/saw-1.2-ubuntu-20.04-X64.tar.gz' CRYPTOL_URL="https://github.com/GaloisInc/cryptol/releases/download/2.11.0/cryptol-2.11.0-Linux-x86_64.tar.gz" fi @@ -56,7 +58,7 @@ then fi # fetch SAW -if [ ! -f bin/saw ] +if [ ! -f bin/saw ] && [ ${IN_SAW_CI:-no} != yes ] then mkdir -p deps/saw wget $SAW_URL -O deps/saw.tar.gz @@ -66,7 +68,7 @@ then fi # fetch Cryptol -if [ ! -f bin/cryptol ] +if [ ! -f bin/cryptol ] && [ ${IN_SAW_CI:-no} != yes ] then mkdir -p deps/cryptol wget $CRYPTOL_URL -O deps/cryptol.tar.gz From 418129e32cff334f9c0120086e62a75ed6d11792 Mon Sep 17 00:00:00 2001 From: David Holland Date: Mon, 27 Jan 2025 17:40:26 -0500 Subject: [PATCH 2/3] Also get abc from a current what4-solvers snapshot. (instead of a long-gone snapshot from saw.galois.com) Needed to unbreak this repository's own CI. --- scripts/install.sh | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/scripts/install.sh b/scripts/install.sh index b55b433d..bbf64d92 100755 --- a/scripts/install.sh +++ b/scripts/install.sh @@ -4,7 +4,8 @@ set -e Z3_URL='https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip' YICES_URL='https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz' -ABC_URL='https://saw.galois.com/builds/abc/abc-c78ee311-Linux.tar.gz' +#ABC_URL='https://saw.galois.com/builds/abc/abc-c78ee311-Linux.tar.gz' +WHAT4_SOLVERS_URL='https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20241119/ubuntu-20.04-X64-bin.zip' if [ $# -ne 0 ] && [ "$1" = "--latest" ]; then # Determine the URL of the latest SAW and Cryptol nightly @@ -48,13 +49,17 @@ then cp deps/yices/*/bin/yices-smt2 bin/yices-smt2 fi -# fetch ABC +# fetch what4_solvers for ABC if [ ! -f bin/abc ] then mkdir -p deps/abc - wget $ABC_URL -O deps/abc.tar.gz - tar -x -f deps/abc.tar.gz --one-top-level=deps/abc - cp deps/abc/*/bin/abc bin/abc + wget $WHAT4_SOLVERS_URL -O deps/what4-solvers.zip + #tar -x -f deps/abc.tar.gz --one-top-level=deps/abc + #cp deps/abc/*/bin/abc bin/abc + unzip -d deps/abc deps/what4-solvers.zip + cp deps/abc/abc bin/abc + # just in case, zip files aren't always good at unix perms + chmod 755 bin/abc fi # fetch SAW From 337cc4d94226e173b1418e881668e830da2c047b Mon Sep 17 00:00:00 2001 From: David Holland Date: Tue, 28 Jan 2025 15:43:16 -0500 Subject: [PATCH 3/3] Fix comment as suggested --- scripts/install.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/install.sh b/scripts/install.sh index bbf64d92..ba2d2dd6 100755 --- a/scripts/install.sh +++ b/scripts/install.sh @@ -49,7 +49,7 @@ then cp deps/yices/*/bin/yices-smt2 bin/yices-smt2 fi -# fetch what4_solvers for ABC +# fetch ABC from what4_solvers if [ ! -f bin/abc ] then mkdir -p deps/abc