Remark: when splitting an `if-then-else` term, the subgoals now have
tags `isTrue` and `isFalse` instead of `inl` and `inr`.
closes#4313
---------
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
this fixes a usability paper cut that just annoyed me. When editing a
larger simp proof, I usually want to see the goal state after the simp,
and this is what I see while the `simp` command is complete. But then,
when I start typing, and necessarily type incomplete lemma names, that
error makes `simp` do nothing again and I see the original goal state.
In fact, if a prefix of the simp theorem name I am typing is a valid
identifier, it jumps even more around.
With this PR, using `logException`, I still get the red squiggly lines
for the unknown identifer, but `simp` just ignores that argument and
still shows me the final goal. Much nicer.
I also demoted the message for `[-foo]` when `foo` isn’t `simp` to a
warning and gave it the correct `ref`.
See it in action here: (in the middle, when you suddenly see the
terminal,
I am switching lean versions.)
https://github.com/leanprover/lean4/assets/148037/8cb3c563-1354-4c2d-bcee-26dfa1005ae0
Extends Lean's incremental reporting and reuse between commands into
various steps inside declarations:
* headers and bodies of each (mutual) definition/theorem
* `theorem ... := by` for each contained tactic step, including
recursively inside supported combinators currently consisting of
* `·` (cdot), `case`, `next`
* `induction`, `cases`
* macros such as `next` unfolding to the above
*Incremental reuse* means not recomputing any such steps if they are not
affected by a document change. *Incremental reporting* includes the
parts seen in the recording above: the progress bar and messages. Other
language server features such as hover etc. are *not yet* supported
incrementally, i.e. they are shown only when the declaration has been
fully processed as before.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Add docstrings, usage examples, and doc tests for `String.prev`,
`.front`, `.back`, `.atEnd`.
Improve docstring examples for `String.next` based on discussion
examples for `String.prev`.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
To eliminate parsing differences between Windows and other platforms,
the frontend now normalizes all CRLF line endings to LF, like [in
Rust](https://github.com/rust-lang/rust/issues/62865).
Effects:
- This makes Lake hashes be faithful to what Lean sees (Lake already
normalizes line endings before computing hashes).
- Docstrings now have normalized line endings. In particular, this fixes
`#guard_msgs` failing multiline tests for Windows users using CRLF.
- Now strings don't have different lengths depending on the platform.
Before this PR, the following theorem is true for LF and false for CRLF
files.
```lean
example : "
".length = 1 := rfl
```
Note: the normalization will take `\r\r\n` and turn it into `\r\n`. In
the elaborator, we reject loose `\r`'s that appear in whitespace. Rust
instead takes the approach of making the normalization routine fail.
They do this so that there's no downstream confusion about any `\r\n`
that appears.
Implementation note: the LSP maintains its own copy of a source file
that it updates when edit operations are applied. We are assuming that
edit operations never split or join CRLFs. If this assumption is not
correct, then the LSP copy of a source file can become slightly out of
sync. If this is an issue, there is some discussion
[here](https://github.com/leanprover/lean4/pull/3903#discussion_r1592930085).
Given `h` with type `x + k = y + k'` (or `h : k = k')`, `cases h`
produced a proof of size linear in `min k k'`. `isDefEq` has support for
offset, but `unifyEq?` did not have it, and a stack overflow occurred
while processing the resulting proof. This PR fixes this issue.
closes#4219
The expression tree elaborator computes a "maxType" that every leaf term
can be coerced to, but the elaborator was not ensuring that the entire
expression tree would have maxType as its type. This led to unexpected
errors in examples such as
```lean
example (a : Nat) (b : Int) :
a = id (a * b^2) := sorry
```
where it would say it could not synthesize an `HMul Int Int Nat`
instance (the `Nat` would propagate from the `a` on the LHS of the
equality). The issue in this case is that `HPow` uses default instances,
so while the expression tree elaborator decides that `a * b^2` should be
referring to an `Int`, the actual elaborated type is temporarily a
metavariable. Then, when the binrel elaborator is looking at both sides
of the equality, it decides that `Nat` will work and coercions don't
need to be inserted.
The fix is to unify the type of the resulting elaborated expression with
the computed maxType. One wrinkle is that `hasUncomparable` being false
is a valid test only if there are no leaf terms with unknown types (if
they become known, it could change `hasUncomparable` to true), so this
unification is only performed if the leaf terms all have known types.
Fixes issue described by Floris van Doorn on
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/elaboration.20issue.20involving.20powers.20and.20sums/near/439243587).
The `simp` tactic uses a discrimination tree to select candidate
theorems that will be used to rewrite an expression. This indexing data
structure minimizes the number of theorems that need to be tried and
improves performance. However, indexing modulo reducibility is
challenging, and a theorem that could be applied, when taking reduction
into account, may be missed. For example, suppose we have a `simp`
theorem `foo : forall x y, f x (x, y).2 = y`, and we are trying to
simplify the expression `f a b <= b`. `foo` will not be tried by `simp`
because the second argument of `f a b` is not a projection of a pair.
However, `f a b` is definitionally equal to `f a (a, b).2` since we can
reduce `(a, b).2`.
In Lean 3, we had a much simpler indexing data structure where only the
head symbol was taken into account. For the theorem `foo`, the head
symbol is `f`. Thus, the theorem would be considered by `simp`.
This commit adds the option `Simp.Config.index`. When `simp (config := {
index := false })`, only the head symbol is considered when retrieving
theorems, as in Lean 3. Moreover, if `set_option diagnostics true`,
`simp` will check whether every applied theorem would also have been
applied if `index := true`, and report them. This feature can help users
diagnose tricky issues in code that has been ported from libraries
developed using Lean 3 and then ported to Lean 4. In the following
example, it will report that `foo` is a problematic theorem.
```lean
opaque f : Nat → Nat → Nat
@[simp] theorem foo : f x (x, y).2 = y := by sorry
example : f a b ≤ b := by
set_option diagnostics true in
simp (config := { index := false })
```
In the example above, the following diagnostic message is produced.
```lean
[simp] theorems with bad keys
foo, key: [f, *, Prod.1, Prod.mk, Nat, Nat, *, *]
```
With the information above, users can annotate theorems such as `foo`
using `no_index` for problematic subterms.
Example:
```lean
opaque f : Nat → Nat → Nat
@[simp] theorem foo : f x (no_index (x, y).2) = y := by sorry
example : f a b ≤ b := by
simp -- `foo` is still applied
```
cc @semorrison
cc @PatrickMassot
Many of our tests in `tests/lean/run/` produce output from `#eval` (or
`#check`) statements, that is then ignored.
This PR tries to capture all the useful output using `#guard_msgs`. I've
only done a cursory check that the output is still sane --- there is a
chance that some "unchecked" tests have already accumulated regressions
and this just cements them!
In the other direction, I did identify two rotten tests:
* a minor one in `setStructInstNotation.lean`, where a comment says `Set
Nat`, but `#check` actually prints `?_`. Weird?
* `CompilerProbe.lean` is generating empty output, apparently indicating
that something is broken, but I don't know the signficance of this file.
In any case, I'll ask about these elsewhere.
(This started by noticing that a recent `grind` test file had an
untested `trace_state`, and then got carried away.)
Summary:
- Take `synthPendingDepth` into account when caching TC results
- Add `maxSynthPendingDepth` option with default := 2.
- Add support for tracking `synthPending` failures when using
`set_option diagnostics true`
closes#2522closes#3313closes#3927
Identical to #4114 but with `maxSynthPendingDepth := 1`
closes#4114
cc @semorrison
Adds `IO.getTaskState` which returns the state of a `Task` in the Lean
runtime's task manager. The `TaskState` inductive has 3 constructors:
`waiting`, `running`, and `finished`. The `waiting` constructor
encompasses the waiting and queued states within the C task object
documentation, because the task object does not provide a low cost way
to distinguish these different forms of waiting. Furthermore, it seems
unlikely for consumers to wish to distinguish between these internal
states. The `running` constructor encompasses both the running and
promised states in C docs. While not ideal, the C implementation does
not provide a way to distinguish between a running `Task` and a waiting
`Promise.result` (they both have null closures).
The main loop logic could be simplified, and `if let` could be used to
make control flow more obvious.
Also adds a check for macro scopes to prevent `unresolveNameGlobal` from
returning names with macro scopes in the event there's an alias with
one.
This is a follow up to #3946.
we keep running into examples where working with well-founded recursion
is slow because defeq checks (which are all over the place, including
failing ones that are back-tracked) unfold well-founded definitions.
The definition of a function defined by well-founded recursion should be
an implementation detail that should only be peeked inside by the
equation generator and the functional induction generator.
We now mark the mutual recursive function as irreducible (if the user
did not
set a flag explicitly), and use `withAtLeastTransparency .all` when
producing
the equations.
Proofs can be fixed by using rewriting, or – a bit blunt, but nice for
adjusting
existing proofs – using `unseal` (a.k.a. `attribute [local
semireducible]`).
Mathlib performance does not change a whole lot:
http://speed.lean-fro.org/mathlib4/compare/08b82265-75db-4a28-b12b-08751b9ad04a/to/16f46d5e-28b1-41c4-a107-a6f6594841f8
Build instructions -0.126 %, four modules with significant instructions
decrease.
To reduce impact, these definitions were changed:
* `Nat.mod`, to make `1 % n` reduce definitionally, so that `1` as a
`Fin 2` literal
works nicely. Theorems with larger `Fin` literals tend to need a `unseal
Nat.modCore`
https://github.com/leanprover/lean4/pull/4098
* `List.ofFn` rewritten to be structurally recursive and not go via
`Array.ofFn`:
https://github.com/leanprover-community/batteries/pull/784
Alternative designs explored were
* Making `WellFounded.fix` irreducible.
One benefit is that recursive functions with equal definitions (possibly
after
instantiating fixed parameters) are defeq; this is used in mathlib to
relate
[`OrdinalApprox.gfpApprox`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Ordinal/FixedPointApproximants.html#OrdinalApprox.gfpApprox)
with `.lfpApprox`.
But the downside is that one cannot use `unseal` in a
targeted way, being explicit in which recursive function needs to be
reducible here.
And in cases where Lean does unwanted unfolding, we’d still unfold the
recursive
definition once to expose `WellFounded.fix`, leading to large terms for
often no good
reason.
* Defining `WellFounded.fix` to unroll defintionally once before hitting
a irreducible
`WellFounded.fixF`. This was explored in #4002. It shares most of the
ups and downs
with the previous variant, with the additional neat benefit that
function calls that
do not lead to recursive cases (e.g. a `[]` base case) reduce nicely.
This means that
the majority of existing `rfl` proofs continue to work.
Issue #4051, which demonstrates how badly things can go if wf recursive
functions can be
unrolled, showed that making the recursive function irreducible there
leads to noticeably
faster elaboration than making `WellFounded.fix` irreducible; this is
good evidence that
the present PR is the way to go.
This fixes https://github.com/leanprover/lean4/issues/3988
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
This fixes#2901, a bug in the old compiler which causes a segfault. The
issue is that when visiting `noConfusion` applications, it assumes that
each constructor case has `nfields` arguments, e.g. `head1 = head2 ->
tail1 = tail2 -> P` has two arguments because `List.cons` has 2 fields,
but in fact propositional fields are skipped by the noConfusion type
generator, so for example `Subtype.noConfusionType` is:
```lean
@[reducible] protected def Subtype.noConfusionType.{u_1, u} : {α : Sort u} →
{p : α → Prop} → Sort u_1 → Subtype p → Subtype p → Sort u_1 :=
fun {α} {p} P v1 v2 ↦
Subtype.casesOn v1 fun val property ↦ Subtype.casesOn v2 fun val_1 property ↦
(val = val_1 → P) → P
```
where `val = val_1 → P` only has the one argument even though
`Subtype.mk` has two fields, presumably because it is useless to have an
equality of propositions. Unfortunately there isn't any easy cache or
getter to use here to get the number of non-propositional fields, so we
just calculate it on the spot.
