Add FORK_STRATEGY.md documenting:
- Purpose: HoTT-compatible kernel extensions (Path types without UIP,
transport, HITs) for polytropos's meta-theory.
- Why kernel-level: library encodings via Quot leak UIP, incompatible
with univalence. Mirrors Cubical Agda's precedent.
- Sync strategy: track upstream leanprover/lean4, merge (not rebase),
preserve HoTT additions on conflict.
- Modification strategy: locality principle (new files under hott/
+ src/kernel/hott/ + src/Init/HoTT/); LEAN4-HTT: tag for modifications
to upstream files; compile-time feature flag (LEAN_HOTT) gates HoTT.
- Patch-series organization for phased primitive additions.
- Forbidden moves: no UIP at kernel level, no Quot.sound dependency for
HoTT reductions, no Classical.choice in HoTT primitives.
Add hott/ directory structure:
- hott/README.md describing the fork-specific directory's purpose.
- hott/design/ for architectural decisions per phase.
- hott/tests/ for HoTT-specific test suites.
No kernel modifications in this phase. Subsequent phases:
Phase 1: Path + Refl + J primitives
Phase 2: transport with computational behavior
Phase 3: HIT support
Phase 4: cubical primitives if needed
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR fixes an issue where `beforeElaboration` attributes were not
being run on `inductive`/`structure`/`coinductive` commands. Closes
#13433.
There is also light refactoring of MutualInductive, as well as a mild
performance enhancement to avoid repeated re-elaboration of `variable`s.
This PR updates the `#where` command to be able to report
`module`-related scope state, for example a `@[expose] public meta
section` line in the output.
This PR improves elaboration performance for structure instance notation
with large numbers of fields. It also uses beta-reducing substitution
for structure parameters, which is already the case for structure
fields.
It substitutes field values into types when they are needed, avoiding
quadratic runtime complexity.
This PR fixes `mconstructor`, `mleft`, and `mright` failing inside
`mhave` blocks (#13691), and `mspecialize` failing after a `mrevert;
mintro` round trip. Both cases stem from hypothesis-naming `Expr.mdata`
leaking from hypothesis-conjunction leaves into non-leaf positions (an
inner target, or the antecedent of an `SPred.imp` target), where
downstream pattern matches did not see through it.
Fixed by stripping the mdata at the offending non-leaf positions in
`elabMHave`, `elabMReplace`, and `mRevert`.
This PR modifies the app elaborator to beta reduce arguments while
substituting them into expected types for later arguments. This makes it
consistent with `inferType` and `instantiateMVars`, which both beta
reduce substitutions. In particular, this change ensures that the app
elaborator behaves as if it creates metavariables for each parameter and
assigns elaborated arguments to the metavariables. **Breaking change:**
tactic proofs may need to be modified to remove unnecessary steps, e.g.
`dsimp only` steps that were previously for beta reductions.
This PR enforces that Verso docstring extensions should always be meta
at attribute application time, giving better error messages, and ensures
that the generated argument parser helper is also meta and has the same
visibility.
This PR adds two new fields to `DoOps`, `splitMonadApp?` and
`mkMonadApp`, so that callers of `elabDoWith` can use indexed monads
like `Measure α` (where `Measure : (α : Type u) → [MeasureSpace α] →
Type u` carries instance arguments) that the default `m α` decomposition
cannot handle. The existing behavior moves into `DoOps.default`.
`splitMonadApp?` replaces the hard-coded `.app m α` step inside the
`extractMonadInfo` recursion, and `mkMonadApp` replaces the hard-coded
`mkApp m α` used to construct the monadic type.
---------
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR renames the `do` elaborator's `mkMonadicType` to `mkMonadApp`,
aligning it with the existing `mkPureApp` / `mkBindApp` naming
convention in `DoOps`.
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR generates specialized code for invoking `dec` on values whose
shape is known. This puts branch prediction pressure off
`lean_dec_ref_cold` as the shape of the constructor should now be
compiled into the executable.
If we're using the downloaded LLVM release and building stage2/stage3,
we need to also copy stage1 to stage2/stage3 respectively before
continuing the build. Previously, the CI did not do this in every case.
Now we do it unconditionally because the overhead is small enough.
This PR is part 2 to #13779. It completes the transition of the
configuration evaluation metaprograms into being builtin elaborators.
After this, building stage1 will not invoke the interpreter when
generating configuration evaluators. A tradeoff is that changes to
ConfigEval will not affect stage1 builds, but these changes ought to be
infrequent.
This PR makes the command elaborators for configuration evaluation
metaprogramming be builtins, to avoid bootstrapping ABI issues in core
Lean due to the interpreter evaluating large parts of the elaborator
before all builtin initializers are run. (This is part 1; #13780 will be
applied after a stage0 update.)
This PR eliminates the use of `liftCommandElabM` from the coinductive
module.
Context: `liftCommandElabM` was decided to be deprecated in issue
#10674.
This PR eliminates the use of `liftCommandElabM` in the `@[ext]`
attribute, since it is unnecessary — all the computations can stay in
`TermElabM`.
Context: `liftCommandElabM` was decided to be deprecated in issue
#10674.
This PR moves the `evalSuggest` combinator and trace-handler dispatch
from a hardcoded `match` on syntax kinds to the existing
`tryTacticElabAttribute` registration mechanism, bringing `try?`'s
extensibility model in line with normal tactics and interactive `grind`.
Each built-in combinator (`<;>`, `first`, `paren`, `try`, `attempt_all`,
`attempt_all_par`, `first_par`, `seq1`) and trace handler (`grind?`,
`simp?`, `simp_all?`, `exact?`) is now registered as
`@[builtin_try_tactic <kind>]`. `evalSuggestImpl` becomes a thin
attribute-driven dispatcher mirroring `evalTactic`/`evalGrindTactic`.
The post-run "no unsolved goals in terminal mode" check is no longer
applied centrally by the dispatcher. Handlers that may leave goals
open (`simp?`, `simp_all?`, the atomic fallback) call the new
`checkTerminalGoals` helper themselves; handlers that close the goal
by construction (`grind?`, `exact?`) and combinators that delegate via
`evalSuggest` need no explicit call.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR makes `try?`'s `expandUserTactic` walk the info tree for
`TryThisInfo`
nodes (introduced in #10524) instead of parsing the rendered `Try this:`
message
text. The previous approach scraped lines prefixed with ` [apply] ` from
the
message log, which would break the moment that wire format changed.
The user tactic is run under `withSaveInfoContext` so the in-flight
trees come
out wrapped with a `PartialContextInfo.commandCtx`, which is what
`InfoTree.foldInfo` needs in order to descend; the structured
suggestions can
then be read directly from the `TryThisInfo` nodes that
`TryThis.addSuggestion`
already pushes. The prior manual `Core.setMessageLog` save/restore dance
is no
longer needed.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR fixes premise selection silently dropping relevant premises when
the goal was reached via `induction`.
`MVarId.getRelevantConstants` and `MVarId.getConstants` walked the raw
goal type returned by `getType`, which after `induction` is `?motive
arg` with `?motive` an assigned-but-unsubstituted metavariable. The
constant fold treats the metavariable as an opaque leaf, so every
constant in the goal predicate is lost. Instantiating metavariables
first recovers them.
Thanks to Xavier Généreux for the report.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR does some refactoring of the function application elaborator,
and it improves `trace.Elab.app` tracing. It also improves asymptotic
complexity by more carefully substituting arguments into the function's
type and by changing how named argument dependency suppression is
implemented. For dot notation, it now constructs base projections
directly rather than using the app elaborator. It fixes a bug in the eta
args feature where more explicit arguments would be turned into implicit
arguments than expected, and it improves expected type propagation by
following the rules from the main app elaborator.
This PR refines MePo premise selection so that (1) candidates are
restricted to theorems, matching the convention already used by
`SineQuaNon` and `SymbolFrequency`, and (2) the result is ordered
lexicographically by `(iteration, score)` rather than by score alone.
Before the theorem filter, `mepoSelector` returned functions, recursors,
and casts (e.g. `Int.add`, `Eq.ndrec`, `cast`, `proof_irrel`) alongside
real premises. With it, those go away and the obvious lemmas — e.g.
`Int.add_comm` for `a + b = b + a` — rank well above the remaining
noise.
The `(iteration, score)` ordering preserves the iteration priority of
the original Meng–Paulson MePo: an iter-1 premise scoring 0.6 always
ranks above an iter-2 premise scoring 1.0, since later iterations score
against a strictly larger `relevant` set and a higher threshold, so
their raw scores are not comparable.
Thanks to Xavier Généreux for the report. Further tuning of the score
function (the remaining problem: small generic theorems still score 1.0)
is tracked in https://github.com/leanprover/lean4/issues/13749.
Depends on https://github.com/leanprover/lean4/pull/13747.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR an intermittent test failure in the Lake environment test caused
by its reuse of the hello test's configuration. The tests are now
properly independent.
This PR closes https://github.com/leanprover/lean4/issues/13770 by
including `Config.zetaUnused` in `Config.toKey`. Without this, two
configs that differ only in `zetaUnused` share a `WHNF`/`isDefEq` cache
key, so reductions performed under one setting can be returned for the
other. The new bit sits at position 22, immediately above `zetaHave`.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR fixes a long-standing bug in `Meta.Config.toKey` and
`Context.setTransparency` where `TransparencyMode` was packed into only
2 bits of the cache key, even though it has 5 constructors (`.all`,
`.default`, `.reducible`, `.instances`, `.none`). The `.none` case
(value `4`, i.e. `0b100`) overlapped with the `foApprox` bit, so
configurations differing only in transparency vs. `foApprox` could
collide in the `isDefEq`/`WHNF` cache, and `Context.setTransparency`
corrupted the neighbouring bit when switching to/from `.none`.
The fix widens the transparency field to 3 bits and shifts every
subsequent flag up by one. Split out from
https://github.com/leanprover/lean4/pull/13637 where the same fix was
needed anyway to accommodate a 6th transparency constructor.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR fixes the MePo premise selector returning its lowest-scoring
premises instead of its best ones.
Since https://github.com/leanprover/lean4/pull/10917 `mepo` returns
suggestions in score-descending order, but `mepoSelector` still applied
a `.reverse` that predated that change. The `.reverse` flipped the order
to score-ascending, so the subsequent `.take config.maxSuggestions` kept
the `maxSuggestions` worst premises.
Thanks to Xavier Généreux for the report.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR removes the `addInfo` flag from `elabSetOption` introduced in
#11313, instead allowing callers to use `withEnableInfoTree` to control
whether infotrees are added.
This PR adds `MessageData.withExprHover`, for creating messages that
show information about an expression when hovered over. A
`withExprHoverM` variant captures the current local context.
This PR fixes an issue where the `pp.universes` option would cause
constants with no universes to not use unexpanders or dot notation. For
example, `p ↔ q` would pretty print as `Iff p q` even though `Iff` has
no universe levels.
This PR improves `Expr.instantiateBetaRevRange` to be more efficient in
the common case where lambda functions are not being instantiated, and
it increases expression sharing in applications.
The motivation is that we would like to use this function more
pervasively in elaboration, so that users do not need to write `dsimp
only` as frequently in applications that involve higher-order functions,
plus `inferType` uses it so there is a UX inconsistency when the
elaborator is not using it.
This PR adds new incremental module serialization functions that
save/load a single module at a time with explicit sharing via dep
regions and compactor state, generalizing the existing batch
saveModuleDataParts API.
Two sharing mechanisms that can be mixed:
- `CompactedRegion` dep regions for sharing with loaded regions
- `CompactorState` for same-process chaining (pre-loaded `m_obj_table`)
This PR adds the missing `ByteArray` push and `set!` lemmas that are
still carried locally in `ZipForStd.ByteArray` downstream.
These lemmas provide one coherent API layer for reasoning about
`ByteArray` pushes and `set!` updates on top of the existing upstream
append, extract, and size lemmas. Previous downstream code had to keep
local compatibility lemmas for these common proof steps.
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR adds `Dyadic.divAtPrec a b prec`, returning the greatest dyadic
with precision at most `prec` which is less than or equal to `a/b` (and
`0` when `b = 0`). Mirroring the existing `invAtPrec`, the
characterising lemmas `divAtPrec_mul_le` and `lt_divAtPrec_add_inc_mul`
are also provided.
Compared to composing `invAtPrec` with multiplication, `divAtPrec`
rounds `a/b` down uniformly (no sign-dependent rounding flip), states
the precision at the output rather than requiring callers to back-solve
from `‖a‖`, and fuses the bignum division with renormalisation.
`invAtPrec` remains the right primitive when the reciprocal is reused.
Closes https://github.com/leanprover/lean4/issues/13653.
🤖 Prepared with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR changes the separator between the plugin file name and the
initialization function in `--plugin` from `:` to `=`. This prevents
clashes with the `:` in drive prefixes on Windows.
