This PR upstreams `unnecessarySeqFocus` linter from batteries to core
lean as a "clippy" linter - i.e. one that is disabled by default and
executed by `lake lint --clippy`.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
This PR adds regression tests for `do`-notation issues that the new
elaborator fixes:
* `tests/elab/doNotation7.lean` collects reproducers for #2663, #2676,
#3126, #5607, #6426, and #8119.
* `tests/elab/12229.lean` covers the `logInfo` and `Std.TreeMap`
reproducers from #12229.
This PR upstreams `dupNamespace` linter from batteries to work with new
core environment linting framework, as a "clippy" linter - i.e. one that
is not enabled by default.
Stacked on top of #13513.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
This PR adds the option `grind.ematch.diagnostics`, which tracks how
E-matching theorem instances depend on each other. When enabled, `grind`
records, for every new theorem instance, the set of previous instances
whose generated terms participated in the match. This produces a
hyper-graph `{thm_1, ..., thm_n} => thm` describing the provenance of
each instantiation.
The hyper-graph is stored in `Grind.Result` so downstream tooling can
inspect it. The trace class `trace.grind.ematch.diagnostics.compact`
prints a compact textual view of the hyper-graph, restricted to
constant-name origins. Example output:
```
[grind.ematch.diagnostics.compact] ✅️ instances
[inst] [] => th1
[inst] [th1] => th3
[inst] [th1] => th2
[inst] [th2, th3] => th4
[inst] [th4] => th5
```
The implementation stores an `ematchDiagSource` field on each `ENode`
and threads a `withEmatchDiagSource` reader through fact assertion so
that newly internalized terms inherit the origin of the instance that
produced them. During E-matching, `Choice` collects the sources of every
matched argument, and the resulting set becomes the predecessor set of
the new instance.
This PR Introduces new foundations for reasoning about monadic Lean
code. Eventually we will port `mvcgen` on top of these new foundations,
to make the framework more general and robust.
Key issues, new metatheory is supposed to solve are
- It gives more flexibility over what an assertion language for
pre-/post-conditions of monadic Hoare triples can be. In particular, any
`CompleteLattice` might become a pre-/post-condtions language, not only
`SPred`. It potentially gives an opportunity to reason about
probabilistic monads, where assertion language are distributions. This
also simplifies the metatheory of monadic Hoare triples, as it does not
require defining the notion of `SPred`, and allows users to work in a
fairly common interface of `CompleteLattice`
- It splits the post-conditions of Hoare triples/ WPs into two: (1)
`post` for post-conditions on terminating paths and (2) `epost` for
post-conditions on abrupt paths. Current foundations always bundle them
into a pair, which inevitably leads to constructing and eliminating such
pairs everywhere in the code.
- It relaxes some conditions that the current foundations require for
instantiating `WPMonad` type class. In particular we do not require `wp`
to distribute over `bind` any more. Instead, we require just `wp x (fun
x => wp (f x) post epost) epost ⊑ wp (x >>= f) post epost`, i.e. the
distributed `wp` must only imply the non-distributed one (and not
necessarily vice versa). With this we can define `WPMonad` for
Separation Logic, where `wp` only distributes over `bind` on
local-footprint computations.
- It solves some universe polymorphism issues. As now universe levels of
assertion languages are independent of universe levels in the monad, one
can define `WPMonad Id.{u} Prop EPost⟨⟩`, which means that for arbitrary
level `Id` the language for pre-/post-conditions is going to be just
`Prop` and the language for post-conditions on abrupt exits is idle.
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR addresses two review points on `IO.CancelToken`:
* `set` now resolves the underlying promise *before* writing the `Bool`
fast-path flag, so observing `isSet = true` implies any synchronously
chained `onSet` callback has already run. The previous order (flag
first,
then resolve) was a subtle footgun: code seeing `isSet = true` could not
rely on the cancellation task having fired.
* The underlying promise and the task it produces are kept private. The
prior `task : Task (Option Unit)` accessor is removed; consumers should
use `onSet` to react to cancellation. A comment on the structure records
that re-exposing the task in the future requires re-auditing the order
in `set` for races between the promise and the `Bool` flag.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
This PR adds source-level comments noting that the constructors of
`Lean.Meta.TransparencyMode` and `Lean.ReducibilityStatus` are not laid
out in the unfolding-amount order suggested by their docstrings, and
that reordering them induces a non-trivial bootstrap problem.
Also rewrites a stale comment in `Lean.Meta.Basic` that listed the
hierarchy in descending order without `.none`.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR fixes a race condition in the Lake build monitor's draining of
the job queue.
Previously, the monitor drained the registered-jobs queue before
checking task states. A finished job in that scan may have registered
new jobs in its body just before terminating. Those jobs landed in the
queue after the drain, so when no other unfinished jobs remained the
monitor exited without ever observing them. If one of the missed jobs
errors, this could produce an "uncaught top-level build failure" message
alongside "Build completed successfully".
To fix this, the monitor loop is restructured so the queue is drained
*after* task states are scanned, with an additional drain before the
loop terminates. `drainQueue` and `scanJobs` are split out from `poll`,
and `Monitor.main` performs an initial drain to capture any jobs
registered before the monitor starts iterating. Finishing jobs cannot
register further work once their state transitions, so a single
post-scan drain is sufficient to close the window.
🤖 Prepared with Claude Code
This PR fixes a bug in `propagateBetaEqs` (in
`Lean.Meta.Tactic.Grind.Beta`)
where new equalities/terms introduced by beta reduction were added to
the goal
without checking the generation threshold. The generation of the new
fact
is the maximum generation of the lambda, the function `f`, and its
arguments, plus one. Without the threshold check, beta reduction can
cascade indefinitely on self-similar lambdas such as
`(fun b => f (b + 1)) = fun b => f b`, which kept producing
`f n = f (n + 1)` for every `n`. The fix aggregates argument generations
before the threshold check and bails out when the resulting generation
reaches `maxGeneration`.
This PR moves `IO.CancelToken` from `Init.System.IO` to its own file
`Init.System.CancelToken`, backed by `IO.Promise Unit` instead of
`IO.Ref Bool`. This enables non-polling cancellation propagation: the
token's underlying promise can be used directly with `IO.waitAny`, and
callbacks can be registered to fire when cancellation is requested.
The structure carries both the promise *and* a plain `IO.Ref Bool` flag,
set in lockstep by `set`. `isSet` reads the flag directly (used on hot
paths like `Core.checkInterrupted`); `task`/`onSet` go through the
promise. The avoids a ~0.4% regression that a pure-promise
representation introduced.
API additions:
- `CancelToken.task : Task (Option Unit)`. Returns the underlying
promise's `result?` task directly — the same task object on every call,
so further `Task.map`/`BaseIO.bindTask` dependencies can be safely
attached. Resolves with `some ()` when `set` is called, or `none` if the
token is dropped without ever being set.
- `CancelToken.onSet : BaseIO Unit → BaseIO Unit`. Registers a callback
that runs synchronously on the cancelling thread when `set` is called
(or immediately if the token is already set). Implemented via
`BaseIO.chainTask` on `result?`, so no fresh `Task.map` per call and no
GC hazard.
Runtime cleanup:
- Add `LEAN_TASK_STATE_{WAITING,RUNNING,FINISHED}` constants in `lean.h`
matching `IO.TaskState`.
- Factor `lean::promise_is_resolved` inline in `object.h`, replacing
three open-coded `lean_io_get_task_state_core(...) == 2` checks (in
`interrupt.cpp`, `uv/timer.cpp`, `uv/signal.cpp`).
- Drop the manual `inc_ref(g_cancel_tk)` in `check_interrupted`; the
token is owned by the enclosing `scope_cancel_tk` for the duration of
the call (documented).
- Replace the bare `lean_always_assert(g_task_manager)` in
`lean_promise_new` with an explicit `lean_internal_panic` carrying a
message that names `Promise.new`, identifies the typical trigger
(`initialize` blocks, transitively via `IO.CancelToken.new`), and
recommends lazy construction. Without this, users got an opaque "LEAN
ASSERTION VIOLATION ... Condition: g_task_manager" with no actionable
hint.
Behavioural notes documented inline:
- `new` cannot be called from `initialize` blocks (task manager not
running yet); construct lazily.
- `task` documents the dropped-promise case (`none`) and steers callers
to `onSet` for callback chaining.
A consumer of `onSet` for parent → child cancel-token propagation in
parallel tactic combinators is in #13428 (fixes#13300).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR prevents memory exhaustion turning into segfaults when using
Lean functions which call into libuv
`malloc` can return `NULL`, in which case this code would previously go
on to dereference a null pointer.
Instead, it now returns a suitable `IO.Error`.
Calling `lean_internal_panic_out_of_memory` would also be an option
here, since the adjacent `lean_promise_new` calls would fail in this
way.
This PR extends `lake lint --builtin-lint` to also support text linters
(i.e. those using `logLint`/`logLintIf`), in addition to the environment
linters added in #13431. Text-linter warnings emitted during the build
are persisted into each module's `.olean` via a new
`Lean.Linter.lintLogExt` environment extension; `lake lint` re-runs the
build for the target modules and reads the entries back, reporting them
alongside the environment linter output.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
This PR adds a `try? => tac` syntax that runs `evalSuggest` directly on
a given tactic, useful for testing the `try?` machinery in isolation. It
also adds a server_interactive test (`cancellation_par.lean`) that
demonstrates a cancellation bug with parallel tactic combinators.
The test contrasts three combinators:
- **`first`** (sequential): cancellation works correctly — the tactic
runs on the main elaboration thread and shares its cancel token.
- **`attempt_all_par`** (parallel): cancellation is broken — the subtask
spawned via `asTask` gets a fresh cancel token that is never set on
re-elaboration.
- **`first_par`** (parallel): same bug as `attempt_all_par`.
The test uses a `check_cancel <label>` helper tactic that detects leaked
cancel tokens without any timing dependency: the second invocation (from
re-elaboration) signals the first, which then checks whether its cancel
token was set.
Related issue: #13300
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR replaces `exit(-1)` with `_exit(-1)` in the forked child
branches of `lean_io_process_spawn` (the `chdir` failure and `execvp`
failure paths). `exit` flushes inherited C stdio buffers, which share
underlying file descriptors with the parent. If the parent had a file
handle open with unflushed data, that data would be written to the file
in the child and then again when the parent later flushes, resulting in
duplicated output. `_exit` skips the stdio flush, so the parent's
buffered writes are no longer duplicated into inherited files.
Closes https://github.com/leanprover/lean4/issues/13463.
🤖 Prepared with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR replaces the catch-all "unsupported pattern in syntax match"
error that the new `do` elaborator produces for typical pattern mistakes
(#2215, #8304, #10393) with the proper diagnostics from the regular
pattern-var collector (e.g. "Invalid pattern: Expected a constructor or
constant marked with `[match_pattern]`", "ambiguous pattern, use fully
qualified name"), pointing at the offending pattern.
`getPatternVarsEx` / `getPatternsVarsEx` in `Lean.Elab.Do` now try the
syntax-quotation collector first (cheaply handling identifiers, holes,
and antiquotations) and fall back to the regular pattern-var collector
for everything else. When both fail, the regular collector's error wins
via `<|>` semantics.
The legacy `do` elaborator is intentionally left untouched, so the
existing `tests/elab/doSyntaxPatternError.lean` guards (which capture
the cryptic messages produced under legacy default) are unchanged. They
will need updating when the new `do` elaborator becomes default.
Fixes#2215, #8304, and #10393 for the new `do` elaborator.
This PR adds a `linter.redundantExpose` option (default `true`) that
warns when `@[expose]` or `@[no_expose]` attributes have no effect:
- `@[expose]` on `abbrev` (always exposed) or non-Prop `instance`
(always exposed)
- `@[expose]` on a `def` inside an `@[expose] section` (already exposed
by the section)
- `@[expose]`/`@[no_expose]` in a non-`module` file (no module system)
- `@[no_expose]` on a declaration that wouldn't be exposed by default
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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 notifies satellite solvers about asserted equalities `lhs = rhs`
even though `lhs = rhs` is not internalized in the E-graph (an existing
optimization). The notification lets solvers that do not inspect
equivalence classes (such as the homomorphism extension) react to
asserted equalities directly. It fires before the equivalence-class
merge so that solvers that mark `lhs` and `rhs` as their internal terms
have them registered before `Solvers.mergeTerms` fires `processNewEq`.
`cutsat` opts out of the notification when the equality has not been
internalized, since it already handles equalities through its `newEq`
handler. The homomorphism demo opts in by forcing `e` to be
internalized, enabling its rewrite rules to apply to asserted equalities
(e.g., `add b b = b` rewrites via `a = b ↔ toInt a = toInt b`).
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR allows tactic macros and elaborators to opt out of automatic
fallback to previous macros/elabs on failure. `throwUnsupportedSyntax`
is unaffected.
This PR removes the Makefile-based Lake test runner and replaces it with
`run_test.sh` and `run_clean.sh`. These are still not designed for use
with the `with_*.sh` runners, but this a step closer to that
eventuality.
It also adds a line to `CLAUDE.md` informing Claude how to build and run
a single Lake test.
This PR replaces the transparency bump from `.reducible` to `.instances`
in `whnfMatcher` with an explicit allowlist in `canUnfoldAtMatcher`.
Previously, `whnfMatcher` would unfold all `implicitReducible`
definitions and all `fromClass` projections when reducing match
discriminants. This made it impossible to mark definitions as
`implicit_reducible` without silently affecting match reduction
behavior.
The new `canUnfoldAtMatcher` delegates to `canUnfoldDefault` first
(respecting the ambient transparency), then allows unfolding of
`match_pattern`-attributed definitions, and finally checks an explicit
allowlist:
- `OfNat.ofNat` — numeric literals in match discriminants
- `NatCast.natCast` — `↑m` coercions (pervasive in Int proofs)
- `Zero.zero`, `One.one` — `0`/`1` class projections in match
discriminants
- `Fin.ofNat`, `HMod.hMod`, `Mod.mod` — Fin literal reduction
- `decEq`, `Nat.decEq` — decidable equality
- `Char.ofNat`, `Char.ofNatAux` — character literals
- `String.decEq`, `List.hasDecEq` — string/list equality
- `UInt{8,16,32,64}.{ofNat,decEq}` — unsigned integer literals and
equality
The key change is removing the blanket `implicitReducible` and
`fromClass` checks, so that marking definitions as `implicit_reducible`
no longer silently affects match reduction.
Additionally, `reduceMatcher?` and `reduceRecMatcher?` now call
`consumeMData` on their input to handle mdata-wrapped matcher
expressions.
Mathlib adaptation: the removal of the `fromClass` projection check
means class projections like `CategoryStruct.comp`, `CategoryStruct.id`,
`Min.min` etc. are no longer auto-unfolded in match discriminants.
Affected proofs add these projections explicitly to `simp`/`dsimp`
calls.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds `namespace Lake` to `Lake.Util.Opaque`, which was missing
it. This is technically a breaking change for any code which used
`Opaque` without `open Lake`, but hopefully no one was doing that.
This PR changes `whnfAux` in the equation-theorem generation machinery
to use
reducible transparency (`whnfR`) instead of instances transparency
(`whnfI`).
Previously, the loop in `Eqns.go` would unfold instances on the LHS,
which
interacts badly with users that mark `dite`/`ite` as
`implicit_reducible`:
equation generation would reduce past the `dite` and get stuck instead
of
committing to a branch. The original motivation for `whnfI` (reducing
`Nat.rec ... (OfNat.ofNat 0)` residuals from `match` on numeric
literals) is
already covered by the surrounding
`simpMatch?`/`simpIf?`/`simpTargetStar`
steps in `Eqns.go`, so the full test suite continues to pass.
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 appends `unreachable!` to the expansion of `break`-less `repeat`
when the expected result type does not unify with `PUnit`. The
continuation then has a polymorphic value, so the enclosing do block's
result type is inferred without a user-written filler, and `ControlInfo`
for break-less `repeat` can report `noFallthrough` honestly — dead-code
warnings on subsequent elements are now actionable.
Co-authored-by: Rob23oba <robin.arnez@web.de>
This PR exposes the `Pure.pure` / `Bind.bind` applications emitted by
the `do` elaborator as pluggable closures, so external surface syntaxes
(e.g. an `ido` notation for indexed monads) can reuse the full `do`
machinery while emitting alternate constants.
`Context` carries a new `DoOps` record (wrapped via an opaque `DoOpsRef`
to break the cycle with `DoElabM`) with `mkPureApp`, `mkBindApp`, and
`isPureApp?` fields. `mkPureApp` and `mkBindApp` become thin
dispatchers; the original bodies move to `DoOps.default`. `isPureApp?`
returns the pure value as an `Expr` rather than a `Bool`, so overrides
aren't locked into `Pure.pure`'s 4-argument layout. A new `elabDoWith`
entry point takes a `DoOps` plus a `doSeq`; `elabDo` is now `elabDoWith
.default` applied to a matched ``(do $doSeq)``.
Control-flow features (`mut`, `return`, `break`, `continue`, `for`) and
the transformer stack (`StateT`, `OptionT`, `ExceptT`, `EarlyReturnT`,
`BreakT`, `ContinueT`) remain hard-coded to `Monad`; generalising them
is deferred to a follow-up. A new
`tests/elab/doNotationPluggableOps.lean` registers an Atkey-style
indexed monad and an `ido` surface syntax that drives `elabDoWith`,
covering the forms of `do` that are supported under the minimal scope.
This PR adds a check for empty `lake build` invocations (as an empty
build usually indicates a misconfiguration). Builds with no jobs will
now print "Nothing to build." and invocations of `lake build` with no
default targets configured will produce a warning. This will be promoted
to an error in the future. The warning (and future error) can be
suppressed with the new `--allow-empty` CLI option.
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR improves metavariable pretty printing and their hovers in the
InfoView. The hovers in the InfoView now include information about
specific metavariables — it includes information such as the kind of the
metavariable, whether it is a blocked delayed assignment and which
metavariables it is blocked on, and the differences in what variables
exist the metavariable's local context. Additionally, named
metavariables now pretty print with tombstones if they are inaccessible.
Delayed assignment pretty printing now more reliably follows chains of
assignments to find the pending metavariable.
**Example hovers**
Hovering over a natural metavariable:
> `?m.7 : Sort ?u.14`
> A metavariable representing an expression that should be solved for by
unification during the elaboration process. They are created during
elaboration as placeholders for implicit arguments and by `_`
placeholder syntax.
>
> Variables absent from this metavariable's local context: `a`, `b`, `y`
Hovering over `?baz`, a tactic goal:
> `?baz : ∀ (a : ?m.7) (a : ?m.8), True`
> A metavariable representing a tactic goal or an expression whose
elaboration is still pending. They usually act like constants until they
are completely solved for. They can be created using `?_` and `?n`
synthetic placeholder syntax.
>
> Variables absent from this metavariable's local context: `a`, `b`, `y`
Hovering over `?refine_1`, which appears under a binder:
> `?m.4 x : Nat`
> A metavariable representing a tactic goal or an expression whose
elaboration is still pending. They usually act like constants until they
are completely solved for. They can be created using `?_` and `?n`
synthetic placeholder syntax.
>
> This metavariable appears here via a *delayed assignment*.
Substitution is delayed until the metavariable's value contains no
metavariables, since all occurrences of the variables from its local
context will need to be replaced with expressions that are valid in the
current context.
>
> Additional variable in this metavariable's local context: `x`
Hovering over `?m.4`:
> `?m.4 : Nat → Nat`
> Part of the encoding of the *delayed assignment* mechanism. Represents
the metavariable `?refine_1`, which has additional local context
variables. Substitution is delayed until the metavariable's value
contains no metavariables, since all occurrences of the variables from
its local context will need to be replaced with expressions that are
valid in the current context.
>
> Additional variable in this metavariable's local context: `x`
The middle paragraph for `?refine_1` when it has been partially
assigned:
> This metavariable has been assigned, but it is a *delayed assignment*.
Substitution is delayed until the metavariable's value contains no
metavariables, since all occurrences of the variables from its local
context will need to be replaced with expressions that are valid in the
current context. Substitution is awaiting assignment of the following
metavariable: `?foo`
This PR adds builtin environment linting support to Lake, accessible via
`lake lint` flags. It also introduces two builtin linters upstreamed
from Mathlib (`defLemma` and `checkUnivs`) and a `builtinLint` package
configuration option.
Builtin linting is triggered via flags on `lake lint`:
- `--builtin-lint`: run default builtin linters (in addition to the lint
driver if configured)
- `--builtin-only`: run only builtin linters, skip the lint driver
- `--clippy`: run only non-default (clippy) linters
- `--lint-all`: run all builtin linters (default + clippy)
- `--lint-only <name>`: run a specific builtin linter by name
- Using `--clippy`, `--lint-all`, or `--lint-only` implicitly enables
builtin lint mode
The `builtinLint` package option is a tristate (`Option Bool`):
- `true`: always run builtin lints via `lake lint`; when a lint driver
is also configured, builtin lints run first, then the driver, and the
command fails if either reports errors.
- `false`: never run builtin lints automatically; `lake check-lint`
fails unless a lint driver is configured.
- `none` (default): currently equivalent to `false`; in a future
release, `none` will fall back to builtin lints when no lint driver is
configured.
The linter framework introduces a `LintScope` enum (`.default`,
`.clippy`, `.all`) replacing the previous boolean `clippy` parameter in
`getChecks` and `formatLinterResults`. A `@[builtin_nolint]` attribute
(available without imports) allows suppressing specific linters per
declaration.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
This PR drops `LEAN_NUM_THREADS=1` from the `run_test.sh` of
`bench/mvcgen/sym`. The single-threaded restriction was originally there
to get reproducible benchmark timings, but `run_test.sh` runs as a test
rather than a benchmark, and we do not care about timing reproducibility
for tests. Allowing the default thread count cuts the wall time of what
was the slowest ctest entry from ~30s to ~20s.
This PR fixes the `ControlInfo` inference for a do-block `match`: the
fold over the match arms started from `ControlInfo.pure` (defaults to
`numRegularExits := 1`, `noFallthrough := false`), but `alternative`
sums `numRegularExits` and ANDs `noFallthrough`, so the fold identity is
`{ numRegularExits := 0, noFallthrough := true }`. With the wrong base,
a `match` whose arms all `break`/`continue`/`return` reported
`numRegularExits = 1` and `noFallthrough = false`, suppressing the
dead-code warning on the continuation after the match. The fix corrects
both the inference handler in `InferControlInfo.lean` and the fold in
`elabDoMatchCore`.
This PR splits `ControlInfo`'s dead-code signal in two.
`numRegularExits` is now purely syntactic: how many times the block
wires its continuation into the elaborated expression, consumed by
`withDuplicableCont` as a join-point duplication trigger (`> 1`). The
new `noFallthrough : Bool` asserts that the next doElem in the enclosing
sequence is semantically irrelevant; `false` asserts nothing. Invariant:
`numRegularExits = 0 → noFallthrough`; the converse does not hold.
`sequence` derives `noFallthrough := a.noFallthrough || b.noFallthrough`
(and aggregates syntactic fields unconditionally); `alternative` derives
it as `a.noFallthrough && b.noFallthrough`. The dead-code warning gate
in `withDuplicableCont` and `ControlLifter.ofCont` now reads
`noFallthrough`.
This PR stops the `repeat` inference handler from reporting
`numRegularExits := 0` for break-less bodies. For break-less `repeat`
the loop never terminates normally, so `0` looks more accurate
semantically, but the loop expression still has type `m Unit` and the do
block's continuation after the loop is what carries that type. Reporting
`0` makes the elaborator flag that continuation as dead code, yet there
is no way for the user to remove it that is also type correct — unless
the enclosing do block's monadic result type happens to be `Unit`.
Pinning `numRegularExits` at `1` (matching `for ... in`) eliminates
those spurious warnings.
This PR fixes a bug where the nesting level in Verso Docstrings is
forgotten when there's a doc comment with no headers.
It changes the `terminalNesting` of `VersoModuleDocs` to be recomputed
rather than stored in the structure; we never want it to be anything
besides the default value, and it's easy to accidentally break this
invariant.
Closes#13485
This PR adds server-side support for incremental diagnostics via a new
`isIncremental` field on `PublishDiagnosticsParams` that is only used by
the language server when clients set `incrementalDiagnosticSupport` in
`LeanClientCapabilities`.
### Context
The goal of this new feature is to avoid quadratic reporting of
diagnostics.
LSP has two means of reporting diagnostics; pull diagnostics (where the
client decides when to fetch the diagnostics of a project) and push
diagnostics (where the server decides when to update the set of
diagnostics of a file in the client).
Pull diagnostics have the inherent problem that clients need to
heuristically decide when the set of diagnostics should be updated, and
that diagnostics can only be incrementally reported per file, so the
Lean language server has always stuck with push diagnostics instead.
In principle, push diagnostics were also intended to only be reported
once for a full file, but all major language clients also support
replacing the old set of diagnostics for a file when a new set of
diagnostics is reported for the same version of the file, so we have
always reported diagnostics incrementally while the file is being
processed in this way.
However, this approach has a major limitation: all notifications must be
a full set of diagnostics, which means that we have to report a
quadratic amount of diagnostics while processing a file to the end.
### Semantics
When `LeanClientCapabilities.incrementalDiagnosticSupport` is set, the
language server will set `PublishDiagnosticsParams.isIncremental` when
it is reporting a set of diagnostics that should simply be appended to
the previously reported set of diagnostics instead of replacing it.
Specifically, clients implementing this new feature should implement the
following behaviour:
- If `PublishDiagnosticsParams.isIncremental` is `false` or the field is
missing, the current diagnostic report for a specific document should
replace the previous diagnostic report for that document instead of
appending to it. This is identical to the current behavior before this
PR.
- If `PublishDiagnosticsParams.isIncremental` is `true`, the current
diagnostic report for a specific document should append to the previous
diagnostic report for that document instead of replacing it.
- Versions should be ignored when deciding whether to replace or append
to a previous set of diagnostics. The language server ensures that the
`isIncremental` flag is set correctly.
### Client-side implementation
A client-side implementation for the VS Code extension can be found at
[vscode-lean4#752](https://github.com/leanprover/vscode-lean4/pull/752).
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Wojciech Nawrocki <13901751+Vtec234@users.noreply.github.com>
This PR fixes an issue with `Workspace.setDepPkgs` (introduced in
#13445) where it did not properly update the workspace `packageMap`. In
addition, this PR further verifies aspects of the workspace construction
during dependency resolution.
