This PR reduces the amount of symbols in our DLLs by cutting open a
linking cycle of the shape:
`Environment -> Compiler -> Meta -> Environment`
This is achieved by introducing a dynamic call to the compiler hidden
behind a `Ref` as previously
done in the pretty printer.
This PR adds a field `isDisplayableTerm` to `TermInfo` and all utility
functions which create `TermInfo` that can be set to force the language
server to render the term in hover popups.
This PR fixes `input_dir` tracking to also recurse through
subdirectories. The `filter` of an `input_dir` will be applied to each
file in the directory tree (the path names of directories will not be
checked).
Closes#10827.
This PR improves the release automation. We link to CI output for
building the release tag, don't give instructions for bumping downstream
repositories until the release it ready, and improve documentation and
prompts.
This PR lets match compilation use exfalso as soon as no alternatives
are left. This way, the compiler does not have to look at subsequent
case splits.
This PR shows that the iterators returned by `String.Slice.split` and
`String.Slice.splitInclusive` are finite as long as the forward matcher
iterator for the pattern is finite (which we already know for all of our
patterns).
At actually also completely redefines the iterators to avoid the inner
loop in `Internal.nextMatch` which generates inefficient code. Instead,
when encountering a mismach from the matcher, we `skip` the split
iterator.
This PR improves the `grind` tactic generated by the `instantiate`
action in tracing mode. It also updates the syntax for the `instantiate`
tactic, making it similar to `simp`. For example:
* `instantiate only [thm1, thm2]` instantiates only theorems `thm1` and
`thm2`.
* `instantiate [thm1, thm2]` instantiates theorems marked with the
`@[grind]` attribute **and** theorems `thm1` and `thm2`.
The action produces `instantiate only [...]` tactics. Example:
```lean
/--
info: Try this:
[apply] ⏎
instantiate only [= Array.getElem_set]
instantiate only [= Array.getElem_set]
-/
#guard_msgs in
example (as bs cs : Array α) (v₁ v₂ : α)
(i₁ i₂ j : Nat)
(h₁ : i₁ < as.size)
(h₂ : bs = as.set i₁ v₁)
(h₃ : i₂ < bs.size)
(h₄ : cs = bs.set i₂ v₂)
(h₅ : i₁ ≠ j ∧ i₂ ≠ j)
(h₆ : j < cs.size)
(h₇ : j < as.size) :
cs[j] = as[j] := by
grind => finish?
```
Recall that `finish?` replays generated tactics before suggesting them.
The `instantiate` action inspects the generated proof term to decide
which theorems to include as parameters in the `instantiate only [...]`
tactic. However, in some cases, a theorem contributes only by adding a
term to the state. In such cases, the generated tactic cannot be fully
replayed, and the action uses
`instantiate approx [<thms instantiated>]` to indicate which parts of
the tactic script are approximate. The `approx` is just a hint for
users.
This PR implements the `finish?` tactic for the `grind` interactive
mode. When it successfully closes the goal, it produces a code action
that allows the user to close the goal using explicit grind tactic
steps, i.e., without any search. It also makes explicit which solvers
have been used.
This is just the first version, we will add many "bells and whistles"
later. For example, `instantiate` steps will clearly show which theorems
have been instantiated.
Example:
```lean
/--
info: Try this:
[apply] ⏎
cases #b0f4
next => cases #50fc
next => cases #50fc <;> lia
-/
#guard_msgs in
example (p : Nat → Prop) (x y z w : Int) :
(x = 1 ∨ x = 2) →
(w = 1 ∨ w = 4) →
(y = 1 ∨ (∃ x : Nat, y = 3 - x ∧ p x)) →
(z = 1 ∨ z = 0) → x + y ≤ 6 := by
grind => finish?
```
The anchors in the generated script are based on stable hash codes.
Moreover, users can hover over them to see the exact term used in the
case split. `grind?` will also be implemented using the new framework.
This PR implements support for `Action` in the `grind` solver extensions
(`SolverExtension`). It also provides the `Solvers.mkAction` function
that constructs an `Action` using all registered solvers. The generated
action is "fair," that is, a solver cannot prevent other solvers from
making progress.
This PR implements infrastructure for evaluating `grind` tactics in the
`GrindM` monad. We are going to use it to check whether auto-generated
tactics can effectively close the original goal.
This PR moves many operations involving `String.Pos.Raw` to a the
`String.Pos.Raw` namespace with the eventual aim of freeing up the
`String` namespace to contain operations using `String.ValidPos` (to be
renamed to `String.Pos`) instead.
This PR adds the `String.ValidPos.set` and `String.ValidPos.modify`
functions.
After this PR, `String.pos_lt_eq` is no longer a `simp` lemma. Add
`String.Pos.Raw.lt_iff` as a `simp` lemma if your proofs break.
This PR renames `String.split` to `String.splitToList`, because soon the
name `String.split` will be used by a new implementation which is
superior because it is polymorphic over the pattern kind and it returns
an iterator of slices instead of a list of strings.
This PR implements a compact notation for inspecting the `grind` state
in interactive mode. Within a `grind` tactic block, each tactic may
optionally have a suffix of the form `| filter?`.
Examples:
```lean
instantiate | gen > 0 -- Displays terms in the `grind` state after executing `instantiate` with generation greater than zero
```
```lean
instantiate | -- Displays the `grind` state after executing `instantiate`
```
Remark: If the user places the cursor one space before `|`, the state
*before* executing `instantiate` is displayed.
This PR removes the code that was silently displaying the `grind` state
after each tactic step, as it was too noisy.
It also updates the notation for the `first` combinator in the `grind`
tactic mode to avoid conflicts with the new syntax.
This PR changes match compilation to reject some pattern matches that
were previously accepted due to inaccessible patterns sometimes treated
like accessible ones. Fixes#10794.
This PR adds more selectors for TCP and Signals.
It also fixes a problem with `Selectors` that they cannot be closures
over a promise, otherwise it causes the waiter promise to never be
dropped.
This PR introduces the `backward.privateInPublic` option to aid in
porting projects to the module system by temporarily allowing access to
private declarations from the public scope, even across modules. A
warning will be generated by such accesses unless
`backward.privateInPublic.warn` is disabled.
This PR fixes `getHexNumSize` to consider underscores. Previously, only
the amount of bytes was counted, making it output 9 for `1234_abcd`
instead of the actual number of digits, which is 8.
the tested situation (kernel runs into deep recursion but elaborator is
happy) is not very stable and depends on, for example, stack size. This
test is not worth that hassle.
This PR adds adds union operation on `DHashMap`/`HashMap`/`HashSet` and
their raw variants and provides lemmas about union operations.
---------
Co-authored-by: Paul-Lez <paul.lezeau@gmail.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
