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.
This PR adds a `trace.profiler.serve` option that, when enabled, serves
the Firefox Profiler-compatible profile JSON on an ephemeral `127.0.0.1`
port and opens `https://profiler.firefox.com/from-url/...` in the user's
default browser, à la `samply`. The server shuts down once the profile
has been fetched.
Compared to `trace.profiler.output`, which writes the profile to a file
that the user must then manually upload to `profiler.firefox.com`, this
is a single-command workflow not touching the file system.
Implementation notes:
* `Std.Http.Server` now exposes the bound socket address so the caller
can read back the OS-assigned ephemeral port when binding to port `0`.
* `addTraceAsMessages` and the import-time trace recording now check a
shared `trace.profiler.isExporting` predicate; the previous
`trace.profiler.output`-only check would otherwise consume the trace
state before serving could see it.
This PR introduces stricter inference for the `@[defeq]` attribute and a
companion `@[backward_defeq]` attribute that preserves the pre-PR
behavior
as an opt-in.
### What changed
* `@[defeq]` is now inferred only when the equation holds at
`.instances` transparency (the transparency `dsimp` operates at).
* `@[backward_defeq]` is the old set: every theorem whose `rfl` proof
the legacy inference would have accepted is tagged `@[backward_defeq]`,
so `defeq ⊆ backward_defeq` holds by construction.
* The option `backward.defeqAttrib.useBackward` (default `false`) makes
`dsimp` also use `@[backward_defeq]` theorems, restoring the pre-PR
behavior for a specific proof or file.
* The option is eqn-affecting: its value at the point of a function's
definition is recorded so that the equation lemmas later generated for
that function use the same value, regardless of the ambient option at
the use site.
### Mathlib adaption
A companion adaption branch (`lean-pr-testing-backward-defeq-attrib` on
mathlib4) builds cleanly against this PR and passes `lake test` without
warnings. Most adaption changes are scoped
`set_option backward.defeqAttrib.useBackward true in` additions on the
failing declarations; a small number of files needed proof-level edits
where the stored form of a `dsimp%`/`@[reassoc]`/`@[elementwise]`
/`@[simps]`/`@[to_app]`-generated lemma had drifted under the stricter
regime.
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR generalizes the `while` syntax in `do` blocks so that the
condition can be any `doIfCond`, the same condition form already
accepted by `if`. As a result, `while let pat := e do …` and `while let
pat ← e do …` are now supported in addition to `while cond do …` and
`while h : cond do …`. The previously separate `doWhile` and `doWhileH`
parsers and their accompanying macros are unified into a single
`doWhile` parser whose macro delegates to the existing `doIf`
desugaring.
This PR fixes `inferControlInfoSeq` and `ControlInfo.sequence` to keep
aggregating `breaks`/`continues`/`returnsEarly`/`reassigns` past
elements whose `ControlInfo` reports `numRegularExits := 0`. Previously
the analysis short-circuited at such elements, so any trailing
`return`/`break`/`continue` was missing from the inferred info. The
elaboration framework only skips subsequent doElems syntactically for
top-level `return`/`break`/`continue`; for every other `numRegularExits
== 0` case (e.g. a `match`/`if`/`try` whose branches all terminate, or a
`repeat` without `break`) the elaborator keeps visiting the continuation
and the for/match elaborator then tripped its invariant check with
`Early returning ... but the info said there is no early return`. With
this change the inferred info matches what the elaborator actually sees,
which also removes the need for the `numRegularExits := 1` workaround on
`repeat` introduced in #13479.
This PR removes the transitional `macro_rules` for `repeat`, `while`,
and `repeat ... until` from `Init.While`. After the latest stage0
update, the `@[builtin_macro]` and `@[builtin_doElem_elab]` definitions
in `Lean.Elab.BuiltinDo.Repeat` are picked up directly, so the bootstrap
duplicates in `Init.While` are no longer needed. `Init.While` now only
provides the `Loop` type and its `ForIn` instance.
This PR also adjusts `repeat`'s `ControlInfo` to match `for ... in`: its
`numRegularExits` is now unconditionally `1` rather than `if info.breaks
then 1 else 0`. Reporting `0` when the body has no `break` causes
`inferControlInfoSeq` (in any enclosing sequence whose `ControlInfo` is
inferred — e.g. a surrounding `for`/`if`/`match`/`try` body) to stop
aggregating after the `repeat` and miss any `return`/`break`/`continue`
that follows. The corresponding elaborator then sees the actual control
flow disagree with the inferred info and throws errors like `Early
returning ... but the info said there is no early return`. The new test
in `tests/elab/newdo.lean` pins down the regression. See
[#13437](https://github.com/leanprover/lean4/pull/13437) for further
discussion.
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 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 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 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 adds an opt-in linter (`set_option simp.rfl.checkTransparency
true`) that warns when a `rfl` simp theorem's LHS and RHS are not
definitionally equal at `.instances` transparency. Bad rfl-simp theorems
— those that only hold at higher transparency — create problems
throughout the system because `simp` and `dsimp` operate at restricted
transparency. The linter suggests two fixes: use `id rfl` as the proof
(to remove the `rfl` status), or mark relevant constants as
`[implicit_reducible]`.
This is part of a broader effort to ensure `isDefEq` respects
transparency levels. The linter helps systematically identify
problematic rfl-simp theorems so they can be fixed incrementally.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR marks any exposed (non-private) auxiliary match declaration as
`[implicit_reducible]`. This is essential when the outer declaration is
marked as `instance_reducible` — without it, reduction is blocked at the
match auxiliary. We do not inherit the attribute from the parent
declaration because match auxiliary declarations are reused across
definitions, and the reducibility setting of the parent can change
independently. This change prepares for implementing the TODO at
`ExprDefEq.lean:465`, which would otherwise cause too many failures
requiring manual `[implicit_reducible]` annotations on match
declarations whose names are not necessarily derived from the outer
function.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a new option `backward.isDefEq.respectTransparency.types`
that controls the transparency used when checking whether the type of a
metavariable matches the type of the term being assigned to it during
`checkTypesAndAssign`. Previously, this check always bumped transparency
to `.default` (via `withInferTypeConfig`), which is overly permissive.
The new option uses `.instances` transparency instead (via
`withImplicitConfig`), matching the behavior already used for implicit
arguments.
The option defaults to `false` (preserving old behavior) until stage0 is
updated and breakage is assessed. If
`backward.isDefEq.respectTransparency` (already in v4.29) is set to
`false`, then `backward.isDefEq.respectTransparency.types` is
automatically treated as `false` too.
When `diagnostics` is enabled, a trace message is emitted if the
stricter transparency fails but `.default` would have succeeded, helping
identify affected code. To investigate failures when enabling
`backward.isDefEq.respectTransparency.types`, use:
```
set_option diagnostics true
set_option trace.diagnostics true
```
Also renames `withInstanceConfig` to `withImplicitConfig` since it now
serves implicit argument and type checking, not just instances.
Registers the `diagnostics` trace class in `CoreM`.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `deprecated_syntax` command that marks syntax kinds as
deprecated. When deprecated syntax is elaborated (in terms, tactics, or
commands), a linter warning is emitted. The warning is also emitted
during quotation precheck when a macro definition uses deprecated syntax
in its expansion.
The `deprecated_syntax` command takes a syntax node kind, an optional
message, and a `(since := "...")` clause. Deprecation warnings correctly
attribute the warning to macro call sites when the deprecated syntax is
produced by macro expansion, including through nested macro chains.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
The stage0 tree hash used by Lake to invalidate stage 1 oleans was
computed via `git ls-tree HEAD`, which fails in jj workspaces (no .git
directory). Fall back to discovering the backing git repo via `jj git
root` and resolving the current workspace's commit via `jj log -r @`
(since git's HEAD points to the root jj workspace, not the current one).
