Support multi-binding var expressions in Lean backend
#1906
Workflow file for this run
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
| 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 --blame-hang-timeout 120s --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 |