e2e_test.yml

name: E2E Test

on:
  push:
    branches:
      - dev
  pull_request:
    types:
      - opened
      - synchronize
      - reopened
      - ready_for_review
      - converted_to_draft
      - edited
    branches:
      - dev
  workflow_dispatch:

jobs:
  success_e2e_test:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout code
        uses: actions/checkout@v6

      - name: Update Lean package
        id: update
        uses: ./
        with:
          on_update_succeeds: "silent"
          on_update_fails: "silent"
          lake_package_directory: "./Fixtures/SmokeSuccess"

      - name: This update should succeed
        if: steps.update.outputs.result != 'update-success'
        run: exit 1

  mathlib_dependency_e2e_test:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout code
        uses: actions/checkout@v6

      - name: Update Lean package with mathlib dependency
        id: update
        uses: ./
        with:
          on_update_succeeds: "silent"
          on_update_fails: "silent"
          lake_package_directory: "./Fixtures/MathlibDep"

      - name: This update should succeed
        if: steps.update.outputs.result != 'update-success'
        run: exit 1

      - name: The fixture should depend on mathlib
        if: steps.update.outputs.has_dependency != 'true'
        run: exit 1

  success_nightly_test:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout code
        uses: actions/checkout@v6

      - name: Update Lean package with nightly
        id: update
        uses: ./
        with:
          on_update_succeeds: "silent"
          on_update_fails: "silent"
          lake_package_directory: "./Fixtures/SmokeSuccess"
          release_kind_to_fetch: "nightly"

      - name: This update should succeed
        if: steps.update.outputs.result != 'update-success'
        run: exit 1

      - name: The latest Lean release should be nightly
        run: |
          echo "Latest Lean version: ${{ steps.update.outputs.latest_lean }}"
          if [[ ! "${{ steps.update.outputs.latest_lean }}" =~ ^nightly- ]]; then
            echo "Error: The latest_lean output should start with 'nightly-'"
            exit 1
          fi

          TOOLCHAIN=$(cat Fixtures/SmokeSuccess/lean-toolchain)
          echo "Updated lean-toolchain: $TOOLCHAIN"
          if [[ ! "$TOOLCHAIN" =~ ^leanprover/lean4:nightly- ]]; then
            echo "Error: lean-toolchain should be updated to a nightly Lean release"
            exit 1
          fi

  fail_e2e_test:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout code
        uses: actions/checkout@v6

      - name: Update Lean package
        id: update
        uses: ./
        with:
          on_update_fails: "silent"
          lake_package_directory: "./Fixtures/Fail"

      - name: This update should fail
        if: steps.update.outputs.result != 'update-fail'
        run: exit 1

  test_driver_failure_e2e_test:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout code
        uses: actions/checkout@v6

      - name: Update Lean package
        id: update
        uses: ./
        with:
          on_update_fails: "silent"
          lake_package_directory: "./Fixtures/TestFail"

      - name: This update should fail
        if: steps.update.outputs.result != 'update-fail'
        run: exit 1

      - name: The fixture should still build
        run: lake build
        working-directory: ./Fixtures/TestFail

  lint_driver_failure_e2e_test:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout code
        uses: actions/checkout@v6

      - name: Update Lean package
        id: update
        uses: ./
        with:
          on_update_succeeds: "silent"
          on_update_fails: "silent"
          lake_package_directory: "./Fixtures/LintFail"

      - name: The fixture should still build
        run: lake build
        working-directory: ./Fixtures/LintFail

      - name: The fixture lint should fail
        run: |
          if lake lint; then
            echo "Expected lake lint to fail"
            exit 1
          fi
        working-directory: ./Fixtures/LintFail

      - name: This update should fail
        if: steps.update.outputs.result != 'update-fail'
        run: exit 1

  # `bump_mode: pinned-tags` moves a dependency's pinned Lean-version tag and
  # `lean-toolchain` together, so the two must agree afterwards and neither may
  # be left behind.
  pinned_tags_e2e_test:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout code
        uses: actions/checkout@v6

      - name: Bump the pinned tag and the toolchain
        id: update
        uses: ./
        with:
          bump_mode: "pinned-tags"
          on_update_succeeds: "silent"
          on_update_fails: "silent"
          lake_package_directory: "./Fixtures/PinnedTags"

      - name: The toolchain and the pinned dependency must move together
        run: |
          toolchain=$(cut -d: -f2 Fixtures/PinnedTags/lean-toolchain)
          pin=$(grep -o '@ "[^"]*"' Fixtures/PinnedTags/lakefile.lean | cut -d'"' -f2)
          echo "toolchain=$toolchain pin=$pin"
          if [ "$toolchain" = "v4.31.0" ]; then
            echo "Error: lean-toolchain was not bumped"
            exit 1
          fi
          if [ "$toolchain" != "$pin" ]; then
            echo "Error: dependency pinned to $pin but toolchain is $toolchain"
            exit 1
          fi

      - name: The manifest must be refreshed to match the new pin
        run: |
          if ! grep -q "\"inputRev\": \"$(cut -d: -f2 Fixtures/PinnedTags/lean-toolchain)\"" \
            Fixtures/PinnedTags/lake-manifest.json; then
            echo "Error: lake-manifest.json still points at the old revision"
            cat Fixtures/PinnedTags/lake-manifest.json
            exit 1
          fi

      - name: This update should succeed
        if: steps.update.outputs.result != 'update-success'
        run: exit 1

  # A dependency pinned to a commit is a deliberate pin: rewriting it to a tag
  # would silently discard it, so it must be left alone and reported — but the
  # toolchain still moves, since updating it is the point of the action.
  pinned_sha_e2e_test:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout code
        uses: actions/checkout@v6

      - name: Bump a package whose dependency is commit-pinned
        id: update
        uses: ./
        with:
          bump_mode: "pinned-tags"
          on_update_succeeds: "silent"
          on_update_fails: "silent"
          lake_package_directory: "./Fixtures/PinnedSha"

      - name: The commit pin must be untouched
        run: |
          if ! git diff --quiet -- Fixtures/PinnedSha/lakefile.lean Fixtures/PinnedSha/lake-manifest.json; then
            echo "Error: a commit-pinned dependency was rewritten"
            git diff -- Fixtures/PinnedSha
            exit 1
          fi

      - name: The toolchain must still be bumped
        run: |
          toolchain=$(cut -d: -f2 Fixtures/PinnedSha/lean-toolchain)
          echo "toolchain=$toolchain"
          if [ "$toolchain" = "v4.31.0" ]; then
            echo "Error: lean-toolchain was not bumped"
            exit 1
          fi

      - name: An update must be reported
        if: steps.update.outputs.result == 'no-update'
        run: exit 1

  # A package with no git requires has nothing gating its toolchain, so
  # pinned-tags mode must still bump `lean-toolchain` by itself.
  pinned_tags_no_deps_e2e_test:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout code
        uses: actions/checkout@v6

      - name: Bump the toolchain of a dependency-free package
        id: update
        uses: ./
        with:
          bump_mode: "pinned-tags"
          on_update_succeeds: "silent"
          on_update_fails: "silent"
          lake_package_directory: "./Fixtures/SmokeSuccess"

      - name: The toolchain must be bumped
        run: |
          toolchain=$(cut -d: -f2 Fixtures/SmokeSuccess/lean-toolchain)
          echo "toolchain=$toolchain"
          if [ "$toolchain" = "v4.16.0" ]; then
            echo "Error: lean-toolchain was not bumped"
            exit 1
          fi

      - name: This update should succeed
        if: steps.update.outputs.result != 'update-success'
        run: exit 1

  # Multiple directories in one invocation: both packages must land on the
  # same release, and the outputs must aggregate across them.
  pinned_tags_multi_dir_e2e_test:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout code
        uses: actions/checkout@v6

      - name: Bump two packages at once
        id: update
        uses: ./
        with:
          bump_mode: "pinned-tags"
          on_update_succeeds: "silent"
          on_update_fails: "silent"
          lake_package_directory: "./Fixtures/PinnedTags ./Fixtures/SmokeSuccess"

      - name: Both toolchains must be bumped to the same release
        run: |
          a=$(cut -d: -f2 Fixtures/PinnedTags/lean-toolchain)
          b=$(cut -d: -f2 Fixtures/SmokeSuccess/lean-toolchain)
          echo "PinnedTags=$a SmokeSuccess=$b"
          if [ "$a" = "v4.31.0" ] || [ "$b" = "v4.16.0" ]; then
            echo "Error: a package was not bumped"
            exit 1
          fi
          if [ "$a" != "$b" ]; then
            echo "Error: packages diverged"
            exit 1
          fi

      - name: The release must be reported as an output
        run: |
          echo "latest_lean=${{ steps.update.outputs.latest_lean }}"
          expected=$(cut -d: -f2 Fixtures/PinnedTags/lean-toolchain)
          if [ "${{ steps.update.outputs.latest_lean }}" != "$expected" ]; then
            echo "Error: expected $expected"
            exit 1
          fi

      - name: This update should succeed
        if: steps.update.outputs.result != 'update-success'
        run: exit 1