test #3695
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: test | |
| 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. Has to be "stable" or "nightly".' | |
| required: true | |
| default: 'stable' | |
| tag_name: | |
| description: 'Tag name for stable release. Ignored if a nightly release will be created.' | |
| required: true | |
| release_name: | |
| description: 'Release title for stable release. Ignored if a nightly release will be created.' | |
| required: true | |
| schedule: | |
| - cron: '0 7 * * *' # run every day at 07:00 UTC | |
| jobs: | |
| build-and-test-server: | |
| # build-and-test-server 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/gobra-ide') || (github.event_name != 'schedule') | |
| runs-on: ubuntu-latest | |
| container: gobraverifier/gobra-base:v5_z3_4.8.7 | |
| steps: | |
| - name: Checkout Gobra-IDE | |
| uses: actions/checkout@v4 | |
| with: | |
| path: gobra-ide | |
| submodules: recursive | |
| - name: Java Version | |
| run: java --version | |
| - name: Z3 Version | |
| run: z3 -version | |
| - name: Get Silver commits referenced by Silicon and Carbon | |
| run: | | |
| echo "SILICON_SILVER_REF=$(git -C gobra-ide/server/gobra/viperserver/silicon/silver rev-parse HEAD)" >> $GITHUB_ENV | |
| echo "CARBON_SILVER_REF=$(git -C gobra-ide/server/gobra/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 "Gobra-IDE: commit $(git -C gobra-ide rev-parse HEAD)" > versions.txt | |
| echo "Gobra: commit $(git -C gobra-ide/server/gobra rev-parse HEAD)" >> versions.txt | |
| echo "ViperServer: commit $(git -C gobra-ide/server/gobra/viperserver rev-parse HEAD)" >> versions.txt | |
| echo "Silicon: commit $(git -C gobra-ide/server/gobra/viperserver/silicon rev-parse HEAD)" >> versions.txt | |
| echo "Carbon: commit $(git -C gobra-ide/server/gobra/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@v4 | |
| 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. | |
| # hence, invoking sbt in server folder means that sbt cache will be in gobra-ide/server/sbt-cache | |
| - name: Cache SBT | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| gobra-ide/server/sbt-cache/.sbtboot | |
| gobra-ide/server/sbt-cache/.boot | |
| gobra-ide/server/sbt-cache/.ivy/cache | |
| # <x>/project/target and <x>/target, where <x> is e.g. 'gobra-ide/server' or 'gobra', 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: Assemble Gobra server | |
| run: sbt "set test in assembly := {}" clean assembly | |
| working-directory: gobra-ide/server | |
| - name: Upload Gobra server artifact | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: server.jar | |
| path: gobra-ide/server/target/scala-2.13/server.jar | |
| - name: Test Gobra server | |
| run: sbt test | |
| working-directory: gobra-ide/server | |
| create-gobra-tools: | |
| name: create-gobra-tools - ${{ matrix.gobra-tools-platform }} | |
| needs: build-and-test-server | |
| strategy: | |
| # tests should not be stopped when they fail on one of the OSes: | |
| fail-fast: false | |
| matrix: | |
| viper-tools-platform: ["ViperToolsWin", "ViperToolsLinux", "ViperToolsMac"] | |
| include: | |
| - viper-tools-platform: "ViperToolsWin" | |
| gobra-tools-platform: "GobraToolsWin" | |
| - viper-tools-platform: "ViperToolsLinux" | |
| gobra-tools-platform: "GobraToolsLinux" | |
| - viper-tools-platform: "ViperToolsMac" | |
| gobra-tools-platform: "GobraToolsMac" | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Install prerequisites | |
| run: sudo apt-get install zip unzip | |
| - name: Download Gobra server artifact | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: server.jar | |
| - name: Download Viper Tools | |
| run: wget --no-verbose https://viper.ethz.ch/downloads/${{ matrix.viper-tools-platform }}.zip --output-document=${{ matrix.viper-tools-platform }}.zip | |
| - name: Unzip Viper Tools | |
| run: unzip ${{ matrix.viper-tools-platform }}.zip -d ${{ matrix.viper-tools-platform }} | |
| - name: Create a Gobra Tools folder | |
| run: mkdir -p ${{ matrix.gobra-tools-platform }} | |
| - name: Copy boogie from ViperTools to Gobra Tools | |
| run: cp -R ${{ matrix.viper-tools-platform }}/boogie ${{ matrix.gobra-tools-platform }}/boogie/ | |
| - name: Copy z3 from ViperTools to Gobra Tools | |
| run: cp -R ${{ matrix.viper-tools-platform }}/z3 ${{ matrix.gobra-tools-platform }}/z3/ | |
| - name: Copy Gobra server artifact to Gobra Tools | |
| run: mkdir -p ${{ matrix.gobra-tools-platform }}/server && cp server.jar ${{ matrix.gobra-tools-platform }}/server/server.jar | |
| - name: Create folder to store Gobra Tools platform zip files | |
| run: mkdir deploy | |
| # note that we change into the tool folder to zip it. This avoids including the parent folder in the zip | |
| - name: Zip Gobra Tools | |
| run: zip -r ../deploy/${{ matrix.gobra-tools-platform }}.zip ./* | |
| working-directory: ${{ matrix.gobra-tools-platform }} | |
| - name: Upload Gobra Tools | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: ${{ matrix.gobra-tools-platform }}.zip | |
| path: deploy/${{ matrix.gobra-tools-platform }}.zip | |
| prepare-matrix: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout Gobra-IDE | |
| uses: actions/checkout@v4 | |
| with: | |
| path: gobra-ide | |
| # we do not need any submodules here as we only test the client | |
| - id: set-matrix | |
| run: | | |
| # find files with ending '.json' in client/src/test/data/settings and store them as a JSON array | |
| CONFIG_FILES=$(find src/test/data/settings -type f -name "*.json" | jq -R . | jq -s --compact-output) | |
| echo "matrix={\"config-file\": $CONFIG_FILES}" >> $GITHUB_OUTPUT | |
| working-directory: gobra-ide/client | |
| outputs: | |
| matrix: ${{ steps.set-matrix.outputs.matrix }} | |
| build-and-test-client: | |
| name: build-and-test-client - ${{ matrix.os }}, ${{ matrix.config-file }} | |
| needs: [prepare-matrix, create-gobra-tools] | |
| 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] | |
| config-file: ${{ fromJson(needs.prepare-matrix.outputs.matrix).config-file }} | |
| include: | |
| - os: macos-latest | |
| gobra-tools-zip-file: "GobraToolsMac.zip" | |
| - os: ubuntu-latest | |
| gobra-tools-zip-file: "GobraToolsLinux.zip" | |
| - os: windows-latest | |
| gobra-tools-zip-file: "GobraToolsWin.zip" | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - name: Checkout Gobra-IDE | |
| uses: actions/checkout@v4 | |
| with: | |
| path: gobra-ide | |
| # we do not need any submodules here as we only test the client | |
| - name: Download Gobra tools | |
| uses: actions/download-artifact@v4 | |
| id: tools-download | |
| with: | |
| name: ${{matrix.gobra-tools-zip-file}} | |
| path: local | |
| # note that download-path is the parent folder, i.e. `local` and not the download zip file | |
| - name: Unzip Gobra tools | |
| run: 7z x ${{matrix.gobra-tools-zip-file}} -oGobraTools | |
| working-directory: local | |
| - name: Install Node.js | |
| uses: actions/setup-node@v4 | |
| with: | |
| node-version: '18' | |
| - name: Setup Java JDK | |
| uses: actions/setup-java@v4 | |
| with: | |
| java-version: '11' | |
| distribution: 'temurin' | |
| - run: java --version | |
| - name: Cache npm | |
| uses: actions/cache@v4 | |
| with: | |
| path: gobra-ide/client/.npm | |
| key: ${{ runner.os }}-node-${{ hashFiles('**/package-lock.json') }} | |
| restore-keys: | | |
| ${{ runner.os }}-node- | |
| # npm ci fails to clone GitHub repos referenced in package.json with recent node versions | |
| # the following work around has been proposed here: https://github.com/actions/setup-node/issues/214#issuecomment-810829250 | |
| - name: Reconfigure git to use HTTPS authentication | |
| run: > | |
| git config --global url."https://github.com/".insteadOf | |
| ssh://git@github.com/ | |
| - run: npm ci --cache .npm --prefer-offline | |
| working-directory: gobra-ide/client | |
| - name: Run tests (headless - non-ubuntu) | |
| if: "!startsWith(matrix.os, 'ubuntu')" | |
| run: npm test --full-trace -- --gobraTools "${{steps.tools-download.outputs.download-path}}/GobraTools" --configFile "${{matrix.config-file}}" | |
| working-directory: gobra-ide/client | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - name: Run tests (headless - ubuntu only) | |
| if: startsWith(matrix.os, 'ubuntu') | |
| run: xvfb-run -a npm test --full-trace -- --gobraTools "${{steps.tools-download.outputs.download-path}}/GobraTools" --configFile "${{matrix.config-file}}" | |
| working-directory: gobra-ide/client | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - name: Collect coverage | |
| run: npx nyc report --reporter=lcov | |
| working-directory: gobra-ide/client | |
| # - name: Upload coverage to Codecov | |
| # uses: codecov/codecov-action@v1 | |
| # with: | |
| # token: ${{ secrets.CODECOV_TOKEN }} | |
| # file: gobra-ide/client/coverage/lcov.info | |
| # make sure that the following actions (in particular the artifact upload) are only executed for a single matrix configuration | |
| - name: Clean 'dist' folder (only once) | |
| if: startsWith(matrix.os, 'ubuntu') && endsWith(matrix.config-file, 'local.json') | |
| run: npm run clean | |
| working-directory: gobra-ide/client | |
| # `npm run package` resp. `@vscode/vsce` complains that it cannot find | |
| # locate-java-home and vs-verification-toolbox dependencies (the two non-npm dependencies). | |
| # this seems related to https://github.com/npm/cli/issues/791 | |
| # the current workaround is to `run npm install` first: | |
| - name: Run 'npm install' as a workaround to later being able to package Gobra-IDE (only once) | |
| if: startsWith(matrix.os, 'ubuntu') && endsWith(matrix.config-file, 'local.json') | |
| run: npm install | |
| working-directory: gobra-ide/client | |
| - name: List all files that will be packaged (only once) | |
| if: startsWith(matrix.os, 'ubuntu') && endsWith(matrix.config-file, 'local.json') | |
| run: npx @vscode/vsce ls | |
| working-directory: gobra-ide/client | |
| - name: Package Gobra-IDE extension (only once) | |
| if: startsWith(matrix.os, 'ubuntu') && endsWith(matrix.config-file, 'local.json') | |
| # note that baseContentUrl has to be manually provided as @vscode/vsce does not know that it is run in the client subfolder: | |
| run: npm run package -- --baseContentUrl https://github.com/viperproject/gobra-ide/raw/master/client --out gobra-ide.vsix | |
| working-directory: gobra-ide/client | |
| - name: Upload packaged Gobra-IDE (only once) | |
| if: startsWith(matrix.os, 'ubuntu') && endsWith(matrix.config-file, 'local.json') | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: gobra-ide.vsix | |
| path: gobra-ide/client/gobra-ide.vsix | |
| create-nightly-release: | |
| # this job creates a new nightly pre-release, set Gobra tools as artifacts, and deletes old releases | |
| if: (github.event_name == 'workflow_dispatch' && github.event.inputs.type == 'nightly') || github.event_name == 'schedule' | |
| needs: build-and-test-client | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Download Gobra Tools for Windows | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: GobraToolsWin.zip | |
| path: deploy | |
| - name: Download Gobra Tools for Linux | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: GobraToolsLinux.zip | |
| path: deploy | |
| - name: Download Gobra Tools for macOS | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: GobraToolsMac.zip | |
| path: deploy | |
| - name: Download packaged Gobra IDE | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: gobra-ide.vsix | |
| path: gobra-ide/client | |
| - name: Download version file | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: versions.txt | |
| - name: Create release tag | |
| shell: bash | |
| run: echo "TAG_NAME=$(date +v-%Y-%m-%d-%H%M)" >> $GITHUB_ENV | |
| - name: Create nightly release | |
| 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 | |
| - name: Upload Gobra tools for Windows | |
| uses: actions/upload-release-asset@v1.0.2 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| upload_url: ${{ steps.create_release.outputs.upload_url }} | |
| asset_path: deploy/GobraToolsWin.zip | |
| asset_name: GobraToolsWin.zip | |
| asset_content_type: application/zip | |
| - name: Upload Gobra tools for Ubuntu | |
| uses: actions/upload-release-asset@v1.0.2 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| upload_url: ${{ steps.create_release.outputs.upload_url }} | |
| asset_path: deploy/GobraToolsLinux.zip | |
| asset_name: GobraToolsLinux.zip | |
| asset_content_type: application/zip | |
| - name: Upload Gobra tools for macOS | |
| uses: actions/upload-release-asset@v1.0.2 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| upload_url: ${{ steps.create_release.outputs.upload_url }} | |
| asset_path: deploy/GobraToolsMac.zip | |
| asset_name: GobraToolsMac.zip | |
| asset_content_type: application/zip | |
| - name: Upload packaged Gobra IDE | |
| uses: actions/upload-release-asset@v1.0.2 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| upload_url: ${{ steps.create_release.outputs.upload_url }} | |
| asset_path: gobra-ide/client/gobra-ide.vsix | |
| asset_name: gobra-ide.vsix | |
| asset_content_type: application/octet-stream | |
| create-stable-release: | |
| # this job creates a stable draft-release and set Gobra tools as artifacts | |
| if: github.event_name == 'workflow_dispatch' && github.event.inputs.type == 'stable' | |
| needs: build-and-test-client | |
| runs-on: ubuntu-latest | |
| steps: | |
| # we have to checkout the repo to read client/package.json later on: | |
| - name: Checkout Gobra-IDE | |
| uses: actions/checkout@v4 | |
| with: | |
| path: gobra-ide | |
| # we do not need any submodules here as we only test the client | |
| - name: Download Gobra Tools for Windows | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: GobraToolsWin.zip | |
| path: deploy | |
| - name: Download Gobra Tools for Linux | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: GobraToolsLinux.zip | |
| path: deploy | |
| - name: Download Gobra Tools for macOS | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: GobraToolsMac.zip | |
| path: deploy | |
| - name: Download packaged Gobra IDE | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: gobra-ide.vsix | |
| path: gobra-ide/client | |
| - name: Download version file | |
| uses: actions/download-artifact@v4 | |
| 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 Gobra tools for Windows | |
| uses: actions/upload-release-asset@v1.0.2 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| upload_url: ${{ steps.create_release.outputs.upload_url }} | |
| asset_path: deploy/GobraToolsWin.zip | |
| asset_name: GobraToolsWin.zip | |
| asset_content_type: application/zip | |
| - name: Upload Gobra tools for Ubuntu | |
| uses: actions/upload-release-asset@v1.0.2 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| upload_url: ${{ steps.create_release.outputs.upload_url }} | |
| asset_path: deploy/GobraToolsLinux.zip | |
| asset_name: GobraToolsLinux.zip | |
| asset_content_type: application/zip | |
| - name: Upload Gobra tools for macOS | |
| uses: actions/upload-release-asset@v1.0.2 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| upload_url: ${{ steps.create_release.outputs.upload_url }} | |
| asset_path: deploy/GobraToolsMac.zip | |
| asset_name: GobraToolsMac.zip | |
| asset_content_type: application/zip | |
| - name: Upload packaged Gobra IDE | |
| uses: actions/upload-release-asset@v1.0.2 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| upload_url: ${{ steps.create_release.outputs.upload_url }} | |
| asset_path: gobra-ide/client/gobra-ide.vsix | |
| asset_name: gobra-ide.vsix | |
| asset_content_type: application/octet-stream | |
| # compare version in client/package.json with last published version on | |
| # VS Marketplace and deploy this version if newer. | |
| # credits go to @fpoli! | |
| - name: Obtain version information | |
| run: | | |
| VSCE_OUTPUT="$( | |
| npx @vscode/vsce show viper-admin.gobra-ide --json | |
| )" | |
| if [[ $(echo $VSCE_OUTPUT | grep --fixed-strings --line-regexp undefined) ]]; then | |
| LAST_PUBLISHED_VERSION="0" | |
| else | |
| LAST_PUBLISHED_VERSION="$( | |
| echo $VSCE_OUTPUT | jq '.versions[0].version' --raw-output | |
| )" | |
| fi | |
| CURRENT_VERSION="$( | |
| cat gobra-ide/client/package.json | jq '.version' --raw-output | |
| )" | |
| echo "LAST_PUBLISHED_VERSION=$LAST_PUBLISHED_VERSION" >> $GITHUB_ENV | |
| echo "CURRENT_VERSION=$CURRENT_VERSION" >> $GITHUB_ENV | |
| - name: Publish the extension to Visual Studio Marketplace | |
| uses: HaaLeo/publish-vscode-extension@v1 | |
| if: env.CURRENT_VERSION != env.LAST_PUBLISHED_VERSION | |
| with: | |
| pat: ${{ secrets.VSCE_TOKEN }} | |
| registryUrl: https://marketplace.visualstudio.com | |
| extensionFile: gobra-ide/client/gobra-ide.vsix | |
| packagePath: '' | |
| - name: Publish the extension to Open VSX Registry | |
| uses: HaaLeo/publish-vscode-extension@v1 | |
| if: env.CURRENT_VERSION != env.LAST_PUBLISHED_VERSION | |
| with: | |
| pat: ${{ secrets.OPEN_VSX_TOKEN }} | |
| registryUrl: https://open-vsx.org | |
| extensionFile: gobra-ide/client/gobra-ide.vsix | |
| packagePath: '' |