Repository navigation
Conversation
Collaborator
Author
|
!bench |
github-actions
Bot
added
the
toolchain-available
Collaborator
Author
|
!bench |
|
Benchmark results for f1b97ea against da4295a are in. There are significant results. @nomeata
Large changes (5✅, 153🟥)
Medium changes (3✅, 137🟥)
Small changes (12✅, 2559🟥)
|
Collaborator
Author
|
!bench |
|
Benchmark results for c19e9cc against da4295a are in. There are significant results. @nomeata
Large changes (5✅, 214🟥)
Medium changes (3✅, 149🟥)
Small changes (11✅, 2572🟥)
|
Collaborator
Author
|
!bench |
|
Benchmark results for cf1c79f against da4295a are in. There are significant results. @nomeata
Large changes (5✅, 203🟥)
Medium changes (4✅, 141🟥)
Small changes (10✅, 2582🟥)
|
Collaborator
Author
|
!bench |
|
Benchmark results for feb42b1 against da4295a are in. There are significant results. @nomeata
Large changes (8✅, 189🟥)
Medium changes (4✅, 118🟥)
Small changes (9✅, 2608🟥)
|
Collaborator
Author
|
!bench |
|
Benchmark results for 522ac85 against da4295a are in. There are significant results. @nomeata
Large changes (5✅, 170🟥)
Medium changes (6✅, 123🟥)
Small changes (8✅, 2620🟥)
|
`Lean.Replay` (used by `leanchecker`, also `--from-export`) replays constants in dependency order, but a literal records no dependency on `Nat`/`String` and their constructors, which the InLean kernel requires to be present before it types a literal. Replay them first. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This PR makes InLean, the Lean port of con-leche's verified checker added in `src/Lean/Kernel/InLean/`, the kernel, and deletes the C++ type checker, inductive-type and quotient modules (`src/kernel/{type_checker,inductive,quot}.cpp`).
The kernel entry points `lean_add_decl`, `lean_add_decl_without_checking`, `lean_elab_add_decl`, `lean_elab_add_decl_without_checking` and `lean_kernel_{is_def_eq,whnf,check}` are `@[export]` functions in the new module `Lean.Kernel.InLean.Core`, which `Lean` now imports; the `@&` borrow annotations of their `@[extern]` declarations in `Lean.Environment` are dropped, as an `@[export]` function takes owned arguments. `Kernel.Environment.add`, `markQuotInit` and `Environment.updateBaseAfterKernelAdd` stay private; `Core` reaches them with `import all Lean.Environment`. The C++ helpers only the old checker used are deleted; `mk_rec_name` moves to `library/util`.
`addDecl` honours the C++ kernel's limits: the nesting depth is bounded by 16 times `maxRecDepth`, numerals by `LEAN_NAT_MAX_SIZE`, and the checker polls the cancellation token and `maxHeartbeats`. Kernel errors are `Kernel.Exception.other "(InLean) …"`, with the C++ kernel's wording where the check is the same. In core the axiom policy is the official kernel's (any axiom, `sorryAx` usable); a STOPGAP flag (`uncertifiedNatOps`) lets the literal fast path fire on pinned Nat operations whose certificates cannot be checked in Init's source order or that a `module` importer sees as axioms. A second quotient declaration is a no-op, as in the C++ kernel.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The kernel reports its errors as `Kernel.Exception.other "(InLean) …"`, so the tests that compare kernel error text expect that text; where InLean's message differs from the C++ kernel's (e.g. a type mismatch in `12520_1`, projections of indexed structure-like types, which the kernel declines in `inductive_rec_proj`), the tests expect InLean's. * `issue14484`: the error of `assumptionFreeFalse` is now shown: the C++ kernel's message mentioned the synthetic `sorry` in the axiom's type and was filtered, InLean's text does not. * `10475`: `Kernel.check` substitutes the `let` values in the inferred type, so the types are `True` and `Prop`; the second check succeeds as the issue requires. * `grind_nestedDecidable_kernel_issue` also checks its regular-wrapper control. * `completion7` and `completionEOF` declare their own `And` in a `prelude` file; InLean reserves the names of the basis blocks it pins, so they use `Duo` (the same length, so the positions stay). * `kernelQuotNameCollision` is deleted: it declares an axiom at `Quot.lift` before `init_quot` and expects the quotient declaration to be rejected; InLean reserves the quotient's names and rejects the axiom itself, so that situation cannot arise. * `inleanQuotTwice` (new) checks that a second quotient declaration is a no-op. * The `leanchecker` and `module` package tests expect the new messages. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
nomeata
force-pushed
the
joachim/inlean-kernel
branch
from
November 12, 2026 00:12
522ac85 to
409fb81
Compare
Collaborator
Author
|
!bench |
|
Benchmark results for 409fb81 against 1c92992 are in. There are significant results. @nomeata
Large changes (7✅, 148🟥)
Medium changes (3✅, 91🟥)
Small changes (25✅, 2218🟥)
|
This branch has not been deployed
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
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.
This PR replaces the kernel's C++ type checker with InLean, a Lean port of the con-leche checker that works directly on
Lean.ExprandLean.Kernel.Environmentand that con-leche proves sound. It is based on the companion PR from branchjoachim/inlean-add, which adds InLean (src/Lean/Kernel/InLean/) to the stdlib without using it, together with the Lean bodies ofExpr.mkData,Expr.mkAppDataandLevel.mkDataand a cherry-pick of #16146; the split lets the benchmarks show the cost of compiling InLean separately from the cost of switching the kernel. This PR's own diff is the switch:src/kernel/{type_checker,inductive,quot}.cppand the C++ helpers only they used are deleted, and the new moduleLean.Kernel.InLean.Coreprovideslean_add_decl,lean_elab_add_decl(and their_without_checkingvariants) andlean_kernel_{is_def_eq,whnf,check}as@[export]functions;Leanimports it instead ofLean.Kernel.InLean.AddDecl.Lean.Replayreplays a literal's support declarations (Nat,Stringand their constructors) before it, as InLean requires them to be present. The rest ofsrc/Lean/Kernel/InLean/is the checker. It is generated from con-leche'sInLean/by a script that only adds the copyright header andprelude, renames the namespace and drops InLean's copy ofInit.Util'swithIsExclusive(con-leche's toolchain, v4.35.0, lacks it). The core (whnf, inference, definitional equality) follows con-leche's cached checker function by function. Inductive declarations go through an unverified generator (IndGen, the generating half ofinductive.cpp); nothing it produces is added unless con-leche's verified inductive check accepts it. It is an experiment, opened for discussion and to run CI.What is proved (in con-leche,
InLeanProof/AddDeclProof.lean).InLeanProof.addDeclSound: let a kernel environment be related to a con-leche environment that has a model of Lean's type theory, and let InLean accept a safe, non-axiom declaration into it. Then an extension of that con-leche environment, still with a model, is related to the new kernel environment. The relationEnvRelsays that InLean finds a constant at a name exactly where con-leche's environment does, with related entries and projection tables, and that every projection body InLean builds is in range. Proofs ignoreunsafeandpartialconstants (InLean hides them from safe checks), and the relation allowssorryAxon Lean's side. The theorem holds for every setting of the resource limits below. A corollary,InLeanProof.no_false, says that starting from an environment with a model, InLean never adds a safe constant of typeFalse. The proof is a simulation of con-leche's cached checker, whose soundness con-leche proves against its set-theoretic model. It uses the axiomspropext,Classical.choiceandQuot.sound, plus three facts aboutExpr.mkData,Expr.mkAppDataandLevel.mkData. Con-leche states these three as axioms; with the companion PR they are theorems about the new Lean bodies (tests/elab/expr_mkData_bodies.lean;Expr.mkDatatakes a 32-bit hash here, a 64-bit one in con-leche's v4.35.0). The proof stops short of the following, which remain trusted:Kernel.Environment.find?andaddbehave as maps;Core.lean, whoseunsafeBaseIOreads the heartbeat counter and the cancellation token and counts unfoldings;Init.Util'swithIsExclusive, which reads a reference count only to decide what to memoize;The theorem is stated for con-leche's axiom policy. The kernel here runs under the official one (
coreAxioms) and takes the prelude'sNatoperations as given (uncertifiedNatOps).The kernel is slower than the C++ one. Measured on 2026-11-08, on the v4.35.0 base and before the last round of changes, a stage2 build cost 15 % more instructions. In
elab_bench,big_struct_dep1cost 4.0 times the instructions,big_match2.1 times,mut_rec_wf1.7 times,big_beqandbig_beq_rec1.5 times, andbig_struct1.4 times. Its allocations count against the elaborator'smaxHeartbeats. Measured on 2026-11-09 at this head: everyelab_benchfile passes at bench size (TEST_BENCH=1), and the#mutual_blockcommand ofderiving_mutual_blocktakes 182.2 M heartbeats (the limit is 200 M; 268.5 M before the recursor telescopes were closed in one pass).Test changes. With them, all tests pass locally except
elab/async_systems_info, which fails in our sandbox on an unmodified build too.Deleted:
elab_fail/kernelQuotNameCollision: InLean rejects a declaration at a reserved name unless it matches its pin. The axiom the test declares beforeinit_quotis therefore rejected up front, and the collision under test cannot arise. Note that the elaborator keeps the rejected axiom, andinit_quotthen panics inAsyncConsts.add("duplicate normalized declaration name"). The C++ kernel could hit this too; no test covers it now.Semantics changes, expectations updated:
elab/inductive_rec_proj: projections of an indexed structure-like type are declined. Meta issue: Lean Kernel Logic renovation #14977 keeps projections only for non-indexed types.elab/10475:Kernel.checkreturns the type withlets substituted. The issue is about the result being closed, which still holds; the expectation now readsTrue/Prop.elab/grind_nestedDecidable_kernel_issue: the control case, which replacesGrind.nestedDecidableby a definition with aregularhint, no longer times out. The C++ kernel spends its heartbeats comparing theDecidable.reflects_decideproofs' types; InLean does not reduce these proofs.Rewritten to avoid an incidental clash:
server_interactive/completion7andcompletionEOFdeclared their ownAndin apreludefile, where InLean expects the pinnedAnd. It is renamedDuo(same length, so the tested positions stay).Error text only, expectations updated. The verdicts are the C++ kernel's; the messages are
(InLean) …, worded like the C++ ones where the check is the same:elab:10577,bvarcrash,impossibleTactic,invalidProjection,issue10424,issue12746,issue9018,issue_14576,issue_14576_min,issue_14576_nonuniform,kernelErrorFollowup,kernelImaxProp,kernelMutualDupName,kernelNestedAuxName,kernelProjIdx,magical,mutualLevelParams,nat_size_limit,pow_exploit,recconstructorcrash,reprove,skipKernelTC,thmIsProp;elab_fail:1781,2125,partialIssue,sanitychecks;pkg:leanchecker(AddFalse,ReplaceAxiom),module(PartialImported).elab/12520_1matches the rejection's exception: it now also accepts InLean's.othermessage for the type mismatch.issue14484gains a#guard_msgs, because the C++ message contained a syntheticsorryand was filtered out, while InLean's is shown.Added:
elab/inleanQuotTwicechecks that a second quotient declaration is a no-op, as in the C++ kernel (Lean.Replaysends one for each quotient constant).In the companion PR:
elab/expr_mkData_bodieschecks the new Lean bodies against the C implementations,elab/csimpCorelists InLean's@[csimp]lemmas, and perf: hash all bits of largeNatliterals inExpr#16146 addselab/issue15686.The kernel keeps these behaviours: the limits
maxRecDepth(16 times, on the checker's nesting depth),maxHeartbeats(allocations since the kernel was entered, where the C++ kernel counted its own steps), the cancellation token,LEAN_NAT_MAX_SIZE(with #14849's evaluation ofNat.powandNat.shiftLeftat any 32-bit second argument) and the diagnostics' unfold counters; and the C++ messages for an unsafe or partial constant used in a safe declaration. Two binder telescopes are compared asis_def_eq_bindingdoes, each domain and the innermost bodies instantiated once. Theorems are never unfolded, as #14977 plans, and proof irrelevance is tried before head normalisation, as the C++ kernel does since #15103.🤖 Generated with Claude Code