rename lean4checker input to leanchecker

.github/functional_tests/auto_config_false/action.yml

@@ -2,7 +2,7 @@ name: 'Auto Config False Functional Test'
 description: |
   Run `lean-action` with `auto-config: false` and no feature inputs.
   Verify that build and test steps do not run.
-  Run `lean-action` with `auto-config: false` and `lean4checker: true`.
+  Run `lean-action` with `auto-config: false` and `leanchecker: true`.
   Verify that build and tests steps do not run and action succeeds.
 inputs:
   toolchain:
@@ -64,43 +64,43 @@ runs:
       run: .github/functional_tests/test_helpers/verify_action_output.sh
       shell: bash
 
-    - name: "run `lean-action` with `auto-config: false` and `lean4checker: true`"
-      id: lean-action-lean4checker
+    - name: "run `lean-action` with `auto-config: false` and `leanchecker: true`"
+      id: lean-action-leanchecker
       uses: ./
       with:
         auto-config: false
         build: true
-        lean4checker: true
+        leanchecker: true
         use-github-cache: false
 
     - name: verify `lean-action` outcome success
       env:
         OUTPUT_NAME: "lean-action.outcome"
         EXPECTED_VALUE: "success"
-        ACTUAL_VALUE: ${{ steps.lean-action-lean4checker.outcome }}
+        ACTUAL_VALUE: ${{ steps.lean-action-leanchecker.outcome }}
       run: .github/functional_tests/test_helpers/verify_action_output.sh
       shell: bash
 
     - name: verify `lake build` ran
       env:
         OUTPUT_NAME: "build-status"
         EXPECTED_VALUE: "SUCCESS"
-        ACTUAL_VALUE: ${{ steps.lean-action-lean4checker.outputs.build-status }}
+        ACTUAL_VALUE: ${{ steps.lean-action-leanchecker.outputs.build-status }}
       run: .github/functional_tests/test_helpers/verify_action_output.sh
       shell: bash
 
     - name: verify `lake test` not run
       env:
         OUTPUT_NAME: "test-status"
         EXPECTED_VALUE: ""
-        ACTUAL_VALUE: ${{ steps.lean-action-lean4checker.outputs.test-status }}
+        ACTUAL_VALUE: ${{ steps.lean-action-leanchecker.outputs.test-status }}
       run: .github/functional_tests/test_helpers/verify_action_output.sh
       shell: bash
 
     - name: verify `lake lint` not run
       env:
         OUTPUT_NAME: "lint-status"
         EXPECTED_VALUE: ""
-        ACTUAL_VALUE: ${{ steps.lean-action.outputs.test-status }}
+        ACTUAL_VALUE: ${{ steps.lean-action-leanchecker.outputs.test-status }}
       run: .github/functional_tests/test_helpers/verify_action_output.sh
       shell: bash

.github/functional_tests/subdirectory_lake_package_lean_checker/action.yml

@@ -1,9 +1,9 @@
-name: 'Subdirectory Lake Package using lean4checker Functional Test'
+name: 'Subdirectory Lake Package using leanchecker Functional Test'
 description: |
   Run `lean-action` with the `lake-package-directory` input
   on Lake package generated by `lake init` in a subdirectory of the repository.
 
-  Also run lean4checker
+  Also run leanchecker
 inputs:
   toolchain:
     description: 'Toolchain to use for the test'
@@ -33,7 +33,7 @@ runs:
       with:
         use-github-cache: false
         lake-package-directory: "a_subdirectory"
-        lean4checker: true
+        leanchecker: true
 
     - name: verify `lake build` success
       env:

.github/workflows/functional_tests.yml

@@ -19,6 +19,7 @@ on:
 # because the workflow_dispatch input is not available when the workflow is triggered by a pull request
 env:
   toolchain: ${{ github.event.inputs.toolchain || 'leanprover/lean4:v4.26.0' }}
+  modern_toolchain: leanprover/lean4:v4.28.0
 
 jobs:
   lake-init-success:
@@ -62,6 +63,14 @@ jobs:
         with:
           toolchain: ${{ env.toolchain }}
 
+  auto-config-false-modern-leanchecker:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v5
+      - uses: ./.github/functional_tests/auto_config_false
+        with:
+          toolchain: ${{ env.modern_toolchain }}
+
   lake-build-args:
     runs-on: ubuntu-latest
     steps:
@@ -140,7 +149,7 @@ jobs:
       - uses: actions/checkout@v5
       - uses: ./.github/functional_tests/subdirectory_lake_package_lean_checker
         with:
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ env.modern_toolchain }}
 
   reinstall-transient-toolchain:
     runs-on: ubuntu-latest
@@ -175,4 +184,3 @@ jobs:
         with:
           lake-init-arguments: "standalone"
           toolchain: ${{ env.toolchain }}
-

CHANGELOG.md

@@ -7,6 +7,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## Unreleased
 
+### Changed
+
+- rename the `lean4checker` input to `leanchecker`, while keeping `lean4checker` as a deprecated alias
+- use the bundled `leanchecker` binary on Lean `nightly-2026-01-09` / `v4.28.0-rc1` and newer, with fallback to the external `lean4checker` repository on older toolchains
+
 ## v1.4.0 - 2026-01-15
 
 ### Added

README.md

