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.

Sign up for GitHub

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

Support for ARM64 environments #86

Open
wants to merge 12 commits into
base: master
Choose a base branch
from
Open

Support for ARM64 environments #86

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
61917e1
On AArch64, compile Z3 from source
Jan 5, 2022
3bb5a49
syntax
Jan 5, 2022
030d454
Merge ssh://armagnac.local/~/Code/everest into protz_aarch64
msprotz Jan 5, 2022
ff86daa
fixups
msprotz Jan 5, 2022
fd7a84e
path woes
msprotz Jan 5, 2022
7edf0de
Run a test to determine whether z3 segfaults
msprotz Jan 6, 2022
4f105ad
try differently
msprotz Jan 6, 2022
fd0142b
Even better
msprotz Jan 6, 2022
38992bf
semicolon
msprotz Jan 6, 2022
b27512f
typo
msprotz Jan 6, 2022
186cc86
typo
msprotz Jan 7, 2022
b1ec481
Try with older z3.
msprotz Jan 9, 2022
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
95 changes: 64 additions & 31 deletions everest
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -249,7 +249,7 @@ windows_check_or_modify_env_dest_file () {
write_z3_env_dest_file () {
str="
# This line automatically added by $0
export PATH=$(pwd)/$1/bin:\$PATH"
export PATH=$(pwd)/$1:\$PATH"
write_to_env_dest_file "$str"
}

Expand Down Expand Up @@ -356,43 +356,76 @@ parse_z3_version () {
do_update_z3 () {
# Update our clone of FStarLang/binaries and check that we have the blessed z3
# version
if ! [[ -d fstarlang_binaries ]]; then
echo "... cloning FStarLang/binaries"
try_git_clone "git@github.com:FStarLang/binaries.git" "https://github.com/FStarLang/binaries.git" fstarlang_binaries
fi
(cd fstarlang_binaries && git fetch && git checkout z3-4.8.5 && git reset --hard origin/z3-4.8.5)

local current_z3=$(parse_z3_version)
echo "... version of z3 found in PATH: $current_z3"

if is_windows; then
local new_z3_file=fstarlang_binaries/z3-tested/z3-4.8.5*-x64-win.zip
elif is_osx; then
local new_z3_file=fstarlang_binaries/z3-tested/z3-4.8.5*-x64-osx-*.zip
elif [[ $(lsb_release -i | awk '{ print $3; }') == "Ubuntu" ]]; then
local new_z3_file=fstarlang_binaries/z3-tested/z3-4.8.5*-x64-ubuntu-14.04.zip
elif [[ $(lsb_release -i | awk '{ print $3; }') == "Debian" ]]; then
local new_z3_file=fstarlang_binaries/z3-tested/z3-4.8.5*-x64-debian-*.zip
else
red "WARNING: could not figure out your system via lsb_release; defaulting to Debian"
local new_z3_file=fstarlang_binaries/z3-tested/z3-4.8.5*-x64-debian-*.zip
fi
local new_z3=4.8.5
new_z3_file=$(ls $new_z3_file)
echo "... version of z3 found in z3-tested is: $new_z3_file"

if [[ $new_z3 != $current_z3 ]]; then
magenta "Get the freshest z3 from FStarLang/binaries? [Yn]"
prompt_yes true "exit 1"
echo "... ls fstarlang_binaries/z3-tested"
ls -altrh fstarlang_binaries/z3-tested
echo "... ls $new_z3_file"
ls -altrh $new_z3_file
echo "... unzipping $new_z3_file"
unzip $new_z3_file
local new_z3_folder=${new_z3_file%%.zip}
new_z3_folder=${new_z3_folder##fstarlang_binaries/z3-tested/}
find $new_z3_folder -iname '*.dll' -or -iname '*.exe' | xargs chmod a+x
if [[ $(uname -m) == "aarch64" ]]; then
magenta "Get the freshest z3 from source? [Yn]"
prompt_yes true "exit 1"

if [[ ! -d z3-source ]]; then
git clone https://github.com/Z3Prover/z3 z3-source
fi
pushd z3-source
git checkout Z3-$new_z3
mkdir -p build
cd build
cmake -G "Unix Makefiles" ../
make -j4
if ./z3 ../../queries-*.smt2; [[ $? != 1 ]]; then
echo "!!! Z3 crashed, cannot build $new_z3, switching to 8ebeaf03b4a84e150b593d1f5cbcbacca61f1117 instead"
# I ran a git bisect to figure out which commit was the first one that
# fixes the bug. Trying to stay as close to 4.8.5 as possible, since the
# output changed at some point and then we get errors along the lines of
# Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
# (Failure "Parse error: </result> not found"
git checkout 8ebeaf03b4a84e150b593d1f5cbcbacca61f1117
cmake -G "Unix Makefiles" ../
make -j4
fi
popd
local new_z3_folder=z3-source/build

else
magenta "Get the freshest z3 from FStarLang/binaries? [Yn]"
prompt_yes true "exit 1"

if ! [[ -d fstarlang_binaries ]]; then
echo "... cloning FStarLang/binaries"
try_git_clone "git@github.com:FStarLang/binaries.git" "https://github.com/FStarLang/binaries.git" fstarlang_binaries
fi
(cd fstarlang_binaries && git fetch && git checkout z3-4.8.5 && git reset --hard origin/z3-4.8.5)

if is_windows; then
local new_z3_file=fstarlang_binaries/z3-tested/z3-4.8.5*-x64-win.zip
elif is_osx; then
local new_z3_file=fstarlang_binaries/z3-tested/z3-4.8.5*-x64-osx-*.zip
elif [[ $(lsb_release -i | awk '{ print $3; }') == "Ubuntu" ]]; then
local new_z3_file=fstarlang_binaries/z3-tested/z3-4.8.5*-x64-ubuntu-14.04.zip
elif [[ $(lsb_release -i | awk '{ print $3; }') == "Debian" ]]; then
local new_z3_file=fstarlang_binaries/z3-tested/z3-4.8.5*-x64-debian-*.zip
else
red "WARNING: could not figure out your system via lsb_release; defaulting to Debian"
local new_z3_file=fstarlang_binaries/z3-tested/z3-4.8.5*-x64-debian-*.zip
fi
new_z3_file=$(ls $new_z3_file)
echo "... version of z3 found in z3-tested is: $new_z3_file"

echo "... ls fstarlang_binaries/z3-tested"
ls -altrh fstarlang_binaries/z3-tested
echo "... ls $new_z3_file"
ls -altrh $new_z3_file
echo "... unzipping $new_z3_file"
unzip $new_z3_file
local new_z3_folder=${new_z3_file%%.zip}
new_z3_folder=${new_z3_folder##fstarlang_binaries/z3-tested/}/bin
find $new_z3_folder/.. -iname '*.dll' -or -iname '*.exe' | xargs chmod a+x
fi

magenta "Automatically customize $EVEREST_ENV_DEST_FILE with the z3 path? [Yn]"
prompt_yes "write_z3_env_dest_file $new_z3_folder" true
rm -f z3
Expand Down
Loading