Skip to content

Commit

Permalink
Changes related to build for standalone Stainless (#1234)
Browse files Browse the repository at this point in the history
* Tweaking launcher script (for standalone Stainless)
* Changes related to builds
- Upgraded Z3 to 4.8.14 to be in-sync with ScalaZ3
- Removed old ScalaZ3 jars for macOS. As such macOS builds are not shipped with ScalaZ3
- Added standalone build for Windows (without shipping ScalaZ3)
  • Loading branch information
mario-bucev authored Feb 25, 2022
1 parent 691cbe0 commit 38e8a38
Show file tree
Hide file tree
Showing 10 changed files with 266 additions and 29 deletions.
90 changes: 90 additions & 0 deletions bin/launcher-cygwin-noscalaz3.tmpl.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,90 @@
#!/usr/bin/env bash

### The following section defines `realpath` to resolve symbolic links.
###
### Copyright (c) 2014 Michael Kropat
### Licensed under the terms of the MIT License (https://opensource.org/licenses/MIT)
### Original code at https://github.com/mkropat/sh-realpath

realpath() {
canonicalize_path "$(resolve_symlinks "$1")"
}

resolve_symlinks() {
_resolve_symlinks "$1"
}

_resolve_symlinks() {
_assert_no_path_cycles "$@" || return

local dir_context path
path=$(readlink -- "$1")
if [ $? -eq 0 ]; then
dir_context=$(dirname -- "$1")
_resolve_symlinks "$(_prepend_dir_context_if_necessary "$dir_context" "$path")" "$@"
else
printf '%s\n' "$1"
fi
}

_prepend_dir_context_if_necessary() {
if [ "$1" = . ]; then
printf '%s\n' "$2"
else
_prepend_path_if_relative "$1" "$2"
fi
}

_prepend_path_if_relative() {
case "$2" in
/* ) printf '%s\n' "$2" ;;
* ) printf '%s\n' "$1/$2" ;;
esac
}

_assert_no_path_cycles() {
local target path

target=$1
shift

for path in "$@"; do
if [ "$path" = "$target" ]; then
return 1
fi
done
}

canonicalize_path() {
if [ -d "$1" ]; then
_canonicalize_dir_path "$1"
else
_canonicalize_file_path "$1"
fi
}

_canonicalize_dir_path() {
(cd "$1" 2>/dev/null && pwd -P)
}

_canonicalize_file_path() {
local dir file
dir=$(dirname -- "$1")
file=$(basename -- "$1")
(cd "$dir" 2>/dev/null && printf '%s/%s\n' "$(pwd -P)" "$file")
}

### end of realpath code

BASE_DIR="$( dirname "$( realpath "${BASH_SOURCE[0]}" )" )"
Z3_DIR="$BASE_DIR/z3"
STAINLESS_JAR="$BASE_DIR/lib/{STAINLESS_JAR_BASENAME}"

if ! [[ -r "$STAINLESS_JAR" ]]; then
echo "Read access for the jar file $STAINLESS_JAR is required."
exit 1
fi

# NOTE: $JAVA_OPTS not quoted, as it may be empty!
# Cygpath necessary, see https://stackoverflow.com/a/16640483
exec env PATH="$Z3_DIR:$PATH" java -cp $(cygpath -w $STAINLESS_JAR) $JAVA_OPTS stainless.Main "$@"
10 changes: 10 additions & 0 deletions bin/launcher-noscalaz3.tmpl.bat
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
@echo off

rem Absolute path of the script: https://stackoverflow.com/a/33372703
pushd %~dp0
set script_dir=%CD%
popd

set PATH=%PATH%;%script_dir%\z3

java -jar %script_dir%\lib\{STAINLESS_JAR_BASENAME} %*
89 changes: 89 additions & 0 deletions bin/launcher-noscalaz3.tmpl.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,89 @@
#!/usr/bin/env bash

### The following section defines `realpath` to resolve symbolic links.
###
### Copyright (c) 2014 Michael Kropat
### Licensed under the terms of the MIT License (https://opensource.org/licenses/MIT)
### Original code at https://github.com/mkropat/sh-realpath

realpath() {
canonicalize_path "$(resolve_symlinks "$1")"
}

resolve_symlinks() {
_resolve_symlinks "$1"
}

_resolve_symlinks() {
_assert_no_path_cycles "$@" || return

local dir_context path
path=$(readlink -- "$1")
if [ $? -eq 0 ]; then
dir_context=$(dirname -- "$1")
_resolve_symlinks "$(_prepend_dir_context_if_necessary "$dir_context" "$path")" "$@"
else
printf '%s\n' "$1"
fi
}

_prepend_dir_context_if_necessary() {
if [ "$1" = . ]; then
printf '%s\n' "$2"
else
_prepend_path_if_relative "$1" "$2"
fi
}

_prepend_path_if_relative() {
case "$2" in
/* ) printf '%s\n' "$2" ;;
* ) printf '%s\n' "$1/$2" ;;
esac
}

_assert_no_path_cycles() {
local target path

target=$1
shift

for path in "$@"; do
if [ "$path" = "$target" ]; then
return 1
fi
done
}

canonicalize_path() {
if [ -d "$1" ]; then
_canonicalize_dir_path "$1"
else
_canonicalize_file_path "$1"
fi
}

_canonicalize_dir_path() {
(cd "$1" 2>/dev/null && pwd -P)
}

_canonicalize_file_path() {
local dir file
dir=$(dirname -- "$1")
file=$(basename -- "$1")
(cd "$dir" 2>/dev/null && printf '%s/%s\n' "$(pwd -P)" "$file")
}

### end of realpath code

BASE_DIR="$( dirname "$( realpath "${BASH_SOURCE[0]}" )" )"
Z3_DIR="$BASE_DIR/z3"
STAINLESS_JAR="$BASE_DIR/lib/{STAINLESS_JAR_BASENAME}"

if ! [[ -r "$STAINLESS_JAR" ]]; then
echo "Read access for the jar file $STAINLESS_JAR is required."
exit 1
fi

# NOTE: $JAVA_OPTS not quoted, as it may be empty!
exec env PATH="$Z3_DIR:$PATH" java -cp "$STAINLESS_JAR" $JAVA_OPTS stainless.Main "$@"
3 changes: 2 additions & 1 deletion bin/launcher.tmpl.sh
Original file line number Diff line number Diff line change
Expand Up @@ -89,4 +89,5 @@ for JAR in "$STAINLESS_JAR" "$SCALAZ3_JAR"; do
fi
done

exec env PATH="$Z3_DIR:$PATH" java -cp "$JARS $JAVA_OPTS" stainless.Main "$@"
# NOTE: $JAVA_OPTS not quoted, as it may be empty!
exec env PATH="$Z3_DIR:$PATH" java -cp "$JARS" $JAVA_OPTS stainless.Main "$@"
93 changes: 68 additions & 25 deletions bin/package-standalone.sh
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
# and packages them into an archive that contains additional Z3
# dependencies and a launcher script that makes said dependencies available
# to the java process.
# Currently only Linux (i.e. Z3's `ubuntu` binaries) and macOS are implemented.
# Currently, only the Linux version is shipped with ScalaZ3 (macOS & Windows must rely on smt-z3)
# ====
set -e

Expand All @@ -15,19 +15,19 @@ if [[ $(git diff --stat) != '' ]]; then
fi

SCALA_VERSION="3.0.2"
Z3_VERSION="4.8.12"
Z3_VERSION="4.8.14"

SBT_PACKAGE_SCALAC="sbt stainless-scalac-standalone/assembly"
SBT_PACKAGE_DOTTY="sbt stainless-dotty-standalone/assembly"
STAINLESS_SCALAC_JAR_PATH="./frontends/stainless-scalac-standalone/target/scala-$SCALA_VERSION/stainless-scalac-standalone-$STAINLESS_VERSION.jar"
STAINLESS_DOTTY_JAR_PATH="./frontends/stainless-dotty-standalone/target/scala-$SCALA_VERSION/stainless-dotty-standalone-$STAINLESS_VERSION.jar"
# Note: though Stainless is compiled with 3.0.2, we use a 2.13 version of ScalaZ3 (which is binary compatible with Scala 3)
SCALAZ3_JAR_LINUX_PATH="./unmanaged/scalaz3-unix-64-2.13.jar"
SCALAZ3_JAR_MAC_PATH="./unmanaged/scalaz3-mac-64-2.13.jar"

Z3_GITHUB_URL="https://github.com/Z3Prover/z3/releases/download/z3-$Z3_VERSION"
Z3_LINUX_NAME="z3-$Z3_VERSION-x64-glibc-2.31.zip"
Z3_MAC_NAME="z3-$Z3_VERSION-x64-osx-10.15.7.zip"
Z3_MAC_NAME="z3-$Z3_VERSION-x64-osx-10.16.zip"
Z3_WIN_NAME="z3-$Z3_VERSION-x64-win.zip"

LOG="./package-standalone.log"

Expand Down Expand Up @@ -75,8 +75,15 @@ function fetch_z3 {
local NAME="$2"
local ZIPF="$TMP_DIR/$NAME"
local TMPD="$TMP_DIR/$PLAT"
local Z3_EXEC
info " - $PLAT"

if [[ "$PLAT" = "win" ]]; then
Z3_EXEC="z3.exe"
else
Z3_EXEC="z3"
fi

if [ -f "$ZIPF" ]; then
info " (ZIP already exists, skipping download step.)"
else
Expand All @@ -86,34 +93,58 @@ function fetch_z3 {
unzip -d "$TMPD" "$ZIPF" >> $LOG || fail

mkdir -p "$TMPD/z3" >> $LOG || fail
for COPY_FILE in LICENSE.txt bin/z3; do
for COPY_FILE in LICENSE.txt "bin/$Z3_EXEC"; do
cp "$TMPD/${NAME%.*}/$COPY_FILE" "$TMPD/z3" >> $LOG || fail
done

okay
}

function generate_launcher {
local TARGET="$1"
local STAINLESS_JAR_BASENAME="$2"
local SCALAZ3_JAR_BASENAME="$3"

cat "bin/launcher.tmpl.sh" | \
sed "s#{STAINLESS_JAR_BASENAME}#$STAINLESS_JAR_BASENAME#g" | \
sed "s#{SCALAZ3_JAR_BASENAME}#$SCALAZ3_JAR_BASENAME#g" \
> "$TARGET"
chmod +x "$TARGET"
local PLAT="$1"
local TMPD="$2"
local STAINLESS_JAR_BASENAME="$3"
local SCALAZ3_JAR_BASENAME="$4"

if [[ "$PLAT" = "win" ]]; then
# For Windows, we generate two scripts, one .bat (native) and one .sh (executable with Cygwin).
# The .bat version needs to have all '/' converted to '\'. We do this with this //\//\\ thing
# (copied from https://unix.stackexchange.com/a/589316).
# Since we do not ship ScalaZ3, we do not need to do replacing of SCALAZ3_JAR_BASENAME
cat "bin/launcher-noscalaz3.tmpl.bat" | \
sed "s#{STAINLESS_JAR_BASENAME}#${STAINLESS_JAR_BASENAME//\//\\}#g" \
> "$TMPD/stainless.bat"
chmod +x "$TMPD/stainless.bat"
cat "bin/launcher-cygwin-noscalaz3.tmpl.sh" | \
sed "s#{STAINLESS_JAR_BASENAME}#$STAINLESS_JAR_BASENAME#g" \
> "$TMPD/stainless.sh"
chmod +x "$TMPD/stainless.sh"
else
local SCRIPT_TMPLT_NAME
if [[ "$SCALAZ3_JAR_BASENAME" = "" ]]; then
SCRIPT_TMPLT_NAME="bin/launcher-noscalaz3.tmpl.sh"
elif [[ "$PLAT" != "win" ]]; then
SCRIPT_TMPLT_NAME="bin/launcher.tmpl.sh"
fi

cat "$SCRIPT_TMPLT_NAME" | \
sed "s#{STAINLESS_JAR_BASENAME}#$STAINLESS_JAR_BASENAME#g" | \
sed "s#{SCALAZ3_JAR_BASENAME}#$SCALAZ3_JAR_BASENAME#g" \
> "$TMPD/stainless.sh"
chmod +x "$TMPD/stainless.sh"
fi
}

function package {
local PLAT="$1"
local STAINLESS_JAR_PATH="$2"
local SCALAZ3_JAR_PATH="$3"
local FRONTEND="$4"
local STAINLESS_JAR_BASENAME
local SCALAZ3_JAR_BASENAME
STAINLESS_JAR_BASENAME=$(basename "$STAINLESS_JAR_PATH")
SCALAZ3_JAR_BASENAME=$(basename "$SCALAZ3_JAR_PATH")
local STAINLESS_JAR_BASENAME=$(basename "$STAINLESS_JAR_PATH")
local SCALAZ3_JAR_BASENAME=""
if [[ "$SCALAZ3_JAR_PATH" != "" ]]; then
SCALAZ3_JAR_BASENAME=$(basename "$SCALAZ3_JAR_PATH")
fi

local TMPD="$TMP_DIR/$PLAT"
info " - $PLAT (for $FRONTEND)"
Expand All @@ -126,16 +157,25 @@ function package {
info " (Removed old $FRONTEND archive.)"
fi

generate_launcher "$TMPD/stainless" "$STAINLESS_JAR_BASENAME" "$SCALAZ3_JAR_BASENAME" || fail
generate_launcher "$PLAT" "$TMPD" "$STAINLESS_JAR_BASENAME" "$SCALAZ3_JAR_BASENAME" || fail

local TGTLIBD="$TMPD/lib"
mkdir -p "$TGTLIBD" >> $LOG || fail
cp "$STAINLESS_JAR_PATH" "$TGTLIBD/$STAINLESS_JAR_BASENAME" >> $LOG || fail
cp "$SCALAZ3_JAR_PATH" "$TGTLIBD/$SCALAZ3_JAR_BASENAME" >> $LOG || fail
if [[ "$SCALAZ3_JAR_BASENAME" != "" ]]; then
cp "$SCALAZ3_JAR_PATH" "$TGTLIBD/$SCALAZ3_JAR_BASENAME" >> $LOG || fail
fi
cp "stainless.conf.default" "$TMPD/stainless.conf" >> $LOG || fail

local STAINLESS_SCRIPTSS
if [[ "$PLAT" = "win" ]]; then
STAINLESS_SCRIPTS=("stainless.bat" "stainless.sh")
else
STAINLESS_SCRIPTS=("stainless.sh")
fi

cd "$TMPD" && \
zip "$ZIPF" lib/** z3/** stainless stainless.conf >> $LOG && \
zip "$ZIPF" lib/** z3/** "${STAINLESS_SCRIPTS[@]}" stainless.conf >> $LOG && \
cd - >/dev/null || fail
info " Created $FRONTEND archive $ZIPF"

Expand All @@ -155,22 +195,25 @@ info "$(tput bold)[] Assembling fat jar..."
if [[ -f "$STAINLESS_SCALAC_JAR_PATH" && -f "$STAINLESS_DOTTY_JAR_PATH" ]]; then
info " (JAR already exists, skipping sbt assembly step.)" && okay
else
$SBT_PACKAGE_SCALAC >> $LOG && okay || fail
$SBT_PACKAGE_SCALAC >> $LOG || fail
$SBT_PACKAGE_DOTTY >> $LOG && okay || fail
fi

info "$(tput bold)[] Downloading Z3 binaries..."
fetch_z3 "linux" $Z3_LINUX_NAME
fetch_z3 "mac" $Z3_MAC_NAME
fetch_z3 "win" $Z3_WIN_NAME

info "$(tput bold)[] Packaging..."
package "linux" $STAINLESS_SCALAC_JAR_PATH $SCALAZ3_JAR_LINUX_PATH "scalac"
package "linux" $STAINLESS_DOTTY_JAR_PATH $SCALAZ3_JAR_LINUX_PATH "dotty"
package "mac" $STAINLESS_SCALAC_JAR_PATH $SCALAZ3_JAR_MAC_PATH "scalac"
package "mac" $STAINLESS_DOTTY_JAR_PATH $SCALAZ3_JAR_MAC_PATH "dotty"
package "mac" $STAINLESS_SCALAC_JAR_PATH "" "scalac"
package "mac" $STAINLESS_DOTTY_JAR_PATH "" "dotty"
package "win" $STAINLESS_SCALAC_JAR_PATH "" "scalac"
package "win" $STAINLESS_DOTTY_JAR_PATH "" "dotty"

info "$(tput bold)[] Cleaning up..."
# We only clean up the directories used for packaging; we leave the downloaded Z3 binaries.
rm -r "$TMP_DIR/linux" "$TMP_DIR/mac" && okay
rm -r "$TMP_DIR/linux" "$TMP_DIR/mac" "$TMP_DIR/win" && okay

info "$(tput bold)Packaging successful."
Loading

0 comments on commit 38e8a38

Please sign in to comment.