Skip to content

Updates submodules #2587

Updates submodules

Updates submodules #2587

Workflow file for this run

# This Source Code Form is subject to the terms of the Mozilla Public
# License, v. 2.0. If a copy of the MPL was not distributed with this
# file, You can obtain one at http://mozilla.org/MPL/2.0/.
#
# Copyright (c) 2011-2020 ETH Zurich.
name: Build, Test, and Publish
on:
push: # run this workflow on every push
pull_request: # run this workflow on every pull_request
merge_group: # run this workflow on every PR in the merge queue
workflow_dispatch: # allow to manually trigger this workflow
inputs:
type:
description: 'Specifies whether a stable or nightly release should be triggered. Note that "stable" can only be used on branch "release".'
required: true
default: 'nightly'
options:
- stable
- nightly
tag_name:
description: 'Tag name for stable release. Ignored if a nightly release will be created.'
required: true
default: '-'
release_name:
description: 'Release title for stable release. Ignored if a nightly release will be created.'
required: true
default: '-'
schedule:
- cron: '0 7 * * *' # run every day at 07:00 UTC
# some remarks about the high-level structure of this CI script:
# - build
# `build` builds and tests ViperServer using sbt.
# - test
# `test` takes both ViperServer JARs that include tests and executes them on Ubuntu, macOS, and Windows.
# - create-nightly-release
# takes the fat and skinny JARs produced by configuration `latest` during `build` job and creates a nightly release with
# them. This job automatically runs every night.
# - create-stable-release
# takes the fat and skinny JARs produced by configuration `release` during `build` job and creates a draft release with
# them. This only works on branch `release`.
env:
Z3_VERSION: "4.8.7"
jobs:
build:
# build is the base job on which all other jobs depend
# we enforce here that the nightly build job only runs in the main repo:
if: (github.event_name == 'schedule' && github.repository == 'viperproject/viperserver') || (github.event_name != 'schedule')
runs-on: ubuntu-latest
container: viperproject/viperserver:v4_z3_4.8.7
steps:
- name: Checkout ViperServer
uses: actions/checkout@v3
with:
path: viperserver
submodules: recursive
- name: Java Version
run: java --version
- name: Z3 Version
run: z3 -version
- name: Boogie Version
run: boogie /version
- name: Get Silver commits referenced by Silicon and Carbon
run: |
echo "SILICON_SILVER_REF=$(git -C viperserver/silicon/silver rev-parse HEAD)" >> $GITHUB_ENV
echo "CARBON_SILVER_REF=$(git -C viperserver/carbon/silver rev-parse HEAD)" >> $GITHUB_ENV
- name: Silicon and Carbon reference different Silver commits
if: env.SILICON_SILVER_REF != env.CARBON_SILVER_REF
run: |
echo "::error file=.github/workflows/scala.yml::Silicon and Carbon reference different Silver commits (${{ env.SILICON_SILVER_REF }} and ${{ env.CARBON_SILVER_REF }})"
# terminate this job:
exit 1
- name: Create version file
run: |
echo "ViperServer: commit $(git -C viperserver rev-parse HEAD)" >> versions.txt
echo "Silicon: commit $(git -C viperserver/silicon rev-parse HEAD)" >> versions.txt
echo "Carbon: commit $(git -C viperserver/carbon rev-parse HEAD)" >> versions.txt
echo "Silver: commit ${{ env.SILICON_SILVER_REF }}" >> versions.txt
# first line overwrites versions.txt in case it already exists, all other append to the file
- name: Upload version file
uses: actions/upload-artifact@v3
with:
name: versions.txt
path: versions.txt
- name: Set sbt cache variables
run: echo "SBT_OPTS=-Dsbt.global.base=sbt-cache/.sbtboot -Dsbt.boot.directory=sbt-cache/.boot -Dsbt.ivy.home=sbt-cache/.ivy" >> $GITHUB_ENV
# note that the cache path is relative to the directory in which sbt is invoked.
- name: Cache SBT
uses: actions/cache@v3
with:
path: |
viperserver/sbt-cache/.sbtboot
viperserver/sbt-cache/.boot
viperserver/sbt-cache/.ivy/cache
# <x>/project/target and <x>/target, where <x> is e.g. 'viperserver', are intentionally not
# included as several occurrences of NoSuchMethodError exceptions have been observed during CI runs. It seems
# like sbt is unable to correctly compute source files that require a recompilation. Therefore, we have
# disabled caching of compiled source files altogether
key: ${{ runner.os }}-sbt-no-precompiled-sources-${{ hashFiles('**/build.sbt') }}
- name: Test ViperServer
run: sbt test
working-directory: viperserver
- name: Upload log files
if: ${{ failure() }}
uses: actions/upload-artifact@v3
with:
name: TestLogs
path: viperserver/logs
- name: Assemble ViperServer skinny JARs
run: sbt stage
working-directory: viperserver
- name: Zip skinny JARs
run: zip -r ../../../../viperserver-skinny-jars.zip ./*
working-directory: viperserver/target/universal/stage/lib
- name: Upload ViperServer skinny JARs
uses: actions/upload-artifact@v3
with:
name: viperserver-skinny-jars
path: viperserver/viperserver-skinny-jars.zip
- name: Assemble ViperServer fat JAR
run: sbt "set test in assembly := {}" clean assembly
working-directory: viperserver
- name: Upload ViperServer fat JAR
uses: actions/upload-artifact@v3
with:
name: viperserver-fat-jar
path: viperserver/target/scala-2.13/viperserver.jar
- name: Assemble ViperServer test fat JAR
run: sbt clean test:assembly
working-directory: viperserver
- name: Upload ViperServer test fat JAR
uses: actions/upload-artifact@v3
with:
name: viperserver-test-fat-jar
path: viperserver/target/scala-2.13/viperserver-test.jar
test:
name: test - ${{ matrix.os }}
needs: build
strategy:
# tests should not be stopped when they fail on one of the OSes:
fail-fast: false
matrix:
os: [macos-latest, ubuntu-latest, windows-latest]
runs-on: ${{ matrix.os }}
env:
WIN_BOOGIE_URL: 'https://github.com/viperproject/boogie-builder/releases/latest/download/boogie-win.zip'
LINUX_BOOGIE_URL: 'https://github.com/viperproject/boogie-builder/releases/latest/download/boogie-linux.zip'
MAC_BOOGIE_URL: 'https://github.com/viperproject/boogie-builder/releases/latest/download/boogie-osx.zip'
steps:
# we need to checkout the repo to have access to the test files
- name: Checkout ViperServer
uses: actions/checkout@v3
with:
path: viperserver
# we need to checkout the silicon repo to have access to the logback configuration file
# as we do not use anything else except the logback config, we simply take the latest master branch (in all configurations)
- name: Checkout Silicon
uses: actions/checkout@v3
with:
repository: viperproject/silicon
path: silicon
- name: Download ViperServer test fat JAR
uses: actions/download-artifact@v3
with:
name: viperserver-test-fat-jar
path: viperserver
- name: Download Z3 (Ubuntu)
if: startsWith(matrix.os, 'ubuntu')
run: |
curl -L --silent --show-error --fail https://github.com/Z3Prover/z3/releases/download/z3-${{ env.Z3_VERSION }}/z3-${{ env.Z3_VERSION }}-x64-ubuntu-16.04.zip --output z3.zip
unzip z3.zip -d z3/
echo "$GITHUB_WORKSPACE/z3/z3-${{ env.Z3_VERSION }}-x64-ubuntu-16.04/bin" >> $GITHUB_PATH
echo "Z3_EXE=$GITHUB_WORKSPACE/z3/z3-${{ env.Z3_VERSION }}-x64-ubuntu-16.04/bin/z3" >> $GITHUB_ENV
shell: bash
- name: Download Z3 (macOS)
if: startsWith(matrix.os, 'macos')
run: |
curl -L --silent --show-error --fail https://github.com/Z3Prover/z3/releases/download/z3-${{ env.Z3_VERSION }}/z3-${{ env.Z3_VERSION }}-x64-osx-10.14.6.zip --output z3.zip
unzip z3.zip -d z3/
echo "$GITHUB_WORKSPACE/z3/z3-${{ env.Z3_VERSION }}-x64-osx-10.14.6/bin" >> $GITHUB_PATH
echo "Z3_EXE=$GITHUB_WORKSPACE/z3/z3-${{ env.Z3_VERSION }}-x64-osx-10.14.6/bin/z3" >> $GITHUB_ENV
shell: bash
- name: Download Z3 (Windows)
if: startsWith(matrix.os, 'windows')
run: |
curl -L --silent --show-error --fail https://github.com/Z3Prover/z3/releases/download/z3-${{ env.Z3_VERSION }}/z3-${{ env.Z3_VERSION }}-x64-win.zip --output z3.zip
unzip z3.zip -d z3/
echo "$GITHUB_WORKSPACE/z3/z3-${{ env.Z3_VERSION }}-x64-win/bin" >> $GITHUB_PATH
echo "Z3_EXE=$GITHUB_WORKSPACE/z3/z3-${{ env.Z3_VERSION }}-x64-win/bin/z3.exe" >> $GITHUB_ENV
shell: bash
- name: Download Boogie (Ubuntu)
if: startsWith(matrix.os, 'ubuntu')
run: |
curl -L --silent --show-error --fail ${{ env.LINUX_BOOGIE_URL }} --output boogie-linux.zip
unzip boogie-linux.zip -d boogie-linux
echo "$GITHUB_WORKSPACE/boogie-linux/binaries-linux" >> $GITHUB_PATH
echo "BOOGIE_EXE=$GITHUB_WORKSPACE/boogie-linux/binaries-linux/Boogie" >> $GITHUB_ENV
shell: bash
- name: Download Boogie (macOS)
if: startsWith(matrix.os, 'macos')
run: |
curl -L --silent --show-error --fail ${{ env.MAC_BOOGIE_URL }} --output boogie-mac.zip
unzip boogie-mac.zip -d boogie-mac
echo "$GITHUB_WORKSPACE/boogie-mac/binaries-osx" >> $GITHUB_PATH
echo "BOOGIE_EXE=$GITHUB_WORKSPACE/boogie-mac/binaries-osx/Boogie" >> $GITHUB_ENV
shell: bash
- name: Download Boogie (Windows)
if: startsWith(matrix.os, 'windows')
run: |
curl -L --silent --show-error --fail ${{ env.WIN_BOOGIE_URL }} --output boogie-win.zip
unzip boogie-win.zip -d boogie-win
echo "$GITHUB_WORKSPACE/boogie-win/binaries-win" >> $GITHUB_PATH
echo "BOOGIE_EXE=$GITHUB_WORKSPACE/boogie-win/binaries-win/Boogie.exe" >> $GITHUB_ENV
shell: bash
- name: Setup Java JDK
uses: actions/setup-java@v3
with:
java-version: '11'
distribution: 'temurin'
- name: Java Version
run: java --version
- name: Z3 Version
run: z3 -version
- name: Boogie Version
run: Boogie /version
# unfortunately, the JAR seems to be broken and discovering test suites (e.g. using `-w viper.server`) fails.
# thus, the test suites have to be explicitly mentioned
- name: Test ViperServer
run: java -Xss128m -Dlogback.configurationFile=$GITHUB_WORKSPACE/silicon/src/main/resources/logback.xml -cp viperserver-test.jar org.scalatest.tools.Runner -R viperserver-test.jar -o -s viper.server.core.AstGenerationTests -s viper.server.core.CoreServerSpec -s viper.server.core.ViperServerHttpSpec
shell: bash
working-directory: viperserver
- name: Upload log files
if: ${{ failure() }}
uses: actions/upload-artifact@v3
with:
name: TestLogs-${{ runner.os }}
path: viperserver/logs
create-nightly-release:
needs: test
# this job creates a new nightly pre-release, set viperserver.jar as artifacts, and deletes old releases
if: github.ref != 'refs/heads/release' && ((github.event_name == 'workflow_dispatch' && github.event.inputs.type == 'nightly') || github.event_name == 'schedule')
runs-on: ubuntu-latest
steps:
- name: Install prerequisites
run: sudo apt-get install curl
- name: Download ViperServer skinny JARs
uses: actions/download-artifact@v3
with:
name: viperserver-skinny-jars
path: deploy
- name: Download ViperServer fat JAR
uses: actions/download-artifact@v3
with:
name: viperserver-fat-jar
path: deploy
- name: Download version file
uses: actions/download-artifact@v3
with:
name: versions.txt
- name: Check whether commits have changed
# the following command queries all releases (as JSON) and passes it to `jq` that performs the following
# filtering:
# 1. only consider prereleases (instead of stable releases)
# 2. extract body
# 3. check if $VERSIONS is contained in the release's body. $VERSIONS stores the file content of versions.txt
# 4. return 'true" if at least one release satisfies the criterion
# MATCHING_RELEASE is 'true' if a matching release has been found and thus no new release should be created
run: |
MATCHING_RELEASE=$( \
curl --fail --silent \
--header 'Accept: application/vnd.github.v3+json' \
--header 'Authorization: token ${{ secrets.GITHUB_TOKEN }}' \
--url 'https://api.github.com/repos/viperproject/viperserver/releases' \
| \
jq --rawfile VERSIONS versions.txt \
'map(select(.prerelease == true) | .body | contains($VERSIONS)) | any')
echo "MATCHING_RELEASE=$MATCHING_RELEASE" >> $GITHUB_ENV
- name: Create release tag
if: env.MATCHING_RELEASE != 'true'
shell: bash
run: echo "TAG_NAME=$(date +v-%Y-%m-%d-%H%M)" >> $GITHUB_ENV
- name: Create nightly release
if: env.MATCHING_RELEASE != 'true'
id: create_release
uses: actions/create-release@v1
env:
# This token is provided by Actions, you do not need to create your own token
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
with:
tag_name: ${{ env.TAG_NAME }}
release_name: Nightly Release ${{ env.TAG_NAME }}
body_path: versions.txt
draft: false
prerelease: true
- name: Upload ViperServer skinny jars
if: env.MATCHING_RELEASE != 'true'
uses: actions/[email protected]
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
with:
upload_url: ${{ steps.create_release.outputs.upload_url }}
asset_path: deploy/viperserver-skinny-jars.zip
asset_name: viperserver-skinny-jars.zip
asset_content_type: application/zip
- name: Upload ViperServer fat jar artifact
if: env.MATCHING_RELEASE != 'true'
uses: actions/[email protected]
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
with:
upload_url: ${{ steps.create_release.outputs.upload_url }}
asset_path: deploy/viperserver.jar
asset_name: viperserver.jar
asset_content_type: application/octet-stream
create-stable-release:
needs: test
# this job creates a stable draft-release and set viperserver.jar as artifacts
if: github.ref == 'refs/heads/release' && github.event_name == 'workflow_dispatch' && github.event.inputs.type == 'stable'
runs-on: ubuntu-latest
steps:
- name: Download ViperServer skinny JARs
uses: actions/download-artifact@v3
with:
name: viperserver-skinny-jars
path: deploy
- name: Download ViperServer fat JAR
uses: actions/download-artifact@v3
with:
name: viperserver-fat-jar
path: deploy
- name: Download version file
uses: actions/download-artifact@v3
with:
name: versions.txt
- name: Create stable draft-release
id: create_release
uses: actions/create-release@v1
env:
# This token is provided by Actions, you do not need to create your own token
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
with:
tag_name: ${{ github.event.inputs.tag_name }}
release_name: ${{ github.event.inputs.release_name }}
body_path: versions.txt
draft: true
prerelease: false
- name: Upload ViperServer skinny jars
uses: actions/[email protected]
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
with:
upload_url: ${{ steps.create_release.outputs.upload_url }}
asset_path: deploy/viperserver-skinny-jars.zip
asset_name: viperserver-skinny-jars.zip
asset_content_type: application/zip
- name: Upload ViperServer fat jar
uses: actions/[email protected]
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
with:
upload_url: ${{ steps.create_release.outputs.upload_url }}
asset_path: deploy/viperserver.jar
asset_name: viperserver.jar
asset_content_type: application/octet-stream