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
```
This PR enforces rules around arithmetic of `String.Pos.Raw`.
Specifically, it adopts the following conventions:
- Byte indices ("ordinals") in strings should be represented using
`String.Pos.Raw`
- Amounts of bytes ("cardinals") in strings should be represented using
`Nat`.
For example, `String.Slice.utf8ByteSize` now returns `Nat` instead of
`String.Pos.Raw`, and there is a new function `String.Slice.rawEndPos`.
Finally, the `HAdd` and `HSub` instances for `String.Pos.Raw` are
reorganized. This is a **breaking change**.
The `HAdd/HSub String.Pos.Raw String.Pos.Raw String.Pos.Raw` instances
have been removed. For the use case of tracking positions relative to
some other position, we instead provide `offsetBy` and `unoffsetBy`
functions. For the use case of advancing/unadvancing a position by an
arbitrary number of bytes, we instead provide `increaseBy` and
`decreaseBy` functions. For
offsetting/unoffsetting/advancing/unadvancing a position `p` by the size
of a string `s` (resp. character `c`), use `s + p`/`p - s`/`p + s`/`p -
s` (resp. `c + p`/`p - c`/`p + c`/`p - c`).
This PR adds a new helper parser for implementing parsers that contain
hexadecimal numbers. We are going to use it to implement anchors in the
`grind` interactive mode.
This PR aims to fix the Timer API selector to make it finish as soon as
possible when unregistered. This change makes the `Selectable.one`
function drop the `selectables` array as soon as possible, so when
combined with finalizers that have some effects like the TCP socket
finalizer, it runs it as soon as possible.
This PR fixes several causes of test flakiness and re-enables the tests
that were disabled in #10665, #10669 and #10673.
Specifically, it fixes:
- A race condition in the file worker that caused it to report an
incomplete snapshot prefix in the inlay hint request (confirmed to be
the cause of #10665)
- A bug in the test runner where it didn't correctly account for
non-deterministic message ordering inducing different RPC pointer
numbering (confirmed to be the cause of #10673)
- A race condition in the watchdog that would sometimes cause the module
hierarchy to be empty (likely the cause of #10669, but not confirmed as
this issue only reproduced again once in tens of thousands of test runs
on various machines, including CI)
- An unrelated bug in the module hierarchy implementation that would
cause it to report an empty module hierarchy when the file was changed
It also replaces some calls to `Task.get` in the language server with
`IO.wait` to protect the code against unfortunate compiler re-ordering.
This PR adds auto-completion for identifiers after `end`. It also fixes
a bug where completion in the whitespace after `set_option` would not
yield the full option list.
Closes#3885.
### Breaking changes
The `«end»` syntax is adjusted to take an `identWithPartialTrailingDot`
instead of an `ident`.
This PR implements *anchors* (also known as stable hash codes) for
referencing terms occurring in a `grind` goal. It also introduces the
commands `show_splits` and `show_state`. The former displays the anchors
for candidate case splits in the current `grind` goal.
This PR adds a new `allowImportAll` configuration option for packages
and libraries. When enabled by an upstream package or library,
downstream packages will be able to `import all` modules of that package
or library. This enables package authors to selectively choose which
`private` elements, if any, downstream packages may have access to.
This PR adds the `have` tactic for the `grind` interactive mode.
Example:
```lean
example {a b c d e : Nat}
: a > 0 → b > 0 → 2*c + e <= 2 → e = d + 1 → a*b + 2 > 2*c + d := by
grind =>
have : a*b > 0 := Nat.mul_pos h h_1
lia
```
This PR introduces a `coinductive` keyword, that can be used to define
coinductive predicates via a syntax identical to the one for `inductive`
keyword. The machinery relies on the implementation of elaboration of
inductive types and extracts an endomap on the appropriate space of the
predicates from the definition that is then fed to the
`PartialFixpoint`. Upon elaborating definitions, all the constructors
are declared through automatically generated lemmas.
For example, infinite sequence of transitions in a relation, can be
given by the following:
```lean4
section
variable (α : Type)
coinductive infSeq (r : α → α → Prop) : α → Prop where
| step : r a b → infSeq r b → infSeq r a
/--
info: infSeq.coinduct (α : Type) (r : α → α → Prop) (pred : α → Prop) (hyp : ∀ (x : α), pred x → ∃ b, r x b ∧ pred b)
(x✝ : α) : pred x✝ → infSeq α r x✝
-/
#guard_msgs in
#check infSeq.coinduct
/--
info: infSeq.step (α : Type) (r : α → α → Prop) {a b : α} : r a b → infSeq α r b → infSeq α r a
-/
#guard_msgs in
#check infSeq.step
end
```
The machinery also supports `mutual` blocks, as well as mixing inductive
and coinductive predicate definitions:
```lean4
mutual
coinductive tick : Prop where
| mk : ¬tock → tick
inductive tock : Prop where
| mk : ¬tick → tock
end
/--
info: tick.mutual_induct (pred_1 pred_2 : Prop) (hyp_1 : pred_1 → pred_2 → False) (hyp_2 : (pred_1 → False) → pred_2) :
(pred_1 → tick) ∧ (tock → pred_2)
-/
#guard_msgs in
#check tick.mutual_induct
```
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR changes how Lean proves the equational theorems for structural
recursion. The core idea is to let-bind the `f` argument to `brecOn` and
rewriting `.brecOn` with an unfolding theorem. This means no extra case
split for the `.rec` in `.brecOn` is needed, and `simp` doesn't change
the `f` argument which can break the definitional equality with the
defined function. With this, we can prove the unfolding theorem first,
and derive the equational theorems from that, like for all other ways of
defining recursive functions.
Backs out the changes from #10415, the old strategy works well with the
new goals.
Fixes#5667Fixes#10431Fixes#10195Fixes#2962
This PR adds the StreamMap type that enables multiplexing in
asynchronous streams.
This PR depends on: #10366, #10367 and #10370.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This PR adds the `IO.FS.hardLink` function, which can be used to create
hard links.
This is implemented via libuv's `uv_fs_link` function.
Lake hopes to make use of this function to decrease the storage cost of
restoring artifacts.
This PR also fixes some C implementation issues found in nearby similar
functions.
This PR adds a multi-consumer, multi-producer channel to Std.Sync.
This PR depends on: #10366, #10367 and #10370.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This PR implements the basic tactics for the new `grind` interactive
mode. While many additional `grind` tactics will be added later, the
foundational framework is already operational. The following `grind`
tactics are currently implemented: `skip`, `done`, `finish`, `lia`, and
`ring`.
This PR also removes the notion of `grind` fallback procedure since it
is subsumed by the new framework. Examples:
```lean
example (x y : Nat) : x ≥ y + 1 → x > 0 := by
grind => skip; lia; done
open Lean Grind
example [CommRing α] (a b c : α)
: a + b + c = 3 →
a^2 + b^2 + c^2 = 5 →
a^3 + b^3 + c^3 = 7 →
a^4 + b^4 + c^4 = 9 := by
grind => ring
```
This PR records extra mod uses that previously caused wrong unnecessary
import reports from shake.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR "monomorphizes" the structure `Std.PRange shape α`, replacing it
with nine distinct structures `Std.Rcc`, `Std.Rco`, `Std.Rci` etc., one
for each possible shape of a range's bounds. This change was necessary
because the shape polymorphism is detrimental to attempts of automation.
**BREAKING CHANGE:** While range/slice notation itself is unchanged,
this essentially breaks the entire remaining (polymorphic) range and
slice API except for the dot-notation(`toList`, `iter`, ...). It is not
possible to deprecate old declarations that were formulated in a
shape-polymorphic way that is not available anymore.
This PR explicitly tries to synthesize synthetic MVars in `mspec`. Doing
so resolves a bug triggered by use of the loop invariant lemma for
`Std.PRange`.
This PR exposes the definitions about `Int*`. The main reason is that
the `SInt` simprocs require many of them to be exposed. Furthermore,
`decide` now works with `Int*` operations. This fixes#10631.
