Add eink0rn, a clean-room Lean 4 kernel in Haskell - #177
Merged
Conversation
eink0rn normalises the surface language away before checking anything: nested inductives are compiled to mutual blocks, every mutual block is flattened to a single indexed family, and recursors are rederived from the inductive specification rather than believed. No Lean kernel source of any kind was read; the references were Carneiro's thesis, the NDJSON format spec, and this arena's verdicts. Accepts all four exports and declines nothing, in 19s / 35s / 2m17s / 14m53s at a 12.85 GB peak on mathlib. Runs with --enforce-mutual-univ so that it is scored on the same language as every other checker. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Collaborator
|
Interesting contribution! As for running this, can you add ghc to the flake setup so that system dependencies are documented there? |
eink0rn is one `ghc --make` over the GHC boot libraries -- no cabal, no package index -- so the compiler alone is the whole system dependency. Without it the checker's build script installs 9.6.6 with ghcup, which works but documents nothing and costs 2m 55s and 2.6 GB of the build. nixos-26.05's ghc is newer than the 9.6.6 eink0rn is developed against; it was built and tested on 9.10.3 as well, which passes both of its test suites and accepts `std` in the same time. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The preamble still read as instructions for producing this file rather than as a note on the file itself. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
It was 531 words where the next longest entry is 148. What is left is what distinguishes the checker; the resource argument it dropped is already spelled out in the comments around the run line, and the rest belongs in the repository it points at. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
Author
|
Done! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds
checkers/eink0rn.yamlas a kernel implementation written in Haskell. It wasgenerated mostly by Claude, with direction to do as much of a clean-room implementation
as possible, referring only to ndjson spec+tests, and Carneiro's thesis.
Notes for the runner
The build is one
ghc --make: eink0rn depends on the GHC boot libraries andnothing else, so there is no package index to fetch and nothing to resolve.
tools/arena-build.shtries every GHC it can find and installs 9.6.6 with ghcupif none of them can build it.
Run "naturally" the build uses more than the allotted 16GB on runner --
its multithreading is somewhat aggressive, and it caches a lot. This build script
deliberately caps the memory, and is set to eight threads.
Happy to adjust the entry - flags, timeout, description - to whatever
suits the arena.