Add eink0rn, a clean-room Lean 4 kernel in Haskell

checkers/eink0rn.yaml

@@ -0,0 +1,91 @@
+# Source of truth: https://github.com/Timeroot/eink0rn (tools/arena-checker.yaml),
+# so that the recipe travels with the thing it builds.  `rev` there is the
+# commit `ref` points at, filled in on the way here.
+description: |
+  **eink0rn** — a Lean 4 kernel in Haskell, written clean-room, that normalises
+  the surface language away before checking anything.
+
+  - **One inductive type, one recursor.** Nested inductives are compiled to
+    mutual blocks and every mutual block is then flattened to a single indexed
+    family, so the core never sees a nested occurrence or a mutual one.
+  - **Recursors are derived, not believed.** The eliminator and its iota rules
+    are rebuilt from the inductive specification and the exported ones must
+    match, so no export can smuggle in an unwarranted large elimination or an
+    extra reduction rule.
+  - **Clean room.** No Lean kernel source of any kind was read — not `lean4`,
+    not `lean4lean`, not `trepplein`, not `nanoda`. The references were
+    Carneiro's *The Type Theory of Lean*, the NDJSON format specification, and
+    this arena's verdicts.
+
+  The type theory it does implement is written down normatively in `SPEC.md`,
+  and every place it knowingly departs from official Lean is argued in §12 —
+  including the one `--enforce-mutual-univ` turns off below, so that the
+  language scored here is the language every other checker is scored on.
+  Nothing is declined; `mathlib` fits by naming a heap ceiling rather than a
+  ratio.
+version: "1.1.2"
+url: https://github.com/Timeroot/eink0rn
+ref: v1.1.2
+rev: f01ab3cff7795227194463a09e443ef95c4e46a2
+threads: 8
+build: bash tools/arena-build.sh
+# Exit codes are the arena's: 0 accept, 1 reject, 2 declined, 3 a fault in the
+# checker.  A crash is never reported as a rejection.
+#
+# One flag is not about resources.  --enforce-mutual-univ turns off the only
+# place where this kernel accepts a file that official Lean refuses (a mutual
+# inductive block whose types do not all end in the same sort), so that what
+# the arena scores is the same language everyone else is being scored on.  It
+# is a setting and not a repair: with it off the block is derived from
+# admissible declarations and checked, rather than waved through.  No export
+# lean4export produces contains such a block, so it changes no verdict here.
+#
+# The remaining divergences have no such switch, or none worth throwing.  The
+# arithmetic licence of SPEC 6.5 is deliberate in both directions and its
+# --nat-accel=always mode is unsound on purpose -- it exists so that a file the
+# two settings disagree on isolates the rule, not to be run in anger.
+# --pin-std is an extra audit rather than a compatibility knob: it can only
+# reject more than official Lean, never less.  --keep-proofs would close a
+# theoretical false-reject (sealing a proof can only make a reduction stick),
+# but no corpus has ever exhibited one, and keeping every mathlib proof body is
+# exactly what does not fit in this runner.
+#
+# The rest are all mathlib, measured on a box with room to spare and then
+# squeezed back into sixteen gigabytes:
+#
+#   --mem=4000  the live-set budget the thread controller aims at.  Given
+#               explicitly rather than left to the adaptive default, so that
+#               the verdict does not depend on what /proc/meminfo says inside
+#               the runner.
+#   -M13g       the ceiling, and the one flag that decides whether mathlib
+#               fits.  It is a real limit -- over it the checker declines
+#               rather than taking the runner's 16 GB down with it -- but it
+#               also shapes the run well below the limit, because the RTS
+#               collects the oldest generation in place above 30% of -M and
+#               reins in how far the heap may run ahead of the live set as it
+#               approaches -M.  That is the whole point of stating a ceiling
+#               rather than a ratio: mathlib peaks at 12.8 GB under it and at
+#               21.1 GB with it raised out of reach, while the three smaller
+#               exports never come near it and are collected at the fast
+#               default, paying nothing for a flag they do not need.
+#   -A32m       small nursery: eight of them, and the survivors of a big one
+#               are what the old generation has to absorb.
+#
+# The timeout is the same idea for the clock: a decline, not a wrong answer,
+# and not a job that runs the matrix out of its 360 minutes.  mathlib took 15
+# minutes of it on a box under other load; every other export is minutes.
+#
+# The two rewritten statuses are both resource limits reported as such.  124 is
+# the timeout above.  251 is the RTS's own heap-limit exit, taken when the live
+# set grows so fast between two collections that the limit is passed by more
+# than the grace the handler needs to print DECLINE itself; either way -M did
+# its job, and neither is a judgement about the file.
+run: |
+  timeout 5400 ./arena/eink0rn --enforce-mutual-univ --mem=4000 -j8 "$IN" \
+    +RTS -A32m -M13g -RTS
+  rc=$?
+  case $rc in
+    124) exit 2 ;;
+    251) exit 2 ;;
+    *)   exit $rc ;;
+  esac

flake.nix

@@ -27,6 +27,7 @@
           opam
           gmp
           zig
+          ghc
         ];
       };
     };