Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update the SAW integration #78

Merged
merged 3 commits into from
Jan 28, 2025
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 15 additions & 8 deletions scripts/install.sh
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,12 @@ 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
# 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 .*?
Expand All @@ -17,7 +19,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
Expand Down Expand Up @@ -46,17 +49,21 @@ then
cp deps/yices/*/bin/yices-smt2 bin/yices-smt2
fi

# fetch ABC
# fetch ABC from what4_solvers
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
if [ ! -f bin/saw ]
if [ ! -f bin/saw ] && [ ${IN_SAW_CI:-no} != yes ]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See my recommendation in the other PR about the env var name CI_TEST_LEVEL.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(and see there for why I didn't here)

then
mkdir -p deps/saw
wget $SAW_URL -O deps/saw.tar.gz
Expand All @@ -66,7 +73,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
Expand Down
Loading