test.yml

# 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@v3
        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@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.
        # hence, invoking sbt in server folder means that sbt cache will be in gobra-ide/server/sbt-cache

      - name: Cache SBT
        uses: actions/cache@v3
        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@v3
        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:
    needs: build-and-test-server
    runs-on: ubuntu-latest
    steps:
      - name: Install prerequisites
        run: sudo apt-get install zip unzip

      - name: Download Gobra server artifact
        uses: actions/download-artifact@v3
        with:
          name: server.jar

      - name: Download Viper Tools for Windows
        run: wget --no-verbose https://viper.ethz.ch/downloads/ViperToolsWin.zip --output-document=ViperToolsWin.zip
      - name: Unzip Viper Tools for Windows
        run: unzip ViperToolsWin.zip -d ViperToolsWin
      - name: Download Viper Tools for Linux
        run: wget --no-verbose https://viper.ethz.ch/downloads/ViperToolsLinux.zip --output-document=ViperToolsLinux.zip
      - name: Unzip Viper Tools for Linux
        run: unzip ViperToolsLinux.zip -d ViperToolsLinux
      - name: Download Viper Tools for macOS
        run: wget --no-verbose https://viper.ethz.ch/downloads/ViperToolsMac.zip --output-document=ViperToolsMac.zip
      - name: Unzip Viper Tools for macOS
        run: unzip ViperToolsMac.zip -d ViperToolsMac

      - name: Create a Gobra Tools folder per platform
        run: |
          mkdir -p GobraToolsWin
          mkdir -p GobraToolsLinux
          mkdir -p GobraToolsMac

      - name: Copy boogie from ViperTools to Gobra Tools
        run: |
          cp -R ViperToolsWin/boogie GobraToolsWin/boogie/
          cp -R ViperToolsLinux/boogie GobraToolsLinux/boogie/
          cp -R ViperToolsMac/boogie GobraToolsMac/boogie/

      - name: Copy z3 from ViperTools to Gobra Tools
        run: |
          cp -R ViperToolsWin/z3 GobraToolsWin/z3/
          cp -R ViperToolsLinux/z3 GobraToolsLinux/z3/
          cp -R ViperToolsMac/z3 GobraToolsMac/z3/

      - name: Copy Gobra server artifact to Gobra Tools
        run: |
          mkdir -p GobraToolsWin/server && cp server.jar GobraToolsWin/server/server.jar
          mkdir -p GobraToolsLinux/server && cp server.jar GobraToolsLinux/server/server.jar
          mkdir -p GobraToolsMac/server && cp server.jar GobraToolsMac/server/server.jar

      - name: Create folder to store all 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 for Windows
        run: zip -r ../deploy/GobraToolsWin.zip ./*
        working-directory: GobraToolsWin
      - name: Zip Gobra Tools for Linux
        run: zip -r ../deploy/GobraToolsLinux.zip ./*
        working-directory: GobraToolsLinux
      - name: Zip Gobra Tools for macOS
        run: zip -r ../deploy/GobraToolsMac.zip ./*
        working-directory: GobraToolsMac

      - name: Upload Gobra Tools for Windows
        uses: actions/upload-artifact@v3
        with:
          name: GobraToolsWin.zip
          path: deploy/GobraToolsWin.zip
      - name: Upload Gobra Tools for Linux
        uses: actions/upload-artifact@v3
        with:
          name: GobraToolsLinux.zip
          path: deploy/GobraToolsLinux.zip
      - name: Upload Gobra Tools for macOS
        uses: actions/upload-artifact@v3
        with:
          name: GobraToolsMac.zip
          path: deploy/GobraToolsMac.zip


  build-and-test-client:
    name: build-and-test-client - ${{ matrix.os }}
    needs: 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]
        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@v3
        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@v3
        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@v3
        with:
          node-version: '18'

      - name: Setup Java JDK
        uses: actions/setup-java@v3
        with:
          java-version: '11'
          distribution: 'temurin'
      - run: java --version

      - name: Cache npm
        uses: actions/cache@v3
        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"
        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"
        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

      - name: Clean 'dist' folder (ubuntu only)
        if: startsWith(matrix.os, 'ubuntu')
        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 (ubuntu only)
        if: startsWith(matrix.os, 'ubuntu')
        run: npm install
        working-directory: gobra-ide/client

      - name: List all files that will be packaged (ubuntu only)
        if: startsWith(matrix.os, 'ubuntu')
        run: npx @vscode/vsce ls
        working-directory: gobra-ide/client

      - name: Package Gobra-IDE extension (ubuntu only)
        if: startsWith(matrix.os, 'ubuntu')
        # 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 (ubuntu-only)
        if: startsWith(matrix.os, 'ubuntu')
        uses: actions/upload-artifact@v3
        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@v3
        with:
          name: GobraToolsWin.zip
          path: deploy
      - name: Download Gobra Tools for Linux
        uses: actions/download-artifact@v3
        with:
          name: GobraToolsLinux.zip
          path: deploy
      - name: Download Gobra Tools for macOS
        uses: actions/download-artifact@v3
        with:
          name: GobraToolsMac.zip
          path: deploy

      - name: Download packaged Gobra IDE
        uses: actions/download-artifact@v3
        with:
          name: gobra-ide.vsix
          path: gobra-ide/client

      - name: Download version file
        uses: actions/download-artifact@v3
        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@v3
        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@v3
        with:
          name: GobraToolsWin.zip
          path: deploy
      - name: Download Gobra Tools for Linux
        uses: actions/download-artifact@v3
        with:
          name: GobraToolsLinux.zip
          path: deploy
      - name: Download Gobra Tools for macOS
        uses: actions/download-artifact@v3
        with:
          name: GobraToolsMac.zip
          path: deploy

      - name: Download packaged Gobra IDE
        uses: actions/download-artifact@v3
        with:
          name: gobra-ide.vsix
          path: gobra-ide/client

      - 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 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@v0
        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@v0
        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: ''