test.yml

name: 'Test'
on:
  pull_request:
  workflow_dispatch:
concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

jobs:
  code-quality-checks:
    name: 'Code Quality Checks'
    runs-on: ubuntu-latest
    steps:
      - name: 'Check out code'
        uses: actions/checkout@v4
      - name: 'Get uv release'
        id: uv_release
        run: |
          echo uv_version=$(cat deps/uv_release) >> "${GITHUB_OUTPUT}"
      - name: 'Install uv'
        uses: astral-sh/setup-uv@v6
        with:
          version: ${{ steps.uv_release.outputs.uv_version }}
      - name: 'Install Nix'
        uses: cachix/install-nix-action@v31.5.1
        with:
          install_url: https://releases.nixos.org/nix/nix-2.31.2/install
          extra_nix_config: |
            substituters = https://cache.nixos.org
            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
      - name: 'Run code quality checks'
        run: make check

  unit-tests:
    needs: code-quality-checks
    name: 'Unit Tests'
    runs-on: ubuntu-latest
    steps:
      - name: 'Check out code'
        uses: actions/checkout@v4
      - name: 'Get uv release'
        id: uv_release
        run: |
          echo uv_version=$(cat deps/uv_release) >> "${GITHUB_OUTPUT}"
      - name: 'Install uv'
        uses: astral-sh/setup-uv@v6
        with:
          version: ${{ steps.uv_release.outputs.uv_version }}
      - name: 'Run unit tests'
        run: make test-unit

  integration-tests:
    needs: code-quality-checks
    name: 'Integration Tests'
    runs-on: [self-hosted, linux, normal]
    steps:
      - name: 'Check out code'
        uses: actions/checkout@v4
        with:
          token: ${{ secrets.JENKINS_GITHUB_PAT }}
          submodules: recursive
      - name: 'Set up Docker'
        uses: ./.github/actions/with-docker
        with:
          container-name: mir-semantics-ci-${{ github.sha }}
      - name: 'Build stable-mir-json and kmir'
        run: docker exec --user github-user mir-semantics-ci-${GITHUB_SHA} make build
      - name: 'Run integration tests'
        run: docker exec --user github-user mir-semantics-ci-${GITHUB_SHA} make test-integration
      - name: 'Tear down Docker'
        if: always()
        run: docker stop --time 0 mir-semantics-ci-${GITHUB_SHA}

  stable-mir-json-integration-tests:
    needs: code-quality-checks
    name: "Integration with stable-mir-json"
    runs-on: [self-hosted, linux, normal]
    steps:
      - name: 'Check out code'
        uses: actions/checkout@v4
        with:
          token: ${{ secrets.JENKINS_GITHUB_PAT }}
          submodules: recursive
      - name: 'Set up Docker'
        uses: ./.github/actions/with-docker
        with:
          container-name: mir-smir-ci-${{ github.sha }}
      - name: 'Build stable-mir-json'
        run: docker exec --user github-user mir-smir-ci-${GITHUB_SHA} make stable-mir-json
      - name: 'Build kmir (within docker)'
        run: docker exec --user github-user mir-smir-ci-${GITHUB_SHA} make build
      - name: 'Run parser tests (within docker)'
        run: docker exec --user github-user mir-smir-ci-${GITHUB_SHA} make smir-parse-tests
      - name: 'Tear down Docker'
        if: always()
        run: docker stop --time 0 mir-smir-ci-${GITHUB_SHA}

  test-kmir-image:
    name: Test Kmir Image
    needs: [ unit-tests, code-quality-checks ]
    runs-on: ubuntu-latest
    env:
      container_name: "kmir-${{ github.run_id }}"
    outputs:
      image-name: ${{ steps.set-image-name.outputs.image-name }}
      k-version: ${{ steps.set-image-name.outputs.k-version }}
      kmir-version: ${{ steps.set-image-name.outputs.kmir-version }}
      short-sha: ${{ steps.set-image-name.outputs.short-sha }}
    steps:
      - name: Checkout code
        uses: actions/checkout@v4
        with:
          submodules: recursive

      - name: Setup Docker Buildx
        uses: docker/setup-buildx-action@v3.10.0

      - name: Set Image Name Parameters
        id: set-image-name
        run: |
          echo "image-name=ghcr.io/runtimeverification/mir-semantics/kmir" >> $GITHUB_OUTPUT
          echo "k-version=$(cat deps/k_release)" >> $GITHUB_OUTPUT
          echo "kmir-version=$(cat package/version)" >> $GITHUB_OUTPUT
          echo "short-sha=$(git rev-parse --short HEAD)" >> $GITHUB_OUTPUT

      - name: Build Kmir Container
        uses: docker/build-push-action@v6
        with:
          context: .
          file: Dockerfile.kmir
          platforms: linux/amd64
          push: false
          load: true
          build-args: |
            K_VERSION=${{ steps.set-image-name.outputs.k-version }}
          tags: ${{ steps.set-image-name.outputs.image-name }}:ubuntu-jammy-${{ steps.set-image-name.outputs.kmir-version }}-${{ steps.set-image-name.outputs.short-sha }}

      - name: Container Sanity Check
        run: |
          # Create output directories for each test
          for k_file in kmir/src/tests/integration/data/*/*-spec.k; do
            proof_dir="$(dirname ${k_file})/proofs"
            mkdir -p "${proof_dir}"
            chmod 777 "${proof_dir}"
          done

          # Start Container
          docker run --detach --rm -t \
            --name ${{ env.container_name }} \
            -v $PWD:/home/kmir/workspace \
            -w /home/kmir/workspace \
            ${{ steps.set-image-name.outputs.image-name }}:ubuntu-jammy-${{ steps.set-image-name.outputs.kmir-version }}-${{ steps.set-image-name.outputs.short-sha }} \
            /bin/bash

          # Run all tests in a single exec command to maintain fixuid context
          docker exec \
            -w /home/kmir/workspace \
            ${{ env.container_name }} \
            /bin/bash -c '
              for k_file in kmir/src/tests/integration/data/*/*-spec.k; do
                echo "Running ${k_file}"
                proof_dir="$(dirname ${k_file})/proofs"
                if ! kmir prove run "${k_file}" --proof-dir "${proof_dir}" 2>&1; then
                  echo "Proof failed for ${k_file}"
                fi
              done
            '

          # Print test results
          echo "Test results:"
          find kmir/src/tests/integration/data -name "proofs" -type d -exec echo {} >> GITHUB_STEP_SUMMARY \;

      - name: Tear Down Container
        if: always()
        run: docker stop ${{ env.container_name }}


  nix:
    needs: code-quality-checks
    name: 'Nix Tests'
    strategy:
      fail-fast: false
      matrix:
        runner: [normal, MacM1]  # MacM1 / normal are self-hosted, 
    runs-on: ${{ matrix.runner }}
    timeout-minutes: 20
    steps:
      - name: 'Check out code'
        uses: actions/checkout@v4
        with:
          # Check out pull request HEAD instead of merge commit.
          ref: ${{ github.event.pull_request.head.sha }}
          submodules: recursive

      - name: 'Install Nix'
        if: ${{ matrix.runner != 'MacM1' }}
        uses: cachix/install-nix-action@v31.5.1
        with:
          install_url: https://releases.nixos.org/nix/nix-2.31.2/install
          extra_nix_config: |
            substituters = http://cache.nixos.org https://cache.iog.io
            trusted-public-keys = cache.nixos.org

      - name: 'Install Cachix'
        if: ${{ matrix.runner != 'MacM1' }}
        uses: cachix/cachix-action@v16
        with:
          name: k-framework

      - name: 'Build and test'
        run: |
          set -euxo pipefail
          nix --version
          nix flake check # build and run smoke test