ci: Replace Forgive with lake check

.github/workflows/ci.yml

@@ -39,7 +39,13 @@ jobs:
           lean --version
 
       - run: lake build Foundation --wfail
-      - run: just forgive
+      # `lake check` sandboxes the project with `bwrap`, which the runner image does not ship and
+      # whose user namespaces Ubuntu 24.04 restricts for unprivileged users by default.
+      - name: Install bubblewrap
+        run: |
+          sudo apt-get install -y --no-install-recommends bubblewrap
+          sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0
+      - run: just kernel-check
 
       # A merge-queue commit becomes `master` as is, so publishing it there lets the push run that
       # follows, and the jobs below, restore it instead of compiling it again.

Justfile

@@ -14,13 +14,15 @@ cache:
 build:
     lake build Foundation --wfail
 
-forgive:
-    lake exe forgive Foundation
+# Rebuild and replay the project through the kernel in a sandbox, rejecting `sorry` and any axiom
+# outside `propext`, `Classical.choice`, `Quot.sound`.
+kernel-check:
+    lake check
 
 mk-all:
     lake exe mk_all --module --lib Foundation
 
-check: build forgive
+check: build kernel-check
     lake exe mk_all --module --lib Foundation --check
 
 format-references:

contribute/alpha-centauri.md

@@ -39,7 +39,7 @@ From the worktree root:
 1. `lake build <module>` with `--wfail`: no errors or warnings.
 2. `lake build Foundation`.
 3. `just mk-all`: no diff in `Foundation.lean`.
-4. `just forgive`.
+4. `just kernel-check`.
 5. No `sorry` in the ported files.
 6. `lake shake --keep-public <module>`, dropping the imports it reports as redundant (not the project-wide `just shake`, which passes `--fix`).
 7. No development-time artifacts (`grep -n "see plan\|issue #\|Step [0-9]\|§[0-9]\|L[0-9]-[0-9]\|PR [0-9]"`).

contribute/index.md

@@ -36,7 +36,7 @@ PRs (title and body) are written in English.
 ## Before submitting
 
 - The affected modules build with `lake build --wfail`, which turns every warning (including a remaining `sorry`) into an error.
-- 🤖 Run `just forgive` and confirm it passes before submitting a PR. This checks sorry-freeness and the axiom allowlist across the project, and CI re-runs it on every PR — a failing audit blocks the merge.
+- 🤖 Run `just kernel-check` (`lake check`) and confirm it passes before submitting a PR. It rebuilds the project in a `bwrap` sandbox, replays it through the kernel, and rejects `sorry` and axioms outside the allowlist (`propext`, `Classical.choice`, `Quot.sound`). It needs `bubblewrap` and takes several minutes. CI re-runs it on every PR — a failing audit blocks the merge.
 - Run import-all to keep `Foundation.lean` up to date:
   ```shell
   just mk-all

contribute/style.md

@@ -162,7 +162,7 @@ Register a new function with `@[primrec]`, stating the lemma pointwise — `Prim
 
 ## No `sorry`
 
-`sorry` is never acceptable in submitted proofs. CI runs `just forgive`, which fails the build on any remaining `sorry` (as well as on axioms outside the allowlist) — a proof left in a skeleton state cannot land. If a proof is incomplete, keep it out of the PR rather than submitting it with `sorry` placeholders.
+`sorry` is never acceptable in submitted proofs. CI runs `lake check` (`just kernel-check`), which fails the build on any remaining `sorry` (as well as on axioms outside the allowlist) — a proof left in a skeleton state cannot land. If a proof is incomplete, keep it out of the PR rather than submitting it with `sorry` placeholders.
 
 ## `set_option`
 

lake-manifest.json

@@ -1,17 +1,7 @@
 {"version": "1.3.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/FormalizedFormalLogic/forgive",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "bd8a14884321a120ff973c1a2f5f6856b1068232",
-   "name": "Forgive",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.35.0",
-   "inherited": false,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/doc-gen4",
+ [{"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
@@ -31,16 +21,6 @@
    "inputRev": "v4.35.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover",
-   "rev": "c24fe6078c630e89b489bffe59b3e20ac30d12c8",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.35.0",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/leansqlite",
    "type": "git",
    "subDir": null,
@@ -51,6 +31,16 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "c24fe6078c630e89b489bffe59b3e20ac30d12c8",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,

lakefile.toml

@@ -40,8 +40,3 @@ rev = "v4.35.0"
 scope = "leanprover"
 name = "doc-gen4"
 rev = "v4.35.0"
-
-[[require]]
-name = "Forgive"
-git = "https://github.com/FormalizedFormalLogic/forgive"
-rev = "v4.35.0"