@@ -89,7 +89,7 @@ If `lean-action` is unable to successfully run the step, `lean-action` will fail
 - `lint`
 - `mk_all-check`
 - `check-reservoir-eligibility`
-- `lean4checker`
+- `leanchecker`
 
 ### Automatic configuration
 
@@ -113,15 +113,15 @@ across multiple workflows with different triggers,
 e.g., one workflow for PRs and another workflow scheduled by a cron job.
 `auto-config: false` allows users to run only a specific subset of features of `lean-action`.
 
-For example, run only `lean4checker` in a cron job workflow:
+For example, run only `leanchecker` in a cron job workflow:
 
 ```yaml
-- name: "run `lean-action` with only `lean4checker: true`"
+- name: "run `lean-action` with only `leanchecker: true`"
   id: lean-action
   uses: leanprover/lean-action@v1
   with:
     auto-config: false
-    lean4checker: true
+    leanchecker: true
 ```
 
 ### Differences between using `auto-config` and feature inputs
@@ -195,11 +195,14 @@ To be certain `lean-action` runs a step, specify the desire feature with a featu
     # Default: "false"
     check-reservoir-eligibility: ""
 
-    # Check environment with lean4checker.
-    # Lean version must be 4.8 or higher.
-    # The version of lean4checker is automatically detected using `lean-toolchain`.
+    # Check environment with leanchecker.
+    # Uses the bundled `leanchecker` binary on Lean `nightly-2026-01-09` / `v4.28.0-rc1`
+    # and newer, and falls back to the external `lean4checker` repository on older versions.
     # Allowed values: "true" | "false".
     # Default: "false"
+    leanchecker: ""
+
+    # Deprecated alias for `leanchecker`.
     lean4checker: ""
 
     # Enable GitHub caching.

action.yml

@@ -8,7 +8,7 @@ description: |
     - lake test (optional)
     - lake exe runLinter (optional, must be downstream of Batteries)
     - check reservoir eligibility (optional)
-    - check environment with lean4checker (optional)
+    - check environment with leanchecker (optional)
 inputs:
   auto-config:
     description: |
@@ -75,11 +75,19 @@ inputs:
       Allowed values: "true" | "false".
     required: false
     default: "false"
+  leanchecker:
+    description: |
+      Check environment with leanchecker.
+      Uses the bundled `leanchecker` binary on Lean `nightly-2026-01-09` / `v4.28.0-rc1` and newer.
+      Falls back to building the external `lean4checker` repository on older Lean versions.
+      Allowed values: "true" | "false".
+    required: false
+    default: "false"
   lean4checker:
     description: |
-      Check environment with lean4checker.
-      Lean version must be 4.8 or higher.
-      The version of lean4checker is automatically detected using `lean-toolchain`.
+      Deprecated alias for `leanchecker`.
+      Uses the bundled `leanchecker` binary on Lean `nightly-2026-01-09` / `v4.28.0-rc1` and newer.
+      Falls back to building the external `lean4checker` repository on older Lean versions.
       Allowed values: "true" | "false".
     required: false
     default: "false"
@@ -253,10 +261,13 @@ runs:
       shell: bash
       working-directory: ${{ inputs.lake-package-directory }}
 
-    - name: check environment with lean4checker
-      if: ${{ inputs.lean4checker == 'true' }}
+    - name: check environment with leanchecker
+      if: ${{ inputs.leanchecker == 'true' || inputs.lean4checker == 'true' }}
+      env:
+        LEANCHECKER_INPUT: ${{ inputs.leanchecker }}
+        LEAN4CHECKER_INPUT: ${{ inputs.lean4checker }}
       run: |
-        : Check Environment with lean4checker
-        ${GITHUB_ACTION_PATH}/scripts/run_lean4checker.sh
+        : Check Environment with leanchecker
+        ${GITHUB_ACTION_PATH}/scripts/run_leanchecker.sh
       shell: bash
       working-directory: ${{ inputs.lake-package-directory }}

scripts/run_leanchecker.sh

@@ -0,0 +1,42 @@
+#!/bin/bash
+set -euo pipefail
+
+echo "::group::leanchecker Output"
+echo "Checking environment with leanchecker"
+
+if [ "${LEAN4CHECKER_INPUT:-false}" = "true" ] && [ "${LEANCHECKER_INPUT:-false}" != "true" ]; then
+  echo "::warning::\`lean4checker\` is deprecated; use \`leanchecker\` instead."
+fi
+
+leanchecker_path="$(elan which leanchecker 2>/dev/null || true)"
+if [ -n "$leanchecker_path" ] && [ -x "$leanchecker_path" ]; then
+  echo "Using bundled leanchecker from the active Lean toolchain"
+  lake env leanchecker
+  echo "::endgroup::"
+  echo
+  exit 0
+fi
+
+echo "Bundled leanchecker is unavailable for this toolchain; falling back to external lean4checker"
+
+echo "Cloning and building lean4checker"
+git clone https://github.com/leanprover/lean4checker
+
+(
+toolchain_version=$(< lean-toolchain cut -d: -f 2)
+echo "Detected toolchain version: $toolchain_version"
+
+cd lean4checker || exit
+git config advice.detachedHead false
+git checkout "$toolchain_version"
+cp ../lean-toolchain .
+
+lake build
+./test.sh
+)
+
+echo "Running external lean4checker"
+lake env lean4checker/.lake/build/bin/lean4checker
+
+echo "::endgroup::"
+echo