This PR promotes the `repeat`, `while`, and `repeat ... until` parsers
from `syntax` declarations in `Init.While` to `@[builtin_doElem_parser]`
definitions in `Lean.Parser.Do`, alongside the other do-element parsers.
The `while` variants and `repeat ... until` get `@[builtin_macro]`
expansions; `repeat` itself gets a `@[builtin_doElem_elab]` so a
follow-up can extend it with an option-driven choice between `Loop.mk`
and a well-founded `Repeat.mk`.
The new builtin parsers are registered at `low` priority so that the
bootstrapping `syntax` declarations in `Init.While` (still needed for
stage0 compatibility) take precedence during the transition. After the
next stage0 update, the `Init.While` syntax and macros can be removed.
This PR fixes a bug in EmitC that can be caused by working with the
string literal `"\x01abc"` in
Lean and causes a C compiler error.
The error is as follows:
```
run.c:29:189: error: hex escape sequence out of range
29 | static const lean_string_object l_badString___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 5, .m_capacity = 5, .m_length = 4, .m_data = "\x01abc"};
| ^~~~~~~
1 error generated.
```
This happens as hex escape sequences can be arbitrarily long while lean
expects them to cut off
after two chars. Thus, the C compiler parses the string as one large hex
escape sequence `01abc` and
subsequently notices this is too large.
Discovered by @datokrat
This PR names the `repeat` syntax (`doRepeat`) and installs dedicated
elaborators for it in both the legacy and new do-elaborators. Both
currently expand to `for _ in Loop.mk do ...`, identical to the existing
fallback macro in `Init.While`.
The elaborators are dead code today because that fallback macro fires
first. A follow-up PR will drop the macro (after this PR's stage0 update
lands) and extend `elabDoRepeat` to choose between `Loop.mk` and a
well-founded `Repeat.mk` based on a `backward.do.while` option.
This PR adds two validation checks to `addInstance` that provide early
feedback for common mistakes in instance declarations:
1. **Non-class instance check**: errors when an instance target type is
not a type class. This catches the common mistake of writing `instance`
for a plain structure. Previously handled by the `nonClassInstance`
linter in Batteries (`Batteries.Tactic.Lint.TypeClass`), this is now
checked directly at declaration time.
2. **Impossible argument check**: errors when an instance has arguments
that cannot be inferred by instance synthesis. Specifically, it flags
arguments that are not instance-implicit and do not appear in any
subsequent instance-implicit argument or in the return type. Previously
such instances would be silently accepted but could never be
synthesised.
Supersedes #13237 and #13333.
This PR globally enables `warning.simp.varHead` (added in #13325) and
silences the warning in `Lake.Util.Family.Mathlib` adaptations were
already merged as part of adaptations for #13325. This is a separate PR
from #13325 due to warning appearing when re-bootstrapping, so we needed
`stage0` update before enabling this option.
This PR fixes two minor bugs in `io.cpp`:
1. A resource leak in a Windows error path of
`Std.Time.Database.Windows.getNextTransition`
2. A buffer overrun in `IO.appPath` on linux when the executable is a
symlink at max path length.
This PR fixes `processDefDeriving` to propagate the `meta` attribute to
instances derived via delta deriving, so that `deriving BEq` inside a
`public meta section` produces a meta instance. Previously the derived
`instBEqFoo` was not marked meta, and the LCNF visibility checker
rejected meta definitions that used `==` on the alias — this came up
while bumping verso to v4.30.0-rc1.
`processDefDeriving` now computes `isMeta` from two sources:
1. `(← read).isMetaSection` — true inside a `public meta section`,
covering the original issue #13313.
2. `isMarkedMeta (← getEnv) declName` — true when the type being derived
for was individually marked `meta` (e.g. `meta def Foo := Nat`), via
`elabMutualDef` in `src/Lean/Elab/MutualDef.lean`.
This value is passed to `wrapInstance` for aux declarations and to the
new `addAndCompile (markMeta := ...)` parameter from #13311, matching
how the regular command elaboration pipeline handles meta definitions.
Existing regression tests `tests/elab/13043.lean` and
`tests/elab/12897.lean` already cover meta-section + `wrapInstance` aux
def interaction. The new `tests/elab/13313.lean` specifically covers the
delta-derived `BEq` + LCNF-use case (the original issue) and an explicit
`meta def ... deriving BEq` outside a meta section (motivating the
second disjunct).
- [ ] depends on: #13311Closes#13313🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR fixes#12846, where the new do elaborator produced confusing
errors when a do element's continuation had a mismatched monadic result
type. The errors were misleading both in location (e.g., pointing at the
value of `let x ← value` rather than the `let` keyword) and in content
(e.g., mentioning `PUnit.unit` which the user never wrote).
The fix introduces `DoElemCont.ensureUnitAt`/`ensureHasTypeAt`, which
check the continuation result type early and report mismatches with a
clear message ("The `do` element has monadic result type ... but the
rest of the `do` block has monadic result type ..."). Each do-element
elaborator (`let`, `have`, `let rec`, `for`, `unless`, `dbg_trace`,
`assert!`, `idbg`, etc.) now captures its keyword token via `%$tk` and
passes it to `ensureUnitAt` so that the error points at the do element
rather than at an internal elaboration artifact. The old ad-hoc type
check in `for` and the confusing `ensureHasType` call in
`continueWithUnit` are replaced by this uniform mechanism. Additionally,
`extractMonadInfo` now calls `instantiateMVars` on the expected type,
and `While.lean`/`If.lean` macros propagate token info through their
expansions.
Closes#12846
---------
Co-authored-by: Rob23oba <robin.arnez@web.de>
This PR fixes an issue in the expand reset reuse pass that causes
segfaults in very rare situations.
This bug occurs in situations where two projections from the same field
happen right before a reset,
for example:
```
let x.2 := oproj[0] _x.1;
inc x.2;
let x.3 := oproj[0] _x.1;
inc x.3;
let _x.4 := reset[1] _x.1;
```
when expand reset reuse we optimize situations like this to only `inc`
on the cold path as on the
hot path we are going to keep the projectees alive until at least
`reuse` by just not `dec`-ing the
resetee. However, the algorithm for this assumed that we do not project
more than once from each
field and thus removed both `inc x.2` and `inc x.3` which is too much.
The bug was masked compared to the original #13407 that was reproducible
in 4.29, because the
presented code relied on semantics of global constants which were
changed in 4.30. The PR contains a
modified (and more consistent) reproducer.
Closes: #13407
Co investigated with @Rob23oba
This PR fixes a panic when `coinductive` predicates are defined inside
macro scopes where constructor names carry macro scopes. The existing
guard only checked the declaration name for macro scopes, missing the
case where constructor identifiers are generated inside a macro
quotation and thus carry macro scopes. This caused
`removeFunctorPostfixInCtor` to panic on `Name.num` components from
macro scope encoding.
Closes#13415
This PR adds a basic support for `lake builtin-lint` command that is
used to run environment linters and in the future will be extend to deal
with the core syntax linters.
This PR adds an internal `skip` syntax for do blocks, intended for use
by the `if` and `unless` elaborators to replace `pure PUnit.unit` in
implicit else branches. This gives the elaborator a dedicated syntax
node to attach better error messages and location info to, rather than
synthesizing `pure PUnit.unit` which leaks internal details into
user-facing errors.
Includes a stage0 trigger comment so that the new parser is available
during bootstrapping.
Co-authored-by: Rob23oba <robin.arnez@web.de>
This PR fixes a bug where tactic auto-completion would produce tactic
completion items in the entire trailing whitespace of an empty tactic
block. Since #13229 further restricted top-level `by` blocks to be
indentation- sensitive, this PR adjusts the logic to only display
completion items at a "proper" indentation level.
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR adds level instantiation and normalization in `getDecLevel` and
`getDecLevel?` before calling `decLevel`.
`getLevel` can return levels with uninstantiated metavariables or
un-normalized structure, such as `max ?u ?v` where the metavariables
have already been assigned. After instantiation and normalization (via
`normalizeLevel`), a level like `max ?u ?v` (with `?u := 1, ?v := 0`)
simplifies to `1 = succ 0`, which `decLevel` can decrement. Without this
step, `decLevel` sees `max ?u ?v`, tries to decrement both arms, fails
on a zero-valued arm, and reports "invalid universe level".
Concretely, this fixes `for` loops with `mut` variables of
sort-polymorphic type (e.g. `PProd Nat True`) where the state tuple's
universe level ends up as an uninstantiated `max`.
The expected-output change in `doNotation1.lean` is because the `for`
loop's unit type now resolves to `Unit` instead of `PUnit` due to the
improved level handling.
This PR adds the option `LEAN_MI_SECURE` to our CMake build. It can be
configured with values `0`
through `4`. Every increment enables additional memory safety
mitigations in mimalloc, at the cost
of 2%-20% instruction count, depending on the benchmark. The option is
disabled by default in our
release builds as most of our users do not use the Lean runtime in
security sensitive situations.
Distributors and organization deploying production Lean code should
consider enabling the option as
a hardening measure. The effects of the various levels can be found at
https://github.com/microsoft/mimalloc/blob/v2.2.7/include/mimalloc/types.h#L56-L60.
This PR fixes the incorrect name `String.Pos.skipWhile_le` to be
`String.Pos.le_skipWhile`.
No deprecation since this is not in any release yet (also no release
candidate). `String.Slice.Pos.le_skipWhile` is correct, as are the
`revSkipWhile` counterparts.
This PR makes the `deriving Inhabited` handler for `structure`s be able
to inherit `Inhabited` instances from structure parents, using the same
mechanism as for class parents. This fixes a regression introduced by
#9815, which lost the ability to apply `Inhabited` instances for parents
represented as subobject fields. With this PR, now it works for all
parents in the hierarchy.
Implementation detail: adds `struct_inst_default%` for synthesizing a
structure default value using `Inhabited` instances for parents and
fields.
Closes#13372
This PR fixes#12827, where hovering over `for` loop variables `x` and
`h` in `for h : x in xs do` showed no type information in the new do
elaborator. The fix adds `Term.addLocalVarInfo` calls for the loop
variable and membership proof binder after they are introduced by
`withLocalDeclsD` in `elabDoFor`.
Closes#12827
This PR improves error reporting when the `do` elaborator produces an
ill-formed expression that fails `checkedAssign` in
`withDuplicableCont`. Previously the failure was silently discarded,
making it hard to diagnose bugs in the `do` elaborator. Now a
descriptive error is thrown showing the join point RHS and the
metavariable it failed to assign to.
Closes#12826
This PR fixes#12768, where the new `do` elaborator produced a
"declaration has free variables" kernel error when the bind
continuation's result type was definitionally but not syntactically
independent of the bound variable. The fix moves creation of the result
type metavariable before `withLocalDecl`, so the unifier must reduce
away the dependency.
For example, given `def Quoted (x : Nat) := Nat`, the expression `do let
val ← pure 3; withStuff val do return 3` would fail because `β` was
assigned `Quoted val` rather than `Nat`.
This PR adds warnings when registering `@[simp]` theorems whose
left-hand side has a problematic head symbol in the discrimination tree:
- **Variable head** (`.star` key): The theorem will be tried on every
`simp` step, which can be expensive. The warning notes this may be
acceptable for `local` or `scoped` simp lemmas. Controlled by
`warning.simp.varHead` (default: `true`).
- **Unrecognized head** (`.other` key, e.g. a lambda expression): The
theorem is unlikely to ever be applied by `simp`. Controlled by
`warning.simp.otherHead` (default: `true`).
This PR fixes a heap buffer overflow in `lean_io_prim_handle_read` that
was triggered through an
integer overflow in the size computation of an allocation. In addition
it places several checked
arithmetic operations on all relevant allocation paths to have potential
future overflows be turned
into crashes instead. The offending code now throws an out of memory
error instead.
Closes: #13388
This PR introduces the H1 module, a pure HTTP/1.1 state machine that
incrementally parses incoming byte streams and emits response bytes
without side effects.
This contains the same code as #10478, divided into separate pieces to
facilitate easier review.
The pieces of this feature are:
- Core data structures: #12126
- Headers: #12127
- URI: #12128
- Body: #12144
- H1: #12146
- Server: #12151
- Client:
---------
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
This PR changes the linear BEq derivation strategy to use `Nat.decEq`
instead of `decEq` when comparing constructor indices. Since constructor
indices are always `Nat`, using `Nat.decEq` directly is more appropriate
because it is `@[reducible]`, whereas the generic `decEq` is only
semireducible and does not unfold at `.reducible` transparency. This
makes the generated code more transparent-friendly.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes#13268 where `local macro` (and other local declarations)
with compound names of depth ≥ 3 would silently lose their local
entries.
When `expandNamespacedDeclaration` rewrites e.g. `local macro (name :=
A.B.C) ...` into `namespace A.B.C; end_local_scope; ...; end A.B.C`, the
compound `namespace A.B.C` pushes multiple scopes, but `end_local_scope`
only marked the topmost scope as non-delimiting. This meant
`addLocalEntry`'s stack traversal would stop at the first unmarked
scope, and the local entry would be lost when the namespace scopes were
popped.
The fix parameterizes `end_local_scope` with a depth argument so it
marks exactly the right number of scope levels as non-delimiting.
`expandNamespacedDeclaration` now passes `ns.getNumParts` as the depth,
and `expandInCmd` passes `1`.
Closes#13268
This PR fixes a compiler panic when a structure constructor receives a
noncomputable instance as an instance-implicit argument.
The LCNF translation first visits the instance in an irrelevant position
(type parameter) where `ignoreNoncomputable` is `true`, caches the
result, and then reuses that cached entry in a relevant position,
bypassing `checkComputable`. Adding `ignoreNoncomputable` to the cache
key ensures the two contexts do not share cache entries.
Fixes#13371
This PR adds a `linter.redundantVisibility` option (default `true`) that
warns
when a visibility modifier has no effect because it matches the default
for the
current context:
- `private` outside a `public section` in a `module` file, where
declarations
are already module-scoped by default
- `public` in a non-`module` file or inside a `public section`, where
declarations are already public by default
The check is integrated directly into `elabModifiers` so it covers all
declaration types uniformly.
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR fixes `SizeOf` instance generation for public inductive types
that have
private constructors. The spec theorem proof construction needs to
unfold
`_sizeOf` helper functions which may not be exposed in the public view,
so
we use `withoutExporting` for the proof construction and type check.
Closes#13373
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes git revision detection in worktrees where the worktree's
gitdir path passes through another git repository.
The vendored `GetGitRevisionDescription.cmake` module detects worktrees
and then calls `_git_find_closest_git_dir` to find the shared git
directory by walking up the filesystem looking for a `.git` entry. This
fails when the worktree's gitdir is stored inside another git repository
(e.g. when the project is a git submodule whose objects live at
`~/.git/modules/...` and `~` is itself a git repo) — the walk finds the
wrong `.git`.
The fix reads the `commondir` file that git places in every worktree's
gitdir, which directly points to the shared git object directory. Falls
back to the old filesystem walk if `commondir` doesn't exist (shouldn't
happen with any modern git, but safe to keep).
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Previously, `elabInitialize` only checked for explicit `private` when
deciding whether to mangle `fullId`, ignoring the `module` system's
default-private semantics. It also overrode the user's visibility for
the generated `initFn` via `visibility.ofBool`.
Now, `elabInitialize` uses `elabVisibility` + `isInferredPublic` to
correctly handle all visibility contexts. The generated `initFn`
inherits the user's visibility rather than being forced public.
Also factors out `elabVisibility` from `elabModifiers` for reuse.
This PR is based on a systematic review of all read-only operations on
the default containers in core. Where sensible it applies specialize
annotations on higher order operations that lack them or borrow
annotations on parameters that should morally be borrowed (e.g. the
container when iterating over it).
This PR changes the `Inhabited` deriving handler for `structure` types
to use default field values when present; this ensures that `{}` and
`default` are interchangeable when all fields have default values. The
handler effectively uses `by refine' {..} <;> exact default` to
construct the inhabitant. (Note: when default field values cannot be
resolved, they are ignored, as usual for ellipsis mode.)
Implementation note: the handler now constructs the `Expr` directly and
adds it to the environment, though the `instance` is still added using
`elabCommand`.
Closes#9463
This PR adds a check for OS-forbidden names and characters in module
names. This implements the functionality of `modulesOSForbidden` linter
of mathlib.
Instead of unconditionally wrapping value of fields that were copied
from flattened parent structures, try finding an existing instance and
projecting it first.
This PR extends Lean's syntax to allow explicit universe levels in
expressions such as `e.f.{u,v}`, `(f e).g.{u}`, and `e |>.f.{u,v} x y
z`. It fixes a bug where universe levels would be attributed to the
wrong expression; for example `x.f.{u}` would be interpreted as
`x.{u}.f`. It also changes the syntax of top-level declarations to not
allow space between the identifier and the universe level list, and it
fixes a bug in the `checkWsBefore` parser where it would not detect
whitespace across `optional` parsers.
Closes#8743
This PR changes the Lake core build to use `weakLeanArgs` for the Lake
plugin.
This fixes a trace mismatch between local builds and the CI caused by
the differing paths.
This PR fixes universe unification for `for` loops with `mut` variables
whose types span multiple implicit universes. The old approach used
`ensureHasType (mkSort mi.u.succ)` per variable, which generated
constraints like `max (?u+1) (?v+1) =?= ?u+1` that the universe solver
cannot decompose. The new approach uses `getDecLevel`/`isLevelDefEq` on
the decremented level, producing `max ?u ?v =?= ?u` which `solveSelfMax`
handles directly.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR wraps the top-level command parser with `withPosition` to
enforce indentation in `by` blocks, combined with an empty-by fallback
for better error messages.
This subsumes #3215 (which introduced `withPosition commandParser` but
without the empty-by fallback). It is also related to #9524, which
explores elaboration with empty tactic sequences — this PR reuses that
idea for the empty-by fallback, so that a `by` not followed by an
indented tactic produces an elaboration error (unsolved goals) rather
than a parse error.
**Changes:**
- `topLevelCommandParserFn` now uses `(withPosition commandParser).fn`,
setting the saved position at the start of each top-level command
- `tacticSeqIndentGt` gains an empty tactic sequence fallback
(`pushNone`) so that missing indentation produces an elaboration error
(unsolved goals) instead of a parse error
- `isEmptyBy` in `goalsAt?` removed: with strict `by` indentation, empty
`by` blocks parse successfully via `pushNone` (producing empty nodes)
rather than producing `.missing` syntax, making the `isEmptyBy` check
dead code. The `isEmpty` helper in `isSyntheticTacticCompletion`
continues to work correctly because it handles both `.missing` and empty
nodes from `pushNone` (via the vacuously-true `args.all isEmpty` on
`#[]`)
- Test files updated to indent `by` blocks and expression continuations
that were previously at column 0
**Behavior:**
- Top-level `by` blocks now require indentation (column > 0 for commands
at column 0)
- Commands indented inside `section` require proofs to be indented past
the command's column
- `#guard_msgs in example : True := by` works because tactic indentation
is checked against the outermost command's column
- Expression continuations (not just `by`) must also be indented past
the command, which is slightly more strict but more consistent
- `have : True := by` followed by a dedent now correctly puts `this` in
scope in the outer tactic block (the `have` is structurally complete
with an unsolved-goal error, rather than a parse error)
**Code changes observed in practice (lean4 test suite + Mathlib):**
- `by` blocks: top-level `theorem ... := by` / `decreasing_by` followed
by tactics at column 0 must be indented
- `variable` continuations: `variable {A : Type*} [Foo A]\n{B : Type*}`
where the second line starts at column 0 must be indented (most common
category in Mathlib)
- Expression continuations: `def f : T :=\nexpr` or `#synth Foo\n[args]`
where the body/arguments start at column 0
- Structure literals: `.symm\n{ toFun := ...` where the struct literal
starts at column 0
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
