The linters in Batteries can be used to spot mistakes in Lean. See the
message on
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Go-to-def.20on.20typeclass.20fields.20and.20type-dependent.20notation/near/442613564).
These are the different linters with errors:
- unusedArguments:
There are many unused instance arguments, especially a redundant `[Monad
m]` is very common
- checkUnivs:
There was a problem with universes in a definition in
`Init.Control.StateCps`. I fixed it by adding a `variable` statement for
the implicit arguments in the file.
- defLemma:
many proofs are written as `def` instead of `theorem`, most notably
`rfl`. Because `rfl` is used as a match pattern, it must be a def. Is
this desirable?
The keyword `abbrev` is sometimes used for an alias of a theorem, which
also results in a def. I would want to replace it with the `alias`
keyword to fix this, but it isn't available.
- dupNamespace:
I fixed some of these, but left `Tactic.Tactic` and `Parser.Parser` as
they are as these seem intended.
- unusedHaveSuffices:
I cleaned up a few proofs with unused `have` or `suffices`
- explicitVarsOfIff:
I didn't fix any of these, because that would be a breaking change.
- simpNF:
I didn't fix any of these, because I think that requires knowing the
intended simplification order.
Continuation of #3958. To ensure that lean code is able to uphold the
invariant that `String`s are valid UTF-8 (which is assumed by the lean
model), we have to make sure that no lean objects are created with
invalid UTF-8. #3958 covers the case of lean code creating strings via
`fromUTF8Unchecked`, but there are still many cases where C++ code
constructs strings from a `const char *` or `std::string` with unclear
UTF-8 status.
To address this and minimize accidental missed validation, the
`(lean_)mk_string` function is modified to validate UTF-8. The original
function is renamed to `mk_string_unchecked`, with several other
variants depending on whether we know the string is UTF-8 or ASCII and
whether we have the length and/or utf8 char count on hand. I reviewed
every function which leads to `mk_string` or its variants in the C code,
and used the appropriate validation function, defaulting to `mk_string`
if the provenance is unclear.
This PR adds no new error handling paths, meaning that incorrect UTF-8
will still produce incorrect results in e.g. IO functions, they are just
not causing unsound behavior anymore. A subsequent PR will handle adding
better error reporting for bad UTF-8.
this is a first step towards porting the code `constructions.cpp` to
Lean: It leaves the construction of the `Declaration` untouched, but
moves adding the declarations to the environment, and setting various
attributes, to the Lean world.
This allows the remaining logic (the construction of the `Declaration`)
to be implemented in Lean separately and easily compared to the C++
implementation, before we replace that too.
To that end, `Declaraion` gains an `BEq` instance.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
Co-authored-by: Arthur Adjedj <arthur.adjedj@ens-paris-saclay.fr>
Fixes a bug in #4371 where the version of a package used by a dependency
would take precedence over that of a the same package as a direct
dependency if that package had a a manifest. This was because the direct
dependency's manifest entries were added before all the direct
dependencies were visited.
A set of general tweaks of the `require` syntax and docs that provide a
base for #4495.
The sole significant behavioral change is that the `name` field of a
`require` in TOML now falls back to being interpreted as a simple string
name if the value is not a valid Lean identifier. This means that a
require for a package like `doc-gen4` can be written without French
quotes.
I removed a redundant `if tFn.isMVar || sFn.isMVar then ... else return
LBool.undef` in the `else` clause of
```
if !tFn.isMVar && !sFn.isMVar then
return LBool.undef
else
```
I made a modification to the `mkLambdaFVars` function, adding a
`etaReduce : Bool` parameter that determines whether a new lambda of the
form `fun x => f x` should be replaced by `f`. I then set this option to
true at `isDefEq` when processing metavariable assignments.
This means that many unnecessary eta unreduced expression are now
reduced. This is beneficial for users, so that they do not have to deal
with such unreduced expressions. It is also beneficial for performance,
leading to a 0.6% improvement in build instructions. Most notably,
`Mathlib.Algebra.DirectLimit`, previously a top 50 slowest file, has
sped up by 40%.
Quite a number of proof in mathlib broke. Many of these involve removing
a now unnecessary `simp only`. In other cases, a simp or rewrite doesn't
work anymore, such as a `simp_rw [mul_comm]` that was used to rewrite
`fun x => 2*x`, but now this term has turned into `HMul.hMul 2`.
Closes#4386
This is not the most exciting place to start, but I started here to:
* pick a function with little development in Batteries and Mathlib, so I
wouldn't have conflicts
* that is easy!
* to see how much effort it is to get fairly complete coverage
* and to set up some infrastructure to be used later, i.e.
`tests/lean/run/list_simp.lean`
This assigns priorities to the equational lemmas so that more specific
ones
are tried first before a possible catch-all with possible
side-conditions.
We assign very low priorities to match the simplifiers behavior when
unfolding
a definition, which happens in `simpLoop`’ `visitPreContinue` after
applying
rewrite rules.
Definitions with more than 100 equational theorems will use priority 1
for all
but the last (a heuristic, not perfect).
fixes#4173, to some extent.
`Nat.succ_eq_add_one` and `Nat.pred_eq_sub_one` are now simp lemmas. For
theorems about `Nat.succ` or `Nat.pred` without corresponding theorem
for `+ 1` or `- 1`, this adds the corresponding theorem.
This PR neither adds nor removes material, but improves the organization
of `Init/Data/List/*`.
These files are essentially completely re-ordered, to ensure that
material is developed in a consistent order between `List.Basic`,
`List.Impl`, `List.BasicAux`, and `List.Lemmas`.
Everything is organised in subsections, and I've added some module docs.
presumably this avoids unnecessary work when `omega` is used in tactic
combinators where the error message is never seen. Measurement did not
show
any significant changes, though.
With an artificial sleep in
```diff
diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean
index fd297eef60..31ea3f6bd0 100644
--- a/src/Lean/Elab/Tactic/Omega/Frontend.lean
+++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean
@@ -538,6 +538,7 @@ def formatErrorMessage (p : Problem) : OmegaM MessageData := do
else
let as ← atoms
return .ofLazyM (es := as) do
+ IO.sleep 10000
let mask ← mentioned as p.constraints
let names ← varNames mask
return m!"a possible counterexample may satisfy the constraints\n" ++
```
I can observe that `omega` is slow and `try omega` fast, so it seems to
work at least.
When an implicit argument cannot be inferred, the error should show the
name of the argument.
Showing the argument name in the error message for an uninstantiated
metavariable was introduced in da33f498f5,
but this implementation causes some argument names to get lost.
The modules `CollectMVars` and `FindMVars` only search for expression
metavariables and not level metavariables, so we should use
`Expr.hasExprMVar` instead of `Expr.hasMVar`.
This came up when watching new Lean users in a class situation. A number
of them were confused when they omitted a namespace on a constructor
name, and Lean treated the variable as a pattern that matches anything.
For example, this program is accepted but may not do what the user
thinks:
```
inductive Tree (α : Type) where
| leaf
| branch (left : Tree α) (val : α) (right : Tree α)
def depth : Tree α → Nat
| leaf => 0
```
Adding a `branch` case to `depth` results in a confusing message.
With this linter, Lean marks `leaf` with:
```
Local variable 'leaf' resembles constructor 'Tree.leaf' - write '.leaf' (with a dot) or 'Tree.leaf' to use the constructor.
note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
```
Additionally, the error message that occurs when invalid names are
applied in patterns now suggests similar names. This means that:
```
def length (list : List α) : Nat :=
match list with
| nil => 0
| cons x xs => length xs + 1
```
now results in the following warning on `nil`:
```
warning: Local variable 'nil' resembles constructor 'List.nil' - write '.nil' (with a dot) or 'List.nil' to use the constructor.
note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
```
and error on `cons`:
```
invalid pattern, constructor or constant marked with '[match_pattern]' expected
Suggestion: 'List.cons' is similar
```
The list of suggested constructors is generated before the type of the
pattern is known, so it's less accurate, but it truncates the list to
ten elements to avoid being overwhelming. This mostly comes up with
`mk`.
This restores the behavior prior to
9f6bbfa106
for `MessageData.ofSyntax` `MessageData.ofExpr`, and
`MessageData.ofLevel` while staying within the new `.ofLazy` paradigm.
Also adds some documentation to help developers understand the missing
context issue.
Closes#4432
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
We recently discovered inconsistencies in Mathlib and Std over the
ordering of the arguments for `==`.
The most common usage puts the "more variable" term on the LHS, and the
"more constant" term on the RHS, however there are plenty of exceptions,
and they cause unnecessary pain when switching (particularly, sometimes
requiring otherwise unneeded `LawfulBEq` hypotheses).
This convention is consistent with the (obvious) preference for `x == 0`
over `0 == x` when one term is a literal.
We recently updated Std to use this convention
https://github.com/leanprover/std4/pull/430
This PR changes the two major places in Lean that use the opposite
convention, and adds a suggestion to the docstring for `BEq` about the
preferred convention.
This incorporates many general Lake DSL changes from #2439 and adds some
new related changes.
* Rework configuration names (e.g., `package <name>`)
* String literals ca now be used instead of identifiers for names.
* The name syntax is now optional and can instead be set via the `name`
field.
* Avoid French quotes in `lake new` / `lake init` templates (except in
`lean_lib` names). This is not done for `lean_lib` because it needs a
proper identifier for its root. It could use a string and reparse it as
an identifier, but this seems liable to produce confusion.
* The `exe` templates now names it main module `Main` like the `std`
template.
* Improve `math` template error if `lean-toolchain` fails to download.
* Lake now logs a warning rather than an error on unknown configuration
fields. This increases the Lake DSL's cross-version compatibility.
Closes#3385.
Moves the cached log into the trace file (no more `.log.json`). This
means logs are no longer cached on fatal errors and this ensures that an
out-of-date log is not associated with an up-to-date trace. Separately,
`.hash` file generation was changed to be more reliable as well. `.hash`
files are deleted as part of the build and always regenerate with
`--rehash`.
Closes#2751.
Use a TOML file for the Lake configuration of the `src/lake` directory
instead of a Lean file. This avoids having to load a version of the Lake
library to build Lake.
This is from a ~~pair~~triple programming session with @tydeu and
@mhuisi.
If stage 1 is built with `-DUSE_LAKE=ON`, the CMake run will generate
`lakefile.toml` files for the root, `src`, and `tests`. These Lake
configuration files can then be used to build core oleans. While they do
not yet allow Lake to be used to build the Lean binaries. they do allow
Lake to be used for working interactively with the Lean source. In our
preliminary experiments, this allowed updates to `Init.Data.Nat` to be
noticed automatically when reloading downstream files, rather than
requiring a full manual compiler rebuild. This will make it easier to
work on the system.
As part of this change, Lake is added to stage 0. This allows Lake to
function in `src`, which uses the stage 0 toolchain.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
