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 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 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 the `check_cancel` two-way coordination protocol used
by
`tests/server_interactive/cancellation_par.lean` with a single tactic
`block_until_cancelled "<label>"`. The first invocation for a label
registers
a promise, prints `<label>: blocked`, and loops on
`Core.checkInterrupted`
until the cancel token fires (then `finally` resolves the promise). Any
later
invocation for the same label waits on that promise — so the test only
terminates if the first invocation actually exited the loop. If
cancellation
fails to propagate, the second invocation's `IO.wait` blocks forever and
the
test hangs (timeout = failure), with no false-success path.
The test was disabled in `tests/CMakeLists.txt` due to flakiness in the
old
two-way protocol; this PR re-enables it. Verified that reverting #13428
makes the test deadlock as expected.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
This PR fixes parallel tactic combinators (`attempt_all_par`,
`first_par`) leaking their subtasks when the server cancels elaboration
on re-elaboration. Subtasks spawned via `CoreM.asTask` (and its
`MetaM`/`TermElabM`/`TacticM` variants) get a fresh `IO.CancelToken`,
which previously had no link to the parent token; `cancelRec` would set
the command-level token but the children kept running.
The fix is one line in `CoreM.asTask`: when a parent token is in scope,
register `cancelToken.set` as an `onSet` callback on the parent.
Server-level cancellation now flows down to every parallel subtask, and
`Core.checkInterrupted` inside the child sees the token set as expected.
Fixes#13300.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.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 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 refines how the `apply` tactic (and related tactics like
`rewrite`) name and tag the remaining subgoals. Assigned metavariables
are now filtered out *before* computing subgoal tags. As a consequence,
when only one unassigned subgoal remains, it inherits the tag of the
input goal instead of being given a fresh suffixed tag.
User-visible effect: proof states that previously displayed tags like
`case h`, `case a`, or `case upper.h` for a single remaining goal now
display the input goal's tag directly (e.g. no tag at all, or `case
upper`). This removes noise from `funext`, `rfl`-style, and
`induction`-alternative goals when the applied lemma introduces only one
non-assigned metavariable. Multi-goal applications are unaffected —
their subgoals continue to receive distinguishing suffixes.
This may affect users whose proofs rely on the previous tag names (for
example, `case h => ...` after `funext`). Such scripts need to be
updated to use the input goal's tag instead.
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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 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 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>
This PR adds test infrastructure and tests for tactic completion in
empty `by` blocks.
**Test runner improvements (`src/Lean/Server/Test/Runner.lean`):**
- Add `--⬑` marker variant that targets the column of `--` itself,
enabling column 0 tests (which `--^` cannot reach since `^` is always at
column 2+).
**New test file (`tests/server_interactive/completionEmptyBy.lean`):**
- Tests tactic completion in empty `by` blocks for both top-level `by`
and nested `by` (inside `id <| have := by`).
- Tests at various column positions on the line below `by`: indented
past `by`, at column 2, and at column 0.
- Tests on the `by` token itself (no completions expected).
- All positions below `by` currently offer tactic completions.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
The tests need to run with certain environment variables set that only
cmake really knows and that differ between stages. Cmake could just set
the variables directly when running the tests and benchmarks, but that
would leave no good way to manually run a single benchmark. So cmake
generates some stage-specific scripts instead that set the required
environment variables.
Previously, those scripts were sourced directly by the individual
`run_*` scripts, so the env scripts of different stages would overwrite
each other. This PR changes the setup so they can instead be generated
next to each other. This also simplifies the `run_*` scripts themselves
a bit, and makes `tests/bench/build` less of a hack.
This PR adjusts the JSON encoding of RPC references from `{"p": "n"}` to
`{"__rpcref": "n"}`. Existing clients will continue to work unchanged,
but should eventually move to the new format by advertising the
`rpcWireFormat` client capability.
- This came up in leanprover/vscode-lean4#712.
- The new encoding is far less likely to clash with real-world names,
and is now documented as a "reserved internal name".
- At 8 bytes vs. 1 byte, it incurs a ~5% size increase on the JSON size
of interactive terms, e.g. from 868KiB to 903KiB on the
leanprover/vscode-lean4#500 test.
- Make `deriving RpcEncodable` throw an error when it encounters the
reserved name. We cannot easily guard against clashes in user-provided
JSON, however, so we just assume it does not clash.
- Add a notion of *RPC wire format* with corresponding `rpcWireFormat`
client and server capabilities. The format before this PR is now called
`v0`, whereas here we implement `v1`. Existing clients should eventually
implement compatibility with `v1` (because doing so fixes the above
bug), but will continue to work in the meantime. The format may be
revised again in the future (but we don't expect to revise it so often
that semver would be useful).
- Document everything.
## Alternative designs (abandoned for now)
- Option 1. Add a method `$/lean/rpc/metadata` which, given the name of
an RPC method `foo`, returns metadata containing a description of where
the RPC refs in any return value of `foo` would be (essentially a
description of the structure of the return type).
- Option 2. Wrap every response to `$/lean/rpc/call` in such metadata.
This would be a different change to the wire format.
- To implement this in an extensible way, we extend `RpcEncodable` by a
`refPaths` field. But how does `refPaths` describe where the refs are?
- Option A. Emit the code of a JS method that extracts the refs. This is
maybe simplest, but it would leave non-JS clients (e.g. `lean.nvim`)
behind.
- Option B. Give the description in some query language. The query
language must be able to describe paths into arbitrary inductive types.
- The most popular option,
[JSONPath](https://www.rfc-editor.org/rfc/rfc9535), seemingly cannot
describe non-uniform paths (e.g. both the `a`s in `{a: 1, {b: {a:
2}}}`).
- [JMESPath](https://jmespath.org/) can describe non-uniform paths, and
has 'fully compliant' implementations in many languages, but doesn't
seem to handle recursive paths.
- The most expressive option is [jq](https://github.com/jqlang/jq), but
the most popular way to run it is via an Emscripten WASM blob in
[jq-web](https://github.com/fiatjaf/jq-web) which seems heavy. There is
[jqjs](https://github.com/mwh/jqjs) as well; I'm not sure how
production-ready that is.
This PR adds a `result? : Option TraceResult` field to `TraceData` and
populates it in `withTraceNode` and `withTraceNodeBefore`, so that
metaprograms walking trace trees can determine success/failure
structurally instead of string-matching on emoji.
`TraceResult` has three cases: `.success` (checkEmoji), `.failure`
(crossEmoji), and `.error` (bombEmoji, exception thrown). An
`ExceptToTraceResult` typeclass converts `Except` results to
`TraceResult` directly, with instances for `Bool` and `Option`.
`TraceResult.toEmoji` converts back to emoji for display. This replaces
the previous `ExceptToEmoji` typeclass — `TraceResult` is now the
primary representation rather than being derived from emoji strings.
`withTraceNodeBefore` (used by `isDefEq`) uses
`ExceptToTraceResult.toTraceResult` directly, correctly handling `Bool`
(`.ok false` = failure) and `Option` (`.ok none` = failure), with
`Except.error` mapping to `.error`.
For `withTraceNode`, `result?` defaults to `none`. Callers can pass
`mkResult?` to provide structured results; when set, the corresponding
emoji is auto-prepended to the message.
Motivated by mathlib's `#defeq_abuse` diagnostic tactic
(https://github.com/leanprover-community/mathlib4/pull/35750) which
currently string-matches on emoji to determine trace node outcomes. See
https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR migrates most remaining tests to the new test suite. It also
completes the migration of directories like `tests/lean/run`, meaning
that PRs trying to add tests to those old directories will now fail.
