integration-tests-reusable.yml

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'
        type: string
        required: false
        default: ""

env:
  dotnet-version: 8.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-22.04\", \"macos-14\", \"windows-2022\"]" >> $GITHUB_OUTPUT
      - name: Populate OS list (one platform)
        id: populate-os-list-one
        if: "!inputs.all_platforms"
        run: echo "os-list=[\"ubuntu-22.04\"]" >> $GITHUB_OUTPUT
      - name: Populate OS mapping for package.py
        id: populate-os-mapping
        run: |
          echo "os-mapping={\"ubuntu-22.04\": \"ubuntu\", \"macos-14\": \"macos\", \"windows-2022\": \"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 }}
    #  Setup dotnet 6.0 for running Boogie. Alternatively we could try running Boogie with a roll forward policy, or updating Boogie.
    - name: Setup dotnet
      uses: actions/setup-dotnet@v4
      with:
        dotnet-version: 6.0.x
    - name: C++ for ubuntu 22.04
      if: matrix.os == 'ubuntu-22.04'
      run: |
        sudo apt-get install -y build-essential
    - 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: Use the default Rust linker (Non-Windows)
      if: runner.os != 'Windows'
      run: rustup default 1.85.1
    - name: Use specific Toolchain (Windows)
      if: runner.os == 'Windows'
      run: rustup default 1.85.1-x86_64-pc-windows-gnu
    - name: Rust-related System information
      run: |
        echo "What is the Rust version?"
        rustc -vV
        echo "What is the cargo version?"
        cargo --version
        echo "What is the architecture?"
        uname -m
        echo "What are Rust toolchains installed?"
        rustup toolchain list
    - 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 update && 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-2025-07-02/z3-4.12.1-x64-ubuntu-22.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\dafny
        DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS: ${{ inputs.compilers }}
      run: |
        cmd /c mklink ${{ env.DAFNY_RELEASE }}\z3\bin\z3-4.12.1 ${{ env.DAFNY_RELEASE }}\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 }}
        DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS: ${{ inputs.compilers }}
      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