test.yml

name: Boogie CI

on:
  workflow_dispatch:
  push:
    tags:
      - 'v*'
  pull_request:
    branches:
      - master

env:
  SOLUTION: Source/Boogie.sln
  Z3URL: https://github.com/Z3Prover/z3/releases/download/z3-4.11.2/z3-4.11.2-x64-glibc-2.31.zip
  CVC5URL: https://github.com/cvc5/cvc5/releases/download/cvc5-0.0.7/cvc5-Linux

jobs:
  job0:
    name: Boogie CI
    runs-on: ubuntu-22.04
    strategy:
      matrix:
        configuration: [Debug, Release]
        lit_param: ["batch_mode=True", "batch_mode=False"]
    steps:
      - name: Setup dotnet
        uses: actions/setup-dotnet@v3
        with:
          dotnet-version: '6.0.x'
      - name: Checkout Boogie
        uses: actions/checkout@v3
        with:
          fetch-depth: 0
      - name: Determine version
        id: get_version
        uses: battila7/get-version-action@v2
      - name: Install tools, build Boogie, test Boogie
        run: |
          # Download a Z3 release
          wget ${Z3URL}
          unzip z3*.zip
          export PATH="$(find $PWD/z3* -name bin -type d):$PATH"
          # Download a CVC5 release
          mkdir -p bin
          (cd bin && wget ${CVC5URL} && mv cvc5-Linux cvc5 && chmod +x cvc5)
          export PATH="$PWD/bin:$PATH"
          # Install python tools
          sudo pip3 install setuptools
          sudo pip3 install lit OutputCheck pyyaml psutil
          # Change directory to Boogie root folder
          cd $GITHUB_WORKSPACE
          # Restore dotnet tools
          dotnet tool restore
          # Check that generated scanner and parser are consistent with attributed grammar
          dotnet tool run coco Source/Core/BoogiePL.atg -namespace Microsoft.Boogie -frames Source/Core/
          diff --strip-trailing-cr Source/Core/Parser.cs Source/Core/Parser.cs.old
          diff --strip-trailing-cr Source/Core/Scanner.cs Source/Core/Scanner.cs.old
          # Build Boogie
          dotnet build -warnaserror -c ${{ matrix.configuration }} ${SOLUTION}
          # Create packages
          dotnet pack --no-build -c ${{ matrix.configuration }} ${SOLUTION}
          # Run unit tests
          dotnet test --no-build -c ${{ matrix.configuration }} ${SOLUTION}
          # Run lit test suite
          lit --param ${{ matrix.lit_param }} -v --timeout=120 -D configuration=${{ matrix.configuration }} Test
      - name: Deploy to nuget
        # Note: if you change the build matrix, update the following
        # line to ensure it matches only one element of the matrix.
        if: matrix.configuration == 'Release' && matrix.lit_param == 'batch_mode=False' && startsWith(github.ref, 'refs/tags/v')
        run: dotnet nuget push "Source/**/bin/${{ matrix.configuration }}/Boogie*.nupkg" -k ${{ secrets.NUGET_API_KEY }} -s https://api.nuget.org/v3/index.json
      - name: Create draft GitHub release containing .nupkg file
        # Note: if you change the conditional above, update the one below to match
        if: matrix.configuration == 'Release' && matrix.lit_param == 'batch_mode=False' && startsWith(github.ref, 'refs/tags/v')
        uses: softprops/action-gh-release@v1
        with:
          name: Boogie ${{ steps.get_version.version }}
          tag_name: ${{ steps.get_version.version }}
          draft: false
          prerelease: false
          files: |
            Source/**/bin/${{ matrix.configuration }}/Boogie*.nupkg
          fail_on_unmatched_files: true