feat: add lake-check-sandbox to make the sandbox startable

.github/functional_tests/lake_check/action.yml

@@ -4,6 +4,10 @@ inputs:
   toolchain:
     description: 'Toolchain to use for the test'
     required: true
+  sandbox:
+    description: 'Value for the `lake-check-sandbox` input. GitHub-hosted runners need one; a privileged Namespace container needs none.'
+    required: false
+    default: 'none'
 runs:
   using: 'composite'
   steps:
@@ -27,6 +31,7 @@ runs:
       with:
         use-github-cache: false
         lake-check: paranoid
+        lake-check-sandbox: ${{ inputs.sandbox }}
 
     - name: verify lake check success on the clean package
       env:
@@ -50,6 +55,7 @@ runs:
       with:
         use-github-cache: false
         lake-check: paranoid
+        lake-check-sandbox: ${{ inputs.sandbox }}
 
     - name: verify lake check failure once a sorry is introduced
       env:

.github/workflows/functional_tests.yml

@@ -264,6 +264,16 @@ jobs:
         with:
           toolchain: ${{ env.lake_check_toolchain }}
 
+  lake-check:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v7
+      - uses: ./.github/functional_tests/lake_check
+        with:
+          toolchain: ${{ env.lake_check_toolchain }}
+          # GitHub-hosted runners restrict the user namespaces bubblewrap needs.
+          sandbox: apparmor
+
   # 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:

CHANGELOG.md

@@ -11,6 +11,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 - 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
+- new `lake-check-sandbox` input (`"none"` | `"apparmor"` | `"sysctl"` | `"setuid"`, default `"none"`) choosing how to make bubblewrap's sandbox able to start on a runner that restricts unprivileged user namespaces, as GitHub-hosted runners do. `"apparmor"` is narrowest: it grants the capability through an AppArmor profile and leaves the restriction in force for everything else. `lean-action` never changes a runner's configuration unless asked, and only when the sandbox is found not to work
 
 ## v1.6.0 - 2026-08-22
 

README.md

@@ -420,17 +420,29 @@ adversarial input.
 
 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:
+**GitHub-hosted runners** restrict them, so `lake-check` fails there until you grant them. Set
+`lake-check-sandbox` to have `lean-action` do it:
 
 ```yaml
-- run: sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0
 - uses: leanprover/lean-action@v1
   with:
     lake-check: "paranoid"
+    lake-check-sandbox: "apparmor"
 ```
 
+| value | effect |
+| --- | --- |
+| `"none"` (default) | Change nothing. `lake-check` fails if the sandbox cannot start. |
+| `"apparmor"` | Install an AppArmor profile granting bubblewrap, and the processes it starts, permission to create user namespaces. The restriction stays in force for everything else, so this is the narrowest option and the usual choice. |
+| `"sysctl"` | Relax `kernel.apparmor_restrict_unprivileged_userns`. Affects every program on the runner. |
+| `"setuid"` | Install `bwrap` setuid root. |
+
+All three need passwordless sudo and are applied only when the sandbox is found not to work, so a
+runner that already permits user namespaces is left untouched. None of them is undone afterwards:
+on a persistent self-hosted runner they outlive the job, so prefer configuring such runners once
+yourself and leaving this at `"none"`. `"apparmor"` and `"setuid"` refuse to act on anything but a
+root-owned distribution bubblewrap, and never on one named by `COMPARATOR_BWRAP`.
+
 **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

action.yml

@@ -131,6 +131,26 @@ inputs:
       Allowed values: "true" | "false" | "paranoid".
     required: false
     default: "false"
