Fix bug, allow datatypes with type aliases #1619
Workflow file for this run
This file contains hidden or 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: Build | |
| on: | |
| pull_request: | |
| merge_group: | |
| env: | |
| SOLUTION: Tools/BoogieToStrata/BoogieToStrata.sln | |
| jobs: | |
| get-branch-name: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Get branch name | |
| shell: bash | |
| # The workflow is triggered by pull_request so we use `GITHUB_BASE_REF` | |
| run: echo "branch_name=${GITHUB_BASE_REF}" >> $GITHUB_OUTPUT | |
| id: get_branch_name | |
| outputs: | |
| branch_name: ${{ steps.get_branch_name.outputs.branch_name }} | |
| build_and_test_lean: | |
| name: Build and test Lean | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| toolchain: | |
| - stable | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Install cvc5 | |
| shell: bash | |
| run: | | |
| ARCH=$(uname -m) | |
| if [ "$ARCH" = "x86_64" ]; then | |
| ARCH_NAME="x86_64" | |
| elif [ "$ARCH" = "aarch64" ] || [ "$ARCH" = "arm64" ]; then | |
| ARCH_NAME="arm64" | |
| else | |
| echo "Unsupported architecture: $ARCH" | |
| exit 1 | |
| fi | |
| wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.1/cvc5-Linux-${ARCH_NAME}-static.zip | |
| unzip cvc5-Linux-${ARCH_NAME}-static.zip | |
| chmod +x cvc5-Linux-${ARCH_NAME}-static/bin/cvc5 | |
| echo "$GITHUB_WORKSPACE/cvc5-Linux-${ARCH_NAME}-static/bin/" >> $GITHUB_PATH | |
| - name: Install z3 | |
| shell: bash | |
| run: | | |
| ARCH=$(uname -m) | |
| if [ "$ARCH" = "x86_64" ]; then | |
| ARCH_NAME="x86_64" | |
| wget https://github.com/Z3Prover/z3/releases/download/z3-4.15.2/z3-4.15.2-x64-glibc-2.39.zip | |
| ARCHIVE_NAME="z3-4.15.2-x64-glibc-2.39" | |
| elif [ "$ARCH" = "aarch64" ] || [ "$ARCH" = "arm64" ]; then | |
| ARCH_NAME="arm64" | |
| wget https://github.com/Z3Prover/z3/releases/download/z3-4.15.2/z3-4.15.2-arm64-glibc-2.34.zip | |
| ARCHIVE_NAME="z3-4.15.2-arm64-win" | |
| else | |
| echo "Unsupported architecture: $ARCH" | |
| exit 1 | |
| fi | |
| unzip "${ARCHIVE_NAME}.zip" | |
| chmod +x "${ARCHIVE_NAME}/bin/z3" | |
| echo "$GITHUB_WORKSPACE/${ARCHIVE_NAME}/bin/" >> $GITHUB_PATH | |
| - name: Install .NET | |
| uses: actions/setup-dotnet@v4 | |
| with: | |
| dotnet-version: '8.0.x' | |
| - name: Build and test Strata | |
| uses: leanprover/lean-action@v1 | |
| - name: Build and run StrataVerify | |
| run: lake exe StrataVerify Examples/SimpleProc.core.st | |
| - name: Build BoogieToStrata | |
| run: dotnet build -warnaserror ${SOLUTION} | |
| - name: Test BoogieToStrata | |
| run: dotnet test ${SOLUTION} | |
| - name: Test Strata Command line | |
| run: .github/scripts/testStrataCommand.sh | |
| - name: Validate examples against expected output | |
| working-directory: Examples | |
| shell: bash | |
| run: ./run_examples.sh | |
| - uses: actions/setup-python@v5 | |
| with: | |
| python-version: '3.14' | |
| - name: Build using pip | |
| run: pip install . | |
| working-directory: Tools/Python | |
| - name: Run pyAnalyze tests | |
| working-directory: StrataTest/Languages/Python | |
| shell: bash | |
| run: ./run_py_analyze.sh | |
| lint_checks: | |
| name: Run lint checks | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: read | |
| strategy: | |
| matrix: | |
| toolchain: | |
| - stable | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Check copyright headers | |
| run: python3 .github/scripts/check_copyright_headers.py . | |
| shell: bash | |
| - name: Check for trailing whitespace | |
| run: .github/scripts/lintWhitespace.sh | |
| - name: Check for import Lean | |
| run: .github/scripts/checkLeanImport.sh | |
| - name: Check Lean version consistncy | |
| run: .github/scripts/check_lean_consistency.sh | |
| build_doc: | |
| name: Build documentation | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: read | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Build documentation package | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| build-args: '--wfail' | |
| lake-package-directory: 'docs/verso' | |
| - name: Build documentation | |
| run: ./generate.sh | |
| working-directory: docs/verso | |
| build_python: | |
| name: Build and test Python | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: read | |
| strategy: | |
| matrix: | |
| python_version: [3.12, 3.13, 3.14] | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-python@v5 | |
| with: | |
| python-version: ${{ matrix.python_version }} | |
| - name: Build using pip | |
| run: pip install . | |
| working-directory: Tools/Python | |
| - name: Build Lean strata executable for testing purposes. | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| auto-config: false | |
| build: true | |
| build-args: "strata:exe" | |
| - name: Run test script | |
| run: FAIL_FAST=1 ./scripts/run_cpython_tests.sh ${{ matrix.python_version }} | |
| working-directory: Tools/Python | |
| cbmc: | |
| needs: build_and_test_lean | |
| permissions: | |
| contents: read | |
| uses: ./.github/workflows/cbmc.yml |