feat: add lake-check input for sandboxed independent kernel checks

.github/actionlint.yaml

@@ -0,0 +1,7 @@
+# Namespace runner labels used by the `lake-check-namespace` functional test. `lake check`
+# sandboxes with bubblewrap, which needs a privileged container on Namespace; the
+# `-with-features` suffix is what makes the feature label apply.
+self-hosted-runner:
+  labels:
+    - nscloud-ubuntu-24.04-amd64-2x4-with-features
+    - namespace-features:container.privileged=true

.github/functional_tests/lake_check/action.yml

@@ -0,0 +1,60 @@
+name: 'lake check test'
+description: 'Verify `lake-check: paranoid` succeeds on a clean package and fails once a sorry is introduced.'
+inputs:
+  toolchain:
+    description: 'Toolchain to use for the test'
+    required: true
+runs:
+  using: 'composite'
+  steps:
+    # TODO: once `lean-action` supports just setup, use it here
+    - name: install elan
+      run: |
+        set -o pipefail
+        curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain ${{ inputs.toolchain }}
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      shell: bash
+
+    - name: create a clean lake library
+      run: |
+        lake init foo lib
+        lake update
+      shell: bash
+
+    - name: "run `lean-action` (clean package)"
+      id: lean-action-clean
+      uses: ./
+      with:
+        use-github-cache: false
+        lake-check: paranoid
+
+    - name: verify lake check success on the clean package
+      env:
+        OUTPUT_NAME: "lake-check-status"
+        EXPECTED_VALUE: "SUCCESS"
+        ACTUAL_VALUE: ${{ steps.lean-action-clean.outputs.lake-check-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
+
+    # `lake check` permits only the standard axioms, so a `sorry` is enough to make every kernel
+    # it runs reject the project.
+    - name: introduce a sorry
+      run: |
+        printf '\ntheorem fooSorry : True := by sorry\n' >> Foo/Basic.lean
+      shell: bash
+
+    - name: "rerun `lean-action` (sorry introduced)"
+      id: lean-action-dirty
+      uses: ./
+      continue-on-error: true # required so that the failing check does not fail the workflow
+      with:
+        use-github-cache: false
+        lake-check: paranoid
+
+    - name: verify lake check failure once a sorry is introduced
+      env:
+        OUTPUT_NAME: "lake-check-status"
+        EXPECTED_VALUE: "FAILURE"
+        ACTUAL_VALUE: ${{ steps.lean-action-dirty.outputs.lake-check-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash

.github/functional_tests/lake_check_unsupported/action.yml

@@ -0,0 +1,51 @@
+name: 'lake check unsupported toolchain test'
+description: 'Verify `lake-check` fails loudly, rather than silently passing, on a toolchain without `lake check`.'
+inputs:
+  toolchain:
+    description: 'Toolchain to use for the test. Must be older than v4.35.0-rc1.'
+    required: true
+runs:
+  using: 'composite'
+  steps:
+    # TODO: once `lean-action` supports just setup, use it here
+    - name: install elan
+      run: |
+        set -o pipefail
+        curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain ${{ inputs.toolchain }}
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      shell: bash
+
+    - name: create a clean lake library
+      run: |
+        lake init foo lib
+        lake update
+      shell: bash
+
+    - name: "run `lean-action` on a toolchain without `lake check`"
+      id: lean-action-unsupported
+      uses: ./
+      continue-on-error: true # required so that the expected failure does not fail the workflow
+      with:
+        use-github-cache: false
+        lake-check: "true"
+
+    # A check that cannot run has to be reported as a failure. Silently passing would tell a
+    # project its kernel was independently replayed when nothing ran at all.
+    - name: verify lake check fails on an unsupported toolchain
+      env:
+        OUTPUT_NAME: "lake-check-status"
+        EXPECTED_VALUE: "FAILURE"
+        ACTUAL_VALUE: ${{ steps.lean-action-unsupported.outputs.lake-check-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
+
+    - name: verify the action step itself failed
+      env:
+        STEP_OUTCOME: ${{ steps.lean-action-unsupported.outcome }}
+      run: |
+        if [ "$STEP_OUTCOME" != "failure" ]; then
+          echo "::error::expected the lean-action step to fail, but its outcome was '$STEP_OUTCOME'"
+          exit 1
+        fi
+        echo "lean-action failed as expected"
+      shell: bash

.github/workflows/functional_tests.yml

@@ -28,6 +28,9 @@ env:
   # Toolchain without the bundled `leanchecker` binary,
   # used to cover the external `lean4checker` fallback path
   legacy_toolchain: leanprover/lean4:v4.26.0
+  # `lake check --paranoid` landed in v4.35.0-rc2, which is newer than the toolchain pinned in
+  # `.github/functional_test_toolchain`, so the `lake-check` test pins its own.
+  lake_check_toolchain: leanprover/lean4:v4.35.0-rc2
 
 jobs:
   # The default toolchain is pinned in `.github/functional_test_toolchain`
@@ -243,6 +246,34 @@ jobs:
           # axiom-audit builds with the project's toolchain, so use a recent one.
           toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
+  # `lake check` sandboxes with bubblewrap, which GitHub-hosted runners do not permit without a
+  # privileged change to the runner. Namespace serves a privileged container, which permits it
+  # outright, so that is where this runs. The `-with-features` suffix is what makes the feature
+  # label apply. These labels are per-organisation configuration, and a job whose labels an
+  # organisation does not serve sits queued rather than failing, so keep this to the repository
+  # known to be provisioned for them.
+  lake-check-namespace:
+    if: github.repository == 'leanprover/lean-action'
+    runs-on:
+      - nscloud-ubuntu-24.04-amd64-2x4-with-features
+      - namespace-features:container.privileged=true
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
+      - uses: ./.github/functional_tests/lake_check
+        with:
+          toolchain: ${{ env.lake_check_toolchain }}
+
+  # Pinned to a toolchain that predates `lake check`, rather than to the moving default: once the
+  # default supports it, this would otherwise quietly stop testing feature detection.
+  lake-check-unsupported-toolchain:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
+      - uses: ./.github/functional_tests/lake_check_unsupported
+        with:
+          toolchain: ${{ env.legacy_toolchain }}
+
   macos-runner:
     needs: resolve-toolchain
     runs-on: macos-latest

CHANGELOG.md

@@ -7,6 +7,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## Unreleased
 
+### Added
+
+- new `lake-check` input to check the project with `lake check`: build it and replay the result through one or more kernels inside a sandbox, erroring on any use of a non-standard axiom. `"true"` uses Lean's own kernel; `"paranoid"` additionally runs every external checker the toolchain bundles (`leanchecker-paranoid`, `lean4lean`, `nanoda`, `con-leche` and `con-ron`), none of which has to be built. Requires a Linux runner, Lean `v4.35.0-rc1` or newer (`"paranoid"` needs `v4.35.0-rc2`), and a runner permitting the user namespaces bubblewrap needs; see the README. Default: false
+- new `lake-check-status` output parameter
+
 ## v1.6.1 - 2026-10-02
 
 ### Changed

README.md

@@ -90,6 +90,7 @@ If `lean-action` is unable to successfully run the step, `lean-action` will fail
 - `mk_all-check`
 - `check-reservoir-eligibility`
 - `leanchecker`
+- `lake-check`
 - `nanoda`
 
 ### Automatic configuration
@@ -226,6 +227,17 @@ To be certain `lean-action` runs a step, specify the desire feature with a featu
     # Deprecated alias for `leanchecker`.
     lean4checker: ""
 
+    # Check the project with `lake check`: build it and replay the result through one or
+    # more kernels inside a sandbox, erroring on any use of a non-standard axiom.
+    # "true" checks with Lean's own kernel. "paranoid" additionally runs every external
+    # checker bundled with the toolchain: `leanchecker-paranoid`, `lean4lean`, `nanoda`,
+    # `con-leche` and `con-ron`. None of them has to be built.
+    # Requires a Linux runner, Lean `v4.35.0-rc1`+ ("paranoid" needs `v4.35.0-rc2`+), and a
+    # runner that permits the user namespaces bubblewrap needs.
+    # Allowed values: "true" | "false" | "paranoid".
+    # Default: "false"
+    lake-check: ""
+
     # Check environment with nanoda external type checker.
     # nanoda is an independent Lean 4 type checker written in Rust.
     # Requires Rust toolchain (will be installed automatically if not present).
@@ -286,6 +298,8 @@ To be certain `lean-action` runs a step, specify the desire feature with a featu
   - Values: "SUCCESS" | "FAILURE" | ""
 - `mk_all-status`
   - Values: "SUCCESS" | "FAILURE" | ""
+- `lake-check-status`
+  - Values: "SUCCESS" | "FAILURE" | ""
 - `nanoda-status`
   - Values: "SUCCESS" | "FAILURE" | ""
 - `axiom-audit-status`
@@ -374,6 +388,71 @@ Cap the parallelism by setting `LEAN_NUM_THREADS` on the `lean-action` step:
 
 Higher values trade memory for speed.
 
+## Independent kernel checks with `lake check`
+
+`lake check` builds the project, exports it, and replays the result through a kernel, erroring on
+any use of a non-standard axiom. It treats the project as untrusted input: the code is built and
+exported inside a sandbox, and none of its `.olean` files is loaded into Lake's own address space.
+The reference manual places this among the other ways to validate a proof, in
+[Validating a Lean Proof](https://lean-lang.org/doc/reference/latest/ValidatingProofs/#validating-comparator).
+
+```yaml
+- uses: leanprover/lean-action@v1
+  with:
+    lake-check: "paranoid"
+```
+
+`lake-check: "true"` checks with Lean's own kernel. `lake-check: "paranoid"` additionally runs
+every external checker the toolchain bundles: `leanchecker-paranoid`, `lean4lean`, `nanoda`,
+`con-leche` and `con-ron`. Release toolchains ship all of them, so nothing is cloned or compiled.
+
+Only the standard axioms are permitted, so a project containing a `sorry` is rejected and there is
+no option to allow one.
+
+`lake check` builds the project itself, inside the sandbox. Whether it is *also* built on the
+runner first is the `build` input's business: leaving `build` on is faster, because `lake check`
+then starts from a populated `.lake`, while `build: false` keeps the project's code off the runner
+entirely. Note that the rest of `lean-action` runs project code on the runner, so the action as a
+whole does not give you `lake check`'s isolation; run `lake check` directly for genuinely
+adversarial input.
+
+### Making the sandbox able to start
+
+bubblewrap needs unprivileged user namespaces, and not every runner permits them.
+
+**GitHub-hosted runners** restrict them, so `lake-check` fails there until you grant them. The
+narrowest way is an AppArmor profile covering `bwrap` alone; the blunt way is to lift the
+restriction for the whole runner:
+
+```yaml
+- run: sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0
+- uses: leanprover/lean-action@v1
+  with:
+    lake-check: "paranoid"
+```
+
+**Namespace runners** fail differently: jobs run in a container whose seccomp profile denies
+`pivot_root`, for root as well as for the job user, so relaxing user namespaces does not help.
+Request a privileged container instead, where the `-with-features` suffix on the machine label is
+what makes the feature apply:
+
+```yaml
+jobs:
+  verify:
+    runs-on:
+      - nscloud-ubuntu-24.04-amd64-8x16-with-features
+      - namespace-features:container.privileged=true
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1
+        with:
+          lake-check: "paranoid"
+```
+
+Such a container permits user namespaces too, so nothing else is needed there. These labels are
+per-organisation configuration: a job whose labels your organisation does not serve sits queued
+rather than failing.
+
 ## Axiom Allowlist Audit with axiom-audit
 
 [axiom-audit](https://github.com/leanprover-community/axiom-audit) checks that every declaration in your library depends only on an allowlist of axioms (by default `propext`, `Classical.choice`, `Quot.sound`). Because it inspects the compiled kernel environment, it catches what a `grep` cannot: `sorry`/`admit` (`sorryAx`), `native_decide` (`Lean.ofReduceBool`), and any home-rolled `axiom`, including ones reaching in through imports.

action.yml

@@ -118,6 +118,19 @@ inputs:
       Allowed values: "true" | "false".
     required: false
     default: "false"
+  lake-check:
+    description: |
+      Check the project with `lake check`: build it and replay the result through one or more
+      kernels inside a sandbox, erroring on any use of a non-standard axiom.
+      "true" checks with Lean's own kernel. "paranoid" additionally runs every external checker
+      bundled with the toolchain: `leanchecker-paranoid`, `lean4lean`, `nanoda`, `con-leche` and
+      `con-ron`. None of them has to be built: release toolchains ship all of them.
+      Requires a Linux runner, Lean `v4.35.0-rc1` or newer ("paranoid" needs `v4.35.0-rc2`), and
+      a runner that permits the user namespaces bubblewrap needs. See the README for what that
+      takes on GitHub-hosted and Namespace runners.
+      Allowed values: "true" | "false" | "paranoid".
+    required: false
+    default: "false"
   nanoda:
     description: |
       Check environment with nanoda external type checker.
@@ -204,6 +217,11 @@ outputs:
       If lean-action detected a mathlib dependency equals "true"
       otherwise equals "false".
     value: ${{ steps.detect-mathlib.outputs.detected-mathlib }}
+  lake-check-status:
+    description: |
+      The status of the `lake check` step.
+      Allowed values: "SUCCESS" | "FAILURE" | "".
+    value: ${{ steps.lake-check.outputs.lake-check-status }}
   nanoda-status:
     description: |
       The status of the nanoda check step.
@@ -355,6 +373,17 @@ runs:
       shell: bash
       working-directory: ${{ inputs.lake-package-directory }}
 
+    - name: check the project with lake check
+      id: lake-check
+      if: ${{ inputs.lake-check != 'false' }}
+      env:
+        LAKE_CHECK_INPUT: ${{ inputs.lake-check }}
+      run: |
+        : Check the project with lake check
+        ${GITHUB_ACTION_PATH}/scripts/run_lake_check.sh
+      shell: bash
+      working-directory: ${{ inputs.lake-package-directory }}
+
     - name: check environment with nanoda
       id: nanoda
       if: ${{ inputs.nanoda == 'true' }}