+  lake-check-sandbox:
+    description: |
+      How to make `lake check`'s bubblewrap sandbox able to start, when it cannot.
+      GitHub-hosted runners restrict the unprivileged user namespaces bubblewrap needs, so
+      `lake-check` fails there without one of these. A runner that already permits them, such as
+      a privileged Namespace container, needs nothing.
+      "none" changes nothing, and `lake-check` fails with an error naming this input.
+      "apparmor" installs an AppArmor profile granting bubblewrap, and the processes it starts,
+      permission to create user namespaces, leaving the runner's restriction in force for
+      everything else. The narrowest option, and the usual choice on GitHub-hosted runners.
+      "sysctl" relaxes `kernel.apparmor_restrict_unprivileged_userns`, which affects every
+      program on the runner.
+      "setuid" installs `bwrap` setuid root.
+      All three need passwordless sudo, are applied only when the sandbox is found not to work,
+      and are not restored afterwards: on a persistent self-hosted runner they outlive the job.
+      "apparmor" and "setuid" are applied only to a root-owned distribution bubblewrap, never to
+      one named by COMPARATOR_BWRAP.
+      Allowed values: "none" | "apparmor" | "sysctl" | "setuid".
+    required: false
+    default: "none"
   nanoda:
     description: |
       Check environment with nanoda external type checker.
@@ -378,6 +398,7 @@ runs:
       if: ${{ inputs.lake-check != 'false' }}
       env:
         LAKE_CHECK_INPUT: ${{ inputs.lake-check }}
+        LAKE_CHECK_SANDBOX_INPUT: ${{ inputs.lake-check-sandbox }}
       run: |
         : Check the project with lake check
         ${GITHUB_ACTION_PATH}/scripts/run_lake_check.sh

scripts/run_lake_check.sh

@@ -35,6 +35,15 @@ case "$mode" in
         ;;
 esac
 
+sandbox_setup="${LAKE_CHECK_SANDBOX_INPUT:-none}"
+case "$sandbox_setup" in
+    none | apparmor | sysctl | setuid) ;;
+    *)
+        failure_message="\`lake-check-sandbox\` must be \"none\", \"apparmor\", \"sysctl\" or \"setuid\", got \"${sandbox_setup}\""
+        exit 1
+        ;;
+esac
+
 # `lake check` sandboxes the code it checks with bubblewrap, which needs Linux namespaces; Lake
 # refuses to run anywhere else, so say so here rather than letting it fail further in.
 runner_os="$(uname -s)"
@@ -94,11 +103,94 @@ fi
 # reported as a setup problem naming the remedy, not as a failed check: `lake check` exits 1 both
 # when it rejects a project and when bubblewrap fails to start, so by the time it has run the two
 # are hard to tell apart.
+#
+# Exercise the namespace and mount operations Lake itself uses, not just a bind: a runner can
+# permit `--ro-bind` and still refuse the sandbox Lake actually builds.
 sandbox_probe_output=""
 sandbox_works() {
-    sandbox_probe_output="$("$sandbox_exe" --ro-bind / / true 2>&1)"
+    sandbox_probe_output="$("$sandbox_exe" --unshare-all --ro-bind / / --proc /proc --dev /dev true 2>&1)"
+}
+
+# Privileged setup is only ever applied to a distribution bubblewrap at a root-owned path. The
+# executable to modify would otherwise be decided by PATH or by COMPARATOR_BWRAP, and neither
+# establishes that the target is bubblewrap or that modifying it is safe.
+assert_trusted_sandbox_exe() {
+    if [ -n "${COMPARATOR_BWRAP:-}" ]; then
+        failure_message="\`lake-check-sandbox: ${sandbox_setup}\` will not modify the executable named by COMPARATOR_BWRAP. Provision that sandbox yourself, or unset COMPARATOR_BWRAP to use the distribution's bubblewrap."
+        exit 2
+    fi
+    if [ -L "$sandbox_exe" ]; then
+        failure_message="\`lake-check-sandbox: ${sandbox_setup}\` will not modify ${sandbox_exe}, which is a symbolic link; the target it resolves to today need not be the one modified."
+        exit 2
+    fi
+    case "$sandbox_exe" in
+        /usr/bin/bwrap | /bin/bwrap) ;;
+        *)
+            failure_message="\`lake-check-sandbox: ${sandbox_setup}\` only modifies a distribution bubblewrap at /usr/bin/bwrap or /bin/bwrap, and this runner's is at ${sandbox_exe}. Grant it user namespaces yourself instead."
+            exit 2
+            ;;
+    esac
+    if [ "$(stat -c '%U' "$sandbox_exe")" != "root" ]; then
+        # `chmod u+s` on a file owned by the job user grants that user's own privileges, not
+        # root's, so it would not make the sandbox work and would not mean what it appears to.
+        failure_message="\`lake-check-sandbox: ${sandbox_setup}\` will not modify ${sandbox_exe}, which is not owned by root."
+        exit 2
+    fi
 }
 
