Exclude dir #22
Workflow file for this run
This file contains hidden or 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: E2E Test | |
| on: | |
| push: | |
| branches: | |
| - dev | |
| pull_request: | |
| types: | |
| - opened | |
| - synchronize | |
| - reopened | |
| - ready_for_review | |
| - converted_to_draft | |
| - edited | |
| branches: | |
| - dev | |
| workflow_dispatch: | |
| # Every job updates fixtures inside the runner's own checkout and never writes back. The | |
| # action's `gh` calls only read the public list of Lean releases. | |
| permissions: | |
| contents: read | |
| 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" | |
| # batteries does not tag every Lean patch release — there is no batteries v4.33.1 — so the | |
| # pin is expected to land on the newest stable batteries tag that does not exceed the | |
| # toolchain, which equals the toolchain only when batteries tagged that release. | |
| - name: The pinned dependency must move as close to the toolchain as its tags allow | |
| 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 | |
| tags=$(git ls-remote --tags --refs \ | |
| https://github.com/leanprover-community/batteries \ | |
| | sed 's#.*refs/tags/##' \ | |
| | grep -E '^v[0-9]+\.[0-9]+\.[0-9]+$') | |
| if printf '%s\n' "$tags" | grep -qx "$toolchain"; then | |
| expected="$toolchain" | |
| else | |
| expected=$(printf '%s\n%s\n' "$tags" "$toolchain" \ | |
| | sort -V \ | |
| | awk -v t="$toolchain" '$0 == t { exit } { last = $0 } END { print last }') | |
| fi | |
| echo "expected=$expected" | |
| if [ "$pin" != "$expected" ]; then | |
| echo "Error: pinned to $pin, but $expected is the newest batteries tag <= $toolchain" | |
| exit 1 | |
| fi | |
| - name: The manifest must be refreshed to match the new pin | |
| run: | | |
| pin=$(grep -o '@ "[^"]*"' Fixtures/PinnedTags/lakefile.lean | cut -d'"' -f2) | |
| if ! grep -q "\"inputRev\": \"$pin\"" 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 | |
| # An exclusion carves a package back out of the set the action would otherwise | |
| # update, leaving its lean-toolchain untouched. | |
| excluded_directory_e2e_test: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v6 | |
| - name: Bump two packages, excluding one of them | |
| id: update | |
| uses: ./ | |
| with: | |
| bump_mode: "pinned-tags" | |
| on_update_succeeds: "silent" | |
| on_update_fails: "silent" | |
| lake_package_directory: "./Fixtures/PinnedTags ./Fixtures/SmokeSuccess !./Fixtures/SmokeSuccess" | |
| - name: The excluded package must be left alone | |
| 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" ]; then | |
| echo "Error: the included package was not bumped" | |
| exit 1 | |
| fi | |
| if [ "$b" != "v4.16.0" ]; then | |
| echo "Error: the excluded package was bumped to $b" | |
| exit 1 | |
| fi | |
| - name: This update should succeed | |
| if: steps.update.outputs.result != 'update-success' | |
| run: exit 1 |