-
Notifications
You must be signed in to change notification settings - Fork 54
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
Add scripts for CI #1574
Add scripts for CI #1574
Changes from all commits
81b748b
403ff2e
7463c9e
afd3d8b
488d719
c466c26
ac65a59
57850f8
c9e19dc
63bd368
c75ba8d
6404211
80bf3d0
c70385d
dcb62a7
28977df
df8f1cf
fe28192
d883f21
e59f0db
f730eb2
2992da6
d41aa60
cfe9f94
4e69854
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,44 @@ | ||
name: Stainless CI | ||
on: | ||
pull_request: | ||
types: [opened, synchronize, reopened, ready_for_review] | ||
push: | ||
branches: | ||
- main | ||
jobs: | ||
tests: | ||
if: github.event.pull_request.draft == false | ||
runs-on: [self-hosted, linux] | ||
env: | ||
# define Java options for both official sbt and sbt-extras | ||
JAVA_OPTS: -Dsbt.io.implicit.relative.glob.conversion=allow -Xss512M -Xms1024M -Xmx12G -XX:MaxMetaspaceSize=2G -XX:+UseCodeCacheFlushing -XX:ReservedCodeCacheSize=768M | ||
JVM_OPTS: -Dsbt.io.implicit.relative.glob.conversion=allow -Xss512M -Xms1024M -Xmx12G -XX:MaxMetaspaceSize=2G -XX:+UseCodeCacheFlushing -XX:ReservedCodeCacheSize=768M | ||
steps: | ||
- name: Checkout | ||
uses: actions/checkout@v4 | ||
with: | ||
submodules: recursive | ||
- name: Setup JDK | ||
uses: actions/setup-java@v3 | ||
with: | ||
distribution: temurin | ||
java-version: 17 | ||
- name: Install solvers | ||
run: ./stainless-ci.sh --install-solvers $GITHUB_WORKSPACE/.local/bin | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I don't see any caching here, does this run every time? Why not install the solvers once and for all on the CI server? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yes, it's run everytime, which is quick, specially compared to the duration of the CI. We can setup them on the server indeed, that step is required if running on Github servers though. I'll check with Fabien if he can install them, then I'll run this only if the solvers are not available 👍 |
||
- name: Add solvers to PATH | ||
run: echo "$GITHUB_WORKSPACE/.local/bin" >> $GITHUB_PATH | ||
- name: Test solvers availability | ||
run: cvc5 --version && z3 --version && cvc4 --version | ||
- name: Build and Package | ||
run: ./stainless-ci.sh --build-only | ||
- name: Run Tests and Integration Tests | ||
run: ./stainless-ci.sh --skip-build --skip-bolts --skip-sbt-plugin | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why not just define this CLI interface as |
||
- name: Sbt Plugin Tests | ||
run: ./stainless-ci.sh --skip-build --skip-tests --skip-bolts | ||
fail_if_pull_request_is_draft: | ||
if: github.event.pull_request.draft == true | ||
runs-on: [self-hosted, linux] | ||
steps: | ||
- name: Fails in order to indicate that pull request needs to be marked as ready to review and tests workflows need to pass. | ||
run: exit 1 | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,31 @@ | ||
name: Stainless CI | ||
on: | ||
schedule: | ||
- cron: '0 1 * * *' | ||
jobs: | ||
bolts: | ||
runs-on: [self-hosted, linux] | ||
env: | ||
# define Java options for both official sbt and sbt-extras | ||
JAVA_OPTS: -Dsbt.io.implicit.relative.glob.conversion=allow -Xss512M -Xms1024M -Xmx12G -XX:MaxMetaspaceSize=2G -XX:+UseCodeCacheFlushing -XX:ReservedCodeCacheSize=768M | ||
JVM_OPTS: -Dsbt.io.implicit.relative.glob.conversion=allow -Xss512M -Xms1024M -Xmx12G -XX:MaxMetaspaceSize=2G -XX:+UseCodeCacheFlushing -XX:ReservedCodeCacheSize=768M | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I am wondering if you could avoid duplication with strategies described at https://docs.github.com/en/actions/sharing-automations/avoiding-duplication. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. indeed 👍 There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'll check though :) |
||
steps: | ||
- name: Checkout | ||
uses: actions/checkout@v4 | ||
with: | ||
submodules: recursive | ||
- name: Setup JDK | ||
uses: actions/setup-java@v3 | ||
with: | ||
distribution: temurin | ||
java-version: 17 | ||
- name: Install solvers | ||
run: ./stainless-ci.sh --install-solvers $GITHUB_WORKSPACE/.local/bin | ||
- name: Add solvers to PATH | ||
run: echo "$GITHUB_WORKSPACE/.local/bin" >> $GITHUB_PATH | ||
- name: Test solvers availability | ||
run: cvc5 --version && z3 --version && cvc4 --version | ||
- name: Build and Package | ||
run: ./stainless-ci.sh --build-only | ||
- name: Bolts Tests | ||
run: ./stainless-ci.sh --skip-build --skip-tests --skip-sbt-plugin |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,178 @@ | ||
#!/usr/bin/env bash | ||
|
||
# Run the complete CI pipeline | ||
|
||
# Record the time to compute the total duration | ||
TIME_BEFORE=$(date +%s) | ||
|
||
BUILD_ONLY=false | ||
SKIP_BOLTS=false | ||
SKIP_BUILD=false | ||
SKIP_SBT_PLUGIN=false | ||
SKIP_TESTS=false | ||
|
||
# First parse the options | ||
while [[ $# -gt 0 ]]; do | ||
key="$1" | ||
|
||
case $key in | ||
-h|--help) | ||
usage | ||
exit 0 | ||
;; | ||
--bolts-dir) | ||
BOLTS_DIR="$2" | ||
shift # past argument | ||
shift # past value | ||
;; | ||
--build-only) | ||
BUILD_ONLY=true | ||
shift # past argument | ||
;; | ||
--skip-bolts) | ||
SKIP_BOLTS=true | ||
shift # past argument | ||
;; | ||
--skip-build) | ||
SKIP_BUILD=true | ||
shift # past argument | ||
;; | ||
--skip-sbt-plugin) | ||
SKIP_SBT_PLUGIN=true | ||
shift # past argument | ||
;; | ||
--skip-tests) | ||
SKIP_TESTS=true | ||
shift # past argument | ||
;; | ||
--install-solvers) | ||
SOLVERS_DIR="$2" | ||
shift # past argument | ||
shift # past value | ||
;; | ||
*) # unknown option | ||
usage | ||
exit 1 | ||
;; | ||
esac | ||
done | ||
|
||
usage() { | ||
cat <<EOM | ||
Usage: external-tests.sh [options] | ||
|
||
-h | -help Print this message | ||
--bolts-dir <DIR> Directory where bolts is located (default: clones from GitHub). | ||
--build-only Only build the project, do not run tests. | ||
--skip-build Do not build the project (saves time if the build is already up-to-date). | ||
--skip-bolts Do not run the Bolts benchmarks. | ||
--skip-sbt-plugin Do not run the sbt plugin tests. | ||
--skip-tests Do not run the unit and integration tests. | ||
--install-solvers <DIR> Install the solvers required for the tests (cvc5, CVC4, and z3) FOR LINUX. | ||
|
||
EOM | ||
} | ||
|
||
# Download the solvers | ||
if [ -n "$SOLVERS_DIR" ]; then | ||
TEMP_DIR="temp" | ||
mkdir -p "$SOLVERS_DIR" | ||
mkdir -p "$TEMP_DIR" | ||
# cvc5 | ||
wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.1.2/cvc5-Linux-static.zip -O "$TEMP_DIR/downloaded.zip" | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. haha 👍 |
||
unzip "$TEMP_DIR/downloaded.zip" -d "$TEMP_DIR" | ||
CVC5_DIR=$(ls "$TEMP_DIR" | grep cvc5) | ||
mv "$TEMP_DIR/$CVC5_DIR/bin/cvc5" "$SOLVERS_DIR/cvc5" | ||
chmod +x "$SOLVERS_DIR/cvc5" | ||
rm -rf "$TEMP_DIR" | ||
|
||
# CVC4 | ||
wget https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.8-x86_64-linux-opt -O "$SOLVERS_DIR/cvc4" | ||
chmod +x "$SOLVERS_DIR/cvc4" | ||
|
||
# z3 | ||
mkdir -p "$TEMP_DIR" | ||
wget https://github.com/Z3Prover/z3/releases/download/z3-4.13.0/z3-4.13.0-x64-glibc-2.35.zip -O "$TEMP_DIR/downloaded.zip" | ||
unzip "$TEMP_DIR/downloaded.zip" -d "$TEMP_DIR" | ||
Z3_DIR=$(ls "$TEMP_DIR" | grep z3) | ||
mv "$TEMP_DIR/$Z3_DIR/bin/z3" "$SOLVERS_DIR/z3" | ||
chmod +x "$SOLVERS_DIR/z3" | ||
rm -rf "$TEMP_DIR" | ||
|
||
echo "************** Solvers Installed **************" | ||
exit 0 | ||
fi | ||
|
||
if [ "$SKIP_BUILD" = true ]; then | ||
echo "************** Skipping build **************" | ||
else | ||
sbt universal:stage | ||
if [ $? -ne 0 ]; then | ||
echo "************** Failed to build the universal package **************" | ||
exit 1 | ||
fi | ||
if [ "$BUILD_ONLY" = true ]; then | ||
echo "************** Build only done **************" | ||
exit 0 | ||
fi | ||
fi | ||
|
||
if [ "$SKIP_TESTS" = true ]; then | ||
echo "************** Skipping tests **************" | ||
else | ||
# Run the tests | ||
sbt -batch -Dtestsuite-parallelism=5 test | ||
if [ $? -ne 0 ]; then | ||
echo "************** Unit tests failed **************" | ||
exit 1 | ||
fi | ||
|
||
# Run the integration tests | ||
sbt -batch -Dtestsuite-parallelism=3 -Dtestcase-parallelism=5 it:test | ||
if [ $? -ne 0 ]; then | ||
echo "************** Integration tests failed **************" | ||
exit 1 | ||
fi | ||
|
||
fi | ||
|
||
# Run the Bolts benchmarks | ||
# if BOLTS_DIR is set, pass it to the script | ||
if [ "$SKIP_BOLTS" = true ]; then | ||
echo "************** Skipping Bolts tests **************" | ||
else | ||
if [ -z "$BOLTS_DIR" ]; then | ||
bash bin/external-tests.sh --skip-build | ||
else | ||
bash bin/external-tests.sh --skip-build --bolts-dir $BOLTS_DIR | ||
fi | ||
if [ $? -ne 0 ]; then | ||
echo "Bolts benchmarks failed" | ||
exit 1 | ||
fi | ||
fi | ||
|
||
# Run sbt scripted | ||
if [ "$SKIP_SBT_PLUGIN" = true ]; then | ||
echo "************** Skipping sbt plugin tests **************" | ||
else | ||
sbt -batch scripted | ||
if [ $? -ne 0 ]; then | ||
echo "sbt scripted failed" | ||
exit 1 | ||
fi | ||
fi | ||
|
||
# bash bin/build-slc-lib.sh | ||
# if [ $? -ne 0 ]; then | ||
# echo "build-slc-lib.sh failed" | ||
# exit 1 | ||
# fi | ||
|
||
TIME_AFTER=$(date +%s) | ||
DURATION=$((TIME_AFTER - TIME_BEFORE)) | ||
|
||
echo "" | ||
echo "********************************* CI PASSED! *********************************" | ||
|
||
echo "Total time: $DURATION seconds" |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think
ready_for_review
is useful. The default is[opened, synchronize, reopened]
, it seems to me you could just remove that line.