This PR implements zero cost `BaseIO` by erasing the `IO.RealWorld`
parameter from argument lists and structures. This is a **major breaking
change for FFI**.
Concretely:
- `BaseIO` is defined in terms of `ST IO.RealWorld`
- `EIO` (and thus `IO`) is defined in terms of `EST IO.RealWorld`
- The opaque `Void` type is introduced and the trivial structure
optimization updated to account for it. Furthermore, arguments of type
`Void s` are removed from the argument lists of the C functions.
- `ST` is redefined as `Void s -> ST.Out s a` where `ST.Out` is a pair
of `Void s` and `a`
This together has the following major effects on our generated code:
- Functions that return `BaseIO`/`ST`/`EIO`/`IO`/`EST` now do not take
the dummy world parameter anymore. To account for this FFI code needs to
delete the dummy world parameter from the argument lists.
- Functions that return `BaseIO`/`ST` now return their wrapped value
directly. In particular `BaseIO UInt32` now returns a `uint32_t` instead
of a `lean_object*`. To account for this FFI code might have to change
the return type and does not need to call `lean_io_result_mk_ok` anymore
but can instead just `return` values right away (same with extracting
values from `BaseIO` computations.
- Functions that return `EIO`/`IO`/`EST` now only return the equivalent
of an `Except` node which reduces the allocation size. The
`lean_io_result_mk_ok`/`lean_io_result_mk_error` functions were updated
to account for this already so no change is required.
Besides improving performance by dropping allocation (sizes) we can now
also do fun new things such as:
```lean
@[extern "malloc"]
opaque malloc (size : USize) : BaseIO USize
```
This PR renames the cast functions on `String.ValidPos` for `set` and
`modify` to adhere to the established naming convention.
It also fixes two typos and very slighly tweaks the import graph,
shortening the critical path by a negligible amount.
This PR fixes a bug with Lake's cache where revisions were stored at the
incorrect path. Revisions were stored at `<rev>/<pkg>.jsonl` rather than
the correct `<pkg>/<rev>.jsonl`.
This PR fixes a proof instability source in `grind`.
We say a proof is *unstable* if minor changes in the `.lean` file
containing the proof **affect** it.
This PR adds a missing move assignment operator, and deletes the copy
assignment operator.
C++ types should not implement move constructors without also
implementing move assignment. This also ensures that `m_fn` is correctly
emptied after a move, which is not guaranteed by the standard.
This change is also needed to allow `lean::optional` to be eventually
replaced by `std::optional`.
This PR improves the performance of `mvcgen` by an optimized
implementation for `try (mpure_intro; trivial)`. This tactic sequence is
used to eagerly discharge VCs and in the process instantiates schematic
variables.
This PR renames `String.endPos` to `String.rawEndPos`, as in a future
release the name `String.endPos` will be taken by the function that is
currently called `String.endValidPos`.
This PR fixes a bug in `String.Slice.takeWhile` which caused it to get
its bookkeeping wrong and panic. The new version only uses safe
operations on `String.Slice.Pos`.
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.
