Skip to content

Fix hanging when solver exits with a non-zero exit code #1409

Fix hanging when solver exits with a non-zero exit code

Fix hanging when solver exits with a non-zero exit code #1409

Workflow file for this run

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