+if ! sandbox_works; then
+    case "$sandbox_setup" in
+        apparmor)
+            # Ubuntu's own mechanism: the restriction denies unprivileged user namespaces to
+            # programs whose AppArmor profile does not grant `userns`. Granting it here covers
+            # bubblewrap and the processes it starts, which inherit an unconfined profile; it does
+            # not cover the rest of the runner.
+            assert_trusted_sandbox_exe
+            if ! command -v apparmor_parser > /dev/null 2>&1; then
+                failure_message="\`lake-check-sandbox: apparmor\` needs \`apparmor_parser\`, which is not on this runner. Use \"sysctl\" or \"setuid\" instead."
+                exit 2
+            fi
+            if [ -e /etc/apparmor.d/bwrap ]; then
+                failure_message="\`lake-check-sandbox: apparmor\` will not overwrite the existing AppArmor policy at /etc/apparmor.d/bwrap. Remove it, or grant bubblewrap user namespaces yourself."
+                exit 2
+            fi
+            echo "::warning::\`lake-check-sandbox: apparmor\` is installing an AppArmor profile granting ${sandbox_exe}, and the processes it starts, permission to create user namespaces. The runner's restriction stays in force for everything else. On a persistent self-hosted runner the profile outlives this job."
+            if ! sudo tee /etc/apparmor.d/lean-action-bwrap > /dev/null <<PROFILE
+abi <abi/4.0>,
+include <tunables/global>
+
+profile lean-action-bwrap ${sandbox_exe} flags=(unconfined) {
+  userns,
+  include if exists <local/lean-action-bwrap>
+}
+PROFILE
+            then
+                failure_message="\`lake-check-sandbox: apparmor\` could not write /etc/apparmor.d/lean-action-bwrap. This runner probably does not offer passwordless sudo."
+                exit 2
+            fi
+            if ! sudo apparmor_parser -r /etc/apparmor.d/lean-action-bwrap; then
+                failure_message="\`lake-check-sandbox: apparmor\` could not load the AppArmor profile for ${sandbox_exe}. Use \"sysctl\" or \"setuid\" instead."
+                exit 2
+            fi
+            ;;
+        sysctl)
+            echo "::warning::\`lake-check-sandbox: sysctl\` is relaxing kernel.apparmor_restrict_unprivileged_userns on this runner. This affects every program on the runner, not just bubblewrap, and nothing restores it: on a persistent self-hosted runner it stays relaxed for later jobs too. \`lake-check-sandbox: apparmor\` is narrower."
+            if ! sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0; then
+                failure_message="\`lake-check-sandbox: sysctl\` could not set \`kernel.apparmor_restrict_unprivileged_userns\`. This runner either does not have that knob, in which case its sandbox is blocked by something else, or does not offer passwordless sudo."
+                exit 2
+            fi
+            ;;
+        setuid)
+            assert_trusted_sandbox_exe
+            echo "::warning::\`lake-check-sandbox: setuid\` is installing ${sandbox_exe} setuid root. The setuid bit persists on disk, so on a persistent self-hosted runner it outlives this job."
+            if ! sudo chmod u+s "$sandbox_exe"; then
+                failure_message="\`lake-check-sandbox: setuid\` could not make ${sandbox_exe} setuid root. This runner probably does not offer passwordless sudo."
+                exit 2
+            fi
+            ;;
+    esac
+fi
+
 if ! sandbox_works; then
     # The remedy depends on which half of the sandbox was refused, so name the one that fits.
     # A denied uid map means user namespaces are blocked; a denied `pivot_root` means the job is