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.
This PR replaces the previous tactic configuration system with a
significantly more efficient one that supports custom configuration
syntaxes and processing. On a simple benchmark, configuration evaluation
takes 6.2% of the time it used to. The `declare_config_elab` command
generates a configuration elaborator that now directly constructs
configuration objects; previously it relied on `Meta.evalExpr'`, which
involved running a configuration through the full term elaboration,
compilation, and evaluation processes. The generated configuration
elaborators now also have the capability to do direct `Syntax`
evaluation in common cases, skipping term elaboration. Furthermore, the
elaborator accepts configurations more liberally: any user-defined
syntax that has the form of an `optConfig`-style configuration or
configuration item (including, e.g., `namedArgument`s) is accepted.
Import `Lean.Elab.ConfigEval` to use the system; see this module for
some documentation in addition to the docstrings in
`Lean.Elab.ConfigEval.Commands`. Furthermore, the `simp` tactic now also
has `(user.optionName := ...)` user configuration options, which can be
declared using a global `tactic.simp.user.optionName` option; use
`getUserConfigOption` and `withUserConfig` to access and set these in
metaprograms.
Other features:
- `declare_config_elab` creates a function that exposes an `init`
parameter for the configuration that will be modified. It also now has a
`where` clause, enabling defining custom handlers for specific keys.
- Elaborators can be given additional binders, to make parameterized
elaborators. This is used by `simp` and `grind ` to support multiple
default configurations with the correct expected type for `(config :=
...)` elaboration.
- The `EvalTerm` class supports direct evaluation of `Syntax`, skipping
term elaboration. The system will attempt to automatically derive this
class when generating the elaborator.
- In case `EvalTerm` does not recognize the term, then the syntax is
elaborated to an expression and an `EvalExpr` instance is applied to
evaluate the expression. The system will similarly automatically derive
these instances if possible.
- Automatic derivation is *transitive*. It is able to seek instances
through other instances; e.g. if it needs an `EvalTerm (List T)`
instance it will be able to reduce this to seeking an `EvalTerm T`
instance.
- The system is designed to be flexible, and the various components can
be combined to construct a configuration elaborator. There are also now
`declare_core_config_elab` and `declare_term_config_elab` for
conveniently generating elaborators for `CoreM` and `TermElabM`. The
difference is that the first takes an explicit flag for whether to log
exceptions, and the second uses the current `errToSorry` state.
**Warning:** if you use the `TermElabM` one from `TacticM`, it will be
unaware of the current `recover` state. The only differences between
these macros are the ways error recovery is handled per monad.
Other changes:
- `#reduce` tactic configuration now makes use of this system and has
more options
- The module `Lean.Elab.Tactic.ConfigSetter` is removed; the
`declare_config_elab`-family macros subsume its functionality.
- The module `Lean.Elab.Tactic.Config` is deprecated and will be
removed; migration notes appear in the module docs there. Import
`Lean.Elab.ConfigEval` instead.
- One of the mvcgen benchmarks got significantly slower, but it turned
out to be caused by the new tactic configuration elaboration no longer
resetting the MetaM caches. Adding an explicit `resetCache` into the
test driver fixed the benchmark.
### Notes for metaprogram authors
If you are using the module system, you just need a `meta import
Lean.Elab.ConfigEval` to use the macros, and it should serve as a
drop-in replacement to the previous system so long as
1. your configuration type is a `structure` with no parameters, indices,
or universes (only `Type` is supported);
2. default values are self-contained and not dependent on other fields;
and
3. all fields have types that are composed from `Option`, `List`,
`Array`, `String`, `DataValue`, and inductive types in `Type` with no
parameters or indices, whose fields are similarly composed.
The macros synthesize a self-contained configuration elaboration
procedure, analyzing the `EvalTerm` and `EvalExpr` instances that are
currently available or can be automatically derived. These are the
components of the system:
- `EvalTerm` instances provide `Term → TermElabM α` functions for
evaluation of raw syntax; these handle the common cases where an option
value is a identifier, application, or other simple expression. They are
responsible for adding TermInfo when info is enabled, to support hovers.
One can invoke derivation of a `EvalTerm T` instance with the
`ensure_eval_term_instance T` command (after `open scoped
Lean.Elab.ConfigEval`).
- `EvalExpr` instances provide `Expr → TermElabM α` functions for
evaluation of elaborated expressions; these handle cases where an option
value may require reduction to evaluate. Similarly, one can invoke
derivation of an `EvalExpr T` instance with the
`ensure_eval_expr_instance T` command. If needed, there's also
`derive_eval_expr_instance_using_meta_eval T` for creating a
`Meta.evalExpr'`-based evaluator.
- Functions like `ConfigEval.evalExprWithElab` compose `EvalTerm` and
`EvalExpr` instances into a single procedure that first attempts
`EvalTerm`, and, if that fails, applies the standard term elaborator and
then attempts `EvalExpr`. This way term elaboration can be skipped in
all but uncommon cases.
- Configuration item interpretation is through `ConfigEval.foldConfigM`,
which is a procedure with a lax specification for what counts as a
configuration item, calling the provided function on each recognized
configuration item. The idea is:
- Null nodes are lists of configurations
- One-argument nodes are considered to be wrappers like `optConfig` or
`configItem`
- Two-argument nodes of the form `("+"<|>"-") (atom<|>ident)` are
considered to be boolean options
- Five-argument nodes of the form `"(" (atom<|>ident) ":=" syntax ")"`
are considered to be general configuration items. (It only checks for
the presence of `(` and that there are two-to-five arguments.)
- Bare atoms are considered to be positive boolean options
- Configuration evaluation then uses `EvalConfigItem.set` on each item
produced by the fold, for an `EvalConfigItem` structure defined for the
given configuration type. The `def_eval_config_item` command can be used
to generate this structure. It analyzes which `EvalTerm` and `EvalExpr`
instances exist and derives missing ones, then builds an efficient
procedure to process configuration items and apply evaluators.
- Lastly, there are the `declare_core_config_elab`,
`declare_term_config_elab`, `declare_config_elab`, and
`declare_command_config_elab` macros for conveniently running the
`def_eval_config_item` command and constructing a self-contained
elaboration function.
The derivation procedures analyze which `EvalTerm`/`EvalExpr` instances
already exist and only derive the "leaf" instances that are necessary to
construct `EvalTerm` and `EvalExpr` instances. The derived instances are
made `private local` — since configuration elaborators are meant to be
self-contained, we decided not to let the additional instances be a side
effect of the macros. The instances can be globally added by manually
using the `ensure_*` commands.
The macros support making parameterized elaborators with arbitrary
additional binders. See `make_elab_grind_config` and
`make_elab_simp_config` in core Lean for examples of generating a single
elaborator that's used with multiple default value configurations.
To see how to create a key handler that matches all configuration keys
with a given prefix, see `make_elab_simp_config`.
There is a todo item at `Lean.Elab.ConfigEval.ReflectConfigItems` for
reflecting configurations back to syntax, which is not yet supported.
### Performance evaluation
A legacy configuration parser was temporarily added to
`Lean.Elab.Tactic.Grind.Config` using `declare_term_config_elab_legacy
elabGrindConfigLegacy Grind.Config`, and then this file was used for
measuring elaboration time:
```lean
import Lean
open Lean Elab Meta Tactic Parser
def cfgs : Array Syntax := Unhygienic.run do
return #[
← `(Tactic.optConfig| ),
← `(Tactic.optConfig| +clean),
← `(Tactic.optConfig| +trace +markInstances -lookahead -useSorry),
← `(Tactic.optConfig| (trace := true) (markInstances := true) (lookahead := false) (useSorry := false)),
← `(Tactic.optConfig| -trace (splits := 20) +revert (maxSuggestions := some 3) (ematch := 2)),
← `(Tactic.optConfig| (gen := 5) -reducible +splitImp -funCC),
← `(Tactic.optConfig| (config := { trace := true, lookahead := false, maxSuggestions := some 3 })),
]
def testGrindElab (cfgs : Array Syntax) (n : Nat) : TacticM Unit := do
profileitM Exception "test grind elab" (← getOptions) do
let mut ematch := 0
for _ in [0:n] do
for cfg in cfgs do
let c ← Tactic.elabGrindConfig cfg
ematch := ematch + c.ematch
logInfo m!"sum = {ematch}"
def testGrindElabLegacy (cfgs : Array Syntax) (n : Nat) : TacticM Unit := do
profileitM Exception "test grind elab legacy" (← getOptions) do
let mut ematch := 0
for _ in [0:n] do
for cfg in cfgs do
let c ← Tactic.elabGrindConfigLegacy cfg
ematch := ematch + c.ematch
logInfo m!"sum = {ematch}"
def runTest (info : Bool) (test : TacticM Unit) : TermElabM Unit := do
withEnableInfoTree info do
let mvar ← mkFreshExprMVar none
discard <| Tactic.run mvar.mvarId! test
set_option maxHeartbeats 0
set_option profiler true
set_option profiler.threshold 1
def iters : Nat := 1000
#eval runTest false <| testGrindElab cfgs iters
#eval runTest true <| testGrindElab cfgs iters
#eval runTest false <| testGrindElabLegacy cfgs iters
#eval runTest true <| testGrindElabLegacy cfgs iters
```
A representative output is
```
test grind elab took 315ms
test grind elab took 333ms
test grind elab legacy took 5.22s
test grind elab legacy took 5.33s
```
Computing `(315.0 + 333.0) / (5220 + 5330)` and rounding up to the
nearest tenth gives the 6.2% figure.
---
The #13426 draft PR includes some LSP modifications to support
completions for `simp` user configuration options.
This PR upstreams `unusedDecidableInType` linter from mathlib.
Stacked on top of #11313.
---------
Co-authored-by: thorimur <thomasmurrills@gmail.com>
Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
This PR improves the logic and performance of the
`checkImpossibleInstance` function to detect more arguments that are
impossible to
infer for typeclass synthesis. It also improves the formatting of the
error messages for `checkImpossibleInstance` and `checkNonClassInstance`
to be more readable.
This integrates [independent (temporarily merged)
work](https://github.com/leanprover-community/batteries/pull/1717) on
these former Batteries linters which has been reverted in Batteries
because of the unprecedented upstreaming of these linters.
We also disable these checks (if the declaration contains any `sorry`s
so that partially completing instances is still possible without being
terrorized by obvious errors. We also swap the order of the checks, such
that now `checkNonClassInstance` is called first - it would be wrong to
warn for synthesis impossibility if the return type isn't even
synthesizable because it is not class-valued.
Co-authored by: @thorimur
---------
Co-authored-by: Wojciech Rozowski <wojciech@lean-fro.org>
This PR fixes a regression introduced in #7166 where, after fixed and
varying
parameters were allowed to be reordered, three places in
`Lean.Elab.Structural.FindRecArg` still indexed the concatenation `xs ++
ys`
with `recArgInfo.recArgPos` even though `recArgPos` refers to the
original
parameter order. With fixed parameters interleaved with the structural
argument, this picked the wrong element: error messages named the wrong
parameter, and `argsInGroup`'s nested-inductive recognition silently
rejected
otherwise-valid mutual definitions.
All three sites now use `recArgInfo.fixedParamPerm.buildArgs xs ys` so
the
index matches `recArgPos` and `indicesPos`.
Closes#13729.
This PR improves hovers and completions for compound field names in
structure instance notation. Previously a field like `x.fst` would only
have information associated to `x` attached to the entire syntax, but
now `x` and `fst` are treated separately.
Additionally, the `trace.Elab.struct` trace class is now
`trace.Elab.structInst`, and the messages have been cleaned up and
reorganized. Furthermore, `ExceptToTraceResult` has an `Expr` instance
that shows a failure emoji when there are synthetic sorries. Lastly,
`Syntax.identComponents` has an early return for names with at most one
component, saving a re-parsing step.
This PR fixes toml_escape so it does not emit moreLeancArgs = [""] when
internal leanc flags are both empty (the combined placeholder was only
whitespace). This led GCC to see an extra empty argv entry and fail with
a confusing linker error.
Co-authored-by: Cursor <cursoragent@cursor.com>
This PR resurrects the tests about cancellation of `try?` tactics.
They were flaky before. By introducing an option
(`debug.tactic.try.onlyUserSuggestions`) to make these tests not run
`exact?` as part of `try?`, and thus be generally faster and use less
memory, the flakiness seems to have disappeared, at least in
non-`master` testing. We’ll see.
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR improves the message of `unusedVariables` linter, by replacing
potentially confusing "unused variable `x`" message with "Variable name
`x` is not explicitly referenced. The binding can be removed (if unused)
or named `_` (if used implicitly)."
Related issue: https://github.com/leanprover/lean4/issues/13269
This PR makes the test-only `waitForMessage` helper abort promptly
when the Lean language server reports a fatalError, instead of
blocking until the outer test framework's timeout kills the process.
`waitForMessage` is used to implement the `waitFor` directive in
`tests/server_interactive` tests: it reads server messages in a loop
and returns when it sees a `textDocument/publishDiagnostics`
notification containing a given message. It has no pending request,
so the watchdog's `responseError` (which already terminates
`collectDiagnostics` and `waitForILeans` on a fatalError) doesn't
help here, and it would silently discard `$/lean/fileProgress`
notifications. When the file worker crashes or its header processing
fails fatally (e.g. an unresolved import), the awaited diagnostic
will never be emitted -- so `waitForMessage` would block indefinitely
and report nothing useful, which made several CI failures of
server_interactive tests look like generic 1500s timeouts. With this
change, `waitForMessage` also reacts to `$/lean/fileProgress` with
`fatalError` kind and throws a descriptive error.
The detection is scoped to `waitForMessage` only, not the underlying
`Ipc.readMessage`, so that other IPC paths (notably
`importCompletion.lean`, which intentionally elaborates a file with
an incomplete `import` line and observes the resulting fatalError
fileProgress while still using the alive worker for completion
requests) keep working unchanged. As part of this PR, `waitForMessage`
has been moved out of `Lean.Lsp.Ipc` and into
`Lean.Server.Test.Runner` next to its sole caller `processWaitFor`,
since it is a test-driver helper rather than a general-purpose IPC
primitive (it discards all unrelated messages, which would be unsafe
outside of a test driver).
To exercise the new behavior, `tests/server_interactive/run_test.sh`
now sources `<file>.init.sh` and uses `check_exit_is "${TEST_EXIT:-0}"`,
matching the convention in `tests/compile/`. The new
`worker_crash.lean` test forces the file worker to die via
`IO.Process.forceExit 9` from inside an `elab` command and then
issues a `waitFor` directive that can never be satisfied;
`TEST_EXIT=1` and `.out.expected` capture the abort path. Without
this PR the test would sit at the framework timeout; with this PR it
returns in well under a second.
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR adds Locale and LocaleSymbols for configurable date/time
formatting. It also modifies alignedWeekOfMonth and weekOfYear so it
contains a parameter to the first of the week.
This PR is useful for the TR35 formatting PR.
This PR moves the `dupNamespace` linter from the `EnvLinter` framework
to the `Lean.Linter` (text linter) framework, upstreaming the code from
`mathlib`.
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR adds a `WallTime` type representing a point in time as
nanoseconds since `1970-01-01T00:00:00` local time. It also removes the
`sinceUNIXEpoch` and `AssumingUTC` suffixes because `Timestamp` implies
UTC, and `WallTime` implies it is based on the WallTime epoch (defined
in the comment as `1970-01-01T00:00:00`).
---------
Co-authored-by: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
This PR re-enables all of the Lake tests by default. The previous
flakiness appears to have been fixed by #13559, as multiple runs of
#8580 demonstrate. The `LAKE_CI` CMake setting and the `lake-ci` label
is kept to potentially enable expensive Lake tests in the future (e.g.,
the online tests that are not currently run in CI).
This PR ensures that `withSetOptionIn` does not modify the infotrees or
error on malformed option values, and thus avoids panics in linters that
traverse the infotrees with `visitM`.
`withSetOptionIn` is only intended to be used in linters, and thus
should provide the linter action with the infotrees produced during
elaboration without modification. However, `withSetOptionIn` had not
only been modifying the infotrees by elaborating the option, but had
been producing context-free info nodes in doing so. These caused uses of
`visitM` and related functions to panic in typical linters.
Likewise, `withSetOptionIn` also should not cause the linter to error if
somehow it consumes a malformed option value, but instead should fail
silently; the error should (only) be logged during the original
elaboration.
We give an optional flag `(addInfo := true)` to `Elab.elabSetOption`
which controls whether info is added to the infotrees.
To clarify that `withSetOptionIn` is used only in linters, we move it
into `Lean.Linter.Basic`. To avoid import cycles, we move the current
contents of `Lean.Linter.Basic` back to `Lean.Linter.Init`. We also
publicly import both `Lean.Linter.Init` and `Lean.Elab.Command` into
`Lean.Linter.Basic`, meaning that going forward, linter files need only
import `Lean.Linter.Basic` to access the standard linter API.
This was brought up on Zulip
[here](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/bug.3A.20withSetOptionIn.20creates.20context-free.20info.20nodes/with/556905420),
and discussed briefly in office hours.
---------
Co-authored-by: Wojciech Rozowski <wojciech@lean-fro.org>
This PR fixes issues with flaky cancellation_empty_by test.
The original test gated the runner's `waitFor: blocked` on `t1`'s
`wait_for_cancel_once_async`, which had no causal relationship to
`tracerSuggestion` having actually run inside the empty-`by` snapshot
task. On CI under load the runner could trigger the insert before
`tracerSuggestion` registered its `onSet` callback, leading to
intermittent timeouts.
Add a label-keyed `IO.Promise` registry (`syncPromisesRef`) plus
`getSyncPromise` / `resolveSyncPromise` primitives and a
`wait_for_sync <label>` tactic to `Lean.Server.Test.Cancel`. The
empty-`by` test's `tracerSuggestion` now resolves a sync promise
after registering its onSet, and `t1` waits on that promise before
emitting `blocked`. The empty-`by` example must precede `t1` because
`try?` inside the snapshot task synchronously waits on prior pending
async theorem bodies during library search (likely a separate upstream
issue); with that ordering the test is fully deterministic.
`t1` also drops `wait_for_cancel_once_async` in favor of plain
`trace "blocked"`. The test now also `dbg_trace`s at each sync point
(`tracerSuggestion ready`, `sync received`, `cancelTokenSet`) so the
.out.expected captures the deterministic execution sequence.
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 tightens how the `cbv` tactic interacts with the `Sym.Simp`
framework. It propagates the `contextDependent` flag through cbv
simprocs so cd-marked sub-results from `simp` are no longer dropped at
congruence and projection sites, and rejects `@[cbv_opaque]` on
`@[reducible]` declarations - `Sym` eliminates reducibles before `cbv`
runs, so the combination has no consistent meaning. With that guarantee
the cbv-specific `unfoldReducible`/`preprocessMVar` clones are removed
in favor of their stock `Sym` counterparts.
This PR makes an empty `by` block run `try?` in the background and
surface its suggestions, while still producing the usual unsolved-goals
diagnostic. The implicit `try?` is informational only — it does not
change elaboration behavior beyond emitting messages. Behaviour is
controlled by a new option `tactic.tryOnEmptyBy`, disabled by default
for now; set it to `true` to opt in. The default may flip in a future
release.
Behaviour summary, when the option is enabled:
* The empty `by` reports unsolved goals immediately, before the
(possibly slow) `try?` has finished.
* The `try?` work is spawned as an asynchronous snapshot task
(`Term.wrapAsyncAsSnapshot` + `Core.logSnapshotTask`), so subsequent
elaboration is not blocked and the suggestions arrive when ready.
* `try?` is gated on its parser infrastructure being available, so
working on the prelude (before `Init.Try` is imported) keeps the regular
empty-`by` behaviour.
* No effect when the empty `by` appears inside a backtracking combinator
(e.g. `first | exact (by) | …`) or when `try?` finds no applicable
suggestion.
Implementation notes:
* `elabEmptyByAsTry` (in `Lean.Elab.Tactic.Try`) is registered as a
second `@[builtin_term_elab byTactic]`, alongside the existing
`elabByTactic` in `Lean.Elab.BuiltinTerm`. The gate
`shouldElabEmptyByAsTry` is checked in both elaborators so the
empty-`by` path takes the `try?` route while non-empty `by` follows the
regular path. The body shared between them is factored as
`elabByTacticCore`. The two-elaborator setup avoids a circular module
dependency between `BuiltinTerm.lean` and `Tactic/Try.lean`; an inline
comment in `Try.lean` explains this.
* A latent bug from #13229 is fixed along the way: `evalSepTactics`
returned at the very top for an empty tactic sequence without resolving
the `tacSnap` promise that `MutualDef.mkTacTask` sets up for `:= by …`
bodies. The dangling promise was harmless in typical use because the
cmd's cancellation token would fire shortly after elaboration and drop
it, but with a slow async snapshot task in the same command (as the
implicit `try?` here) the language-server info-tree walk would block on
it and the editor's Messages view would only update once the task
finished. Resolved at the early-return in `evalSepTactics`.
* The test infrastructure in `Lean.Server.Test.Cancel` gains a
label-keyed `testTasksRef` registry plus `mkTestTask` /
`wait_for_test_task`. The pre-existing `block_until_cancelled` is
reimplemented on top of `mkTestTask` and the redundant
`blockUntilCancelledOnce` ref is removed.
Tests:
* `tests/elab/tryOnEmptyBy.lean`, `tests/elab/try_prelude.lean` —
feature behaviour and prelude gating.
* `tests/server_interactive/cancellation_empty_by.lean` — verifies that
on document re-elaboration `cancelRec` reaches the empty-`by` snapshot's
cancel token registered with `Core.logSnapshotTask`. A
`[try_suggestion]` generator wires the outer cancel token's `onSet` to
resolve a `mkTestTask "T_outer"` promise, and the candidate
`wait_for_test_task "T_outer"` waits on it. If `cancelTk? := none` is
passed to `Core.logSnapshotTask`, `cancelRec` cannot reach the token,
the wait blocks, and the runner times out. If `cancelTk? := none` is
also passed to `wrapAsyncAsSnapshot`, no `onSet` resolver is registered,
the promise drops without resolution, and `wait_for_test_task` surfaces
a `"task dropped"` diagnostic on stderr.
* `tests/server_interactive/cancellation_try_plain.lean` — verifies
cancellation of plain `try?` (no `=>`) when its `[try_suggestion]`
candidate runs synchronously inside `expandUserTactic`, by chaining
through `wait_for_cancel_once_async`'s shared promise. Breaking
`SnapshotTask.cancelRec` to skip walking children causes a runner
timeout.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a new `grind` configuration option, `genLocal`, that
controls the
maximum term generation for local theorems (e.g., hypotheses). It
defaults to
`8`, same value as `gen` and applies whenever
`grind` instantiates a theorem whose origin is local rather than a
declaration
or user-provided term. Since users have little control over the patterns
used
for local theorems, a tighter generation bound is a reasonable default.
Internally, E-matching now selects the generation bound via a new
`getMaxGeneration` helper that dispatches on the theorem's `Origin`:
`.stx` and
`.decl` use `gen`, everything else uses `genLocal`.
This PR improves the `grind` diagnostics output so that local hypotheses
used
as E-matching theorems show up with their user-facing names and
instantiation
counters, instead of being silently dropped or reported under an
anonymous
`local.<idx>` identifier.
Previously, `mkGlobalDiag` filtered the `E-Matching instances` table
down to
origins of the form `.decl declName`, discarding every counter coming
from a
local hypothesis (`.fvar`, `.local`, `.stx`). Even when an origin was
kept, the
local-theorem path in `addLocalEMatchTheorems` only recognized `eq_true
h` for
a bare `h : fvar` and fell back to a synthetic `.local <idx>` origin in
all
other cases, including the common one where the proof has been wrapped
by an
`Eq.mp` cast.
swap and move constructors should be noexcept to enable use in STL
containers
A quick inspection suggests that these functions can never throw
exceptions anyway.
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 generalizes a number of `Vector` lemmas about `++` so that the
two appended vectors no longer need to share the same size index:
`sum_append`, `prod_append`, their `_nat` / `_int` variants,
`flatMap_append`, `unattach_append`, `eraseIdx_append_of_lt_size`, and
`eraseIdx_append_of_length_le`.
Reported on Zulip:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Vector.2Esum_append.20should.20allow.20vectors.20of.20different.20size🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR adds a short guidance note to `.claude/CLAUDE.md` clarifying
that "rebase onto X" requests should only change the local branch base,
never the PR's `--base` target on GitHub. The Lean4 workflow
specifically uses `nightly-with-mathlib` as a rebase target to get a
mathlib-tested snapshot for CI, while the PR continues to target
`master`.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR moves the compiled Lake configurations (e.g., `lakefile.olean`)
from the package's `.lake/config` directory to the workspace's
`.lake/config`. This removes a potential source contention between
workspaces sharing a dependency.
This PR pins the `test-summary/action` GitHub Action to the immutable
commit SHA for `v2.4` to work around a broken upstream `v2` tag.
Upstream retagged `v2` to point at `v2.5`, which ships without the
bundled `index.js`, causing every job using the shared build template to
fail in the `Test Summary` post-step with `File not found:
'/home/runner/work/_actions/test-summary/action/v2/index.js'`, even when
all tests pass.
Pinning to the SHA (rather than another floating tag like `@v2.4`)
matches GitHub's [security
guidance](https://docs.github.com/en/actions/security-for-github-actions/security-guides/security-hardening-for-github-actions)
for third-party actions and avoids a repeat of this exact incident if
`v2.4` is later retagged. Dependabot is already configured for
`github-actions` updates in `.github/dependabot.yml`, so version bumps
remain low-cost.
Verification:
- `curl -sI
https://raw.githubusercontent.com/test-summary/action/v2/index.js`
returns 404
- `curl -sI
https://raw.githubusercontent.com/test-summary/action/31493c76ec9e7aa675f1585d3ed6f1da69269a86/index.js`
returns 200
The summary action is shared across every workflow that includes
`build-template.yml`, so this affects all CI Lake jobs, not just one.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR adds an experimental tactic `mvcgen'` that will soon replace
`mvcgen`. It has been reimplemented from the ground up using the new
`SymM`-based framework for efficient symbolic evaluation and can
outperform `mvcgen` by a factor of >100x for some synthetic benchmarks.
`mvcgen'` aspires to be feature-complete with `mvcgen`. Known exceptions
currently are join point sharing, introduction of local specs and
smaller bugs.
The implementation of `mvgen'` used to live in the benchmark suite for
rapid prototyping; this commit merely moves it into the Lean toolchain.
Doing so results in an build time instruction count increase in
seemingly unrelated tests such as `elab/delayed_assign//instructions`;
the reason is that the builtin elaborator attribute now pulls in
substantially more import code on startup.
---------
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR adds `whileM`, a counterpart to `Lean.Loop.forIn` that admits a
one-step unfolding lemma `whileM_eq` (impossible to prove for the
original `partial def`). `Lean.Loop.forIn` now expands to `whileM`, so
`repeat`/`while` keep working without source changes, and the
`Spec.whileM`/`Spec.forIn_loop` `@[spec]` theorems let `mvcgen`
discharge their bodies given a Nat variant and an `α ⊕ β` invariant.
`whileM.impl` is still a `partial def`, but returns a `Subtype
(whileM.Pred f a)` whose property pins the value to an `Acc.recOn` term
whenever an `Acc` and a `MonadAttach` witness exist; `whileM_eq`
extracts that property. A `@[implemented_by]` `whileM.erased` keeps the
runtime a tail call after specialization and would be unnecessary if the
compiler were able eta-expand through the trivial `Subtype` structure.
Supporting infrastructure:
`Internal.Ensures`/`MayReturn`/`ErasesTo`/`IsAttach` and `WPAdequate`
for `Id`/`ReaderT`/`StateT`/`ExceptT`/`OptionT`.
The resulting `while` loops take more work to optimize, hence a modest
increase in build time instructions.
This PR ensures that one can hover over the function name in
fun_induction. Fixes#13673
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This PR replaces `Meta.mkCongrArg` call sites in `handleProj` and
`simplifyAppFn` are replaced with direct `congrArg` constructions that
reuse types already in the `Sym` pointer cache. A few stray unqualified
`inferType` / `getLevel` / `isDefEq` calls in the same file are also
routed through the cached `Sym` equivalents.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR optimizes `lean_dec_ref_cold` by outlining the "freezing cold"
path and performing a small microarchitecural optimization. The latter
is better as it makes clear to LLVM that we believe the pointer to only
use 48 bits.
This PR adds support for blockquotes to Verso docstrings, which had been
missing before. It also substantially improves the robustness of
Verso->Markdown rendering of docstrings, especially the handling of
blockquote line prefixes.
This PR fixes the semantics of `mvcgen' with grind`: it now logs an
error per VC that `grind` cannot close and throws at the end, instead of
silently leaving the unsolved VC as a residual. The previous
silent-fallback behaviour is preserved as `mvcgen' with (try grind)`,
which `elabPreTac` recognises and routes to the same efficient `.grind`
path with a `silent` flag.
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
