This PR adds `.vscode/settings.json` to our `.gitignore`, which allows
Lean 4 developers to set local workspace settings. We already use the
the workspace file for settings in core, so this shouldn't cause any
problems.
This PR fixes a bug in the unknown identifier code actions where the
identifiers wouldn't be correctly minimized in nested namespaces. It
also fixes a bug where identifiers would sometimes be minimized to
`[anonymous]`.
The first bug was introduced in #10619.
This PR adds a silent info message with the `grind` state in its
interactive mode. The message is shown only when there is exactly one
goal in the grind interactive mode. The condition is a workaround for
current limitations of our `InfoTree`.
This PR lets match compilation look only at the first remaining
alternative in `processLeaf`. At this point we have no further variables
we can split on, so if the first one isn’t applicable, match compilation
should fail.
This PR fixes a regression introduced by #10307, where hovering the name
of an inductive type or constructor in its own declaration didn't show
the docstring. In the process, a bug in docstring handling for
coinductive types was discovered and also fixed. Tests are added to
prevent the regression from repeating in the future.
This PR ensures that `grind` interactive mode is hygienic. It also adds
tactics for renaming inaccessible names: `rename_i h_1 ... h_n` and
`next h_1 ... h_n => ..`, and `expose_names` for automatically generated
tactic scripts. The PR also adds helper functions for implementing
case-split actions.
This PR improves the scripts assisting with cutting Lean releases (by
reporting CI status of open PRs, and adding documentation), and adds a
`.claude/commands/release.md` prompt file so Claude can assist.
This PR introduces a no-op version of `Shrink`, a type that should allow
shrinking small types into smaller universes given a proof that the type
is small enough, and uses it in the iterator library. Because this type
would require special compiler support, the current version is just a
wrapper around the inner type so that the wrapper is equivalent, but not
definitionally equivalent.
While `Shrink` is unable to shrink universes right now, but introducing
it now will allow us to generalize the universes in the iterator library
with fewer breaking changes as soon as an actual `Shrink` is possible.
This PR fixes a bug in combination with VS Code where Lean code that
looks like CSS color codes would display a color picker decoration.
VS Code displays this decoration by default for all languages, not just
CSS. Due to https://github.com/microsoft/vscode/issues/91533, this
setting cannot be disabled in the client on a per-language basis.
However, we can override the default behavior by providing a color
provider of our own. This PR implements an empty color provider to
override the VS Code one.
This PR adds support for interactivity to the combined "try this"
messages that were introduced in #9966. In doing so, it moves the link
to apply a suggestion to a separate `[apply]` button in front of the
suggestion. Hints with diffs remain unchanged, as they did not
previously support interacting with terms in the diff, either.
<img width="379" height="256" alt="Suggestion with interactive message"
src="https://github.com/user-attachments/assets/7838ebf6-0613-46e7-bc88-468a05acbf51"
/>
This PR restores the change in #8656, which removed `autoImplicit =
false` from the default lake template (per previous discussions linked
there). This was accidentally reverted in #8866.
This PR fixes a performance regression introduced in #10518. More
generally, it ensures both message log and info state are per-command,
which has been the case in practice ever since the asynchronous language
driver was introduced.
This PR fixes a bug where partially up-to-date files built with `--old`
could be stored in the cache as fully up-to-date. Such files are no
longer cached. In addition, builds without traces now only perform an
modification time check with `--old`. Otherwise, they are considered
out-of-date.
This PR changes the Lake's remote cache interface to scope cache outputs
by toolchain and/or platform were useful.
Packages that set `platformIndependent = true` will not be scoped by
platform and the core build (i.e., `bootstrap = true`) will not be
scoped by toolchain. Lake's detected platform and toolchain can be
overridden with the new `--platform` and `--toolchain` options to `cache
get` and `cache put`.
Lake no longer accepts the `--scope` option when using `cache get` with
Reservoir.. The `--repo` option must be used instead.
This PR follows upon #10606 and creates equational theorems uniformly
from the unfold theorem, there is only one handler registered in
`registerGetEqnsFn`.
For now we keep `registerGetEqnsFn`, because it’s used by mathlib’s
`irreducible_def`, but I’d like to get rid of it in the long term,
relying only on `registerGetUnfoldEqnFn` for constructions that should
unfold differently.
This PR improves the tactics `ac`, `linarith`, `lia`, `ring` tactics in
`grind` interactive mode. They now fail if no progress has been made.
They also generate an info message with counterexample/basis if the goal
was not closed.
This PR provides range support for the signed finite number types
`Int{8,16,32,64}` and `ISize`. The proof obligations are handled by
reducing all of them to proofs about an internal `UpwardEnumerable`
instance for `BitVec` interpreted as signed numbers.
This PR changes where errors are displayed when trying to use
`coinductive` keyword when targeting things that do not live in `Prop`.
Instead of displaying the error above the first element of the mutual
block, it is displayed above the erroneous definition.
---------
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
This PR removes support for reducible well-founded recursion, a Breaking
Change. Using `@[semireducible]` on a definition by well-founded
recursion prints a warning that this is no longer effective.
With the upcoming module system, proofs are often not available. With
this change, we remove a fringe use case hat may require proofs, and
that would not be supported under the module system anyways.
At least for now, direct use of `WellFounded.fix` is not affected.
This fixes: #5192
This PR re-enables semantic tokens for Verso docstrings, after a prior
change accidentally disabled them. It also adds a test to prevent this
from happening again.
In the process, it became clear that there was a bug. The highlighting
strategy led to overlapping but not identical tokens, but the code had
previously assumed that this couldn't happen at the delta-encoding step.
So this PR additionally replaces the removal of duplicate tokens with
priority-based handling of overlapping tokens.
---------
Co-authored-by: Marc Huisinga <mhuisi@protonmail.com>
This PR adds the following tactics to the `grind` interactive mode:
- `focus <grind_tac_seq>`
- `next => <grind_tac_seq>`
- `any_goals <grind_tac_seq>`
- `all_goals <grind_tac_seq>`
- `grind_tac <;> grind_tac`
- `cases <anchor>`
- `tactic => <tac_seq>`
Example:
```lean
def g (as : List Nat) :=
match as with
| [] => 1
| [_] => 2
| _::_::_ => 3
example : g bs = 1 → g as ≠ 0 := by
grind [g.eq_def] =>
instantiate
cases #ec88
next => instantiate
next => finish
tactic =>
rw [h_2] at h_1
simp [g] at h_1
```
