Merge #163 #1715
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # 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 | |
| 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: viperproject/create-nightly-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 | |
| keep_num: 1 # keep the previous nightly release such that there are always two | |
| keep_tags: 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 | |
| - name: Trigger Viper-IDE CI | |
| if: env.MATCHING_RELEASE != 'true' | |
| run: | | |
| curl --fail --request POST \ | |
| --user 'viper-admin:${{ secrets.VIPER_ADMIN_TOKEN }}' \ | |
| --header 'Accept: application/vnd.github.v3+json' \ | |
| --url 'https://api.github.com/repos/viperproject/viper-ide/actions/workflows/test.yml/dispatches' \ | |
| --data "{ \ | |
| \"ref\":\"master\", \ | |
| \"inputs\":{ \ | |
| \"type\":\"nightly\", \ | |
| \"viperserver_tag_name\":\"${{ env.TAG_NAME }}\", \ | |
| \"boogie_tag_name\":\"latest\", \ | |
| \"z3_version\":\"${{ env.Z3_VERSION }}\", \ | |
| \"tag_name\":\"${{ env.TAG_NAME }}\", \ | |
| \"release_name\":\"Nightly Release ${{ env.TAG_NAME }}\" \ | |
| } \ | |
| }" | |
| 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 |