This PR replaces `List.lt` with `List.Lex`, from Mathlib, and adds the
new `Bool` valued lexicographic comparatory function `List.lex`. This
subtly changes the definition of `<` on Lists in some situations.
`List.lt` was a weaker relation: in particular if `l₁ < l₂`, then
`a :: l₁ < b :: l₂` may hold according to `List.lt` even if `a` and `b`
are merely incomparable
(either neither `a < b` nor `b < a`), whereas according to `List.Lex`
this would require `a = b`.
When `<` is total, in the sense that `¬ · < ·` is antisymmetric, then
the two relations coincide.
Mathlib was already overriding the order instances for `List α`,
so this change should not be noticed by anyone already using Mathlib.
We simultaneously add the boolean valued `List.lex` function,
parameterised by a `BEq` typeclass
and an arbitrary `lt` function. This will support the flexibility
previously provided for `List.lt`,
via a `==` function which is weaker than strict equality.
This reduces the number of reimplemented functions which complicate
proofs. After inlining it ends up the same as before.
`ltOfOrd` is also changed to use `compare a b = .lt` instead of
`(compare a b == .lt) = true`, for consistency with the normal form in
std.
This is a rewrite of the `UnusedVariables` lint to inline and simplify
many of the dependent functions to try to improve the performance of
this lint, which quite often shows up in perf reports.
* The mvar assignment scanning is one of the most expensive parts of the
process, so we do two things to improve this:
* Lazily perform the scan only if we need it
* Use an object-pointer hashmap to ensure that we don't have quadratic
behavior when there are many mvar assignments with slight differences.
* The dependency on `Lean.Server` is removed, meaning we don't need to
do the LSP conversion stuff anymore. The main logic of reference finding
is inlined.
* We take `fvarAliases` into account, and union together fvars which are
aliases of a base fvar. (It would be great if we had `UnionFind` here.)
More docs will be added once we confirm an actual perf improvement.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Sends a diagnostic informing the user to run Restart File when a file
dependency is saved.
Based on #3014 because this feature was easier to implement with the new
architecture.
ToDo:
- [x] Adjust vscode-lean4 to display a notification when this diagnostic
appears in a non-annoying way
(https://github.com/leanprover/vscode-lean4/pull/393)
- [x] Use a file watcher to identify changes to files not tracked by VS
Code
- [x] Rebase onto master when #3014 is merged
For many data structures having an ordering is necessary. This one adds the `Ord` type class and a deriving handler for it. The ordering is based on order of constructors followed by lexicographical ordering within a constructor.
