Extends the functionality of `lake test` and adds a parallel command in
`lake lint`.
* Rename `@[test_runner]` / `testRunner` to `@[test_driver]` /
`testDriver`. The old names are kept as deprecated aliases.
* Extend help page for `lake test` and adds one for `lake check-test`.
* Add `lake lint` and its parallel tag `@[lint_driver]` , setting
`lintDriver`, and checker `lake check-lint`.
* Add support for specifying test / lint drivers from dependencies.
* Add `testDriverArgs` / `lintDriverArgs` for fixing additional
arguments to the invocation of a driver script or executable.
* Add support for library test drivers (but not library lint drivers).
* `lake check-test` / `lake check-lint` only load the package (without
dependencies), not the whole workspace.
Closes#4116. Closes#4121. Closes#4142.
The type class `MonadStore1` and friends have an outParam, which should
not be an outParam, because there are multiple possible values for this
parameter. At this function
[fetchOrCreate](1382e9fbc4/src/lake/Lake/Load/Main.lean (L196C49-L196C63)),
there are multiple stacked `StateT` monad transformers that each give a
different instance to `MonadStore1`. It is an implementation detail of
type class synthesis which instance is found. This particular type class
synthesis fails when the unused instance
`Lake.instMonadStore1OfMonadDStoreOfFamilyOut` is set to a lower
priority, because then the synthesis order happens to go differently, so
the wrong instance is found.
Replacing the outParam with a semiOutParam solves this issue. Thus, we
make a new type class `MonadStore1Of`, which is the same, but with a
semiOutParam. This follows the design of `MonadState` and
`MonadStateOf`.
However, then it turns out that the instance cannot anymore be
synthesised.
There are two instances for `MonadStore1`:
```
instance [MonadDStore κ β m] : MonadStore1 k (β k) m
instance [MonadDStore κ β m] [FamilyOut β k α] : MonadStore1 k α m
```
The first one is problematic during unification, especially when `β`
should be instantiated as a constant function. We make the second one
sufficient by adding an instance for the general type family:
```
/-- The general type family -/
instance (priority := low) : FamilyDef Fam a (Fam a) where
family_key_eq_type := rfl
```
So then we can get rid of the first instance.
Without this, it would not easy but perhaps be feasible to break
incrementality when editing command prefixes such as `set_option ... in
theorem` or also `theorem namesp.name ...` (which is a macro),
especially if at some later point we support incrementality in input
shifted by an edit. Explicit, sound support for these common cases will
be brought back soon.
Changing document string in `Attributes.lean`, in order to consistent
with code in `Lean.Parser.Attr`.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
We are switching to a new system for preparing release notes.
* Release notes will be compiled when creating a release candidate from
all the commits that are part of that release.
* PRs can include suggestions for release notes in PR messages. Please
use language such as "release notes" and "breaking changes" to call
attention to the suggestions. Release notes are user-centric rather than
developer-centric.
* For more complicated release notes, these can be put into the
`releases_drafts` folder.
This solves an issue where PRs that include release notes can, when
merged, have those notes appear under the wrong Lean version, since they
might have been created before a release but not merged until after. It
also solves merge conflicts due to multiple PRs updating the release
notes.
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>
This PR extracts `msb_eq_false_iff_two_mul_lt` and
`msb_eq_true_iff_two_mul_ge` from #4179, and uses them to prove a
theorem that characterizes `BitVec.toInt` in terms of `BitVec.msb`. This
lemma will be useful to prove a bit-blasting theorem for `BitVec.slt`
and `BitVec.sle`.
Also cleans up an existing proof (`toInt_eq_toNat_cond `), which turns
out to be provable by `rfl`.
---------
Co-authored-by: Kim Morrison <scott@tqft.net>
this fixes#4078. It is an alternative fix to the one in #4137,
suggested
by @kmill.
Incidentially, it makes the unused variable linter better. My theory is
that
if we don’t reset the info when backtracking, the binder shows up more
than
once in the info tree, and then it is considered “used”, although there
are
just multiple binders.
for SSFT24 summer school: https://github.com/david-christiansen/ssft24
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
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>
This ensures that rotateLeft/Right behave correctly even when the
rotation amount is larger than the bitwidth.
This shall be followed up with `getLsb` theorems for rotations for
LeanSAT.
We choose to write `aux` definitions since it is cleaner to reason about
the `aux` theorems with the assumption that `rotation-amount <
bit-width`, followed by auxiliary lemmas that link the behavior of
rotation to the canonical case when `rotation-amount < bit-width`.
Proof strategy we will execute based on these definitions: [Link to
proof of
`getLsb_rotateLeft`](a0b18ec0f4/src/Init/Data/BitVec/Lemmas.lean (L1129-L1204))
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
The ANSI mode build monitor now now longer displays built jobs (instead
only those that print info or failed). Also upgrades the progress ticker
with a spinner icon and information on the number of running jobs.
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
Show that shifting a natural number left and then shifting right by the
same amount is a no-op.
I originally proved this in a different PR, ended up not needing the
fact after all, but it still seemed like a generally useful simp lemma
to have.
Fixes two output bugs with cloud releases: (1) the fetch as part of an
`extraDep` was not properly isolated in a job, and (2) the release job
would be shown even if the release had already been successfully
fetched.
Also includes some related touchups, including the addition of show all
jobs on `-v` which helps with debugging job counts.
### Explanation
In the case that `assignSyntheticOpaque := true` and the given
metavariable is `syntheticOpaque` and the depth of the metavariable is
not the current depth, `isReadOnlyOrSyntheticOpaque` returns false, even
though the metavariable is read-only because of being declared at a
smaller depth. This causes the metavariable to (wrongly) be able to be
instantiated by `isDefEq`.
This bug was found at the proof of
[RingHom.PropertyIsLocal.sourceAffineLocally_of_source_openCover](https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.html#RingHom.PropertyIsLocal.sourceAffineLocally_of_source_openCover),
which involves a type class synthesis for `CommRing ?m.2404`, and the
synthesis manages to instantiate this metavariable into different
values, even though `synthInstance?` increases the metavariable depth.
This synthesis fails after 1 second.
I found the bug while modifying the instance synthesis code: the
modified code spent several minutes on this failed synthesis.
### Test
The problem can be verified with the test:
```
run_meta do
let m ← mkFreshExprMVar (Expr.sort levelOne) MetavarKind.syntheticOpaque
withAssignableSyntheticOpaque do
withNewMCtxDepth do
let eq ← isDefEq m (.const ``Nat [])
Lean.logInfo m! "{eq}"
```
this unification used to succeed, giving `true`, and this fix makes it
return `false`.
### Impact on Mathlib
This fix causes a change in the behaviour of `congr`, `convert` and
friends, which breaks a couple of proofs in mathlib. Most of these are
fixed by supplying more arguments.
I fixed these proofs, and
[benched](http://speed.lean-fro.org/mathlib4/compare/b821bfd9-3769-4930-b77f-0adc6f9d218f/to/e7b27246-a3e6-496a-b552-ff4b45c7236e?hash2=4f3c460cc1668820c9af8418a87a23db44c7acab)
mathlib. The result is that most files are unaffected, but some files
are significantly improved. This is most prominent in
Mathlib.RingTheory.Jacobson, where the number of instructions has
decreased by 28%. The overall improvement is a 0.3% reduction in
instructions.
[Zulip
message](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Ways.20to.20speed.20up.20Mathlib/near/439218960)
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).
