# Summary
This makes a small addition to our take on the LSP protocol
in the form of supporting snippet text edits.
It has been discussed
[here](https://github.com/microsoft/language-server-protocol/issues/592)
on the LSP issue tracker for a while,
but seems unlikely to be added anytime soon.
This feature was requested by @PatrickMassot for the purposes
of supporting Lean code templates in code actions and widgets.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
There were no `quot_precheck` instances registered for the expression
tree elaborators, which prevented them from being usable in a `notation`
expansion without turning off the quotation prechecker.
Users can evaluate whether `set_option quotPrecheck false` is still
necessary for their `notation` definitions.
Switches from encoding `let_fun` using an annotated `(fun x : t => b) v`
expression to a function application `letFun v (fun x : t => b)`.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Fixes reference implementation of `ByteArray.copySlice`, as reported
https://github.com/leanprover/lean4/issues/2966.
Adds tests.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
If a user deleted `lakefile.olean` manually without deleting
`lakefile.olean.lock`, Lake would still attempt to load it and thus
produce an error. Now it should properly re-elaborate the configuration
file.
This adds a `test_extern` command.
Usage:
```
import Lean.Util.TestExtern
test_extern Nat.add 17 37
```
This:
* Checks that the head symbol has an `@[extern]` attribute.
* Writes down `t == t'`, where `t` is the term provided, and `t'` is the
reference implementation (specifically, `t` with the head symbol
unfolded).
* Tries to reduce this to `true`, and complains if this fails.
Note that the type of the term must have a `BEq` instance for this to
work: there's a self-explanatory error message if it isn't available.
This definition was clearly meant to be in the `List` namespace, but it
is also in a `namespace Lean` so it ended up as `Lean.List.toSMap`
instead of `List.toSMap`. It would be nice if #3031 made this
unnecessary, but for now this seems to be the convention.
I noticed this because of another side effect: it defines `Lean.List` as
a namespace, which means that
```lean
import Std
namespace Lean
open List
#check [1] <+ [2]
```
does not work as expected, it opens the `Lean.List` namespace instead of
the `List` namespace. Should there be a regression test to ensure that
the `Lean.List` namespace (and maybe others) are not accidentally
created? (Unfortunately this puts a bit of a damper on #3031.)
Fixes an issue reported on Zulip; see the test case.
* Modifies the `MonadBacktrack` instance for `SimpM` to also backtrack
the `UsedSimps` field.
* When calling the discharger, `saveState`, and then `restoreState` if
something goes wrong.
I'm not certain that it makes sense to restore the `MetaM` state if
discharging fails. I can easily change this to more conservatively just
backtrack the `UsedSimps` after failed discharging.
Changes the implementation of `List.all` and `List.any` so they
short-circuit. The implementations are tail-recursive.
This replaces https://github.com/leanprover/std4/pull/392, which was
going to do this with `@[csimp]`.
until around 7fe6881 the way to define well-founded recursions was to
specify a `WellFoundedRelation` on the argument explicitly. This was
rather low-level, for example one had to predict the packing of multiple
arguments into `PProd`s, the packing of mutual functions into `PSum`s,
and the cliques that were calculated.
Then the current `termination_by` syntax was introduced, where you
specify the termination argument at a higher level (one clause per
functions, unpacked arguments), and the `WellFoundedRelation` is found
using type class resolution.
The old syntax was kept around as `termination_by'`. This is not used
anywhere in the lean, std, mathlib or the theorem-proving-in-lean
repositories,
and three occurrences I found in the wild can do without
In particular, it should be possible to express anything that the old
syntax
supported also with the new one, possibly requiring a helper type with a
suitable instance, or the following generic wrapper that now lives in
std
```
def wrap {α : Sort u} {r : α → α → Prop} (h : WellFounded r) (x : α) : {x : α // Acc r x}
```
Since the old syntax is unused, has an unhelpful name and relies on
internals, this removes the support. Now is a good time before the
refactoring that's planned in #2921.
The test suite was updated without particular surprises.
The parametric `terminationHint` parser is gone, which means we can
match on syntax more easily now, in `expandDecreasingBy?`.
The elaborator is prone to duplicate terms, including recursive calls,
even if the user only wrote a single one. This duplication is wasteful
if we run the tactics on duplicated calls, and confusing in the output
of GuessLex. So prune the list of recursive calls, and remove those
where another call exists that has the same goal and context that is no
more specific.
Implements "gaps" in string literals. These are escape sequences of the
form `"\" newline whitespace+` that have the interpretation of an empty
string. For example,
```
"this is \
a string"
```
is equivalent to `"this is a string"`. These are modeled after string
continuations in
[Rust](https://doc.rust-lang.org/beta/reference/tokens.html#string-literals).
Implements RFC #2838
before code like
def dup (a : Nat) (b : Nat := a) := a + b
def rec : Nat → Nat
| 0 => 1
| n+1 => dup (dup (dup (rec n)))
decreasing_by decreasing_tactic
would run the `decreasing_tactic` 8 tims, because the recursive call
`rec n` gets duplicate due to the default paramter. Similar effects can
be observed due to dependent types or tactics like `cases`.
This is wasteful, and is confusing to the user when they use
`decreasing_by` interactively. Therfore, we now go through the proof
obligations (MVars) and if solving one would imply solving another one,
we assign the mvars to each other accordingly.
This PR is a sibling of #3004.
I found the documentation page hard to parse, so I figured I should fix
this. It's mostly indentation (e.g. in lists), some line breaks and
making URLs clickable.
With
set_option showInferredTerminationBy true
this prints a message like
Inferred termination argument:
termination_by
ackermann n m => (sizeOf n, sizeOf m)
it tries hard to use names that
* match the names that the user used, if present
* have no daggers (so that it can be copied)
* do not shadow each other
* do not shadow anything from the environment (just to be nice)
it does so by appending sufficient `'` to the name.
Some of the emitted `sizeOf` calls are unnecessary, but they are needed
sometimes with dependent parameters. A follow-up PR will not emit them
for non-dependent arguments, so that in most cases the output is pretty.
Somewhen down the road we also want a code action, maybe triggered by
`termination_by?`. This should come after #2921, as that simplifies that
feature (no need to merge termination arguments from different cliques
for example.)
by showing the matrix of calls and measures, and what we know about that
call (=, <, ≤, ?), e.g.
guessLexFailures.lean:27:0-33:31: error: Could not find a decreasing
measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
x1 x2 x3
1) 29:6-25 = = =
2) 30:6-23 = ? <
3) 31:6-23 < _ _
Please use `termination_by` to specify a decreasing measure
It’s a bit more verbose for mutual functions.
It will use the user-specified argument names for functions written
```
foo (n : Nat) := …
```
but not with pattern matching like
```
foo : Nat → …
| n => …
```
This can be refined later and separately (and maybe right away in
`expandMatchAltsWhereDecls`).
This is pure refactoring: Instead of solving each subgoal as we
encounter it while traversing the syntax tree, we leave the `MVar`
there, at the end collect them all using `getMVarsNoDelayed`, and then
solve them.
This is a refactoring preparing for two upcoming changes:
* removing unexpected duplicate goals that can arise from term
duplication
* running interactive tactics on all, not each goal (#2921)
In order to not regress with error locations, we have to associated the
`TermElabM`’s syntax refernce with the `MVar` somehow. I do this using
the existing `mkRecAppWithSyntax` expression annotation, on the `MVar`’s
type. Alternatives would be stack another `StateT` on the traversal
and accumulate `Array (MVarId, Syntax)` explicitly, but that did not
seem to be more appealing.
In order to familiarize myself with this code, and so that the next
person has an easier time, I
* added docstrings explaining what I found out these things to
* rewrote the syntax expansion functions using syntax pattern matches,
to the extend possible
else I see
```
[ 69%] Building CXX object runtime/CMakeFiles/leanrt.dir/platform.cpp.o
/home/jojo/build/lean/lean4/src/runtime/io.cpp:509:75: warning: 'static_assert' with no message is a C++17 extension [-Wc++17-extensions]
static_assert(sizeof(std::chrono::milliseconds::rep) <= sizeof(uint64));
^
, ""
/home/jojo/build/lean/lean4/src/runtime/io.cpp:517:74: warning: 'static_assert' with no message is a C++17 extension [-Wc++17-extensions]
static_assert(sizeof(std::chrono::nanoseconds::rep) <= sizeof(uint64));
^
, ""
2 warnings generated.
```
when building
which also removes an error condition at the use site.
While I am at it, I rename a parameter in `GuessLex` that I forgot to
rename earlier.
The effect will be user-visible (in obscure corner cases) with #2960, so
I’ll have the test there.
A few places would benefit from a `lambdaTelescopeBounded` that
garantees the result has the right length (eta-expanding when
necessary). I’ll look into that separately, and left TODOs here.
Now that there is a helpful message at the point of use when
`supportInterpreter` is required, we don't need to clutter every
`lakefile` with the advice.
If here is only one plausible measure, there is no point having the
`GuessLex` code see if it
is terminating, running all the tactics, only for the `MkFix` code then
run the tactics again.
So if there is only one plausible measure (non-mutual recursion with
only one varying
parameter), just use that measure.
Side benefit: If the function isn’t terminating, more detailed error
messages are shown
(failing proof goals), located at the recursive calls.
Removes the `CI` option from the `math` template. Since the template
does not currently generate a GitHub workflow, it does not do anything
out of the box except add unnecessary complexity.
The `math` template is also now tested in `tests/init` (minus the
Mathlib `require`).
This improves Lean’s capabilities to guess the termination measure for
well-founded
recursion, by also trying lexicographic orders. For example:
def ackermann (n m : Nat) := match n, m with
| 0, m => m + 1
| .succ n, 0 => ackermann n 1
| .succ n, .succ m => ackermann n (ackermann (n + 1) m)
now just works.
The module docstring of `Lean.Elab.PreDefinition.WF.GuessLex` tells the
technical story.
Fixes#2837
Closes#2548.
Later packages and libraries in the dependency tree are now preferred
over earlier ones. That is, the later ones "shadow" the earlier ones.
Such an ordering is more consistent with how declarations generally work
in programming languages.
This will break any package that relied on the previous ordering.
Also includes a related fix to `findModule?` that mistakenly treated
executable roots as importable.
Improves executable handling in `lake exe` and `lake init`:
* `lake exe <target>` now parses `target` like a build target (as the
help text states it should) rather than as a basic name.
* `lake new foo.bar [std]` now generates executables named `foo-bar`.
* `lake new foo.bar exe` now properly creates `foo/bar.lean`.
these are compagnions to `MatcherApp.addArg` and `CasesOnApp.addArg`
when one only has an
expression (which may not be a type) to transform, but not a concret
values.
This is a prerequisite for guessing lexicographic order (#2874). Keeping
this on a separate PR because it’s sizable, and has a clear independent
specification.
