Fix the nightly build #5
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: Integration Tests (Reusable Workflow) | ||
| on: | ||
| workflow_call: | ||
| inputs: | ||
| all_platforms: | ||
| required: true | ||
| type: boolean | ||
| num_shards: | ||
| required: true | ||
| type: number | ||
| ref: | ||
| required: true | ||
| type: string | ||
| compilers: | ||
| description: 'Compilers to use' | ||
| required: false | ||
| default: '' | ||
| env: | ||
| dotnet-version: 6.0.x # SDK Version for building Dafny | ||
| jobs: | ||
| # This job is used to dynamically calculate the matrix dimensions. | ||
| # For now that just makes the sharding a little cleaner, but it will shortly | ||
| # be used to switch between one platform and all platforms based on an input parameter. | ||
| populate-matrix-dimensions: | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - name: Populate OS list (all platforms) | ||
| id: populate-os-list-all | ||
| if: inputs.all_platforms | ||
| run: echo "os-list=[\"ubuntu-20.04\", \"macos-13\", \"windows-2019\"]" >> $GITHUB_OUTPUT | ||
| - name: Populate OS list (one platform) | ||
| id: populate-os-list-one | ||
| if: "!inputs.all_platforms" | ||
| run: echo "os-list=[\"ubuntu-20.04\"]" >> $GITHUB_OUTPUT | ||
| - name: Populate OS mapping for package.py | ||
| id: populate-os-mapping | ||
| run: | | ||
| echo "os-mapping={\"ubuntu-20.04\": \"ubuntu\", \"macos-13\": \"macos\", \"windows-2019\": \"windows\"}" >> $GITHUB_OUTPUT | ||
| - name: Populate target runtime version list (all platforms) | ||
| id: populate-target-runtime-version-all | ||
| if: inputs.all_platforms | ||
| run: echo "target-runtime-version=[\"oldest\", \"newest\"]" >> $GITHUB_OUTPUT | ||
| - name: Populate target runtime version list (one platform) | ||
| id: populate-target-runtime-version-one | ||
| if: "!inputs.all_platforms" | ||
| run: echo "target-runtime-version=[\"oldest\"]" >> $GITHUB_OUTPUT | ||
| - name: Populate shard list | ||
| id: populate-shard-list | ||
| run: echo "shard-list=[`seq -s , 1 ${{ inputs.num_shards }}`]" >> $GITHUB_OUTPUT | ||
| outputs: | ||
| os-list: ${{ steps.populate-os-list-all.outputs.os-list }} ${{ steps.populate-os-list-one.outputs.os-list }} | ||
| os-mapping: ${{ steps.populate-os-mapping.outputs.os-mapping }} | ||
| shard-list: ${{ steps.populate-shard-list.outputs.shard-list }} | ||
| test: | ||
| needs: populate-matrix-dimensions | ||
| timeout-minutes: 120 | ||
| runs-on: ${{ matrix.os }} | ||
| strategy: | ||
| matrix: | ||
| os: ${{ fromJson(needs.populate-matrix-dimensions.outputs.os-list) }} | ||
| shard: ${{ fromJson(needs.populate-matrix-dimensions.outputs.shard-list) }} | ||
| fail-fast: false | ||
| steps: | ||
| - name: Manually sync certs | ||
| if: runner.os == 'Linux' | ||
| run: cert-sync /etc/ssl/certs/ca-certificates.crt | ||
| - name: Setup dotnet | ||
| uses: actions/setup-dotnet@v4 | ||
| with: | ||
| dotnet-version: ${{ env.dotnet-version }} | ||
| - name: C++ for ubuntu 20.04 | ||
| if: matrix.os == 'ubuntu-20.04' | ||
| run: | | ||
| sudo apt-get install -y build-essential | ||
| - name: Choose the right C++ for ubuntu 20.04 | ||
| if: matrix.os == 'ubuntu-20.04' | ||
| run: | | ||
| sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-9 60 | ||
| - name: Set up oldest supported JDK | ||
| if: matrix.target-language-version != 'newest' | ||
| uses: actions/setup-java@v4 | ||
| with: | ||
| java-version: 8 | ||
| distribution: corretto | ||
| - name: Set up newest supported JDK | ||
| if: matrix.target-language-version == 'newest' | ||
| uses: actions/setup-java@v4 | ||
| with: | ||
| java-version: 18 | ||
| distribution: corretto | ||
| - name: Set up oldest supported Go | ||
| uses: actions/setup-go@v5 | ||
| with: | ||
| go-version: '1.21' | ||
| cache: false | ||
| - name: Set up goimports | ||
| env: | ||
| GO111MODULE: on | ||
| run: go install golang.org/x/tools/cmd/goimports@latest | ||
| - name: Set up Python | ||
| uses: actions/setup-python@v5 | ||
| with: | ||
| python-version: '3.11' | ||
| - name: Upgrade outdated pip | ||
| run: python -m pip install --upgrade pip | ||
| - name: Install lit | ||
| run: pip install lit OutputCheck pyyaml | ||
| - uses: actions/setup-node@v4 | ||
| - run: npm install bignumber.js | ||
| - name: Checkout Dafny | ||
| uses: actions/checkout@v4 | ||
| with: | ||
| path: dafny | ||
| ref: ${{ inputs.ref }} | ||
| submodules: true # Until the libraries work again | ||
| - name: Install Java runtime locally (non-Windows) | ||
| if: runner.os != 'Windows' | ||
| working-directory: dafny/Source/DafnyRuntime/DafnyRuntimeJava | ||
| run: ./gradlew publishToMavenLocal | ||
| - name: Install Java runtime locally (Windows) | ||
| if: runner.os == 'Windows' | ||
| working-directory: dafny/Source/DafnyRuntime/DafnyRuntimeJava | ||
| run: ./gradlew.bat publishToMavenLocal | ||
| # - name: Clean up libraries for testing | ||
| # run: | | ||
| # rm dafny/Test/libraries/lit.site.cfg # we remove the lit configuration file in the library repo (a git submodule) to prevent override | ||
| - name: Create release | ||
| if: inputs.all_platforms | ||
| run: | | ||
| python dafny/Scripts/package.py 0.0.0-CI --platform x64 --os ${{ fromJson(needs.populate-matrix-dimensions.outputs.os-mapping)[matrix.os] }} --skip_manual=true --trial=true --github_secret=${{ secrets.GITHUB_TOKEN }} --out=CI.zip | ||
| - if: runner.os == 'Windows' && inputs.all_platforms | ||
| shell: pwsh | ||
| run: | | ||
| Expand-Archive dafny/Package/CI.zip unzippedRelease | ||
| - if: runner.os != 'Windows' && inputs.all_platforms | ||
| run: | | ||
| unzip dafny/Package/CI.zip -d unzippedRelease | ||
| - name: Load Z3 | ||
| if: "!inputs.all_platforms" | ||
| run: | | ||
| sudo apt-get install -qq libarchive-tools | ||
| mkdir -p dafny/Binaries/z3/bin | ||
| wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf - | ||
| mv z3-4.12.1 dafny/Binaries/z3/bin/ | ||
| chmod +x dafny/Binaries/z3/bin/z3-4.12.1 | ||
| mkdir -p unzippedRelease/dafny/z3/bin | ||
| ln dafny/Binaries/z3/bin/z3-4.12.1 unzippedRelease/dafny/z3/bin/z3-4.12.1 | ||
| - name: Run integration tests (Windows) | ||
| if: runner.os == 'Windows' | ||
| env: | ||
| XUNIT_SHARD: ${{ matrix.shard }} | ||
| XUNIT_SHARD_COUNT: ${{ inputs.num_shards }} | ||
| DAFNY_RELEASE: ${{ github.workspace }}\unzippedRelease\dafnyenv: | ||
| DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS: ${{ inputs.compilers }} | ||
| run: | | ||
| cmd /c mklink D:\a\dafny\dafny\unzippedRelease\dafny\z3\bin\z3-4.12.1 D:\a\dafny\dafny\unzippedRelease\dafny\z3\bin\z3-4.12.1.exe | ||
| dotnet test --logger trx --logger "console;verbosity=normal" --collect:"XPlat Code Coverage" --settings dafny/Source/IntegrationTests/coverlet.runsettings dafny/Source/IntegrationTests/IntegrationTests.csproj | ||
| - name: Generate tests (non-Windows) | ||
| ## This step creates lit tests from examples in documentation | ||
| ## These are then picked up by the integration tests below | ||
| ## and both tested and included in coverage metrics | ||
| if: runner.os != 'Windows' | ||
| run: | | ||
| cd dafny/docs | ||
| ./check-examples -c HowToFAQ/Errors-*.md | ||
| - name: Run integration tests (non-Windows) | ||
| if: runner.os != 'Windows' | ||
| env: | ||
| XUNIT_SHARD: ${{ matrix.shard }} | ||
| XUNIT_SHARD_COUNT: ${{ inputs.num_shards }} | ||
| run: | | ||
| ${{ inputs.all_platforms }} && export DAFNY_RELEASE="${{ github.workspace }}/unzippedRelease/dafny" | ||
| dotnet test --logger trx --logger "console;verbosity=normal" --collect:"XPlat Code Coverage" --settings dafny/Source/IntegrationTests/coverlet.runsettings dafny/Source/IntegrationTests | ||
| - uses: actions/upload-artifact@v4 | ||
| if: always() | ||
| with: | ||
| name: integration-test-results-${{ matrix.os }}-${{ matrix.shard }} | ||
| path: | | ||
| dafny/Source/*/TestResults/*.trx | ||
| dafny/Source/*/TestResults/*/coverage.cobertura.xml | ||
