test.yml

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

jobs:

  version-bump:
    name: 'Version Bump'
    runs-on: ubuntu-latest
    steps:
      - name: 'Check out code'
        uses: actions/checkout@v4
        with:
          token: ${{ secrets.JENKINS_GITHUB_PAT }}
          fetch-depth: 0  # deep clone the repo
          ref: ${{ github.event.pull_request.head.sha }}
      - name: 'Configure GitHub user'
        run: |
          git config user.name devops
          git config user.email devops@runtimeverification.com
      - name: 'Update version'
        run: |
          og_version=$(git show origin/${GITHUB_BASE_REF}:package/version)
          ./package/version.sh bump ${og_version}
          ./package/version.sh sub
          new_version=$(cat package/version)
          git add --update && git commit --message "Set Version: ${new_version}" || true
      - name: 'Push updates'
        run: git push origin HEAD:${GITHUB_HEAD_REF}

  python-code-quality-checks:
    name: 'Code Quality Checks'
    runs-on: ubuntu-latest
    steps:
      - name: 'Check out code'
        uses: actions/checkout@v4
        with:
          token: ${{ secrets.JENKINS_GITHUB_PAT }}
          submodules: recursive
      - name: 'Install Python'
        uses: actions/setup-python@v5
        with:
          python-version: '3.10'
      - name: 'Install Poetry'
        uses: Gr1N/setup-poetry@v9
      - name: 'Build kmxwasm'
        run: poetry -C kmxwasm install
      - name: 'Run code quality checks'
        run: make -C kmxwasm check
      - name: 'Run unit tests'
        run: make -C kmxwasm test-unit

  integration-tests:
    name: 'Kmxwasm integration tests'
    runs-on: [self-hosted, linux, normal]
    needs: [python-code-quality-checks]
    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: mx-wasm-ci-${{ github.sha }}
      - name: 'Build kmxwasm'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make kmxwasm
      - name: 'Build semantics'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make build
      - name: 'Run integration tests'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make -C kmxwasm test-integration
      - name: 'Tear down Docker'
        if: always()
        run: docker stop --time 0 mx-wasm-ci-${GITHUB_SHA}

  booster-tests:
    name: 'Kmxwasm booster tests'
    runs-on: [self-hosted, linux, normal]
    needs: [python-code-quality-checks]
    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: mx-wasm-ci-${{ github.sha }}
      - name: 'Build kmxwasm'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make kmxwasm
      - name: 'Build semantics'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make build
      - name: 'Run booster tests'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make -C kmxwasm test-booster
      - name: 'Tear down Docker'
        if: always()
        run: docker stop --time 0 mx-wasm-ci-${GITHUB_SHA}

  claim-generation-tests:
    name: 'Kasmer claim generation tests'
    runs-on: [self-hosted, linux, normal]
    needs: [python-code-quality-checks]
    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: mx-wasm-ci-${{ github.sha }}
      - name: 'Build kmxwasm'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make kmxwasm
      - name: 'Build semantics'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make build-kasmer
      - name: 'Generate claims'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} ./generate-claims.sh
      - name: 'Tear down Docker'
        if: always()
        run: docker stop --time 0 mx-wasm-ci-${GITHUB_SHA}

  lemma-tests:
    name: 'Build and Test lemmas'
    runs-on: [self-hosted, linux, normal]
    needs: [python-code-quality-checks]
    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: mx-wasm-ci-${{ github.sha }}
      - name: 'Build kmxwasm'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make kmxwasm
      - name: 'Build semantics'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make build
      - name: 'Check lemmas are up to date'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make -C kmxwasm test-lemmas-not-changed
      - name: 'Test lemmas'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make -C kmxwasm test-lemmas
      - name: 'Prove lemmas'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make -C kmxwasm test-proofs
      - name: 'Tear down Docker'
        if: always()
        run: docker stop --time 0 mx-wasm-ci-${GITHUB_SHA}

  smoke-tests:
    name: 'Smoke tests'
    runs-on: [self-hosted, linux, normal]
    needs: [python-code-quality-checks]
    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: mx-wasm-ci-${{ github.sha }}
      - name: 'Build kmxwasm'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make kmxwasm
      - name: 'Build semantics'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make build
      - name: 'Build kasmer semantics'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make build-kasmer
      - name: 'Run smoke tests'
        run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} poetry -C kmxwasm run ./package/smoke-test.sh
      - name: 'Tear down Docker'
        if: always()
        run: docker stop --time 0 mx-wasm-ci-${GITHUB_SHA}

  nix:
    name: 'Nix'
    strategy:
      fail-fast: false
      matrix:
        include:
          - runner: [self-hosted, linux, normal]
          - runner: self-macos-14
    needs: [python-code-quality-checks]
    runs-on: ${{ matrix.runner }}
    steps:
      - name: 'Check out code'
        uses: actions/checkout@v4
        with:
          submodules: recursive
      - name: 'Build Kasmer'
        run: GC_DONT_GC=1 nix build .#kmxwasm --extra-experimental-features 'nix-command flakes' --print-build-logs
      - name: 'Run smoke tests'
        run: GC_DONT_GC=1 nix develop .#kmxwasm-test-shell --extra-experimental-features 'nix-command flakes' --print-build-logs --command './package/smoke-test.sh'
      - name: 'Run claim generation tests'
        run: GC_DONT_GC=1 nix develop .#kmxwasm-test-shell --extra-experimental-features 'nix-command flakes' --print-build-logs --command './generate-claims.sh'