Changes:
- We avoid the thread local storage.
- We use a hash map to ensure that cached values are not lost.
- We remove `check_system`. If this becomes an issue in the future we
should precompute the remaining amount of stack space, and use a cheaper
check.
- We add a `Expr.replaceImpl`, and will use it to implement
`Expr.replace` after update-stage0
Declarations with `@[elab_as_elim]` could elaborate as type-incorrect
expressions. Reported by Jireh Loreaux [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/bug.20in.20revert/near/450522157).
(In principle the elabAsElim routine could revert fvars appearing in the
expected type that depend on the discriminants (if the discriminants are
fvars) to increase the likelihood of type correctness, but that's at the
cost of some complexity to both the elaborator and to the user.)
Now it suggests using `@[ext (iff := false)]` to disable generating the
`ext_iff` lemma.
This PR also adjusts error messages and attribute documentation.
Additionally, to simplify the code now the `x` and `y` arguments can't
come in reverse order (this feature was was added in the refactor
#4543).
Closes#4758
A more restrictive but efficient max sharing primitive.
**Motivation:** Some software verification proofs may contain
significant redundancy that can be eliminated using hash-consing (also
known as `shareCommon`). For example, [theorem
`sha512_block_armv8_test_4_sym`](460fe5d74c/Proofs/SHA512/SHA512Sym.lean (L29))
took a few seconds at [`addPreDefinitions`
](1a12f63f74/src/Lean/Elab/PreDefinition/Main.lean (L155))
and one second at `fixLevelParams` on a MacBook Pro (with M1 Pro). The
proof term initially had over 16 million subterms, but the redundancy
was indirectly and inefficiently eliminated using `Core.transform` at
`addPreDefinitions`. I tried to use `shareCommon` method to fix the
performance issue, but it was too inefficient. This PR introduces a new
`shareCommon'` method that, although less flexible (e.g., it uses only a
local cache and hash-consing table), is much more efficient. The new
procedure minimizes the number of RC operations and optimizes the
caching strategy. It is 20 times faster than the old `shareCommon`
procedure for theorem `sha512_block_armv8_test_4_sym`.
I noticed that a change to `Lean.PrettyPrinter.Delaborator.Builtins`
rebuilt more modules than I expected, so I moved a definition and
reduced some dependcies.
More reduction would be possible to move const-delaboration out of the
big `Lean.PrettyPrinter`, and import from `Lean.PrettyPrinter`
selectively.
Add helper function for computing the number of allocated
sub-expressions in a given expression. Note: Use this function primarily
for diagnosing performance issues.
This PR addresses the absence of the `profileitM` function in two
auxiliary functions. The added `profileitM` instances are particularly
useful for diagnosing performance issues in declarations that contain
many repeated sub-terms.
The name `remove` was chosen because it is more popular in mainstream
programming languages, but being consistent with other Lean container
types (including `Lean.HashMap` and `Batteries.HashMap`) is more
important, so let's change the name while we still can.
the internal constructions for structural and well-founded recursion
use plenty of `PProd` and `MProd`, and reading these, deeply
nested and in prefix notation, is unnecessarily troublesome.
Therefore this introduces notations
```
a ×ₚ b -- PProd a b
a ×ₘ b -- MProd a b
()ₚ -- PUnit.unit
(x,y,z)ₚ -- PProd.mk x (PProd.mk y z)
(x,y,z)ₘ -- MProd.mk x (MProd.mk y z)
```
(This is the post-stage0-part 2.)
the internal constructions for structural and well-founded recursion
use plenty of `PProd` and `MProd`, and reading these, deeply
nested and in prefix notation, is unnecessarily troublesome.
Therefore this introduces notations
```
a ×ₚ b -- PProd a b
a ×ₘ b -- MProd a b
()ₚ -- PUnit.unit
(x,y,z)ₚ -- PProd.mk x (PProd.mk y z)
(x,y,z)ₘ -- MProd.mk x (MProd.mk y z)
```
(This is part 1, the rest will follow in #4730 after a stage0 update.)
This now works:
```lean
inductive Tree where | node : List Tree → Tree
mutual
def Tree.size : Tree → Nat
| node ts => list_size ts
def Tree.list_size : List Tree → Nat
| [] => 0
| t::ts => t.size + list_size ts
end
```
It is still out of scope to expect to be able to use nested recursion
(e.g. through `List.map` or `List.foldl`) here.
Depends on #4718.
---------
Co-authored-by: Tobias Grosser <tobias@grosser.es>
the support for mutual structural recursion (new since #4575) is
extended so that Lean tries to infer it even without annotations.
* The error message when termination checking fails looks quite
different now. Maybe a bit better, maybe with more room for
improvements.
* If there are too many combinations (with an arbitrary cut-off) for a
given argument type, it will just give up and ask the user to use
`termination_by structural`.
* It is now legal to specify `termination_by structural` on not
necessarily all functions of a clique; this simply restricts the
combinations of arguments that Lean considers.
---------
Co-authored-by: Tobias Grosser <tobias@grosser.es>
This adds the types
* `IndGroupInfo`, a variant of `InductiveVal` with information that
applies to a whole group of mutual inductives and
* `IndGroupInst` which extends `IndGroupInfo` with levels and parameters
to indicate a instantiation of the group.
One purpose of this abstraction is to make it clear when a fuction
operates on a group as a whole, rather than a specific inductive within
the group.
This is extracted from #4718 and #4733 to reduce PR size and improve
bisectability.
Improves a number of elements related to Git checkouts, cloud releases,
and related error handling.
* On error, Lake now prints all top-level logs. Top-level logs are those
produced by Lake outside of the job monitor (e.g., when cloning
dependencies).
* When fetching a remote for a dependency, Lake now forcibly fetches
tags. This prevents potential errors caused by a repository recreating
tags already fetched.
* Tweaked Git error handling to hopefully be more informative.
* The builtin package facets `release`, `optRelease`, `extraDep` are now
caption in the same manner as other facets. Previously, they were
attempting to be too clever.
* `afterReleaseSync` and `afterReleaseAsync` now fetch `optRelease`
rather than `release`.
* Added support for optional jobs, whose failure does not cause the
whole build to failure (and made `optRelease` such a job).
Closes#4302.
We now get `.below` and `.brecOn` definitions for nested inductives.
No surprises in the implementation: the kernel already gives us suitable
`.rec_1` etc. recursors, and our construction follows the structure of
this recursor.
---------
Co-authored-by: Tobias Grosser <tobias@grosser.es>
Adds a command and tactic to print the `Array <| DiscrTree.Key` for
equalities helping the user to debug perceived `simp` failures.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
this idiom shows up multiple times, is non-trivial (in the sense that
the `localInsts` has to be updated, and I am about to use it once more.
Hence time to abstract this out.
When the `decide` tactic fails, it can try to give hints about the
failure:
- It tells you which `Decidable` instances it unfolded, by making use of
the diagnostics feature.
- If it encounters `Eq.rec`, it gives you a hint that one of these
instances was likely defined using tactics.
- If it encounters `Classical.choice`, it hints that you might have
classical instances in scope.
- During this, it tries to process `Decidable.rec`s and matchers to pin
blame on a particular instance that failed to reduce.
This idea comes from discussion with Heather Macbeth [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Decidable.20with.20structures/near/449409870).
this code
```
inductive N where
| cons : (Nat -> N) -> N
mutual
def f : N -> Nat
| .cons a => g (a 32) + 1
termination_by structural n => n
def g : N -> Nat
| .cons a => f (a 42) + 1
termination_by structural n => n
end
```
would break. When searching for the right `belowDict` we now have to,
evne after instantiating the paramters for a reflexive argument, again
search through a bunch of `PProd`s.
(Instead of searching we could pass down the index, but since we are
searching anyways in this function let's just re-use.)
Fixes: #4726
Matchers usually have implicit arguments, and even if they don't the
notation hides the name of the matcher function.
Now when hovering over `match` expressions you can see the actual
underlying matcher expression.
if will fail otherwise, but with a worse error message, and it's helpful
in later transformation to know that the parameters are the same for the
whole group.
This makes it reflect how we are writing release notes for 4.9.0,
including how to handle the `releases_drafts` folder and how and when to
update `RELEASES.md`.
Co-authored-by: Kim Morrison <kim@tqft.net>
Upstreaming of basic material on `List.Pairwise` and `List.Nodup`. More
complete API to follow later, this is just a first approximation of what
leansat will need.
When a definition is redeclared, the original code would clobber the
value of `const2ModIdx` every time, meaning that a constant would be
attributed to a module which occurs later than the modules for constants
referencing this one. Preferring the original module ensures that these
module indexes are dependency-ordered. This originally came up as a bug
in `shake`, which assumes this property, see
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/check.20for.20unused.20imports.20doesn't.20stop/near/449139309).
I'll update `list_simp.lean` (simp normal form testing) and add missing
lemmas in follow-up PRs.
This just upstreams the material, and reorders the lemmas to match the
other sections.
Adds syntactic sugar specifying a git revision as a dependency version
in a `require` command. For example:
```
require "leanprover-community" / "proofwidgets" @ git "v0.0.39"
```
This PR refactors the 'ext' attribute and implements the following
features:
- The 'local' and 'scoped' attribute kinds are now usable.
- The attribute realizes the `ext`/`ext_iff` lemmas when they do not
already exist, rather than always generating them. This is useful in
conjunction with `@[local ext]`.
- Adding `@[ext]` to a user ext lemma now realizes an `ext_iff` lemma as
well; formerly this was only for structures. The name of the generated
`ext_iff` theorem for a user `ext` theorem named `A.B.myext` is
`A.B.myext_iff`. If this process leads to an error, the user can write
`@[ext (iff := false)]` to disable this feature.
Breaking changes:
- Now the "x" and "y" term arguments to the realized `ext` and `ext_iff`
lemmas are implicit.
- Now the realized `ext` and `ext_iff` lemmas are protected.
Bootstrapping notes:
- There are a few `ext_iff` lemmas to address after the next stage0
update.
Closes https://github.com/leanprover/lean4/issues/3643
Suggested by Floris [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.22Missing.20Tactics.22.20list/near/446267660).
right now, in order to find out how many auxilary datatype are in a
mutual group of inductive with nested data type, one has to jump
through hoops like this:
```
private def numNestedInducts (indName : Name) : MetaM Nat := do
let .inductInfo indVal ← getConstInfo indName | panic! "{indName} is an inductive"
let .recInfo recVal ← getConstInfo (mkRecName indName) | panic! "{indName} has a recursor"
return recVal.numMotives - indVal.all.lengt
```
The `InductiveVal` data structure already has `.isNested : Bool`, so it
seems to be a natural extension to beef that up to `.numNested: Nat`.
This touched kernel code.
This adds support for mutual structural recursive functions.
For now this is opt-in: The functions must have a `termination_by
structural …` annotation (new since #4542) for this to work:
```lean
mutual
inductive A
| self : A → A
| other : B → A
| empty
inductive B
| self : B → B
| other : A → B
| empty
end
mutual
def A.size : A → Nat
| .self a => a.size + 1
| .other b => b.size + 1
| .empty => 0
termination_by structural x => x
def B.size : B → Nat
| .self b => b.size + 1
| .other a => a.size + 1
| .empty => 0
termination_by structural x => x
end
```
The recursive functions don’t have to be in a one-to-one relation to a
set of mutually recursive inductive data types. It is possible to ignore
some of the types:
```lean
def A.self_size : A → Nat
| .self a => a.self_size + 1
| .other _ => 0
| .empty => 0
termination_by structural x => x
```
or have more than one function per argument type:
```lean
def isEven : Nat → Prop
| 0 => True
| n+1 => ¬ isOdd n
termination_by structural x => x
def isOdd : Nat → Prop
| 0 => False
| n+1 => ¬ isEven n
termination_by structural x => x
```
This does not include
* Support for nested inductive data types or nested recursion
* Inferring mutual structural recursion in the absence of
`termination_by`.
* Functional induction principles for these.
* Mutually recursive functions that live in different universes. This
may be possible,
maybe after beefing up the `.below` and `.brecOn` functions; we can look
into this some
other time, maybe when there are concrete use cases.
---------
Co-authored-by: Richard Kiss <him@richardkiss.com>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
This file has comments that recall the data type definitions in Lean.
Most of them were still using lean3 syntax, and at least one of them was
out of date (one field missing), so I updated them.
I took the liberty to shorten the comments from the original file, or
omit them if they don’t add much over the field names.
Generalizes #3556 to not suppressing errors in tactic steps either when
the parse error is in a later step, as otherwise changes to the end of a
proof would affect (correctness or effectiveness of) incrementality of
preceding steps.
Fixes#4623, in combination with #4643
As we do not build multiple shared libraries on non-Windows anymore,
count the max exported symbols per static library instead.
Unfortunately, this still does seem to match the number on Windows.
The previous check, looking only at the type of the parameter, was too
permissive and led to ill-typed terms later on.
This fixes#4671.
In some cases the previous code might have worked by accident, in this
sense this is a breaking change. Affected functions can be fixed by
reordering their parameters to that all the function parameters that
occur in the parameter of the inductive type of the parameter that the
function recurses on come first.
Fixes the Windows build. As libLean is by far the biggest component,
there is no need for a separate libStd_shared for now.
```
$ find build/release/stage1/lib/lean -name '*.a' -exec bash -c 'echo -n "{} " ; nm {} | grep " T " | wc -l' \;
build/release/stage1/lib/lean/libleanrt.a 497
build/release/stage1/lib/lean/libleancpp.a 1320
build/release/stage1/lib/lean/libInit.a 7476
build/release/stage1/lib/lean/libStd.a 1696
build/release/stage1/lib/lean/libLean.a 64339
build/release/stage1/lib/lean/libLake.a 5722
```
In #3911, a refactor to share `MessageData` code between `ppConst` and
the signature pretty printer unintentionally caused the signature pretty
printer to use the `pp.tagAppFns` option. This causes, for example, `+`
in `a + b` to independently have its own hover information due to the
fact that `notation` app unexpanders use the head function's syntax as
the `ref` when constructing the notation syntax. This behavior of
`pp.tagAppFns` is intentional, and it is used by docgen, but it should
not be activated for signatures.
This affects `#check` and was reported by Kevin Buzzard [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/degraded.20hover.20experience.20on.20.23check/near/449380674).
This PR also makes sure the initial `ref` when applying app unexpanders
is `.missing`, rather than whatever random value might be present in the
`CoreM` context.
### Preliminary PRs:
- [x] #4597
- [x] #4599
- [x] #4600
- [x] #4602
- [x] #4603
- [x] #4604
- [x] #4605
- [x] #4607
- [x] #4627
- [x] #4629
### Quick overview over API/naming changes compared to `Lean.HashMap`
and `Batteries.HashMap`:
#### Lean
* `find?` -> `get?`/`getElem?`
* `find!` -> `get!`/`gtetElem!`
* `findD` -> `getD`
* `findEntry?` -> not implemented for now
* `insert'` -> `containsThenInsert` (order reversed in result)
* `insertIfNew` -> `getThenInsertIfNew?` (order reversed in result)
* `numBuckets` -> `Internal.numBuckets`
* `ofListWith` -> not implemented for now
* `Array.groupByKey` -> not implemented for now
* `merge` -> not implemented for now, but you can use `insertMany`
#### Batteries
* `modify` -> not implemented for now
* `mergeWith` -> not implemented for now
* `mergeWithM` -> not implemented for now
I made a mistake in #4517, fixed here, so about time to add a test.
I wonder if this generic level optimization should be moved into
`mkLevelMax'`, but not today.
fixes#4650
Split from #4583
There are two open questions, opinions appreciated:
- Should this material be part of `Init` or `Std`?
- Should the typeclasses be in the `Std` namespace?
This is an auxiliary procedured used by `rw` and `apply` tactics. It
synthesizes pending type class instances.
The new test contains an example where it failed. The comment at
`synthAppInstances.step` explains why, and the fix.
we have a `forallBoundedTelescope`, and for a long while I was
wondering why we also don't have `lambdaBoundedTelescope`, and every now
and then felt the need for it. So let's just add it.
this job sometimes fails, maybe a race condition with the `gh run
cancel` not happenign quickly enough. Maybe more verbose output will
help understand this better.
Now syntax nodes have their formatters run even if the parsers they wrap
are all arity zero. This fixes an issue where if `ppSpace` appears in a
`macro`/`elab` then it does not format with a space due to the fact that
macro argument processing wraps this as `group(ppSpace)`, and `ppSpace`
has arity zero.
Implementation note: the fix is to make the `visitArgs` formatter
combinator always visit the last child, even if it does not exist (in
which case the visited node will be `Syntax.missing`). To compensate,
parser combinators like many and optional need to be sure to keep track
of whether there any children. Only optional's needed to be modified.
Closes#4561
Summary:
- Adds configuration option `exponentiation.threshold`
- An expression `b^n` where `b` and `n` are literals is not reduced by
`whnf`, `simp`, and `isDefEq` if `n > exponentiation.threshold`.
Motivation: prevents system from becoming irresponsive and/or crashing
without memory.
TODO: improve support in the kernel. It is using a hard-coded limit for
now.
Before, `pp.instantiateMVars` generally had no effect because most call
sites for the pretty printer instantiated metavariables first, but now
this functionality is entrusted upon the `pp.instantiateMVars` option.
This also has an effect in hovers, where metavariables can be unfolded
one assignment at a time. However, the goal state still sees all
metavariables instantiated due to the fact that the algorithm relies on
expression equality post-instantiation (see
`Lean.Widget.goalToInteractive`).
Closes#4406
Closes#2736
See comment at `ExprDefEq.lean` for explanation.
Side effects:
- Improved error messages in two tests.
- Had to improve `getSuccesses` procedure at `App.lean`. It now
discards candidates that contain postponed elaboration problems.
If it is too disruptive for Mathlib, we should try to discard the
ones that have postponed metavariables.
Split from #4583
`exists_of_set` appears in Batteries as `exists_of_set'`. The
`exists_of_set` version is unused in batteries and mathlib at least and
I would argue that the primed version (i.e., the one added in this PR)
is always better anyway.
`isEmpty_iff` appears in mathlib as `isEmpty_iff_eq_nil`.
Fixes#4591. The extra code already existed in the only other user of
`unresolveNameGlobal` (in the pretty printer), although I did not make
it use this function because it has some additional behavior around
universes and in pattern position.
This implements the recurrence theorems `getLsb_mul`, `mulRec_zero_eq`,
`mulRec_succ_eq` to allow bitblasting multiplication.
---------
Co-authored-by: Kim Morrison <scott@tqft.net>
This implements the `termination_by structural` syntax proposed in
#3909.
I went with `termination_by structural` over, say,
`termination_by (config := {method := .structural})` mainly because it
was
easier to get going (otherwise I’d have to look into how to define
recursive
parsers, as `Parser.config` depends on `term` and `termination_by` is
part of
term. But also because I find it more ergonomic and aesthetic as a user.
But syntax can still change.
The `termination_by?` syntax will no longer force well-founded
recursion,
and instead the inferred `termination_by structurally` annotation will
be shown
if structural termination is possible.
While I was it, this fixes#4546 the easy way (log errors about but
otherwise
ignore incomplete `termination_by` sets for mutual recursion). Maybe we
get
multiple replacements (#4551), but even then this this good behavior.
Involves a bit of shuffling around `TerimationHints` (now validated for
a
clique already by `PreDefinition.main`) and `TerminationArguments` (now
lifted
out of the `WF` namespace, and a bit simplified).
Fixes#3909
---------
Co-authored-by: Richard Kiss <him@richardkiss.com>
using the order as it comes out of the `HashMap` led to annying test
suite output variations. Moreover, sorting by the canonical order leads
to messages that are probably easier to digest as a user.
Adds linkage to `Std` so the build behaviour on darwin is in line with
linux
I'm not sure why linking with `Std` is needed. I deleted it in the
previous patch https://github.com/leanprover/lean4/pull/3811 and Lean
still builds and runs. @tydeu mentioned this issue so I created this PR.
Adds a new type of `require` which fetches package metadata from a
registry API endpoint (i.e., Reservoir) and then clones a Git package
using the information provided. To require such a dependency, the new
syntax is:
```lean
require <scope> / <pkg-name> [@ "git#<rev>"] -- e.g., require "leanprover" / "doc-gen4"
```
Or in TOML:
```toml
[[require]]
name = "<pkg-name>"
scope = "<scope>"
rev = "<rev>"
```
Unlike with Git dependencies, Lake can make use of the richer
information provided by the registry to determine the default branch of
the package. This means for repositories of packages like `doc-gen4`
which have a default branch that is not `master`, Lake will now use said
default branch (e.g., in `doc-gen4`'s case, `main`).
Lake also supports configuring the registry endpoint via an environment
variable: `RESERVIOR_API_URL`. Thus, any server providing a similar
interface to Reservoir can be used as the registry. Further
configuration options paralleling those of Cargo's [Alternative
Registries](https://doc.rust-lang.org/cargo/reference/registries.html)
and [Source
Replacement](https://doc.rust-lang.org/cargo/reference/source-replacement.html)
will come in the future.
Updated and split from #3174.
This example, reported from LNSym, started failing when we changed the
definition of `Fin.sub` in
https://github.com/leanprover/lean4/pull/4421.
When we use the new definition, `omega` produces a proof term that the
kernel is very slow on.
To work around this for now, I've removed `BitVec.toNat_sub` from the
`bv_toNat` simp set,
and replaced it with `BitVec.toNat_sub'` which uses the old definition
for subtraction.
This is only a workaround, and I would like to understand why the term
chokes the kernel.
```
example
(n : Nat)
(addr2 addr1 : BitVec 64)
(h0 : n ≤ 18446744073709551616)
(h1 : addr2 + 18446744073709551615#64 - addr1 ≤ BitVec.ofNat 64 (n - 1))
(h2 : addr2 - addr1 ≤ addr2 + 18446744073709551615#64 - addr1) :
n = 18446744073709551616 := by
bv_omega
```
The new option `set_option debug.skipKernelTC true` is meant for
temporarily working around kernel performance issues.
It compromises soundness because a buggy tactic may produce an invalid
proof, and the kernel will not catch it if the new option is set to true.
Remark: I had to comment
```
if debug.skipKernelTC.get opts then
addDeclWithoutChecking env decl
else
```
because the build was crashing when trying to compile Lake.
Going to perform `update-stage0` and try again.
Addresses a few issues with precompile library computation.
* Fixes a bug where Lake would always precompile the package of a
module.
* If a module is precompiled, it now precompiles its imports.
Previously, it would only do this if imported.
Closes#4565.
This appears to have been a semantic merge conflict between #3940 and
#4129. The effect on the language server is that if two edits are
sufficiently close in time to create an interrupt, some elaboration
steps like `simp` may accidentally catch the exception when it is
triggered during their execution, which makes incrementality assume that
elaboration of the body was successful, which can lead to incorrect
reuse, presenting the interrupted state to the user with symptoms such
as "uses sorry" without accompanying errors and incorrect lints.
When the type of a definition or example is a proposition,
we should elaborate on them as we elaborate on theorems.
This is particularly important for examples that are often
used in educational material.
Recall that when elaborating theorem headers, we convert unassigned
universe metavariables into universe parameters. The motivation is
that the proof of a theorem should not influence its statement.
However, before this commit, this was not the case for definitions and
examples when their type was a proposition. This discrepancy often
confused users.
Additionally, we considered extending the above behavior whenever
the type of a definition is provided. That is, we would keep the
current behavior only if `: <type>` was omitted in a definition.
However, this proved to be too restrictive.
For example, the following instance in `Core.lean` would fail:
```
instance {α : Sort u} [Setoid α] : HasEquiv α :=
⟨Setoid.r⟩
```
and we would have to write instead:
```
instance {α : Sort u} [Setoid α] : HasEquiv.{u, 0} α :=
⟨Setoid.r⟩
```
There are other failures like this in the core, and we assume many more
in Mathlib.
closes#4398
@semorrison @jcommelin: what do you think?
this is in preparation for #4542, and extracts from `findRecArg` the
functionality for trying one particular argument.
It also refactors the code a bit. In particular
* It reports errors in the order of the parameters, not the order of
in which they are tried (it tries non-indices first).
* For every argument it will say why it wasn't tried, even if the
reason is quite obviously (fixed prefix, or `Prop`-typed etc.)
Therefore there is some error message churn.
This ports the `.below` and `.brecOn` constructions to lean.
I kept them in the same file, as they were in the C code, because they
are
highly coupled and the constructions are very analogous.
For validation I developed this in a separate repository at
https://github.com/nomeata/lean-constructions/tree/fad715e
and checked that all declarations found in Lean and Mathlib are
equivalent, up to
def canon (e : Expr) : CoreM Expr := do
Core.transform (← Core.betaReduce e) (pre := fun
| .const n ls => return .done (.const n (ls.map (·.normalize)))
| .sort l => return .done (.sort l.normalize)
| _ => return .continue)
It was not feasible to make them completely equal, because the kernel's
type inference code seem to optimize level expressions a bit less
aggressively, and beta-reduces less in inference.
The private helper functions about `PProd` can later move into their own
file, used by these constructions as well as the structural recursion
module.
Fixes some issues with the executable build and bad imports.
**Release notes:**
* A bad import in an executable no longer prevents the executable's root
module from being built., This also fixes a problem where the location
of a transitive bad import would not been shown.
* The root module of the executable now respects `nativeFacets`.
**Technical touchups:**
* Expanded and better documented `tests/badImport`.
* Use `ensureJob` in `recBuildDeps` to catch import errors instead of
individual `try ... catch` blocks.
Issue #4535 is being affected by a bug in the structural inductive
predicate termination checker (`IndPred.lean`). This module did not
exist in Lean 3, and it is buggy in Lean 4. In the given example, it
introduces an auxiliary declaration containing a `sorry`, and the fails.
This PR ensures this kind of declaration is not added to the
environment.
Closes#4535
TODO: we need a new maintainer for the `IndPred.lean`.
The `pp.maxSteps` option is a hard limit on the complexity of pretty
printer output, which is necessary to prevent the LSP from crashing when
there are accidental large terms. We're using the default value from the
corresponding Lean 3 option.
This PR also sets `pp.deepTerms` to `false` by default.
When the type of an `example` is a proposition,
we should elaborate on them as we elaborate on theorems.
This is particularly important for examples that are often
used in educational material.
Recall that when elaborating theorem headers, we convert unassigned
universe metavariables into universe parameters. The motivation is
that the proof of a theorem should not influence its statement.
However, before this commit, this was not the case for examples when
their type was a proposition.
This discrepancy often confused users.
Additionally, we considered extending the above behavior to definitions
when
1- When their type is a proposition. However, it still caused disruption
in Mathlib.
2- When their type is provided. That is, we would keep the current
behavior only if `: <type>` was omitted. This would make the elaborator
for `def` much closer to the one for `theorem`, but it proved to be too
restrictive.
For example, the following instance in `Core.lean` would fail:
```
instance {α : Sort u} [Setoid α] : HasEquiv α :=
⟨Setoid.r⟩
```
and we would have to write instead:
```
instance {α : Sort u} [Setoid α] : HasEquiv.{u, 0} α :=
⟨Setoid.r⟩
```
There are other failures like this in the core, and we assume many more
in Mathlib.
closes#4398closes#4482 Remark: PR #4482 implements option 1 above. We may consider
it again in the future.
We add a new definition `BitVec.twoPow w i` to represent `(1#w <<< i)`.
This expression is used to test bits when building the multiplication
bitblaster.
Patch 1/?, being peeled from https://github.com/opencompl/lean4/pull/6.
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
Fixes typo "reflexivitiy" to "reflexivity", and changes exact Eq.rfl to
exact rfl, since Eq.rfl does not exist.
(I got something confused wrt the bot message on #4367 and accidentally
closed that one, so making this one instead, which I think satisfies the
requirements it wanted.)
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
this is the simplest of the constructions to be ported from C++ to Lean,
so I’ll PR this one first.
This begins to put each construction into its own file, as it was the
case with C++.
For validation I developed this in a separate repository at
https://github.com/nomeata/lean-constructions/tree/fad715e
and checked that all `.recOn` declarations found in Lean and Mathlib are
identical (per `==`) to the ones produced by the C code.
Fixes a bug where Lake incorrectly included the module dynlib in a
platform-independent trace. It was incorrectly excluded only external
native libraries from the trace. Also adds a test.
as #4527 describes there is inconsistency between `by`, `case` and
`next` on the one hand who, if the goal isn’t closed, put squiggly
underlines on the first line, and `.`, which so far only squiggled the
dot (which is a very short symbol!)
With this change the same mechanism as used by `case`, namely
`withCaseRef`, is also used for `.`.
There is an argument for the status quo: The `.` tactic is more commonly
used
with further tactics on the same line, and thus there is now a higher
risk that
the user might think that the first tactic is broken. But
* the same argument does apply to `by` and `case` where there was an
intentional
choice to do it this way
* consistency and
* a squiggly line just under the short `.` is easy to miss, so it is
actually
better to underlining more here (at least until we have a better way to
indicate incomplete proofs, which I have hopes for)
Fixes#4527, at least most of it.
This is the groundwork for a tactic index in generated documentation, as
there was in Lean 3. There are a few challenges to getting this to work
well in Lean 4:
* There's no natural notion of *tactic identity* - a tactic may be
specified by multiple syntax rules (e.g. the pattern-matching version of
`intro` is specified apart from the default version, but both are the
same from a user perspective)
* There's no natural notion of *tactic name* - here, we take the
pragmatic choice of using the first keyword atom in the tactic's syntax
specification, but this may need to be overridable someday.
* Tactics are extensible, but we don't want to allow arbitrary imports
to clobber existing tactic docstrings, which could become unpredictable
in practice.
For tactic identity, this PR introduces the notion of a *tactic
alternative*, which is a `syntax` specification that is really "the same
as" an existing tactic, but needs to be separate for technical reasons.
This provides a notion of tactic identity, which we can use as the basis
of a tactic index in generated documentation. Alternative forms of
tactics are specified using a new `@[tactic_alt IDENT]` attribute,
applied to the new tactic syntax. It is an error to declare a tactic
syntax rule to be an alternative of another one that is itself an
alternative. Documentation hovers now take alternatives into account,
and display the docs for the canonical name.
*Tactic tags*, created with the `register_tactic_tag` command, specify
tags that may be applied to tactics. This is intended to be used by
doc-gen and Verso. Tags may be applied using the `@[tactic_tag TAG1 TAG2
...]` attribute on a canonical tactic parser, which may be used in any
module to facilitate downstream projects introducing tags that apply to
pre-existing tactics. Tags may not be removed, but it's fine to
redundantly add them. The collection of tags, and the tactics to which
they're applied, can be seen using the `#print tactic tags` command.
*Extension documentation* provides a structured way to document
extensions to tactics. The resulting documentation is gathered into a
bulleted list at the bottom of the tactic's docstring. Extensions are
added using the `tactic_extension TAC` command. This can be used when
adding new interpretations of a tactic via `macro_rules`, when extending
some table or search index used by the tactic, or in any other way. It
is a command to facilitate its flexible use with various extension
mechanisms.
Describes the intended modes of use, potential performance tradeoffs,
and data representation in more detail.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
The recent change of the trace format exposed some unexpected issues
with Lake's tracing handling. This aims to fix that.
Lake will now perform a rebuild if the trace file is invalid/unreadable.
However, it will still fall back to modification times if the trace file
is missing. Also, Lake is now backwards compatible with the previous
pure numeric traces (and tolerates the absence of a `log` field in the
JSON trace).
This PR introduces complete simprocs for all the Int versions of
div/mod, and makes some small refactoring of Int lemmas and
library_search.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
#3850 included a commit that added an extra test for `exact?`, but was
otherwise unrelated the to PR. It also removed a test. I've
cherry-picked that test over, and restored the deleted test, and next
will remove the commit from #3850.
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>
This PR addresses some non-critical but annoying issues that sometimes
cause the language server to report an error:
- When using global search and replace in VS Code, the language client
sends `textDocument/didChange` notifications for documents that it never
told the server to open first. Instead of emitting an error and crashing
the language server when this occurs, we now instead ignore the
notification. Fixes#4435.
- When terminating the language server, VS Code sometimes still sends
request to the language server even after emitting a `shutdown` request.
The LSP spec explicitly forbids this, but instead of emitting an error
when this occurs, we now error requests and ignore all other messages
until receiving the final `exit` notification. Reported on Zulip several
times over the years but never materialized as an issue, e.g.
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Got.20.60shutdown.60.20request.2C.20expected.20an.20.60exit.60.20notification/near/441914289.
- Some language clients attempt to reply to the file watcher
registration request before completing the LSP initialization dance. To
fix this, we now only send this request after the initialization dance
has completed. Fixes#3904.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
A pending tactic mvar managed to escape into an unexpected context in
specific circumstances.
```lean
example : True := by
· rw [show 0 = 0 by rfl]
```
* Term elaboration of the `show` creates a pending mvar for the `by rfl`
proof
* `rw` fails with an exception because the pattern does not occur in the
target
* `cdot` catches the exception and admits the goal
* `Term.runTactic` [synthesizes all pending mvars from the tactic's
execution](5f9dedfe5e/src/Lean/Elab/SyntheticMVars.lean (L350)),
including the `by rfl` proof. But this would not have happened without
`cdot` as the exception would have skipped that invocation!
* Now incrementality is confused because the nested `by rfl` proof is
unexpectedly run in the same context as the top-level proof, writing to
the wrong promise, and the error message is lost
Solution: disable incrementality for these pending mvars
The performance issue at #4413 is due to our `Fin.sub` definition.
```
def sub : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + (n - b)) % n, mlt h⟩
```
Thus, the following runs out of stack space
```
example (a : UInt64) : a - 1 = a :=
rfl
```
at the `isDefEq` test
```
(a.val.val + 18446744073709551615) % 18446744073709551616 =?= a.val.val
```
From the user's perspective, this timeout is unexpected since they are
using small numerals, and none of the other `Fin` basic operations (such
as `Fin.add` and `Fin.mul`) suffer from this problem.
This PR implements an inelegant solution for the performance issue. It
redefines `Fin.sub` as
```
def sub : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨((n - b) + a) % n, mlt h⟩
```
This approach is unattractive because it relies on the fact that
`Nat.add` is defined using recursion on the second argument.
The impact on this repo was small, but we want to evaluate the impact on
Mathlib.
closes#4413
It seems:
* there was no actual need for the UInt32 valued version
* downstream we were getting duplicative lemmas about both
* so lets reduce the API surface area!
If anyone would prefer the remaining function is still called
`Char.utf8Size` I will happily change it. (`size` is hopefully still
unambiguous, and it's helpful to rename here so we can give a
deprecation warning that explains the type signature change.)
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Before this commit, the `theorem` and `def` declarations had different
universe parameter orders.
For example, the following `theorem`:
```
theorem f (a : α) (f : α → β) : f a = f a := by
rfl
```
was elaborated as
```
theorem f.{u_2, u_1} : ∀ {α : Sort u_1} {β : Sort u_2} (a : α) (f : α → β), f a = f a :=
fun {α} {β} a f => Eq.refl (f a)
```
However, if we declare `f` as a `def`, the expected order is produced.
```
def f.{u_1, u_2} : ∀ {α : Sort u_1} {β : Sort u_2} (a : α) (f : α → β), f a = f a :=
fun {α} {β} a f => Eq.refl (f a)
```
This commit fixes this discrepancy.
@semorrison @jcommelin: This might be a disruptive change to Mathlib,
but it is better to fix the issue asap. I am surprised nobody has
complained about this issue before. I discovered it while trying to
reduce discrepancies between `theorem` and `def` elaboration.
Closes#4375
The following example raises `error: (kernel) declaration has free
variables '_example'`:
```lean
example: Nat → Nat :=
let a : Nat := Nat.zero
fun (_ : Nat) =>
let b : Nat := Nat.zero
(fun (_ : a = b) => 0) (Eq.refl a)
```
During elaboration of `0`, `elabNumLit` creates a synthetic mvar
`?_uniq.16` which gets abstracted by `elabFun` to `?_uniq.16 :=
?_uniq.50 _uniq.6 _uniq.12`. The `isDefEq` to `instOfNatNat 0` results
in:
```
?_uniq.50 :=
fun (x._@.4375._hyg.13 : Nat) =>
let b : Nat := Nat.zero
fun (x._@.4375._hyg.23 : Eq.{1} Nat _uniq.4 b) =>
instOfNatNat 0
```
This has a free variable `_uniq.4` which was `a`.
When the application of `?_uniq.50` to `#[#2, #0]` is instantiated, the
`let b : Nat := Nat.zero` blocks the beta-reduction and `_uniq.4`
remains in the expression.
fix: add `(useZeta := true)` here:
ea46bf2839/src/Lean/MetavarContext.lean (L567)
As [reported on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/maybe.20a.20cache.20bug.3F).
We expected that for sound reuse of elaboration results, it is
sufficient to compare the old and new syntax tree's structure and atoms
including position info, but not the whitespace in between them.
However, we have at least one request handler, the goal view, that
inspects the whitespace after a tactic and thus could return incorrect
results on reuse. For now we implement the straightforward fix of
checking the whitespace as well. Alternatives like updating the
whitespace stored in the reused info tree are tbd.
This has the slight disadvantage that adding whitespace at the end of a
tactic will re-execute it (or the entire body, but not the header, if
the body is not a tactic block), but only up to typing the first
character of the next tactic or command.
Deprecates `inputFile` and replaces it with `inputBinFile` and
`inputTextFile`. `inputTextFile` normalizes line endings, which helps
ensure text file traces are platform-independent.
The type uses `PUnit`, but the `pure ()` in the body was forcing the
implicit universe level at `PUnit` to be `1`.
We should probably elaborate `def`s like we elaborate theorems when the
resulting type is provided. This kind of mistake is hard to spot.
This `@[inline]` causes Lean to respecialize `RBMap.find?` to `NameMap`
at each call site of `NameMap.find?`, creating lots of unnecessary
duplicate IR.
so that the pretty-printed origin is clickable, and avoid the
unnecessary `@`.
Particularly nice is this fix:
```diff
/--
-info: [Meta.Tactic.simp.discharge] @bar discharge ✅
+info: [Meta.Tactic.simp.discharge] bar discharge ✅
autoParam T _auto✝
- [Meta.Tactic.simp.rewrite] { }:1000, T ==> True
-[Meta.Tactic.simp.rewrite] @bar:1000, U ==> True
+ [Meta.Tactic.simp.rewrite] T.mk:1000, T ==> True
+[Meta.Tactic.simp.rewrite] bar:1000, U ==> True
-/
```
this is an amendment to #4177, after @kmill pointed out an issue:
Users might expect that within a tactic combinator like `first`, `simp
[h]` fails if `h` does not exist. Therefore the behavior introduced in
PR #4177, which is really most useful in mormal interactive use of
`skip`, is restricted to when `recover := true`.
types like
```
inductive Many (α : Type u) where
| none : Many α
| more : α → (Unit → Many α) → Many α
```
have a `.brecOn` only supports motives producing `Type u`, but not `Sort
u`, but our induction principles produce `Prop`. So the previous
implementation of functional induction would fail for functions that
structurally recurse over such types.
We recognize this case now and, rather hazardously, replace `.brecOn`
with `.binductionOn` (and thus `.below ` with `.ibelow` and `PProd` with
`And`). This assumes that these definitions are highly analogous.
This also improves the error message when realizing a reserved name
fails with an exception, by prepending
```
Failed to realize constant {id}:
```
to the error message.
Fixes#4320
The key idea is to notice that `signExtend` behavior is controlled by
the `msb`. When `msb = false`, `sext` behaves the same as `trunc`. When
`msb = true`, `sext` behaves like `trunc` but adds high 1-bits. This is
expressed using the negate-truncate-negate pattern. Lemma statements
below:
```lean
theorem signExtend_eq_neg_truncate_neg_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
(x.signExtend v) = x.truncate v := by
theorem signExtend_eq_neg_truncate_neg_of_msb_true {x : BitVec w} {v : Nat} (hmsb : x.msb = true) :
(x.signExtend v) = ~~~((~~~x).truncate v) := by
```
These give the final theorem statement:
```lean
theorem getLsb_signExtend {x : BitVec w} {v i : Nat} :
(x.signExtend v).getLsb i = (decide (i < v) && if i < w then x.getLsb i else x.msb) := by
```
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Kim Morrison <scott@tqft.net>
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>
The current manner of lifting `LogIO` into `CliM` produces excessive
specializations (due to a nested inlined `forM`). There was also a bug
where `IO` was lifted into `CliM` via `LogIO` rather than directly
through `MainM`.
Stores the dependency trace for a build in the cached build log and then
verifies that it matches the trace of the current build before replaying
the log. Includes test.
Closes#4303.
The `save` happened in a slightly different context from the restore,
which a refinement of the `saveOrRestoreFull` signature now makes
impossible.
Fixes#4328
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
In the course of the development, I grabbed facts about right shifting
over integers [from
`mathlib4`](https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Int/Bitwise.lean).
The core proof strategy is to perform a case analysis of the msb:
- If `msb = false`, then `sshiftRight = ushiftRight`.
- If `msb = true`. then `x >>>s i = ~~~(~~~(x >>>u i))`. The double
negation introduces the high `1` bits that one expects of the arithmetic
shift.
---------
Co-authored-by: Kim Morrison <scott@tqft.net>
These will be used by LeanSAT for bitblasting rotations by constant
distances.
We first reduce the case when the rotation amount is larger than the
width to the case where the rotation amount is less than the width
(`x.rotateLeft/Right r = x.rotateLeft/Right (r%w)`).
Then, we case analyze on the low bits versus the high bits of the
rotation, where we prove equality by extensionality.
---------
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Tobias Grosser <github@grosser.es>
These lemmas are morally equivalent to Mathlib lemmas which are proposed
to be deleted from Mathlib in
[#13286](https://github.com/leanprover-community/mathlib4/pull/13286).
It is only morally equivalent, because the Mathlib lemmas are stated in
terms of Mathlib-defined things: `toFin_natCast` uses a coercion from
`Nat` to `Fin (2^w)` which relies on `NeZero` machinery available only
in Mathlib. Thus, I've rephrased the rhs in terms of the def-eq
`Fin.ofNat'` with an explicit proof that `2^w` is non-zero.
Similarly, the RHS of `toFin_neg` was phrased in terms of negation on
`Fin`s, which is only defined in Mathlib, so I've unfolded the
definition.
Allows embedding user widgets in structured messages. Companion PR is
leanprover/vscode-lean4#449.
Some technical choices:
- The `MessageData.ofWidget` constructor might not be strictly necessary
as we already have `MessageData.ofFormatWithInfos`, and there is
`Info.ofUserWidget`. However, `.ofUserWidget` also requires a `Syntax`
object (as it is normally produced when widgets are saved at a piece of
syntax during elaboration) which we do not have in this case. More
generally, it continues to be a bit cursed that `Elab.Info` nodes are
used both for elaboration and delaboration (pretty-printing), so
entrenching that approach seems wrong. The better approach would be to
have a separate notion of pretty-printer annotation; but such a refactor
would not be clearly beneficial right now.
- To support non-JS-based environments such as
https://github.com/Julian/lean.nvim, `.ofWidget` requires also providing
another message which approximates the widget in a textual form.
However, in practice these environments might still want to support a
few specific user widgets such as "Try this".
---
Closes#2064.
In `v4.8.0-rc2`, due to additional build refactor changes, `JobM` no
longer cleanly lifts in `FetchM`. Generally, a `JobM` action should not
be run `FetchM` directly but spawned asynchronously as job (e.g., via
`Job.async`). However, there may be some edge cases were this is
necessary and it is a backwards compatibility break, so this change adds
back the lift. This change also includes an `example` definition to
ensure the lift works in order to prevent similar accidental breakages
in the future.
This breakage was first reported by Mario on
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/v4.2E8.2E0-rc2.20discussion/near/440407037).
Switches the manifest format to use `major.minor.patch` semantic
versions. Major version increments indicate breaking changes (e.g., new
required fields and semantic changes to existing fields). Minor version
increments (after `0.x`) indicate backwards-compatible extensions (e.g.,
adding optional fields, removing fields). This change is backwards
compatible. Lake will still successfully read old manifest with numeric
versions. It will treat the numeric version `N` as semantic version
`0.N.0`. Lake will also accept manifest versions with `-` suffixes
(e.g., `x.y.z-foo`) and then ignore the suffix.
This change also includes the general cleanup/refactoring of the
manifest code and data structures that was part of #3174.
Adds two new Lake commands, `lake pack` and `lake unpack`, which pack
and unpack, respectively, Lake build artifacts from an archive. If a
path argument is given, creates the archive specified, otherwise uses
the information in a package's `buildArchive` configuration as the
default.
The pack command will be used by Reservoir to prepare crate-style build
archives for packages. In the future, the command will also be
extensible through configuration file hooks.
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.
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).
luckily the necessary functionality already exists in the form of
`addPPExplicitToExposeDiff`. But it is not cheap, and we should not run
this code
when the error message isn’t shown, so we should do this lazily.
We already had `MessageData.ofPPFormat` to assemble the error message
lazily, but it
was restricted to returning `FormatWithInfo`, a data type that doesn’t
admit a nice
API to compose more complex messages (like `Format` or `MessageData`
has; an attempt to
fix that is in #3926).
Therefore we split the functionality of `.ofPPFormat` into
`.ofFormatWithInfo` and `.ofLazy`,
and use `.ofLazy` to compute the more complex error message of `apply`.
Fixes#3232.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Messaged @tydeu about adding a README.md to new lake projects. I decided
to add it with the help of GPT.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
The new Lake build monitor is now more selective, accurate, and prettier
in what it prints.
**Key Changes:**
* Poll jobs at a fixed frequency (100ms), updating the caption and
finished job count.
* Add `action` field to jobs to record information about what jobs do.
It enables distinguishing between jobs which build something, fetch from
a store, or reload logs from the cache.
* At standard verbosity, print build captions only when a job is know to
build or fetch something (i.e., `action >= .fetch`).
* Add an icon and color to job captions based on their log-level / build
status. Also add color to levels in logs.
* Add `--ansi`/`--no-ansi` to toggle Lake's use of ANSI escape codes.
* Fix some `v4.8.0-rc1` bugs and `--old`.
Closes#2822.
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.)
This PR adds theorems that relate unsigned bitvector comparisons
`BitVec.ult` and `BitVec.ule` to `BitVec.carry`. These lemmas are a
prerequisite to bit-blasting these comparisons in LeanSAT.
The trace class Meta.synthInstance.answer isn't registered, so it can't
be used.
I set `inherited := true`, because I think it is a useful trace to have.
In particular it tells you when an instance has been found that has a
too large size. This is very useful information.
as usually, just a matter of using the `WithInfo` variant.
Also simplifying the code a bit, it seems we can use
`realizeGlobalConstNoOverloadWithInfo` here.
(It's somehwatdubious API design that of all the functions in
the `{resolve/realise}GlobalConst{NoOverload,}{WithInfo,}` family
the one with the longest name is the one that should be used
unless one has a reason to use another one.)
Fixes: #4174
in #4158 I was experimenting with a change to the simplifier that
affectes the order in which lemmas were tried, and of course it breaks
proofs all over the place whenever we have a non-confluent simp set.
Among the first breakages encountered, a large fraction was due to
`simp` rewriting with `List.length_pos : 0 < length l ↔ l ≠ []`.
This does not strike me a as a good simp lemma: If `l` is a manifest
constructor, the simplifier will reduce `length` and solve it anyways,
and if it isn't then an inequality usually isn’t very simp friendly. It
is also highly non-confluent with any kind of `length`-lemma we might
have.
This therefore removes it from the standard simp set.
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
This improves job captions, the grouping of logs underneath them, and
the handling of import errors. It also adds a number of log-related
utilities to help achieve this.
**Key Changes:**
* Job captions for facets now include the name of the object (e.g.,
module, library, facet). A caption has also been added to the top-level
build of imports (e.g., for the server and `lake lean`).
* Stray I/O and errors outside the build job in a build function
captioned with `withRegisterJob` (e.g., user-defined targets) will now
be properly grouped under that caption instead of ending up under
"Computing build jobs". Stray I/O will be converted to a single
informational log entry.
* Builds no longer fail immediately on erroneous imports. Lake will now
attempt to recover as best as possible from any import errors.
Information on the import error will appear both in the build of the
erroneous import and in the files which transitive import it. For
example, uf `Lib.B` imports a missing module `Lib.A`, then the build of
`Lib.A` will mention that the file does not exist, and the build of
`Lib.B` will mention the bad import of `Lib.A`.
Closes#3351. Closes#3809.
Previously, the CI would run upon every label addition, including things
like `builds-mathlib`
or `will-merge-soon`, possibly triggering a new PR release, new mathlib
builds etc. Very wasteful!
Unfortunately (but not surprisingly) Github does not offer a nice way of
saying
“this workflow depends on that label, please re-run if changed”. Not
enough
functional programmer or nix enthusiasts there, I guess…
So here is the next iteration trying to work with what we have from
Github:
A new workflow watches for (only) `full-ci` label addition or deletion,
and then re-runs
the CI job for the current PR.
Sounds simple? But remember, this is github!
* `github.event.pull_request.labels.*.name` is *not* updated when a job
is re-run.
(This is actually a reasonable step towards determinism, but doesn't
help us
constructing this work-around.)
Ok, so let’s use the API to fetch the current state of the label.
* There is no good way to say “find the latest run of workflow `"CI"` on
PR `$n`”.
The best approximation seems to search by branch and triggering event.
This can
probably go wrong if there are multiple PRs from different repos with
the same
head ref name (`patch-1` anyone?). Let’s hope that it doesn’t happen too
often.
* You cannot just rerun a workflow. You can only rerun a finished
workflow. So cancel
it first. And `sleep` a bit…
So let’s see how well this will work. It’s plausibly an improvement.
I did not introduce `inductTheoremSuffix` etc, it seems more direct to
just spell out the suffix here. If we ever change it there are many
occurrences where they need to be changed anyways, so the definition
doesn't seem to save much work or add that much robustness.
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.
This reverts commit 706a4cfd73 introduced
in #3970
As explained in #4124, `findM?` can become a footgun if used in monads
which induce side-effects such as caching. This PR removes that
function, and fixes the code introduced by #3398 for which the function
was first added.
cc @semorrison.
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.
Fixes#3270 by moving the deprecation check from
`Lean.Elab.Term.mkConsts` to `Lean.Elab.Term.mkConst`, so
`Lean.Elab.Term.mkBaseProjections`, `.elabAppLValsAux`, `.elabAppFn`,
and `.elabForIn` also hit the check. Not all of these really need to hit
the check, so I'll run `!bench` to see if it's a problem.
this is in preparation for #4061. Once that lands, `1 % 42 = 1` will no
longer hold definitionally (at least not without an ungly `unseal
Nat.modCore in` around). This affects mathlib in a few places,
essentially every time a `1 : Fin (n+1)` literal is written.
So this extends the existing special case for `0 % n = 0` to `1 % n`.
https://live.lean-lang.org/#project=lean-nightly now allows users to
play around with the latest lean nightly, and it seems prudent to ask
them to test bug reports, if possible, there, and not just with whatever
release they use.
Also reformatted the descriptions to look well in a text area. Users
will not see this as rendered markdown, but as plain text.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
As [reported on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/341532-lean4-dev/topic/Find.20references.20broken.20in.20lean.20core/near/437051935).
The `mainModuleName` was being set incorrectly when browsing lean core
sources, resulting in failure of cross-file server requests like "Find
References". Because the `srcSearchPath` is generated asynchronously, we
store it as a `Task Name` which is resolved some time before the header
is finished parsing. (I don't think the `.get` here will ever block,
because the srcSearchPath will be ready by the time the initial command
snap is requested.)
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Add docstrings and usage examples for `String.length`, `.push`,
`.append`, `.get?`, `.set`, `.modyify`, and `.next`. Update docstrings
and add usage examples for `String.toList`, `.get`, and `.get!`.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
This issue was affecting several Mathlib files.
@mattrobball @semorrison This is a different solution for the issue. The
comment at `Extra.lean` describes the new solution and documents the new
issues found with the previous one.
closes#4085
This makes the `leanArts` in `library_data leanArts : BuildJob Unit` get
a hover for the generated axiom. It also simplifies the `quoteFrom`
function so that it delaborates properly by using a name literal (which
elaborates to `mkStr1`, `mkStr2` etc) instead of a `mkStr` application.
otherwise it remains in the equational theorem and may cause the
“unused have linter” to trigger. By moving the proof into
`decreasing_by`, the equational theorems are unencumbered by termination
arguments.
see also
https://github.com/leanprover/std4/pull/690#issuecomment-2095378609
Closes#3386
Currently, when generating the signature of an injectivity lemma for a
certain constructor `c : forall xs, Foo a_1 ... a_n`,
`mkInjectiveTheoremTypeCore?` will differentiate between variables which
are bound to stay the same between the two equal values (i.e inductive
indices), and non-fixed ones. To do that, the function currently checks
whether a variable `x ∈ xs` appears in the final co-domain `Foo a_1 ...
a_n` of the constructor. This condition isn't enough however. As shown
in the linked issue, the codomain may also depend on variables which
appears in the type of free vars contained in `Foo a_1 ... a_n`, but not
in the term itself. This PR fixes the issue by also checking the types
of any free variable occuring in the final codomain, so as to ensure
injectivity lemmas are well-typed.
This PR upstreams lemmas about List/Array operations already defined in
Lean from std/batteries.
Happy to take suggestions about increasing or decreasing scope.
---------
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
On
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Notation.20in.20namespace.20not.20showing.20in.20pp/near/437016468),
Peter Nelson reported that notations that could be pretty printed with
generalized field notation did not pretty print using the intended
notation.
This PR makes it so that app unexpanders are considered before
generalized field notation. The complexity before was that we wanted to
do parent projection collapse, and since we did the collapse before
pretty printing that argument, it meant it wasn't possible to do app
unexpanders when there was a field notation candidate. The new solution
is to collapse parent projections only when actually considering field
notation, which can be done because we can safely strip off projection
syntax in an expression-directed way.
The layout algorithm, while somewhat finicky, is (unfortunately)
necessary for C code to interface with lean structures. This adds a
(AFAIK) complete description of the layout algorithm, including a worked
example large enough to make it possible to reconstruct the whole
decision diagram.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This is still experimental, but it implements identifier support in auto
tactics "in the obvious way". It also converts `quoteAutoTactic` to
generate Expr directly instead of going via syntax (this doesn't have
any effect other than increasing compile cost AFAICT).
Adds `IO.Process.getCurrentDir` and `IO.Process.setCurrentDir` for
retrieving and setting, respectively, the current working directory of a
process. The names of the functions are inspired by Rust (e.g.,
[`set_current_dir`](https://doc.rust-lang.org/std/env/fn.set_current_dir.html)).
even when rewriting the type of `h` becuase there is no expected type.
(When there is an expected type, it already tried both orientations.)
Also feeble attempt to include this information in the docstring without
writing half a manual chapter.
when dealing with well-founded recursive definitions, `tryURefl` isn't
going to be that useful and possibly slow. So disable that code path
when doing well-founded recursion.
(This is a variant of #4025 where I tried using `with_reducible` to
limit the impact of slow unfolding, but if we can get away with
disabling it complete, then even better.)
In the following, hovering over `true` in the infoview was showing
`Nat.succ y`.
```lean
#check fun (x : Nat) =>
match h : x with
| 0 => false
| y + 1 => true
```
Now hovering over `true` shows `true`.
The issue was that SubExpr positions were not being tracked for
patterns, and the position for a pattern could coincide with the
position for a RHS, putting overwriting terminfo. Now the position given
to a pattern is correct and unique.
Refactors the `match` delaborator, makes it handle shadowing of `h :`
discriminant annotations correctly, and makes it use the standard
`withOverApp` combinator to handle overapplication.
Fixes some bugs with the log refactor (#3835). Namely, quiet mode
progress printing and missing string interpolation in the fetching cloud
release caption.
This is a major refactor of Lake's build code. The key changes:
* **Job Registration**: Significant build jobs are now registered by
build functions. The DSL inserts this registration automatically into
user-defined targets and facets, so this change should require no
end-user adaption. Registered jobs are incrementally awaited by the main
build function and the progress counter now indicates how many of these
jobs are completed and left-to-await. On the positive side, this means
the counter is now always accurate. On the negative side, this means
that jobs are displayed even if they are no-ops (i.e., if the target is
already up-to-date).
* **Log Retention**: Logs are now part of a Lake monad's state instead
of being eagerly printed. As a result, build jobs retain their logs.
Using this change, logs are are now always printed after their
associated caption (e.g., `[X/Y] Building Foo`) and are not arbitrarily
interleaved with the output of other jobs.
* **Simplify the build monad stack**: Previously, there was a lot of
confused mixing between the various build monads in the codebase (i.e.,
`JobM`, `ScedulerM`, `BuildM`, `RecBuildM`, and `IndexBuildM` ). This
refactor attempts to make there use more consistent and straightforward:
* `FetchM` (formerly `IndexBuildM`) is the top-level build monad used by
targets and facets and is now uniformly used in the codebase for all
top-level build functions.
* `JobM` is the monad of asynchronous build jobs. It is more limited
than `FetchM` due to the fact that the build cache can not be modified
asynchronously.
* `SpawnM` (formerly `SchedulerM`) is the monad used to spawn build
jobs. It lifts into `FetchM`.
* `RecBuildM` and `CoreBuildM` (formerly `BuildM`) have been relegated
to internal details of how `FetchM` / `JobM` are implemented / run and
are no longer used outside of that context.
* **Pretty progress.** Build progress (e.g., `[X/Y] Building Foo`) is
now updated on a single line via ANSI escape sequences when Lake is
outputting to a terminal. Redirected Lake output still sees progress on
separate lines.
* **Warnings-as-error option.** Adds a `--wfail` option to Lake that
will cause a build to fail if Lake logs any warnings doing a build.
Unlike some systems, this does not convert warnings into errors and it
does not abort jobs which log warnings. Instead, only the top-level
build fails.
* **Build log cache.** Logs from builds are now cached to a file and
replayed when the build is revisited. For example, this means multiple
runs of a `--wfail` Lean build (without changes) will still produce the
same warnings even though there is now an up-to-date `.olean` for the
module.
Closes#2349. Closes#2764.
Lake now errors instead of warns on a mismatch between a package name
and what is required as. This avoids sometimes confusing downstream
errors. Also, this change provides additional information for errors
that may be caused by the upcoming Std rename.
Because of the last-added-tried-first rule for macros, all the special
purpose `decreasing_trivial` rules are tried for most recursive
definitions out there, and because they use `apply` and `assumption`
with default transparency may cause some definitoins to be unfolded over
and over again.
A quick test with one of the functions in the leansat project shows that
elaboration time goes down from 600ms to 375ms when using
```
decreasing_by all_goals decreasing_with with_reducible decreasing_trivial
```
instead of
```
decreasing_by all_goals decreasing_with decreasing_trivial
```
This change uses `with_reducible` in most of these macros.
This means that these tactics will no longer work when the
relations/definitions they look for is hidden behind a definition.
This affected in particular `Array.sizeOf_get`, which now has a
companion `sizeOf_getElem`.
In addition, there were three tactics using `apply` to apply Nat-related
lemmas
that we now expect `omega` to solve. We still need them when building
`Init` modules
that don’t have access to `omega`, but they now live in
`decreasing_trivial_pre_omega`,
meant to be only used internally.
- We can set `[irreducible]`, `[semireducible]`, and `[reducible]` for
imported declarations.
- Support for `scoped` and `local` versions
TODO: discuss whether we need all this power after we add the module
system.
It currently only reports how many times each declaration has been
unfolded, and how often the `isDefEq` heuristic for `f a =?= f b` has
been used. Only counters above the threshold are reported.
The subst notation substitues in the expected type, if present, or in
the type of the argument, if no expected type is known.
If there is an expected type it already fails if it cannot find the
equations' left hand side or right hand side. But if the expected type
is not known and the equation's lhs is not present in the second
argument's type, it will happily do a no-op-substitution.
This is inconsistent and unlikely what the user intended to do, so we
now print an error message now.
This still only looks for the lhs; search for the rhs as well seems
prudent, but I’ll leave that for a separate PR, to better diagnose the
impact on mathlib.
This triggers a small number of pointless uses of subst in mathlib, see
https://github.com/leanprover-community/mathlib4/pull/12451
macos-latest changed to arm64. It should not be hard to switch our setup
to cross-compiling x64 instead of arm64 but let's get master green again
first.
We add a new configuration flag for `isDefEq`:
`Meta.Config.univApprox`.
When it is true, we approximate the solution for universe constraints
such as
- `u =?= max u ?v`, we use `?v := u`, and ignore the solution `?v := 0`.
- `max u v =?= max u ?w`, we use `?w := v`, and ignore the solution `?w
:= max u v`.
We only apply these approximations when there the contraints cannot be
postponed anymore. These approximations prevent error messages such as
```
error: stuck at solving universe constraint
max u ?u.3430 =?= u
```
This kind of error seems to appear in several Mathlib files.
We currently do not use these approximations while synthesizing type
class instances.
`Name.append` has special handling of macro scopes, and it would cause
`unresolveNameGlobal` to panic. Using `Name.appendCore` to append name
parts is justified by the fact that it's being used to reassemble a
disassembled name.
Closes#2291
Adds `ppLevel` to the `PPFns` extension so that the coercion can pass
the pretty printing context (including the `pp.mvars` option setting) to
the `Level` formatter.
Expands on #3971 to do something useful even before the PR enters the
queue:
If stage0 changes are detected in the PR, set the changes-stage0 label
(which
has a tooltip to explain what this entail), and also remove the label if
it no
longer applies.
Previously the `ac_rfl` tactic was only really usable when depending on
mathlib. With these instances, `ac_rfl` can deal with the various
operations defined in Lean.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This makes `exact?%` behave like `by exact?` rather than `by apply?`.
If the underlying function `librarySearch` finds a suggestion which
closes the goal, use it (and add a code action). Otherwise log an error
and use `sorry`. The error is either
```text
`exact?%` didn't find any relevant lemmas
```
or
```text
`exact?%` could not close the goal. Try `by apply` to see partial suggestions.
```
---
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Useful.20term.20elaborators/near/434863856)
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
<!--
# Read this section before submitting
* Ensure your PR follows the [External Contribution
Guidelines](https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md).
* Please make sure the PR has excellent documentation and tests. If we
label it `missing documentation` or `missing tests` then it needs
fixing!
* Include the link to your `RFC` or `bug` issue in the description.
* If the issue does not already have approval from a developer, submit
the PR as draft.
* The PR title/description will become the commit message. Keep it
up-to-date as the PR evolves.
* If you rebase your PR onto `nightly-with-mathlib` then CI will test
Mathlib against your PR.
* You can manage the `awaiting-review`, `awaiting-author`, and `WIP`
labels yourself, by writing a comment containing one of these labels on
its own line.
* Remove this section, up to and including the `---` before submitting.
-->
See RFC #3644 for a discussion of design choices.
Closes#3644
Currently this will fail in two tests, because of changes in #3965.
* Sometimes we need to add an additional universe annotation, or we get
a `stuck at solving universe constraint max u ?u =?= u`.
* Sometimes we need to specify arguments that could previously be found
by unification.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
Complement to #3967 , adds a `(since := "<date>")` field to
`@[deprecated]` so that metaprogramming code has access to the
deprecation date for e.g. bulk removals. Also adds `@[deprecated
"deprecation message"]` to optionally replace the default text
"`{declName}` has been deprecated, use `{newName}` instead".
these need manual rebase merges by an admin, so lets prevent accidential
merges via the squashing merge queue.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Adds a `--json` option to the `lean` CLI. When used, the Lean frontend
will print messages as JSON objects using the default `ToJson` encoding
for the `Message` structure. This allows consumers (such as Lake) to
handle Lean output in a more intelligent, well-structured way.
`Message` has been refactored into `BaseMessage`, `Message`, and
`SerialMessage` to enable deriving `ToJson`/ `FromJson` instances
automatically for `BaseMessage` / `SerialMessage`. `SerialMessage` is a
`Message` with its `MessageData` eagerly serialized to a `String`.
- [x] Depends on: #3958
- [x] Depends on: #3960
This makes the UTF-8 encode and decode functions have lean definitions,
so that we can prove properties about them downstream.
previously, the empty `MessageData` (`m!""`) was used to indicate “no
message”, and `throwTacticEx` would format the message differently then.
But the semantics of `MessageData.isEmpty` isn't entirely clear in the
presence of lazy message data (e.g. `.ofPPFormat`).
So to avoid wondering what `isEmpty` should do there, let's simply use
an optional argument to `throwTacticEx` and get rid of
`MessageData.isEmpty`.
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.
Rather than adding symm hypotheses to the local context, it now adds
them to the list of hypotheses derived from the local context.
This is not ideal for performance reasons, but it at least closes#3922.
In the future, solveByElim could maintain its own cache of facts that it
updates whenever it does intro.
This PR partly addresses #3458, by adding an option `autoPromoteIndices`
to turn off the promotion of fixed indices to parameters. The actual fix
for the issue is in a separate PR #3591.
Because nested inductive datatypes parameters cannot contain local
variables, it is often desirable for a fixed index to not be promoted,
as to allow free variables in that place. See example in `3458_1.lean`
This is intended to fail at present: it just adds a test case containing
a minimization of a Mathlib slowdown from #3807.
Prior to #3807, the declaration `exists_algHom_adjoin_of_splits'''` at
the end of the file would take around 16,000 heartbeats. Now it takes
around 210,000 heartbeats.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
Previously, there was a function `opaque fromUTF8Unchecked : ByteArray
-> String` which would convert a list of bytes into a string, but as the
name implies it does not validate that the string is UTF-8 before doing
so and as a result it produces unsound results in the compiler (because
the lean model of `String` indirectly asserts UTF-8 validity). This PR
replaces that function by
```lean
opaque validateUTF8 (a : @& ByteArray) : Bool
opaque fromUTF8 (a : @& ByteArray) (h : validateUTF8 a) : String
```
so that while the function is still "unchecked", we have a proof witness
that the string is valid. To recover the original, actually unchecked
version, use `lcProof` or other unsafe methods to produce the proof
witness.
Because this was the only `ByteArray -> String` conversion function, it
was used in several places in an unsound way (e.g. reading untrusted
input from IO and treating it as UTF-8). These have been replaced by
`fromUTF8?` or `fromUTF8!` as appropriate.
* Replaces the unused `Lean.PrettyPrinter.ppConst` with
`MessageData.ofConst` (which similarly avoids an unnecessary `@`) and
that further generates a hover for the constant
* Uses this in `TryThis.addRewriteSuggestion`, so that `rw?` suggestions
don't have unnecessary `@`s.
* Add `MessageData.signature`, as a wrapper around
`PrettyPrinter.signature`, using the same machinery to generate hovers
for constants, improving the hover behaviour in #check so that we get
second order pop-up for constants in the signature. (Not sure how to
write tests for second order hovers, so there is no test for this.)
Adds the ability to show a diff when `guard_msgs` fails, using the
histogram diff algorithm pioneered in jgit. This algorithm tends to
produce more user-friendly diffs, but it can be quadratic in the worst
case. Empirically, the quadratic case of this implementation doesn't
seem to be slow enough to matter for messages smaller than hundreds of
megabytes, but if it's ever a problem, we can mitigate it the same way
jgit does by falling back to Myers diff.
See lean/run/guard_msgs.lean in the tests directory for some examples of
its output.
Adds `IO.FS.Handle.isTty` to check whether a handle is a Windows console
or Unix terminal. Also adds an `isTty` field to `IO.FS.Stream`, so that
this can be checked on, e.g., `stdout`.
Go-to-def on `@[builtin_term_parser]` should go to the line
```lean
builtin_initialize registerBuiltinParserAttribute `builtin_term_parser ``Category.term
```
not
```lean
/-- `term` is the builtin syntax category for terms. ... -/
def term : Category := {}
```
While implementing #3925, I noticed that the performance of the
`textDocument/semanticTokens/full` request is *extremely* bad due to a
quadratic implementation. Specifically, on my machine, computing the
full semantic tokens for `Lean/Elab/Do.lean` took a full 5s. In
practice, this means that while elaborating the file, one core is
entirely busy with computing the semantic tokens for the file.
This PR fixes this performance bug by re-implementing the semantic token
handling, reducing the latency for `Lean/Elab/Do.lean` from 5s to 60ms.
As a result, the overly cautious refresh latency of 5s in #3925 can
easily be reduced to 2s again.
Since the previous semantic tokens implementation used a very brittle
hack to identify projections, this PR also changes the projection
notation elaboration to augment the `InfoTree` syntax for the field of a
projection with a special syntax node of kind
`Lean.Parser.Term.identProjKind`. With this syntax kind, projection
fields can now easily be identified in the `InfoTree`.
`Nat.repr` was implemented by generating a list of `Chars`, each created
by a 10-way if-then-else. This can cause significant slow down in some
particular use cases.
Now `Nat.repr` is `implemented_by` a faster implementation that uses
C++’s `std::to_string` on small numbers (< USize.size) and maintains an
array of pre-allocated strings for the first 128 numbers.
The handling of big numbers (≥ USize.size) remains as before.
The `#guard_msgs` command already runs linters by virtue of using
`elabCommandTopLevel`, so linters should *not* be run on `#guard_msgs`
itself. While we could use a more general solution, of the linters the
unused variables linter is the noisiest one, and it's easy enough to
make it not report messages for `#guard_msgs`.
Just a lemma that we noticed is missing when working on #3880 at the
retreat. We also noticed that there are naming inconsistencies in the
lemmas for `bmod` and `emod`, we should fix that in the future.
@semorrison, does this include all the answers to the questions I asked
in our thread? I think so!
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
while trying to help a user who was facing an unhelpful
```
omega did not find a contradiction:
[0, 0, 0, 0, 1, -1] ∈ [1, ∞)
[0, 0, 0, 0, 0, 1] ∈ [0, ∞)
[0, 0, 0, 0, 1] ∈ [0, ∞)
[1, -1] ∈ [1, ∞)
[0, 0, 0, 1] ∈ [0, ∞)
[0, 1] ∈ [0, ∞)
[1] ∈ [0, ∞)
[0, 0, 0, 1, 1] ∈ [-1, ∞)
```
I couldn’t resist and wrote a pretty-printer for these problem that
shows the linear combination as such, and includes the recognized atoms.
This is especially useful since oftem `omega` failures stem from failure
to recognize atoms as equal. In this case, we now get:
```
omega-failure.lean:19:2-19:7: error: omega could not prove the goal:
a possible counterexample may satisfy the constraints
d - e ≥ 1
e ≥ 0
d ≥ 0
a - b ≥ 1
c ≥ 0
b ≥ 0
a ≥ 0
c + d ≥ -1
where
a := ↑(sizeOf xs)
b := ↑(sizeOf x)
c := ↑(sizeOf x.fst)
d := ↑(sizeOf x.snd)
e := ↑(sizeOf xs)
```
and this might help the user make progress (e.g. by using `case x`
first, and investingating why `sizeOf xs` shows up twice)
Reusing the best profiling UI out there
Usage:
```
lean -Dtrace.profiler=true -Dtrace.profiler.output=profile.json foo.lean ...
```
then open `profile.json` in https://profiler.firefox.com/.
See also `script/collideProfiles.lean` for minimizing and merging
profiles.
Implements a new method to generate instance names for anonymous
instances that uses a heuristic that tends to produce shorter names. A
design goal is to make them relatively unique within projects and
definitely unique across projects, while also using accessible names so
that they can be referred to as needed, both in Lean code and in
discussions.
The new method also takes into account binders provided to the instance,
and it adds project-based suffixes. Despite this, a median new name is
73% its original auto-generated length. (Compare: [old generated
names](https://gist.github.com/kmill/b72bb43f5b01dafef41eb1d2e57a8237)
and [new generated
names](https://gist.github.com/kmill/393acc82e7a8d67fc7387829f4ed547e).)
Some notes:
* The naming is sensitive to what is explicitly provided as a binder vs
what is provided via a `variable`. It does not make use of `variable`s
since, when names are generated, it is not yet known which variables are
used in the body of the instance.
* If the instance name refers to declarations in the current "project"
(given by the root module), then it does not add a suffix. Otherwise, it
adds the project name as a suffix to protect against cross-project
collisions.
* `set_option trace.Elab.instance.mkInstanceName true` can be used to
see what name the auto-generator would give, even if the instance
already has an explicit name.
There were a number of instances that were referred to explicitly in
meta code, and these have been given explicit names.
Removes the unused `Lean.Elab.mkFreshInstanceName` along with the
Command state's `nextInstIdx`.
Fixes#2343
As a special case, makes the `rcases` machinery use `Nat.casesAuxOn` so
that goal states see `0` and `n + 1` rather than `Nat.zero` and
`Nat.succ n`. This is a followup to enabling custom eliminators for
`cases` and `induction`.
This doesn't use custom eliminators in general since `rcases` uses
`Lean.MVarId.cases`, which is completely different from what `cases` and
`induction` use.
Adds options to control whitespace normalization and message ordering in
`#guard_msgs`.
Examples:
1. `#guard_msgs (whitespace := lax)` ignores differences in whitespace
completely.
2. `#guard_msgs (whitespace := exact)` requires an exact match for
whitespace (after trimming).
3. `#guard_msgs (ordering := sorted)` sorts the list of messages, to
make it insensitive to message order.
This should improve the performance of the deriving a bit since it
doesn't have to generate so many matchers. The main motivation though is
to make it easier to prove properties about the expression by using more
standard functions. The generated implementation should end up the same,
since `Ordering.then` is `@[macro_inline]`.
This adds some basic lemmas to support commuting ofInt/toInt and
add/mul.
It also removes the simp annotation on `ofNat_add_ofNat` as in some
contexts the other direction or conversion to Int may be desired.
The Canonicalizer creates a “key” expression eliding certain information
(implicit parameters, levels), and `getFunInfo` can be
confused by these terms (in particular, wrong number of level
parameters).
By running `getFunInfo` on the original expression we avoid this, and
can just put `[]` as the level list in the key.
This changes how Nat typeclass checks in offset terms from syntactic
equality to definitional equality with "instances" transparency.
This may have a negative performance penalty in `isOffset?`, but it
should be small in common cases since the relevant instances are small
terms.
This closes#3836
This removes simp attributes from `Nat.succ.injEq` and
`Nat.succ_sub_succ_eq_sub` to replace them with simprocs. This is
because any reductions involving `Nat.succ` has a high risk of leading
proof performance problems when dealing with even moderately large
numbers.
Here are a couple examples that will both report a maximum recursion
depth error currently. These examples are fixed by this PR.
```
example : (123456: Nat) = 12345667 := by
simp
example (x : Nat) (p : x = 0) : 1000 - (x + 1000) = 0 := by
simp
```
Possibly the more principled fix is to not have `simp` invoke
dischargers under `withReducible`.
In the meantime, this ensures that `falseOrByContra` still succeeds with
`intro1` on a `Not` goal, which previously was breaking `omega` as a
simp discharger.
Closes#3805.
This fixes an issue where the completion would use info nodes before the
cursor for computing completions.
Fixes https://github.com/leanprover/lean4/issues/3462.
ToDo:
- [x] Fix test failures for completions that previously worked by
accident (cc: @Kha)
- [x] stage0 update
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
The matches returned by the lazy discriminator tree are partially
constrained by a priority, but ties are broken by the order in which
keys are traversed and the order of declarations.
This PR changes the match key traversal to use an explicit stack rather
than recursion and implicitly changes the order in which results are
returned to favor left-matches first e.g., given the term `f a b` with
constants `f a b`, and a tree with patterns `f a x -> 1` `f x b -> 2`
that have the same priority, this will return `#[1, 2]` since the early
matches for the key `a` are returned before the match for `x` which has
a star.
This appears to address the [lower quality results mentioned on
zulip](https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/Mathlib.20status.20updates/near/429955747).
When `discharge?` failed, the `usedSimps` was being restored, but the
cache wasn't. This bug was exposed by issue #3710.
This PR makes the following changes:
- We restore the `cache` at `discharge?`. We use `SMap` to ensure the
operation is efficient.
- We don't need the field `dischargeDepth` anymore at `Simp.Result`.
- `UsedSimps` should use `PHashMap` since it is not used linearly.
closes#3710
---------
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Now, only `(<- ...)`s occurring in the condition of a pure if-then-else
are lifted.
That is, `if (<- foo) then ... else ...` is ok, but `if ... then (<-
foo) else ...` is not. See #3713closes#3713
This PR also adjusts this repo. Note that some of the `(<- ...)` were
harmless since they were just accessing some
read-only state.
It have to keep it as a private definition for now. We currently only
support duplicate theorems in different modules. Splitters are generated
on demand, and are also used to write code.
Adds a `lake lean` CLI command that builds the imports of a Lean file
and then elaborates it via `lean` with the workspace's configuration
(i.e., adding the `moreLeanArgs` / `leanOptions` of the root `package`
and Lake's environment).
* Setting `pp.mvars` to false causes metavariables to pretty print as
`?_`.
* Setting `pp.mvars.withType` to true causes metavariables to pretty
print with type ascriptions.
Motivation: when making tests, it is inconvenient using `#guard_msgs`
when there are metavariables, since the unique numbering is subject to
change.
This feature does not use `⋯` omissions since a metavariable is already
in a sense an omitted term. If repeated metavariables do not appear in
an expression, there is a chance that a term pretty printed with
`pp.mvars` set to false can still elaborate to the correct term, unlike
for other omissions.
(In the future we could consider an option that pretty prints uniquely
numbered metavariables as `?m✝`, `?m✝¹`, `?m✝²`, etc. to be able to tell
them apart, at least in the same pretty printed expression. It would
take care to make sure that these names are stable across different
hovers.)
Closes#3781
The `conv` tactic tries to close “trivial” goals after itself. As of
now, it uses
`try rfl`, which means it can close goals that are only trivial after
reducing with
default transparency. This is suboptimal
* this can require a fair amount of unfolding, and possibly slow down
the proof
a lot. And the user cannot even prevent it.
* it does not match what `rw` does, and a user might expect the two to
behave the
same.
So this PR changes it to `with_reducible rfl`, matching `rw`’s behavior.
I considered `with_reducible eq_refl` to only solve trivial goals that
involve equality,
but not other relations (e.g. `Perm xs xs`), but a discussion on mathlib
pointed out
that it’s expected and desirable to solve more general reflexive goals:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Closing.20after.20.60rw.60.2C.20.60conv.60.3A.20.60eq_refl.60.20instead.20of.20.60rfl.60/near/429851605
Modifies `withBindingBodyUnusedName` to annotate the syntax for the
variable with its corresponding fvar. Now, for example, you can hover
over the variables in `fun x y => ...` in the infoview to see their
types. This change affects notations such as `∃ n, n = 1`, where
hovering over `n` shows that `n : Nat`.
Also adds such annotations for the variables in `let` and `let_fun`.
Implementation note: the variables are annotated with fresh positions
using `nextExtraPos`.
Removes the unused and unnecessary
`Lean.PrettyPrinter.Delaborator.liftMetaM`.
Closes#1618, closes#2737
This PR includes the following fixes:
- Reserved name resolution inside namespaces
- Equation theorems for `match`er declarations are not private anymore
- Equation theorems for `match`er declarations are realizable
- `foo.match_<idx>.splitter` is now a reserved name
Normalize the relative packages directory paths in the pre-rename check
to avoid renames if the difference in paths is only in the path
separators. Also adds a log message on rename.
Commands that can optionally parse an `ident` or parse any number of
`ident`s generally should require that the `ident` use `colGt`. This
keeps typos in commands from being interpreted as identifiers.
For example, without this rule,
```
universe u
Open Lean
````
parses the same as `universe u Open Lean`. It would be better to get an
error on `Open`.
This PR adds `checkColGt` to `section`, `namespace`, `end`, `variable`,
and `universe`.
Closes#2684
Adds an alternative TOML configuration format to Lake.
* Uses TOML v1.0.0 and is fully specification compliant (tested via
[toml-test v1.4.0](https://github.com/toml-lang/toml-test/tree/v1.4.0)).
* Supports package configuration options, Lean libraries, Lean
executables, and dependencies.
* TOML configurations can be generated for new projects via `lake
new|init <pkg> <template>.toml`.
* Supported configurations can be converted to/from TOML via `lake
translate-config <lang>`.
This makes changes to the `GetElem` class so that it does not lead to
unnecessary overhead in container like `RBMap`.
The changes are to:
1. Make `getElem?` and `getElem!` part of the `GetElem` class so they
can be overridden in instances.
2. Introduce a `LawfulGetElem` class that contains correctness theorems
for `getElem?` and `getElem!` using the original definitions.
3. Reorganize definitions (e.g, by moving `GetElem` out of
`Init.Prelude`) so that the `GetElem` changes are feasible.
4. Provide `LawfulGetElem` instances to complement all existing
`GetElem` instances in Lean core.
To reduce the size of the PR, this doesn't do the work of providing new
`GetElem` instances for `RBMap`, `HashMap` etc. That will be done in a
separate PR (#3688) that depends on this.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
fixes#3657
These functions are mostly not used by lean itself, but it does affect
two occurrences of `ByteArray.toUInt64LE! <$> IO.getRandomBytes 8` which
I left as is instead of switching them to use `toUInt64BE!` to preserve
behavior; but they are random bytes anyway seeded by the OS so it's
unlikely any use of them depending on particular values was sound to
begin with.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
When it was upstreamed, it lost the mention of "revert/intro pattern",
which is helpful for finding this function. Also extended the
description of the function and clarified some points.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Previously we were suggesting rebasing onto the most recently nightly in
the branches history, but that is incorrect and we should *always*
suggest rebasing on `origin/nightly-with-mathlib`.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This avoids printing the entire docstring for `⋯` when hovering over it,
which is rather long, and instead it gives a brief reason for omission
and what option to set to pretty print the omitted term.
Previously:
If the `rfl` macro was going to fail, it would:
1. expand to `eq_refl`, which is implemented by
`Lean.Elab.Tactic.evalRefl`, and call `Lean.MVarId.refl` which would:
* either try kernel defeq (if in `.default` or `.all` transparency mode)
* otherwise try `IsDefEq`
* then fail.
2. Next expand to the `apply_rfl` tactic, which is implemented by
`Lean.Elab.Tactic.Rfl.evalApplyRfl`, and call `Lean.MVarId.applyRefl`
which would look for lemmas labelled `@[refl]`, and unfortunately in
Mathlib find `Eq.refl`, so try applying that (resulting in another
`IsDefEq`)
3. Because of an accidental duplication, if `Lean.Elab.Tactic.Rfl` was
imported, it would *again* expand to `apply_rfl`.
Now:
1. Same behaviour in `eq_refl`.
2. The `@[refl]` attribute will reject `Eq.refl`, and `MVarId.applyRefl`
will fail when applied to equality goals.
3. The duplication has been removed.
[Before](https://github.com/leanprover/lean4/files/14772220/oi.pdf) and
[after](https://github.com/leanprover/lean4/files/14772226/oi2.pdf).
This gets `ByteArray`, `String.Extra`, `ToString.Macro` and `RCases` out
of the imports of `omega`. I'd hoped to get `Array.Subarray` too, but
it's tangled up in the list literal syntax. Further progress could come
from make `split` use available `Decidable` instances, so we could pull
out `Classical` (and possibly some of `PropLemmas`).
I think this was in error in my original Mathlib implementation. We're
not interested in relations other than `=`, so there is no point uses
`MVarId.applyRfl`, which just looks up `@[refl]` tagged lemmas and tries
those.
In a separate PR, I will change `MVarId.applyRfl` so it has a flag to
control whether on `=` it should just hand-off to `MVarId.refl`, or
fail. Failure is appropriate in the version we call from the `rfl`
macro, to avoid doing a double `IsDefEq` check on every `rfl`!
This makes several changes to rw? and lazy discrimination trees based on
test failures in rewrite search.
Changes include:
1. Reverting to Mathlib function for candidate lemma priority in rw?
2. Introducing additional filters for auto-generated named in lazy
discriminator tree.
3. Refactoring lazy discriminator values to clarify what is stored.
4. Including star keys in calculation of match closeness in
prioritization.
5. Using more fields in current core context when initializing lazy
discriminator tree and avoiding max heartbeat issues.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
no need to enter `derive_functional_induction` anymore.
(Will remove the support for `derive_functional_induction` after the
next stage0 update, since we are already using it in Init.)
fixes#3770
Also start `rfl` with a `fail` message that is hopefully more helpful
than what we get now (see updated test output). This would be a cheaper
way to address #3302 without changing the implementation of rfl (as
tried in #3714).
This extends `derive_functional_induction` to work with structural
recursion as well.
It produces the less general, more concrete induction rule where the
induction hypothesis is
specialized for every argument of the recursive call, not just the the
one that the function
is recursing on.
Care is taken so that the induction principle and it's motive take the
arguments in the same
order as the original function.
While I was it, also makes sure that the order of the cases in the
induction principle matches
the order of recursive calls in the function better.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
This shortens `Array.findIdx?` code, by using termination_by (and
well-founded recursion) instead of a structural recursion trick, with
the intent to make it more proof friendly.
One motivation is that it makes it easier to write a proof that
`Array.findIdx?` and `List.findIdx?` are equivalent. Furthermore, this
will be useful to prove that more complex functions are equivalent.
Closes#3646
System.FilePath.parent did not return the correct parent path in the
case of absolute file paths
Example of previous behavior
```
(FilePath.mk "/foo").parent -> some (FilePath.mk "")
(System.FilePath.mk "/").parent -> some (FilePath.mk "")
```
The new behavior is based on rust's std::path::Path::parent function (as
previously described in comment in System.FilePath)
Example of updated behavior
```
(System.FilePath.mk "/foo").parent -> some (FilePath.mk "/")
(System.FilePath.mk "/").parent -> none
```
Behavior for relative file paths is unchanged
Closes#3618
Given a definition `foo`, they were previously called `foo._unfold`
until 4.7.0. We tried to rename them to `foo.def`, but it created too
many issues in the Mathlib repo. We decided to rename it again to
`foo.eq_def`. The new name is also consistent with the `eq_<idx>`
theorems generated for different "cases". That is, `foo.eq_def` is the
equality theorem for the whole definition, and `foo.eq_<idx>` is the
equality theorem for case `<idx>`.
cc @semorrison
`FileMap.lines` is an array that seems to be manually managed to have
the form `#[1, 2, ..., n-1, n-1]` with same length as
`FileMap.positions`. Remove this structure field in favour of
calculating the line number as `min(x+1, positions.size-1)` when needed.
Follow-up on #3221
Given
```lean
structure A where
x : Nat
structure B extends A where
y : Nat
```
rather than pretty printing `{ x := 1, y := 2 : B }` as `{ toA := { x :=
1 }, y := 2 }`, it now pretty prints as `{ x := 1, y := 2 }`.
The option `pp.structureInstances.flatten` controls whether to flatten
structure instances like this.
This updates the rw? tactic from Mathlib to use lazy discriminator trees
and upstreams it.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sets the default value to `pp.fieldNotation.generalized` to `true`.
Updates tests, and fixes some minor flaws in the implementation of the
generalized field notation pretty printer.
Now generalized field notation won't be used for any function that has a
`motive` argument. This is intended to prevent recursors from pretty
printing using it as (1) recursors are more like control flow structures
than actual functions and (2) generalized field notation tends to cause
elaboration problems for recursors.
Note: be sure functions that have an `@[app_unexpander]` use
`@[pp_nodot]` if applicable. For example, `List.toArray` needs
`@[pp_nodot]` to ensure the unexpander prints it using `#[...]`
notation.
The concrete dependency that is stale isn't really actionable
information for users (ideally we'd like something like "amount of
dependencies that will be rebuilt when you restart file"). This also
makes the diagnostic an "information" diagnostic so that non-infoview
users can still see it.
Since we are moving away from using notifications for stale dependency
information, we don't need to provide an ID anymore, either.
Refactors app delaborator, merging in the projection delaborator, to
support pretty printing with generalized field notation.
Renames option `pp.structureProjections` to `pp.fieldNotation` and adds
sub-option `pp.fieldNotation.generalized` to enable/disable generalized
field notation. Adds `@[pp_nodot]` attribute to permanently disable
using field notation for a given declaration.
For now, the default value of `pp.fieldNotation.generalized` is false
since we need a stage0 update to add `@[pp_nodot]` to some core
definitions (such as `List.toArray`) before updating the tests.
[Zulip
discussion](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60pp.2EgeneralizedFieldNotation.60/near/425856054)
This attribute, which was implemented in #3640, is applied to the
following structures: `Sigma`, `PSigma`, `PProd`, `And`, `Subtype`, and
`Fin`. These were given this attribute in Lean 3.
This coercion caused difficult-to-diagnose bugs sometimes. Because there
are some situations where converting a string to a name should be done
by parsing the string, and others where it should not, an explicit
choice seems better here.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
I forgot to use the sticky diagnostics in `getInteractiveDiagnostics` in
#3247, leading to them not consistently showing up in the "Messages"
panel of the InfoView.
This lead to incorrect diagnostic spans in the editor and resulted in
header errors that did not show up under "Messages" everywhere in the
file because the `fullRange?` property was missing.
Also changes the "Import out of date" warning diagnostic severity to
"Hint" so that it doesn't show up in the "Problems" view.
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>
Closes#3706
This derive handler's implementation is very similar to `BEq`'s, which
already ignores unused alternative so as to work correctly on indexed
inductive types. This PR simply implements the same solution as the one
present in
[`BEq.lean`](2c15cdda04/src/Lean/Elab/Deriving/BEq.lean (L94)).
After some tests, it doesn't seem like any other derive handler present
in Core suffers from the same issue (though some handlers don't work on
indexed inductives for other reasons).
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
These are used in Mathlib's `congr!` and `convert` tactics, which will
be upstreamed soon.
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
- Removes the public definitions `Array.eraseIdxAux` and
`Array.eraseIdxSzAux` which were implementation details.
- Motivation: `Array.eraseIdxAux` and `Array.eraseIdxSzAux` were clearly
not intended to remain public, but simply making them private would make
it inconvenient to unfold them when writing proofs in Std.
- Adds documentation comments to the public `Array.eraseIdx`-related
definitions which remain.
- Removes `Array.eraseIdx'` which was just `Array.feraseIdx` wrapped in
a subtype and adds `Array.size_feraseIdx` to prove the subtype property
as a standalone theorem.
Co-Authored-By: Daniel Windham <daniel@atlascomputing.org>
Previously, if there was a `nightly-testing-YYYY-MM-DD` tag at Std, but
not Mathlib, we were erroneously proceeding with Mathlib CI, and hence
using a probably-broken version of Mathlib.
using the `substVars` tactic on the goal can remove too much
information, as it does not take into account that the `motive` may
depend on the fixed parameters.
This is fixed by etracting `substVar` from `subst` which expects the
`x`, not the `h : x = rhs`, and then using this tactic on the local
declarations _after_ the `motive` exclusively.
a common pattern for recursive functions is
```
def countUp (n i acc : Nat) : Nat :=
if i < n then
countUp n (i+1) (acc + i)
else
acc
```
where we increase a value `i` until it hits an upper bound. This is
particularly common with array processing functions:
```
$ git grep 'termination_by.*size.*-' src/|wc -l
26
```
GuessLex now recognizes this pattern. The general approach is:
For every recursive call, check if the context contains hypotheses of
the form `e₁ < e₂` (or similar comparisions), and then consider `e₂ -
e₁` as a termination argument.
Currently, this only fires when `e₁` and `e₂` only depend on the
functions parameters, but not local let-bindings or variables bound in
local pattern matches.
Duplicates are removed.
In the table showing the termination argument failures, long termination
arguments are now given a number and abbreviated as e.g. `#4` in the
table headers.
More examples in the test file, here as some highlights:
```
def distinct (xs : Array Nat) : Bool :=
let rec loop (i j : Nat) : Bool :=
if _ : i < xs.size then
if _ : j < i then
if xs[j] = xs[i] then
false
else
loop i (j+1)
else
loop (i+1) 0
else
true
loop 0 0
```
infers
```
termination_by (Array.size xs - i, i - j)
```
and the weird functions where `i` goes up or down
```
def weird (xs : Array Nat) (i : Nat) : Bool :=
if _ : i < xs.size then
if _ : 0 < i then
if xs[i] = 42 then
weird xs.pop (i - 1)
else
weird xs (i+1)
else
weird xs (i+1)
else
true
decreasing_by all_goals simp_wf; omega
```
infers
```
termination_by (Array.size xs - i, i)
```
but unfortunately needs `decreasing_by` pending the “big
decreasing_tactic refactor” that
I expect we’ll want to do at some point.
this refactor prepares GuessLex to be able to infer more complex
termination arguments.
As a side-effect it fixes an (obscure) bug where `sizeOf` would be
applied to a term of the wrong type and thus a wrong `SizeOf` instance
could be inferred.
On Windows, we now compile all core `.o`s twice, once with and without
`dllexport`, for use in the shipped dynamic and static libraries,
respectively. On other platforms, we export always as before to avoid
the duplicate work.
---------
Co-authored-by: tydeu <tydeu@hatpress.net>
This reverts commit 4e3a8468c3 for PR
#3619. It looks like the CI in that commit didn't inform me that a test
was broken by the PR, so I managed to commit it despite the broken test.
- Add support for reserved declaration names. We use them for theorems
generated on demand.
- Equation theorems are not private declarations anymore.
- Generate equation theorems on demand when resolving symbols.
- Prevent users from creating declarations using reserved names. Users
can bypass it using meta-programming.
See next test for examples.
Before, the termination argument as inferred by `GuessLex` was passed
further
on as `Syntax`, to be elaborated later in `WF.Rel`.
This didn’t feel quite right anymore. In particular if we want to teach
`GuessLex` about guessing more complex termination arguments like
`xs.size -
i`, using `Expr` here is more natural.
So this introduces `TerminationArgument` based on an `Expr` to be used
here.
A side-effect of how the termination arguments are elaborated is that
the unused
variables linter will now look at `termination_by` variables, and that
parameters
past the colon are not even invisibly in scope, so `‹_›` will not find
them
See https://github.com/leanprover-community/mathlib4/pull/11370/files
for examples
of fixing these changes.
This PR fixes an issue where the file worker would not provide the
client with semantic tokens until the file had been elaborated
completely. The file worker now also tells the client to refresh its
semantic tokens after running "Restart File". This PR is based on #3271.
Fixes#1170.
This PR adds the module name to `RefIdent` in order to distinguish
conflicting names from different files. This also fixes related issues
in find-references or the call hierarchy feature.
It also adds some docstrings and stylistically refactors a bunch of
code.
This PR adds support for requests from the server to the client in the
language server. It is based on #3014 and was developed during an
experiment for #3247 that unfortunately did not go anywhere.
This replaces a few uses of initialize with builtin_initialize, and
removes some unneeded functionality added when it was unclear if lazy
discriminator trees would be efficient enough.
This introduces the `ArgsPacker` module and abstraction, to replace the
exising `PackDomain`/`PackMutual` code. The motivation was that we now
have more uses besides `Fix.lean` (`GuessLex` and `FunInd`), and the
code was spread in various places.
The goals are
* consistent function naming withing the the `PSigma` handling, the
`PSum` handling, and the combined interface
* avoid taking a type apart just based on the `PSigma`/`PSum` nesting,
to be robust in case the user happens to be using `PSigma`/`PSum`
somewhere. Therefore, always pass an `arity` or `numFuncs` or `varNames`
around.
* keep all the `PSigma`/`PSum` encoding logic contained within one
module (`ArgsPacker`), and keep that module independent of its users (so
no `EqnInfos` visible here).
* pick good variable names when matching on a packed argument
* the unary function now is either called `fun1._unary` or
`fun1._mutual`, never `fun1._unary._mutual`.
This file has less heavy dependencies than `PackMutual` had, so build
parallelism is improved as well.
This makes trailing whitespace visible and protectes them against
trimming by the editor, by appending the symbol ⏎ to such a line (and
also to any line that ends with such a symbol, to avoid ambiguities in
the case the message already had that symbol).
(Only the code action output / docstring parsing is affected; the error
message as sent
to the InfoView is unaffected.)
Fixes#3571
Modifies `dsimpLocation'` (which implements `dsimp?`) to take a
`simprocs : SimprocsArray` argument, like `simpLocation` and
`dsimpLocation`. This ensures that the behavior of `dsimp` matches
`dsimp?`.
---
Closes#3653
Enables the combination of `noncomputable unsafe` to be used for
definitions. Outside of pure theory, `noncomputable` is also useful to
prevent Lean from compiling a definition which will be implemented with
external code later. Such definitions may also wish to be marked
`unsafe` if they perform morally impure or memory-unsafe functions.
this makes `termination_by?` even slicker.
The heuristics is agressive in the non-mutual case (will omit `sizeOf`
if the argument is non-dependent and the `WellFoundedRelation` relation
is via `sizeOfWFRel`.
In the mutual case we'd also have to check the arguments, as they line
up in the termination argument, have the same types. I did not bother at
this point; in the mutual case we omit `sizeOf` only if the argument
type is `Nat`.
As a drive-by fix, `termination_by?` now also works on functions that
have only one plausible measure.
This is a temporary workaround for a limitation on Windows shared
libraries. We are getting errors of the form:
```
ld.lld: error: too many exported symbols (got 65572, max 65535)
```
Replaces `@[eliminator]` with two attributes `@[induction_eliminator]`
and `@[cases_eliminator]` for defining custom eliminators for the
`induction` and `cases` tactics, respectively.
Adds `Nat.recAux` and `Nat.casesAuxOn`, which are eliminators that are
defeq to `Nat.rec` and `Nat.casesOn`, but these use `0` and `n + 1`
rather than `Nat.zero` and `Nat.succ n`.
For example, using `induction` to prove that the factorial function is
positive now has the following goal states (thanks also to #3616 for the
goal state after unfolding).
```lean
example : 0 < fact x := by
induction x with
| zero => decide
| succ x ih =>
/-
x : Nat
ih : 0 < fact x
⊢ 0 < fact (x + 1)
-/
unfold fact
/-
...
⊢ 0 < (x + 1) * fact x
-/
simpa using ih
```
Thanks to @adamtopaz for initial work on splitting the `@[eliminator]`
attribute.
Floris van Doorn [reported on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/have.20tactic.20error.20recovery/near/425283053)
that it is confusing that the `have : T := e` tactic completely fails if
the body `e` is not of type `T`. This is in contrast to `have : T := by
exact e`, which does not completely fail when `e` is not of type `T`.
This ends up being caused by `elabTermEnsuringType` throwing an error
when it fails to insert a coercion. Now, it detects this case, and it
checks the `errToSorry` flag to decide whether to throw the error or to
log the error and insert a `sorry`.
This is justified by `elabTermEnsuringType` being a frontend to
`elabTerm`, which inserts `sorry` on error.
An alternative would be to make `ensureType` respect `errToSorry`, but
there exists code that expects being able to catch when `ensureType`
fails. Making such code manipulate `errToSorry` seems error prone, and
this function is not a main entry point to the term elaborator, unlike
`elabTermEnsuringType`.
Remark: this commit removes the `jason1.lean` test. Motivation: It
breaks all the time due to changes we make, and it is not clear anymore
what it is testing.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This migrates lemmas about Nat `compare`, `min`, `max`, `dvd`, `gcd`,
`lcm` and `div`/`mod` from Std to Lean itself.
Std still has some additional recursors, `CoPrime` and a few additional
definitions that might merit further discussion prior to upstreaming.
If the `LEAN_GITHASH` environment variable is set, Lake will now use it
instead of the detected Lean's githash when computing traces for builds
and the elaborated Lake configuration. This override allows one to
replace the Lean version used by a library
(e.g., Mathlib) without completely rebuilding it, which is useful for
testing custom builds of Lean.
The `delabConstWithSignature` delaborator is responsible for pretty
printing constants with a declaration-like signature, with binders, a
colon, and a type. This is used by the `#check` command when it is given
just an identifier.
It used to accumulate binders from pi types indiscriminately, but this
led to unfriendly behavior. For example, `#check String.append` would
give
```
String.append (a✝ : String) (a✝¹ : String) : String
```
with inaccessible names. These appear because `String.append` is defined
using patterns, so it never names these parameters.
Now the delaborator stops accumulating binders once it reaches an
inaccessible name, and for example `#check String.append` now gives
```
String.append : String → String → String
```
We do not synthesize names for the sake of enabling binder syntax
because the binder names are part of the API of a function — one can use
`(arg := ...)` syntax to pass arguments by name. The delaborator also
now stops accumulating binders once it reaches a parameter with a name
already seen before — we then rely on the main delaborator to provide
that parameter with a fresh name when pretty printing the pi type.
As a special case, instance parameters with inaccessible names are
included as binders, pretty printing like `[LT α]`, rather than
relegating them (and all the remaining parameters) to after the colon.
It would be more accurate to pretty print this as `[inst✝ : LT α]`, but
we make the simplifying assumption that such instance parameters are
generally used via typeclass inference. Likely `inst✝` would not
directly appear in pretty printer output, and even if it appears in a
hover, users can likely figure out what is going on. (We may consider
making such `inst✝` variables pretty print as `‹LT α›` or
`infer_instance` in the future, to make this more consistent.)
Something we note here is that we do not do anything to make sure
parameters that can be used as named arguments actually appear named
after the colon (nor do we assure that the names are the correct names).
For example, one sees `foo : String → String → String` rather than `foo
: String → (baz : String) → String`. We can investigate this later if it
is wanted.
We also give `delabConstWithSignature` a `universes` flag to enable
turning off pretty printing universe levels parameters.
Closes#2846
this makes the ugly `fst`/`snd` variable names in the functional
induction principles go away.
Ironically I thought in order to fix these name, I should touch the
mutual/n-ary argument packing code used for well-founded recursion, and
embarked on a big refactor/rewrite of that code, only to find that at
least this particular instance of the issue was somewhere else. Hence
breaking this into its own PR; the refactoring will follow (and will
also improve some other variable names.)
closes#3022
With this commit, given the declaration
```
def foo : Nat → Nat
| 0 => 2
| n + 1 => foo n
```
when we unfold `foo (n+1)`, we now obtain `foo n` instead of `foo
(Nat.add n 0)`.
This fixes an issue discovered in Mathlib with the meta cache being
poisoned by using a name generator. It is difficult to reproduce due to
the name collisions being rare, but here is a minimal module with
definitions that result in an error:
```lean
prelude
universe u
inductive Unit2 : Type where
| unit : Unit2
inductive Eq2 {α : Sort u} : α → α → Prop where
| refl (a : α) : Eq2 a a
structure Subtype2 {α : Sort u} (p : α → Prop) where
val : α
def End (α) := α → α
theorem end_app_eq (α : Type u) (f : End α) (a : α) : Eq2 (f a) (f a) := Eq2.refl _
theorem Set.coe_eq_subtype {α : Type u} (s : α → Prop) : Eq2 (Subtype2 s) (Subtype2 s) := Eq2.refl _
def succAboveCases {_ : Unit2} {α : Unit2 → Sort u} (i : Unit2) (v : α i) : α i := v
theorem succAbove_cases_eq_insertNth : Eq2 @succAboveCases.{u + 1} @succAboveCases.{u + 1} := Eq2.refl _
```
Removing any of thee last 5 definitions avoids the error. Testing
against Mathlib shows this PR fixes the issue.
This bug is the real cause of leanprover/vscode-lean4#392.
At the end of a tactic state, the client calls
`getInteractiveDiagnostics` with a range `[last line of proof, last line
of proof + 1)`. The `fullRange` span of the `unresolved goals` error
however is something like `[(first line of proof, start character),
(last line of proof, nonzero end character)).
Since it operates on line numbers, `getInteractiveDiagnostics` would
then check whether `[last line of proof, last line of proof + 1)` and
`[first line of proof, last line of proof)` intersect, which is false
because of the excluded upper bound on the latter interval, despite the
fact that the end character in the last line may be nonzero.
This fix adjusts the intersection logic to use `[first line of proof,
last line of proof]` if the end character is nonzero.
Closesleanprover/vscode-lean4#392.
This PR enables import auto-completion to complete partial words in
imports.
Other inconsistencies that I've found in import completion already seem
to be fixed by #3014. Since it will be merged soon, there is no need to
invest time to fix these issues on master.
This adds the concept of **functional induction** to lean.
Derived from the definition of a (possibly mutually) recursive function,
a **functional
induction principle** is tailored to proofs about that function. For
example from:
```
def ackermann : Nat → Nat → Nat
| 0, m => m + 1
| n+1, 0 => ackermann n 1
| n+1, m+1 => ackermann n (ackermann (n + 1) m)
derive_functional_induction ackermann
```
we get
```
ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
(case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
(case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m))
(x x : Nat) : motive x x
```
At the moment, the user has to ask for the functional induction
principle explicitly using
```
derive_functional_induction ackermann
```
The module docstring of `Lean/Meta/Tactic/FunInd.lean` contains more
details on the
design and implementation of this command.
More convenience around this (e.g. a `functional induction` tactic) will
follow eventually.
This PR includes a bunch of `PSum`/`PSigma` related functions in the
`Lean.Tactic.FunInd`
namespace. I plan to move these to `PackArgs`/`PackMutual` afterwards,
and do some cleaning
up as I do that.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
This is still WIP: the checklist for release candidates will get
finished as I do the release of `v4.7.0-rc1`.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
This adds a number of lemmas for simplification of `Bool` and `Prop`
terms. It pulls lemmas from Mathlib and adds additional lemmas where
confluence or consistency suggested they are needed.
It has been tested against Mathlib using some automated test
infrastructure.
That testing module is not yet included in this PR, but will be included
as part of this.
Note. There are currently some comments saying the origin of the simp
rule. These will be removed prior to merging, but are added to clarify
where the rule came from during review.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Proves
`Nat.mod_mul : x % (a * b) = x % a + a * (x / a % b)` and
`Nat.mod_pow_succ : x % b ^ (k + 1) = x % b ^ k + b ^ k * ((x / b ^ k) %
b)`, helpful for bitblasting.
We use `let_delayed` to elaborate `match_expr` join points, which
elaborate the body of the `let` before its value. Thus, there is a
difference between:
- `let_delayed f (x : Expr) := <val>; <body>`
- `let_delayed f := fun (x : Expr) => <val>; <body>`
In the latter, when `<body>` is elaborated, the elaborator does not know
that `f` takes an argument of type `Expr`, and that `f` is a function.
Before this commit ensures the former representation is used.
In v4.6.0, there was a significant regression in initial server startup
performance because the .ilean files got bigger in #3082 and we load the
information stored in all .ilean files synchronously when the server
starts up.
This PR makes this loading asynchronous. The trade-off is that requests
that are issued right after the initial server start when the references
are not fully loaded yet may yield incomplete results.
Benchmark for this in a separate PR soon after this one.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Else the `case` will now allow introducing all necessary variables.
Induction principles with `let` in the types of the cases will be more
common with #3432.
This implementation no longer reduces the type as it goes, but really
only counts
manifest foralls and lets. I find this more sensible and predictable: If
you have
```
theorem induction₂_symm {P : EReal → EReal → Prop} (symm : Symmetric P) …
```
then previously, writing
```
case symm =>
```
would actually bring a fresh `x` and `y` and variable `h : P x y` into
scope and produce a
goal of `P y x`, because `Symmetric P` happens to be
```
def Symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x
```
After this change, after `case symm =>` will leave `Symmetric P` as the
goal.
This gives more control to the author of the induction hypothesis about
the actual
goal of the cases. This shows up in mathlib in two places; fixes in
https://github.com/leanprover-community/mathlib4/pull/11023.
I consider these improvements.
the user can now write `termination_by?` to see the termination argument
inferred by GuessLex, and turn it into `termination_by …` using the “Try
this” widget or a code action.
To be done later, maybe: Avoid writing `sizeOf` if it's not necessary.
When editing core Lean, the `pp.proofs` feature causes goal states to fail to display in the Infoview, instead showing only "error when printing message: unknown constant '«term⋯»'". This PR moves the `⋯` syntax from Init.NotationExtra to Lean.Elab.BuiltinTerm
It also makes it so that `⋯` elaborates as `_` while logging a warning, rather than throwing an error, which should be somewhat more friendly when copy/pasting from the Infoview.
Closes#3476
When using `set_option tactic.skipAssignedInstances false`, `simp` and
`rw` will synthesize instance implicit arguments even if they have
assigned by unification. If the synthesized argument does not match the
assigned one the rewrite is not performed. This option has been added
for backward compatibility.
```
example (a : Nat) :
(((a + (2 ^ 64 - 1)) % 2 ^ 64 + 1) * 8 - 1 - (a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + 1) = 8 := by
omega
```
used to time out, and now is fast.
(We will probably make separate changes later so the defeq checks would
be fast in any case here.)
During the switch to `.lake`, I overlooked updating the paths in
`LakeInstall`. This fixes that and helps prevent further mistakes by
using the same default definitions as the package configuration itself.
The `decide` tactic produces error messages that users find to be
obscure. Now:
1. If the `Decidable` instance reduces to `isFalse`, it reports that
`decide` failed because the proposition is false.
2. If the `Decidable` instance fails to reduce, it explains what
proposition it failed for, and it shows the reduced `Decidable` instance
rather than the `Decidable.decide` expression. That expression tends to
be less useful since it shows the unreduced `Decidable` argument (plus
it's a lot longer!)
Examples:
```lean
example : 1 ≠ 1 := by decide
/-
tactic 'decide' proved that the proposition
1 ≠ 1
is false
-/
opaque unknownProp : Prop
open scoped Classical in
example : unknownProp := by decide
/-
tactic 'decide' failed for proposition
unknownProp
since its 'Decidable' instance reduced to
Classical.choice ⋯
rather than to the 'isTrue' constructor.
-/
```
When reporting the error, `decide` only shows the whnf of the
`Decidable` instance. In the future we could consider having it reduce
all decidable instances present in the term, which can help with
determining the cause of failure (this was explored in
8cede580690faa5ce18683f168838b08b372bacb).
The elaboration function `Lean.Meta.coerceMonadLift?` inserts these
coercion helper functions into a term and tries to unfolded them with
`expandCoe`, but because that function only unfolds up to
reducible-and-instance transparency, these functions were not being
unfolded. The fix here is to give them the `@[reducible]` attribute.
with this, more functions will be proven terminating automatically,
namely those where after `simp_wf`, lexicographic order handling,
possibly `subst_vars` the remaining goal can be solved by `omega`.
Note that `simp_wf` already does simplification of the goal, so
this adds `omega`, not `(try simp) <;> omega` here.
There are certainly cases where `(try simp) <;> omega` will solve more
goals (e.g. due to the `subst_vars` in `decreasing_with`), and
`(try simp at *) <;> omega` even more. This PR errs on the side of
taking
smaller steps.
Just appending `<;> omega` to the existing
`simp (config := { arith := true, failIfUnchanged := false })` call
doesn’t work nicely, as that leaves forms like `Nat.sub` in the goal
that
`omega` does not seem to recognize.
This does *not* remove any of the existing ad-hoc `decreasing_trivial`
rules based on `apply` and `assumption`, to not regress over the status
quo (these rules may apply in cases where `omega` wouldn't “see”
everything, but `apply` due to defeq works).
Additionally, just extending makes bootstrapping easier; early in `Init`
where
`omega` does not work yet these other tactics can still be used.
(Using a single `omega`-based tactic was tried in #3478 but isn’t quite
possible yet, and will be postponed until we have better automation
including forward reasoning.)
with this, hopefully more obvious array accesses will be handled
automatically.
Just like #3503, this PR does not investiate which of the exitsting
tactics in `get_elem_tactic_trivial` are subsumed now and could be
dropped without (too much) breakage.
Before, app unexpanders would only be applied to entire applications.
However, some notations produce functions, and these functions can be
given additional arguments. The solution so far has been to write app
unexpanders so that they can take an arbitrary number of additional
arguments. However, as reported in [this Zulip
thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/pretty.20printer.20bug/near/420662236),
this leads to misleading hover information in the Infoview. For example,
while `HAdd.hAdd f g 1` pretty prints as `(f + g) 1`, hovering over `f +
g` shows `f`. There is no way to fix the situation from within an app
unexpander; the expression position for `HAdd.hAdd f g` is absent, and
app unexpanders cannot register TermInfo.
This commit changes the app delaborator to try running app unexpanders
on every prefix of an application, from longest to shortest prefix. For
efficiency, it is careful to only try this when app delaborators do in
fact exist for the head constant, and it also ensures arguments are only
delaborated once. Then, in `(f + g) 1`, the `f + g` gets TermInfo
registered for that subexpression, making it properly hoverable.
The app delaborator is also refactored, and there are some bug fixes:
- app unexpanders only run when `pp.explicit` is false
- trailing parameters in under-applied applications are now only
considered up to reducible & instance transparency, which lets, for
example, optional arguments for `IO`-valued functions to be omitted.
(`IO` is a reader monad, so it's hiding a pi type)
- app unexpanders will no longer run for delaborators that use
`withOverApp`
- auto parameters now always pretty print, since we are not verifying
that the provided argument equals the result of evaluating the tactic
Furthermore, the `notation` command has been modified to generate an app
unexpander that relies on the app delaborator's new behavior.
The change to app unexpanders is reverse-compatible, but it's
recommended to update `@[app_unexpander]`s in downstream projects so
that they no longer handle overapplication themselves.
If Lake fails to download a cloud release, it will now print a warning
indicating that it is falling back to a local build. For example:
```
[0/2] Downloading cloud_test cloud release
[0/2] Building CloudTest
error: > curl -s -f -o [...] -L [...]
error: external command `curl` exited with code 22
warning: fetching cloud release failed; falling back to local build
```
This PR addresses several performance issues in the auto-completion
implementation. It also fixes a number of smaller bugs related to
auto-completion.
In a file with `import Mathlib`, the performance of various kinds of
completions has improved as follows:
- Completing `C`: 49000ms -> 1400ms
- Completing `Cat`: 14300ms -> 1000ms
- Completing `x.` for `x : Nat`: 3700ms -> 220ms
- Completing `.` for an expected type of `Nat`: 11000ms -> 180ms
The following bugs have been fixed as well:
- VS Code never used our custom completion order. Now, the server fuzzy
completion score decides the order that completions appear in.
- Dot auto-completion for private types did not work at all. It does
now.
- Completing `.<identifier>` (where the expected type is used to infer
the namespace) did not filter by the expected type and instead displayed
all matching constants in the respective namespace. Now, it uses the
expected type for filtering. Note that this is not perfect because
sub-namespaces are technically correct completions as well (e.g.
`.Foo.foobar`). Implementing this is future work.
- Completing `.` was often not possible at all. Now, as long as the `.`
is not used in a bracket (where it may be used for the anonymous lambda
feature, e.g. `(. + 1)`), it triggers the correct completion.
- Fixes#3228.
- The auto-completion in `#check` commands would always try to complete
identifiers using the full declaration name (including namespaces) if it
could be resolved. Now it simply uses the identifier itself in case
users want to complete this identifier to another identifier.
## Details
Regarding completion performance, I have more ideas on how to improve it
further in the future.
Other changes:
- The feature that completions with a matching expected type are sorted
to the top of the server-side ordering was removed. This was never
enabled in VS Code because it would use its own completion item order
and when testing it I found it to be more confusing than useful.
- In the server-side ordering, we would always display keywords at the
top of the list. They are now displayed according to their fuzzy match
score as well.
The following approaches have been used to improve performance:
- Pretty-printing the type for every single completion made up a
significant amount of the time needed to compute the completions. We now
do not pretty-print the type for every single completion that is offered
to the user anymore. Instead, the language server now supports
`completionItem/resolve` requests to compute the type lazily when the
user selects a completion item.
- Note that we need to keep the amount of properties that we compute in
a resolve request to a minimum. When the server receives the resolve
request, the document state may have changed from the state it was in
when the initial auto-completion request was received. LSP doesn't tell
us when it will stop sending resolve requests, so we cannot keep this
state around, as we would have to keep it around forever.
LSP's solution for this dilemma is to have servers send all the state
they need to compute a response to a resolve request to the client as
part of the initial auto completion response (which then sends it back
as part of the resolve request), but this is clearly infeasible for all
real language servers where the amount of state needed to resolve a
request is massive.
This means that the only practical solution is to use the current state
to compute a response to the resolve request, which may yield an
incorrect result. This scenario can especially occur when using
LiveShare where the document is edited by another person while cycling
through available completions.
- Request handlers can now specify a "header caching handler" that is
called after elaborating the header of a file. Request handlers can use
this caching handler to compute caches for information stored in the
header. The auto-completion uses this to pre-compute non-blacklisted
imported declarations, which in turn allow us to iterate only over
non-blacklisted imported declarations where we would before iterate over
all declarations in the environment. This is significant because
blacklisted declarations make up about 4/5 of all declarations.
- Dot completion now looks up names modulo private prefixes to figure
out whether a declaration is in the namespace of the type to the left of
the dot instead of first stripping the private prefix from the name and
then comparing it. This has the benefit that we do not need to scan the
full name in most cases.
This PR also adds a couple of regression tests for fixed bugs, but *no
benchmarks*. We will add these in the future when we add proper support
for benchmarking server interaction sessions to our benchmarking
architecture.
All tests that were broken by producing different completion output
(empty `detail` field, added `sortText?` and `data?` fields) have been
manually checked by me to be still correct before replacing their
expected output.
This is still a draft PR, but includes the core exact? and apply?
tactics.
Still need to convert to builtin syntax and test on Std.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
The current `ToExpr Int` instance produces `@Int.ofNat (@OfNat.ofNat Nat
i ...)` for nonnegative `i` and `@Int.negSucc (@OfNat.ofNat Nat (-i+1)
...)` for negative `i`.
However it should be producing `@OfNat.ofNat Int i ...` for nonnegative
`i`, and `@Neg.neg ... (@OfNat.ofNat Int (-i) ...)` for negative `i`.
Make `x.toNat * 2 + b.toNat` the simp normal form of `(concat x
b).toNat`.
The choice for multiplication and addition was inspired by `Nat.bit_val`
from Mathlib.
Also, because we have considerably more lemmas about multiplication and
`_ + 1` than about shifts and `_ ||| 1`.
This is very helpful when dealing with bitvectors, where a case analysis
on the bitwidth leaves one with hypotheses of the form `x<2^(Nat.succ
w)`.
Design decisions I am unsure about:
- Is creating a helper `succ?` the correct way to match on the exponent
`e+1`?
- I'm not certain why the prior call to `Int.ofNat_pow` also checked
that the exponent was a ground natural. I removed this, since we now
explicitly handle cases where the exponent is a term of the form `e+1`.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Joe Hendrix <joe@lean-fro.org>
Co-authored-by: Alex Keizer <alex@keizer.dev>
First (baby)-step to a `concat`-based `bitblast`: a characterization of
`concat` in terms of `getLsb`.
The proof might benefit slightly from a `toNat_concat` lemma, but I
wasn't sure what the normal form there should be, so I avoided it.
---------
Co-authored-by: Scott Morrison <scott@tqft.net>
Every usage of `carry` followed the pattern: `carry _ x.toNat y.toNat`,
so we've refactorod `carry` to take the `BitVec`s as arguments, and made
the `toNat` part of its definition.
PR #3432 will introduce more operations on `MatcherApp`, including somet
that have more dependencies.
This change prepares by introducing `Lean.Meta.Match.MatcherApp.Basic`
for the basic definition, and `Lean.Meta.MatcherApp.Transform` for the
transformations, currently `addArg` and `refineThrough`, but more to
come.
This PR is an effort to improve reasoning at the Nat level about
bitvectors and reduce of Fin and Nat.
It slightly tightens some proofs, but is generally aimed at reducing
inconsistencies between definitions at the Nat and Fin types in favor of
more consistently using Nat operations.
This ports leanprover/std4#664 to Lean core.
Here was the rational I provided in the discussion for
leanprover/std4#664:
It's mostly about consistency. If we use the same types and style in
definitions and proofs, there is less surprise when unfolding or
otherwise using definitions. We use some Nat based operations that
haven't been extended to Fin such as the bitwise operations, and I don't
want to pay the overhead of introducing a Fin version of every Bitvector
operation.
So this basically means Nat is preferred.
One argument potentially in favor of Fin is that we could reuse results
proven there, but that doesn't really seem to be the case so far.
A second argument is that we want to simplify expression to use more
canonical forms and we currently can pretty-print those operations
better using ofNat than ofFin. We could define the notations using ofFin
of course though, but that's additional operators that will show up in
expressions.
Adds a simple error-recovery mechanism to Lean's parser, similar to
those used in other combinator parsing libraries.
Lean itself isn't very amenable to error recovery with this mechanism,
as it requires global knowledge of the grammar in question to write
recovery rules that don't break backtracking or `<|>`. I only found a
few opportunities.
But for DSLs, this is really important. In particular, Verso parse
errors interacted very badly with Lean parse errors in a way that
required frequent "restart file" commands, but this mechanism allows me
to both recover from Verso parse errors and to have Lean skip the rest
of the file rather than repeatedly trying to parse it as Lean commands.
#3408 was somewhat large and didn't properly test the symm and label
attribute code after edits to the builtin versions.
This migrates the code for generating labeled attributes from Init back
to Lean so that the required definitions are in scope.
This also addresses a mistake in the symm elaborator that prevented symm
without location information from elaborating.
Both fixes have been tested on the Std test suite and successfully
passed.
Adds documentation to the `String.Iterator` API, mentored by
@eric-wieser and @david-christiansen
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
This is a quite substantial tactic.
It also includes the infamour `NatCast` typeclass (which I've equipped
with a module-doc). I wasn't at all sure where that should live, so it
is currently randomly in `Lean/Elan/Tactic/NatCast.lean`: presumably if
we're doing this it will go somewhere in `Init`.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
When updating Std, be careful that not every lemma has been upstreamed,
so we need to be careful to only delete things that have already been
declared.
Before the `zeta` / `zetaDelta` split, `dsimp` was performing `zeta`
by going inside of a `let`-expression, performing `zetaDelta`, and
then removing the unused `let`-expression.
Loose fvars are never supposed to be pretty printed, but having them
print with "fvar" in the name can help with debugging broken tactics and
elaborators.
Metaprogramming users often do not realize at first that `_uniq.???` in
pretty printing output refers to fvars not in the current local context.
in all uses of `CasesOnApp`, we treat `MatcherApp`s the same way,
dupliating a fair amount of relatively hairy code (and there is more to
come).
However, the `MatcherApp` abstraction is perfectly capable of
also representing `casesOn` applications, at least for the use cases
encountered so far.
So lets just (optionally) include `casesOn` applications when looking
for matchers,
and remove the `CasesOnApp` abstraction completely.
Incrementally unveil trace children for excessively large nodes to
improve infoview rendering time, adjust particularly chatty
`simp.ground` trace to make use of it.
Lake previously opened the configuration trace as read-write even if it
does not update the configuration. This meant it failed if the trace was
read-only. With this change, it now first acquires a read-only handle
and then, if and only if it determines the need for a reconfigure, does
it re-open the file with a read-write handle. Also, this change fixes a
potential deadlock (Lake will error instead) and generally clarifies the
trace locking code.
Fixes a bug with Lake cloud releases where a cloud release would produce
a different trace if the package was the root of the workspace versus a
dependency. Also, an explicit fetch of a cloud release (e.g., via `lake
build :release`) will now error out with a non-zero exit code if it
fails to find, download, and unpack a release.
Previously, `CasesOn.addArg?` would do that check inline, while
`MatcherApp.addArg?` would do it after the fact.
Now `MatcherApp.addArg?` uses the same idiom.
Also, makes both `addArg?` always fail if the argument was not refined.
The work on functional induction principles calls for more unification
between the handling of `CasesOnApp` and `MatcherApp`, so this is a step
in that direction.
This is pretty big PR that upstreams all of Std.Data.Int.Init in one go.
So far lemmas have seen minimal changes needed to adapt to Lean core
environment.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Changes the goal to `False`, retaining as much information as possible:
* If the goal is `False`, do nothing.
* If the goal is an implication or a function type, introduce the
argument and restart.
(In particular, if the goal is `x ≠ y`, introduce `x = y`.)
* Otherwise, for a propositional goal `P`, replace it with `¬ ¬ P`
(attempting to find a `Decidable` instance, but otherwise falling back
to working classically)
and introduce `¬ P`.
* For a non-propositional goal use `False.elim`.
`nat?` checks if an expression is a "natural number in normal form",
i.e. of the form `OfNat n`, where `n` matches `.lit (.natVal n)` for
some `n`.
and if so returns `n`.
This is a widely used helper function in Std/Mathlib when matching on
expressions.
I've reordered some definitions to keep things together. This
introduces:
```
/-- Return the function (name) and arguments of an application. -/
def getAppFnArgs (e : Expr) : Name × Array Expr :=
withApp e λ e a => (e.constName, a)
```
and
```
/-- If the expression is a constant, return that name. Otherwise return `Name.anonymous`. -/
def constName (e : Expr) : Name :=
e.constName?.getD Name.anonymous
```
This upstreams NatCast and IntCast alone independent of norm_cast in
#3322.
This will allow more efficiently upstreaming parts of Std.Data.Int
relevant for omega.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
By having the `pp.proofs` feature use `⋯` when omitting proofs, when
users copy/paste terms from the InfoView the elaborator can give an
error message explaining why the term cannot be elaborated.
Also adds `pp.proofs.threshold` option to allow users to pretty print
shallow proof terms. By default, only atomic proof terms are pretty
printed.
This adjustment was suggested in PR #3201, which added `⋯` and the
related `pp.deepTerms` option.
This makes it so that when `withOverApp` is handling overapplied
functions, the term produced by the supplied delaborator is hoverable in
the Infoview.
When projection functions are delaborated, intermediate parent
projections are no longer printed. For example, rather than pretty
printing as `o.toB.toA.x` with these `toB` and `toA` parent projections,
it pretty prints as `o.x`.
This feature is being upstreamed from mathlib.
This is not a complete upstreaming of that file (it also supports `∀ᵉ (x
< 2) (y < 3), p x y` as shorthand for `∀ x < 2, ∀ y < 3, p x y`, but I
don't think we need this; it is used in Mathlib).
Syntaxes still need to be made built-in.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
This causes problems when used in conjunction with `#guard_msgs` (which
checks whitespace) and trailing whitespace removal. Discovered by
@PatrickMassot in verbose-lean4.
Again co-developed with @bollu.
Based on top of: #3225
While hunting down the performance discrepancy on qsort.lean between C
and LLVM we noticed there was a single, trivially optimizeable, alloca
(LLVM's stack memory allocation instruction) that had load/stores in the
hot code path. We then found:
https://groups.google.com/g/llvm-dev/c/e90HiFcFF7Y.
TLDR: `mem2reg`, the pass responsible for getting rid of allocas if
possible, only triggers on an alloca if it is in the first BB. The
allocas of the current implementation get put right at the location
where they are needed -> they are ignored by mem2reg.
Thus we decided to add functionality that allows us to push all allocas
up into the first BB.
We initially wanted to write `buildPrologueAlloca` in a `withReader`
style so:
1. get the current position of the builder
2. jump to first BB and do the thing
3. revert position to the original
However the LLVM C API does not expose an option to obtain the current
position of an IR builder. Thus we ended up at the current
implementation which resets the builder position to the end of the BB
that the function was called from. This is valid because we never
operate anywhere but the end of the current BB in the LLVM emitter.
The numbers on the qsort benchmark got improved by the change as
expected, however we are not fully there yet:
```
C:
Benchmark 1: ./qsort.lean.out 400
Time (mean ± σ): 2.005 s ± 0.013 s [User: 1.996 s, System: 0.003 s]
Range (min … max): 1.993 s … 2.036 s 10 runs
LLVM before aligning the types
Benchmark 1: ./qsort.lean.out 400
Time (mean ± σ): 2.151 s ± 0.007 s [User: 2.146 s, System: 0.001 s]
Range (min … max): 2.142 s … 2.161 s 10 runs
LLVM after aligning the types
Benchmark 1: ./qsort.lean.out 400
Time (mean ± σ): 2.073 s ± 0.011 s [User: 2.067 s, System: 0.002 s]
Range (min … max): 2.060 s … 2.097 s 10 runs
LLVM after this
Benchmark 1: ./qsort.lean.out 400
Time (mean ± σ): 2.038 s ± 0.009 s [User: 2.032 s, System: 0.001 s]
Range (min … max): 2.027 s … 2.052 s 10 runs
```
Note: If you wish to merge this PR independently from its predecessor,
there is no technical dependency between the two, I'm merely stacking
them so we can see the performance impacts of each more clearly.
Debugged and authored in collaboration with @bollu.
This PR fixes several performance regressions of the LLVM backend
compared to the C backend
as described in #3192. We are now at the point where some benchmarks
from `tests/bench` achieve consistently equal and sometimes ever so
slightly better performance when using LLVM instead of C. However there
are still a few testcases where we are lacking behind ever so slightly.
The PR contains two changes:
1. Using the same types for `lean.h` runtime functions in the LLVM
backend as in `lean.h` it turns out that:
a) LLVM does not throw an error if we declare a function with a
different type than it actually has. This happened on multiple occasions
here, in particular when the function used `unsigned`, as it was
wrongfully assumed to be `size_t` sized.
b) Refuses to inline a function to the call site if such a type mismatch
occurs. This means that we did not inline important functionality such
as `lean_ctor_set` and were thus slowed down compared to the C backend
which did this correctly.
2. While developing this change we noticed that LLVM does treat the
following as invalid: Having a function declared with a certain type but
called with integers of a different type. However this will manifest in
completely nonsensical errors upon optimizing the bitcode file through
`leanc` such as:
```
error: Invalid record (Producer: 'LLVM15.0.7' Reader: 'LLVM 15.0.7')
```
Presumably because the generate .bc file is invalid in the first place.
Thus we added a call to `LLVMVerifyModule` before serializing the module
into a bitcode file. This ended producing the expected type errors from
LLVM an aborting the bitcode file generation as expected.
We manually checked each function in `lean.h` that is mentioned in
`EmitLLVM.lean` to make sure that all of their types align correctly
now.
Quick overview of the fast benchmarks as measured on my machine, 2 runs
of LLVM and 2 runs of C to get a feeling for how far the averages move:
- binarytrees: basically equal performance
- binarytrees.st: basically equal performance
- const_fold: equal if not slightly better for LLVM
- deriv: LLVM has 8% more instructions than C but same wall clock time
- liasolver: basically equal performance
- qsort: LLVM is slower by 7% instructions, 4% time. We have identified
why the generated code is slower (there is a store/load in a hot loop in
LLVM that is not in C) but not figured out why that happens/how to
address it.
- rbmap: LLVM has 3% less instructions and 13% less wall-clock time than
C (woop woop)
- rbmap_1 and rbmap_10 show similar behavior
- rbmap_fbip: LLVM has 2% more instructions but 2% better wall time
- rbmap_library: equal if not slightly better for LLVM
- unionfind: LLVM has 5% more instructions but 4% better wall time
Leaving out benchmarks related to the compiler itself as I was too lazy
to keep recompiling it from scratch until we are on a level with C.
Summing things up, it appears that LLVM has now caught up or surpassed
the C backend in the microbenchmarks for the most part. Next steps from
our side are:
- trying to win the qsort benchmark
- figuring out why/how LLVM runs more instructions for less wall-clock
time. My current guesses would be measurement noise and/or better use of
micro architecture?
- measuring the larger benchmarks as well
We previously had the syntax for `change` and `change at`, but no
implementation.
This moves Kyle's implementation from Std.
This also changes the `changeLocalDecl` function to push nodes to the
infotree about FVar aliases.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
A small fix to the `DiscrTree` documentation to reflect the fact that
implicit type arguments *are* indexed and do not become `star` or
`other`. The following is a reproduction:
```lean
import Lean
open Lean Meta Elab Tactic
elab "test_tac" t:term : tactic => do
Tactic.withMainContext do
let e ← Term.elabTerm t none
let a : DiscrTree Nat ← DiscrTree.empty.insert e 1 {}
logInfo m!"{a}"
example (α : Type) (ringAdd : Add α) : True := by
/- (Add.add => (node (Nat => (node (* => (node (0 => (node (1 => (node #[1])))))))))) -/
test_tac @Add.add Nat instAddNat 0 1
/- (Add.add => (node (_uniq.1154 => (node (* => (node (◾ => (node (◾ => (node #[1])))))))))) -/
test_tac @Add.add α ringAdd ?_ ?_
```
This moves the `rcases` and `obtain` tactics from Std, and makes them
built-in tactics.
We will separately move the test cases from Std after #3297
(`guard_expr`).
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
Moves the `@[coe]` attribute and associated elaborators/delaborators
from Std to Lean.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
The `push_cast` tactic in Std currently uses a copy-paste version of
`mkSimpContext` that allows overriding `getSimpTheorems`. However it has
been diverging from the version in Lean.
This is one way of generalizing `mkSimpContext` in Lean to allow what is
needed downstream., but I'm not at all set on this one. As far as I can
see there are no other tactics currently using this.
`push_cast` itself just replaces `getSimpTheorems` with
`pushCastExt.getTheorems`, where `pushCastExt` is a simp extension. If
there is another approach that suits that situation it would be fine.
I've tested that the change in this PR works downstream.
This is used in the "Try this:" widget machinery powering `simp?`.
There is a test file in Std, which I am not upstreaming at the same
time, as that relies on more code actions / #guard_msgs material. That
test file will still of course test things from Std, and later it can be
reunited with the code it is testing.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
These additional options are currently implemented in Std in a function
`Format.prettyExtra` (via `open private`), and used to implement the
`simp?` functionality.
This just adds the options to the core function.
This does not completely empty `Std.Lean.Name`, as working out how to
document the difference between `Name.isInternalDetail` and
`Name.isImplementationDetail` requires further thought.
The induction principle used by `induction` may have explicit parameters
that are
not motive, target or “real” alternatives (that have the `motive` as
conclusion), e.g. restrictions on the `motive` or other parameters.
Previously, `induction` would treat them as normal alternatives, and try
to re-introduce the automatically reverted hypotheses. But this only
works when the `motive` is actually the conclusion in the type of that
alternative.
We now pay attention to that, thread that information through, and only
revert when needed.
Fixes#3212.
This PR adds links to some folder references in the docs, making them
easier to navigate.
Please advise if these need to be made to be full URIs rather than
relative paths in order to work correctly with the doc generation
tooling that is in place.
Implements the pretty printer option `pp.numericTypes` for including a
type ascription for numeric literals. For example, `(2 : Nat)`, `(-2 :
Int)`, and `(-2 / 3 : Rat)`. This is useful for debugging how arithmetic
expressions have elaborated or have been otherwise transformed. For
example, with exponentiation is is helpful knowing whether it is `x ^ (2
: Nat)` or `x ^ (2 : Real)`. This is like the Lean 3 option
`pp.numeralTypes` but it has a wider notion of a numeric literal.
Also implements the pretty printer option `pp.natLit` for including the
`nat_lit` prefix for raw natural number literals.
Closes#3021
When we declare a `simp` set using `register_simp_attr`, we
automatically create `simproc` set. However, users may create `simp`
sets programmatically, and the associated `simproc` set may be missing
and vice-versa.
Before this commit, `Simproc`s were defined as `Expr -> SimpM (Option Step)`, where `Step` is inductively defined as follows:
```
inductive Step where
| visit : Result → Step
| done : Result → Step
```
Here, `Result` is a structure containing the resulting expression and a proof demonstrating its equality to the input. Notably, the proof is optional; in its absence, `simp` assumes reflexivity.
A simproc can:
- Fail by returning `none`, indicating its inapplicability. In this case, the next suitable simproc is attempted, along with other simp extensions.
- Succeed and invoke further simplifications using the `.visit`
constructor. This action returns control to the beginning of the
simplification loop.
- Succeed and indicate that the result should not undergo further
simplifications. However, I find the current approach unsatisfactory, as it does not align with the methodology employed in `Transform.lean`, where we have the type:
```
inductive TransformStep where
/-- Return expression without visiting any subexpressions. -/
| done (e : Expr)
/--
Visit expression (which should be different from current expression) instead.
The new expression `e` is passed to `pre` again.
-/
| visit (e : Expr)
/--
Continue transformation with the given expression (defaults to current expression).
For `pre`, this means visiting the children of the expression.
For `post`, this is equivalent to returning `done`. -/
| continue (e? : Option Expr := none)
```
This type makes it clearer what is going on. The new `Simp.Step` type is similar but use `Result` instead of `Expr` because we need a proof.
Modifies the structure instance elaborator to
1. Fill in missing fields from sources in strict left-to-right order. In
`{a, b with}`, sometimes the elaborator
would ignore `a` even if both `a` and `b` provided the same field,
depending on what subobject fields they had.
2. Use the sources, or subobjects of the sources, to fill in entire
subobjects of the target structure as much as possible.
Currently, a field cannot be filled directly by a source itself
resulting in the term being eta expanded.
This change avoids this unnecessary and surprisingly costly extra eta
expansion.
Adds two new tests to illustrate the performance benefit (one courtesy
@semorrison). These are currently failing on master and succeed on this
branch.
There is one additional test to exercise the changes to the elaboration
of structure instances.
Changes to make mathlib build are in leanprover-community/mathlib4#9843
Closes#2451
This combines a few platform-related changes:
* Add a ternary `platformIndependent` Lean configuration option to
assert whether Lake should assume Lean code is platform-independent. If
`true`, Lake will exclude platform-independent objects like external
libraries or dynlibs created through `precompileModules` from module
traces. If `false`, Lake will add the platform to module traces. If
`none` (the default), Lake will retain the current behavior (modules are
platform-dependent if and only if it depends on native objects).
* Use `System.Platform.target` from #3207 as the platform descriptor in
Lake for the configuration file trace, the cloud release archive, and as
the platform trace in Lean modules and native artifacts (e.g., object
files, and static and shared libraries).
* Do not add the platform descriptor into custom build archive names
(i.e., a user-set `buildArchive` configuration). This allows users to
create cross-platform / platform-independent archives via a name
override should they so desire.
Closes#2754.
This replaces the no-op `unusedVariablesIgnoreFnsExt` environment
extension with an actual environment extension which can be extended
using either `@[unused_variables_ignore_fn]` or
`@[builtin_unused_variables_ignore_fn]` (although for the present all
the builtin `unused_variables_ignore_fn`s are being added using direct
calls to `builtin_initialize addBuiltinUnusedVariablesIgnoreFn`, because
this also works and a stage0 update is required before the attribute can
be used).
We would like to use this attribute to disable unused variables in
syntaxes defined in std and mathlib, like
[`proof_wanted`](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Unused.20variables.20and.20proof_wanted/near/408554690).
This PR adds two new delaboration settings: `pp.deepTerms : Bool`
(default: `true`) and `pp.deepTerms.threshold : Nat` (default: `20`).
Setting `pp.deepTerms` to `false` will make the delaborator terminate
early after `pp.deepTerms.threshold` layers of recursion and replace the
omitted subterm with the symbol `⋯` if the subterm is deeper than
`pp.deepTerms.threshold / 4` (i.e. it is not shallow). To display the
omitted subterm in the InfoView, `⋯` can be clicked to open a popup with
the delaborated subterm.
<details>
<summary>InfoView with pp.deepTerms set to false (click to show
image)</summary>
</details>
### Implementation
- The delaborator is adjusted to use the new configuration settings and
terminate early if the threshold is exceeded and the corresponding term
to omit is shallow.
- To be able to distinguish `⋯` from regular terms, a new constructor
`Lean.Elab.Info.ofOmissionInfo` is added to `Lean.Elab.Info` that takes
a value of a new type `Lean.Elab.OmissionInfo`.
- `ofOmissionInfo` is needed in `Lean.Widget.makePopup` for the
`Lean.Widget.InteractiveDiagnostics.infoToInteractive` RPC procedure
that is used to display popups when clicking on terms in the InfoView.
It ensures that the expansion of an omitted subterm is delaborated using
`explicit := false`, which is typically set to `true` in popups for
regular terms.
- Several `Info` widget utility functions are adjusted to support
`ofOmissionInfo`.
- The list delaborator is adjusted with special support for `⋯` so that
long lists `[x₁, ..., xₖ, ..., xₙ]` are shortened to `[x₁, ..., xₖ, ⋯]`.
this way this function does not have to peek at the `altType` to see
when there are no more arguments, which makes it a bit more explicit,
and also a bit more robust should one apply this function to the type of
an alternative with the motive already instantiated.
It seems this uncovered a variable shadow bug, where the counter `i` was
accidentially reset after removing the `i`’th entry in `ys`.
Adds support for `let_fun` to the `intro` and `intros` tactics. Also
adds support to `intro` for anonymous binder names, since the default
variable name for a `letFun` with an eta reduced body is anonymous.
Encouraged by the performance gains from making `rewrite` produce
smaller proof objects
(#3121) I am here looking for low-hanging fruit in `simp`.
Consider this typical example:
```
set_option pp.explicit true
theorem test
(a : Nat)
(b : Nat)
(c : Nat)
(heq : a = b)
(h : (c.add (c.add ((c.add b).add c))).add c = c)
: (c.add (c.add ((c.add a).add c))).add c = c
```
We get a rather nice proof term when using
```
:= by rw [heq]; assumption
```
namely
```
theorem test : ∀ (a b c : Nat),
@Eq Nat a b →
@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c →
@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c :=
fun a b c heq h =>
@Eq.mpr (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c)
(@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c)
(@congrArg Nat Prop a b (fun _a => @Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c _a) c))) c) c) heq) h
```
(this is with #3121).
But with `by simp only [heq]; assumption`, it looks rather different:
```
theorem test : ∀ (a b c : Nat),
@Eq Nat a b →
@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c →
@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c :=
fun a b c heq h =>
@Eq.mpr (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c)
(@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c)
(@id
(@Eq Prop (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c)
(@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c))
(@congrFun Nat (fun a => Prop) (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c))
(@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c))
(@congrArg Nat (Nat → Prop) (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c)
(Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) (@Eq Nat)
(@congrFun Nat (fun a => Nat) (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))))
(Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))))
(@congrArg Nat (Nat → Nat) (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c)))
(Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) Nat.add
(@congrArg Nat Nat (Nat.add c (Nat.add (Nat.add c a) c)) (Nat.add c (Nat.add (Nat.add c b) c)) (Nat.add c)
(@congrArg Nat Nat (Nat.add (Nat.add c a) c) (Nat.add (Nat.add c b) c) (Nat.add c)
(@congrFun Nat (fun a => Nat) (Nat.add (Nat.add c a)) (Nat.add (Nat.add c b))
(@congrArg Nat (Nat → Nat) (Nat.add c a) (Nat.add c b) Nat.add
(@congrArg Nat Nat a b (Nat.add c) heq))
c))))
c))
c))
h
```
Since simp uses only single-step `congrArg`/`congrFun` congruence lemmas
here, the proof
term grows very large, likely quadratic in this case.
Can we do better? Every nesting of `congrArg` (and it's little brother
`congrFun`) can be
turned into a single `congrArg` call.
In this PR I make making the smart app builders `Meta.mkCongrArg` and
`Meta.mkCongrFun` a bit
smarter and not only fuse with `Eq.refl`, but also with
`congrArg`/`congrFun`.
Now we get, in this simple example,
```
theorem test : ∀ (a b c : Nat),
@Eq Nat a b →
@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c →
@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c :=
fun a b c heq h =>
@Eq.mpr (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c)
(@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c)
(@congrArg Nat Prop a b (fun x => @Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c x) c))) c) c) heq) h
```
Let’s see if it works and how much we gain.
right now, the `induction` tactic accepts a custom eliminator using the
`using <ident>` syntax, but is restricted to identifiers. This
limitation becomes annoying when the elminator has explicit parameters
that are not targets, and the user (naturally) wants to be able to write
```
induction a, b, c using foo (x := …)
```
This generalizes the syntax to expressions and changes the code
accordingly.
This can be used to instantiate a multi-motive induction:
```
example (a : A) : True := by
induction a using A.rec (motive_2 := fun b => True)
case mkA b IH => exact trivial
case A => exact trivial
case mkB b IH => exact trivial
```
For this to work the term elaborator learned the `heedElabAsElim` flag,
`true` by default. But in the default setting, `A.rec (motive_2 := fun b
=> True)`
would fail to elaborate, because there is no expected type. So the
induction
tactic will elaborate in a mode where that attribute is simply ignored.
As a side effect, the “failed to infer implicit target” error message
is improved and prints the name of the implicit target that could not be
instantiated.
This PR adds support for the "call hierarchy" feature of LSP that allows
quickly navigating both inbound and outbound call sites of functions. In
this PR, "call" is taken to mean "usage", so inbound and outbound
references of all kinds of identifiers (e.g. functions or types) can be
navigated. To implement the call hierarchy feature, this PR implements
the LSP requests `textDocument/prepareCallHierarchy`,
`callHierarchy/incomingCalls` and `callHierarchy/outgoingCalls`.
<details>
<summary>Showing the call hierarchy (click to show image)</summary>
</details>
<details>
<summary>Incoming calls (click to show image)</summary>
</details>
<details>
<summary>Outgoing calls (click to show image)</summary>
</details>
It is based on #3159, which should be merged before this PR.
To route the parent declaration name through to the language server, the
`.ilean` format is adjusted, breaking backwards compatibility with
version 1 of the ILean format and yielding version 2.
This PR also makes the following more minor adjustments:
- `Lean.Server.findModuleRefs` now also combines the identifiers of
constants and FVars and prefers constant over FVars for the combined
identifier. This is necessary because e.g. declarations declared using
`where` yield both a constant (for usage outside of the function) and an
FVar (for usage inside of the function) with the same range, whereas we
would typically like all references to refer to the former. This also
fixes a bug introduced in #2462 where renaming a declaration declared
using `where` would not rename usages outside of the function, as well
as a bug in the unused variable linter where `where` declarations would
be reported as unused even if they were being used outside of the
function.
- The function converting `Lean.Server.RefInfo` to `Lean.Lsp.RefInfo`
now also computes the `Lean.DeclarationRanges` for parent declaration
names via `MetaM` and must hence be in `IO` now.
- Add a utility function `Array.groupByKey` to `HashMap.lean`.
- Stylistic refactoring of `Watchdog.lean` and `LanguageFeatures.lean`.
In the new snapshot design, we have a tree of `Task`s that represents
the asynchronously processed document structure. When transforming this
tree in response to a user edit, we want to quickly run through
reusable, already computed nodes of the tree synchronously and then
spawn new tasks for the new parts. The new flag allows us to do such
mixed sync/async tree transformations uniformly. This flag exists as
e.g.
[`ExecuteSynchronously`](https://learn.microsoft.com/en-us/dotnet/api/system.threading.tasks.taskcontinuationoptions?view=net-8.0)
in other runtimes.
I deleted internal links that seemed to have the character of "TODO". I
think that the residual TODO is of little value, given that we plan a
big revamp and revision soon anyway, but I could do it some other way as
well.
This makes changes to the definitions of Associativity, Commutativity,
Idempotence and Identity classes to be more aligned with Mathlib's
versions.
The changes are:
* Move classes are moved from `Lean` to root namespace.
* Drop `Is` prefix from names.
* Rename `IsNeutral` to `LawfulIdentity` and add Left and Right
subclasses.
* Change neutral/identity element to outParam.
* Introduce `HasIdentity` for operations not intended for proofs to
implement
The identity changes are to make this compatible with
[Mathlib](718042db9d/Mathlib/Init/Algebra/Classes.lean)
and to enable nicer fold operations in Std that can use type classes to
infer the identity/initial element on binary operations.
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Makes the LLVM triple of the current platform available to Lean code
towards a solution for #2754.
Defaults to the empty string if the compiler is not clang, which can
introduce some divergence between CI and local builds but should not be
noticeable in most cases and is not really possible to avoid.
Recursive predefinitions contains “rec app” markers as mdata in the
predefinitions,
but sometimes these get in the way of termination checking, when you
have
```
[mdata (fun x => f)] arg
```
Therefore, the `preprocess` pass floats them out of applications
(originally
only for structural recursion, since #2818 also for well-founded
recursion).
But the code was incomplete: Because `Meta.transform` calls `post` on `f
x y` only
once (and not also on `f x`) one has to float out of nested applications
as well.
A consequence of this can be that in a recursive proof, `rw [foo]` does
not work
although `rw [foo _ _]` does.
Also adding the testcase where @david-christiansen and I stumbled over
this
(Maybe the two preprocess modules can be combined, now that #2973 is
landed, will try that
in a follow-up).
As suggested by @kmill, removing an unnecessary `let` (possibly only
there in the first place for copy/paste reasons) seems to fix the
included test.
This makes `~q()` matching in quote4 noticeably more useful in things
like `norm_num` (as it fixes
https://github.com/leanprover-community/quote4/issues/29)
It also makes a quote4 bug slightly more visible
(https://github.com/leanprover-community/quote4/issues/30), but the bug
there already existed anyway, and isn't caused by this patch.
Fixes#3065
Give n-ary `Expr.app` constructors such as `mkApp2`, `mkApp3`, ...,
`mkApp10` the `@[match_pattern]` attribute so that it is easier to read
and write pattern matching for applications.
This PR facilitates augmenting the context of an `InfoTree` with
*partial* contexts while elaborating a command. Using partial contexts,
this PR also adds support for tracking the parent declaration name of a
term in the `InfoTree`. The parent declaration name is needed to compute
the call hierarchy in #3082.
Specifically, the `Lean.Elab.InfoTree.context` constructor is refactored
to take a value of the new type `Lean.Elab.PartialContextInfo` instead
of a `Lean.Elab.ContextInfo`, which now refers to a full `InfoTree`
context. The `PartialContextInfo` is then merged into a `ContextInfo`
while traversing the tree using
`Lean.Elab.PartialContextInfo.mergeIntoOuter?`. The partial context
after executing `liftTermElabM` is stored in values of a new type
`Lean.Elab.CommandContextInfo`.
As a result of this, `Lean.Elab.ContextInfo.save` moves to
`Lean.Elab.CommandContextInfo.save`.
For obtaining the parent declaration for a term, a new typeclass
`MonadParentDecl` is introduced to save the parent declaration in
`Lean.Elab.withSaveParentDeclInfoContext`. `Lean.Elab.Term.withDeclName
x` now calls `withSaveParentDeclInfoContext x` to save the declaration
name.
### Migration
**The changes to the `InfoTree.context` constructor break backwards
compatibility with all downstream users that traverse the `InfoTree`
manually instead of going through the functions in `InfoUtils.lean`.**
To fix this, you can merge the outer `ContextInfo` in a traversal with
the `PartialContextInfo` of an `InfoTree.context` node using
`PartialContextInfo.mergeIntoOuter?`. See e.g.
`Lean.Elab.InfoTree.foldInfo` for an example:
```lean
partial def InfoTree.foldInfo (f : ContextInfo → Info → α → α) (init : α) : InfoTree → α :=
go none init
where go ctx? a
| context ctx t => go (ctx.mergeIntoOuter? ctx?) a t
| node i ts =>
let a := match ctx? with
| none => a
| some ctx => f ctx i a
ts.foldl (init := a) (go <| i.updateContext? ctx?)
| _ => a
```
Downstream users that manually save `InfoTree`s may need to adjust calls
to `ContextInfo.save` to use `CommandContextInfo.save` instead and
potentially wrap their `CommandContextInfo` in a
`PartialContextInfo.commandCtx` constructor when storing it in an
`InfoTree` or `ContextInfo.mk` when creating a full context.
### Motivation
As of now, `ContextInfo`s are always *full* contexts, constructed as if
they were always created in `liftTermElabM` after running the
`TermElabM` action. This is not strictly true; we already create
`ContextInfo`s in several places other than `liftTermElabM` and work
around the limitation that `ContextInfo`s are always full contexts in
certain places (e.g. `Info.updateContext?` is a crux that we need
because we can't always create partial contexts at the term-level), but
it has mostly worked out so far. Note that one must be very careful when
saving a `ContextInfo` in places other than `liftTermElabM` because the
context may not be as complete as we would like (e.g. it may lack
meta-variable assignments, potentially leading to a language server
panic).
Unfortunately, the parent declaration of a term is another example of a
context that cannot be provided in `liftTermElabM`: The parent
declaration is usually set via `withDeclName`, which itself lives in
`TermElabM`. So by the time we are trying to save the full
`ContextInfo`, the declaration name is already gone. There is no easy
fix for this like in the other cases where we would really just like to
augment the context with an extra field.
The refactor that we decided on to resolve the issue is to refactor the
`InfoTree` to take a `PartialContextInfo` instead of a `ContextInfo` and
have code that traverses the `InfoTree` merge inner contexts with outer
contexts to produce a full `ContextInfo` value.
### Bumps for downstream projects
- `lean-pr-testing-3159` branch at Std, not yet opened as a PR
- `lean-pr-testing-3159` branch at Mathlib, not yet opened as a PR
- https://github.com/leanprover/LeanInk/pull/57
- https://github.com/hargoniX/LeanInk/pull/1
- https://github.com/tydeu/lean4-alloy/pull/7
- https://github.com/leanprover-community/repl/pull/29
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Currently we create `lean-pr-testing-NNNN` branches at Mathlib
automatically for each Lean PR.
We don't automatically create one at Std; mostly simply because Std
fails less often, so it has been okay to do this manually as needed. It
is conceptually simpler, however, if this is done uniformly.
This PR:
* does not proceed with Std/Mathlib CI unless the appropriate
`nightly-testing-YYYY-MM-DD` tag exists at Std (like it already doesn't
proceed if that tag is missing at Mathlib)
* creates `lean-pr-testing-NNNN` branches at Std
* when it creates `lean-pr-testing-NNNN` branches at Mathlib, updates
the Std dependency to use the `lean-pr-testing-NNNN` branch at Std
- [x] depends on #3199
Note that because most users do not have write access at Std, in order
to make updates to `lean-pr-testing-NNNN` branches there they will need
to make PRs. These will be merged with a very low bar, and feel free to
ping me for assistance on this. If this is annoying we will automate.
Also, frequent contributors to Lean may ask @digama0 or @joehendrix for
write access in order to easily work on these branches.
This PR requires that we have a secret here with write access at Std.
I'm arranging that [on
zulip](https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/bot.20access/near/416686090).
I will update the documentation at
https://leanprover-community.github.io/contribute/tags_and_branches.html
to reflect these changes when they are merged.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
As discussed during the FRO meeting 2024-01-18, we are changing the
`nightly-testing-YYYY-MM-DD` branches at Std and Mathlib from branches
to tags, in:
* https://github.com/leanprover/std4/pull/545
* https://github.com/leanprover-community/mathlib4/pull/9842
This PR updates the script that creates the `lean-pr-testing-NNNN`
branches at Mathlib so it is agnostic about whether
`nightly-testing-YYYY-MM-DD` will be a branch or a tag.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
`Array.set!` and `Array.swap!` are fairly similar operations, both
modify an array, both take an index that it out of bounds.
But they behave different; all of these return `true`
```
#eval #[1,2].set! 2 42 == #[1,2] -- with panic
#reduce #[1,2].set! 2 42 == #[1,2] -- no panic
#eval #[1,2].swap! 0 2 == #[1,2] -- with panic
#reduce #[1,2].swap! 0 2 == default -- no panic
```
The implementations are
```
@[extern "lean_array_set"]
def Array.set! (a : Array α) (i : @& Nat) (v : α) : Array α :=
Array.setD a i v
```
but
```
@[extern "lean_array_swap"]
def swap! (a : Array α) (i j : @& Nat) : Array α :=
if h₁ : i < a.size then
if h₂ : j < a.size then swap a ⟨i, h₁⟩ ⟨j, h₂⟩
else panic! "index out of bounds"
else panic! "index out of bounds"
```
It seems to be more consistent to unify the behaviors, and define
```
@[extern "lean_array_swap"]
def swap! (a : Array α) (i j : @& Nat) : Array α :=
if h₁ : i < a.size then
if h₂ : j < a.size then swap a ⟨i, h₁⟩ ⟨j, h₂⟩
else a
else a
```
Also adds docstrings.
Fixes#3196
Consider
```
import Std.Tactic.ShowTerm
opaque a : Nat
opaque b : Nat
axiom a_eq_b : a = b
opaque P : Nat → Prop
set_option pp.explicit true
-- Using rw
example (h : P b) : P a := by show_term rw [a_eq_b]; assumption
```
Before, a typical proof term for `rewrite` looked like this:
```
-- Using the proof term that rw produces
example (h : P b) : P a :=
@Eq.mpr (P a) (P b)
(@id (@Eq Prop (P a) (P b))
(@Eq.ndrec Nat a (fun _a => @Eq Prop (P a) (P _a))
(@Eq.refl Prop (P a)) b a_eq_b))
h
```
which is rather round-about, applying `ndrec` to `refl`. It would be
more direct to write
```
example (h : P b) : P a :=
@Eq.mpr (P a) (P b)
(@id (@Eq Prop (P a) (P b))
(@congrArg Nat Prop a b (fun _a => (P _a)) a_eq_b))
h
```
which this change does.
This makes proof terms smaller, causing mild general speed up throughout
the code; if the brenchmarks don’t lie the highlights are
* olean size -2.034 %
* lint wall-clock -3.401 %
* buildtactic execution s -10.462 %
H'T to @digama0 for advice and help.
NB: One might even expect the even simpler
```
-- Using the proof term that I would have expected
example (h : P b) : P a :=
@Eq.ndrec Nat b (fun _a => P _a) h a a_eq_b.symm
```
but that would require non-local changes to the source code, so one step
at a time.
The `checkTargets` function introduced in 4a0f8bf2 as
```
checkTargets (targets : Array Expr) : MetaM Unit := do
let mut foundFVars : FVarIdSet := {}
for target in targets do
unless target.isFVar do
throwError "index in target's type is not a variable (consider using the `cases` tactic instead){indentExpr target}"
if foundFVars.contains target.fvarId! then
throwError "target (or one of its indices) occurs more than once{indentExpr target}"
```
looks like it tries to check for duplicate indices, but it doesn’t
actually, as `foundFVars` is never written to.
This adds
```
foundFVars := foundFVars.insert target.fvarId!
```
and a test case.
Maybe a linter that warns about `let mut` that are never writen to would
be useful?
I keep messing things up, so time for some guard rails, so check them
using
[actionlint](https://github.com/raven-actions/actionlint).
This also runs [shellcheck](https://www.shellcheck.net/) on the files.
Shellcheck
is a bit picky about putting double quotes around variables, and will
flag many
cases where we know it’s safe, but why not simply always write the safer
variant.
Unfortunately, actionlint does not (yet) check `actions/github-script`
scripts, which is
unfortunate. Maybe they will in the future
(https://github.com/rhysd/actionlint/issues/389)
there was a check
if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then
that would avoid going through `.refineThrough`/`.addArg` for
matcher/casesOn applications. It seems it tries to detect when refining
the motive/param is pointless, but it was too eager, and cause confusion
with, for example, this reasonably reasonable function:
def foo : (n : Nat) → (i : Fin n) → Bool
| 0, _ => false
| 1, _ => false
| _+2, _ => foo 1 ⟨0, Nat.zero_lt_one⟩
decreasing_by simp_wf; simp_arith
In particular, the `GuessLex` code later expects that the (implict)
`PProd.casesOn` in the implementation of `foo._unary` will refine the
paramter, because else the (rather picky) `unpackArg` fails. But it also
prevents this from being provable.
So let's try without this shortcut.
Fixing this also revealed that `withRecApps` wasn’t looking in all
corners
of a matcherApp/casesOnApp.
Fixes#3175
this didn’t recognize the new comments with an intro, and thus the bot
would post multiple comments.
The code was also out of sync with mathlib, fixing.
The `first(…)` in the `jq` program makes it more robust in case this
went wrong once (as on #3171) and there are now multiple PRs matching.
This uses the improved termination_by syntax to give Nat.gcd a cleaner
definition. It removes the last explicit use of WellFounded.fix in Init.
This was also partly motivated by leanprover/std4#520 so that unfold
Nat.gcd gives a sensible definition.
If the current manifest is from unsupported (or has errors), a bare
`lake update` will now discard it and create a new one from scratch
rather than erroring and requiring you to manually delete the manifest.
Lake will produce warnings noting it is ignoring such invalid manifests.
so far, our reference manual did not mention these at all, this takes
the discussion of recursive definition out of the “equation compiler”
section, put it into its own section, and expands it a bit.
This is more a MVP doc change to at least mention the features briefly,
and not the most polished and thought through didactic exposition. But
it provides a start for more improvements.
---------
Co-authored-by: Arthur Adjedj <arthur.adjedj@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
This change
* moves `termination_by` and `decreasing_by` next to the function they
apply to
* simplify the syntax of `termination_by`
* apply the `decreasing_by` goal to all goals at once, for better
interactive use.
See the section in `RELEASES.md` for more details and migration advise.
This is a hard breaking change, requiring developers to touch every
`termination_by` in their code base. We decided to still do it as a
hard-breaking change, because supporting both old and new syntax at the
same time would be non-trivial, and not save that much. Moreover, this
requires changes to some metaprograms that developers might have
written, and supporting both syntaxes at the same time would make
_their_ migration harder.
To handle delaborating notations that are functions that can be applied
to arguments, extracts the core function application delaborator as a
separate function that accepts the number of arguments to process and a
delaborator to apply to the "head" of the expression.
Defines `withOverApp`, which has the same interface as the combinator of
the same name from std4, but it uses this core function application
delaborator.
Uses `withOverApp` to improve a number of application delaborators,
notably projections. This means Mathlib can stop using `pp_dot` for
structure fields that have function types.
Incidentally fixes `getParamKinds` to specialize default values to use
supplied arguments, which impacts how default arguments are delaborated.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Allow `simproc`s to be declared without setting the `[simproc]`
attribute. A `simproc` declaration is function + pattern.
Motivation: allow them to be provided as arguments to `simp` **and** `simp only`.
TODO: track their use in `simp`.
TODO: builtin simprocs
Motivations:
- We can simplify the big mutual recursion and the implementation.
- We can implement the support for `match`-expressions in the `pre` method.
- It is easier to define and simplify `Simprocs`.
The example was looping with the new `simp` reduction strategy. Here
is the looping trace.
```
List.reverseAux (List.reverseAux as []) bs
==> rewrite using reverseAux_reverseAux
List.reverseAux [] (List.reverseAux (List.reverseAux as []) bs)
==> unfold reverseAux
List.reverseAux (List.reverseAux as []) bs
==> rewrite using reverseAux_reverseAux
List.reverseAux [] (List.reverseAux (List.reverseAux as []) bs)
==> ...
```
See new test for example that takes exponential time without new simp
theorems.
TODO: replace auxiliary theorems with simprocs as soon as we implement them.
I was about to to address the TODO
/- TODO: check arity of the given function. If it takes a PSigma as the
last argument,
this function will produce incorrect results. -/
because we now have an arity-observing variant of `decodePackedArg?` in
`unpackArg` in `PackMutual`, and it would be prudent to use it here.
But I first wanted to create a test case that would actually exhibit
this corner case, and failed.
This code was added in 096e4eb6d0 and it had a test case, but not even
that test case seems to be actually using the `decodePackedArg?`
function, neither back then nor now.
Also, mathlib works without this code.
So this seems to be dead code, possibly due to other changes to the
system, and thus can be removed. A strategically place comments points
back to this PR in case we need to resurrect that code.
The pattern
```
for h : i in [:xs.size] do
let x := xs[i]'h.2
```
is occassionally useful to iterate over an array with the index in
hand. This PR extends the `get_elem_tactic_trivial` so that one can
simply write
```
for h : i in [:xs.size] do
let x := xs[i]
```
fixes#3032.
When looking at a PR I sometimes wonder which `nightly` release is this
based on, and is used for the mathlib testing.
Right now, the action uses a label (`toolchain-available`) for this, but
a label cannot easily carry more information.
It seems a rather simple way to communicate extra information is by
setting [commit
statuses](https://docs.github.com/en/rest/commits/statuses?apiVersion=2022-11-28#create-a-commit-status);
with this change the following statuses will appear in the PR:
One could also use
[checks](https://docs.github.com/en/rest/checks/runs?apiVersion=2022-11-28#create-a-check-run)
to add more information, even with a nicely formatted markdown
description as in [this
example](https://github.com/nomeata/lean4/pull/1/checks?check_run_id=20165137082),
but it seems there you can’t set a summary that’s visible without an
extra click, and Github seems to associate these checks to “the first
workflow”, which is odd. So using statuses seems fine here.
Often one uses bots writing PR comments for this purpose, but that's a
bit noisy (extra notifications etc.), especially for stuff that happens
on every PR, but isn’t always interesting/actionable
If this works well, we can use this for more pieces of information, and
a link can be added as well.
This removes checks in `Lean.Meta.reduceNat?` that caused it to fail on
terms it could handle because they contain meta variables in arguments.
This lead to those operations being reduced using their equational
definitions and slow performance on large patterns:
```
set_option profiler true
set_option profiler.threshold 1
def testMod (x:Nat) :=
match x with
| 128 % 1024 => true
| _ => false
-- elaboration took 3.02ms
def testMul (x:Nat) :=
match x with
| 128 * 1 => true
| _ => false
-- type checking took 11.1ms
-- compilation of testMul.match_1 took 313ms
-- compilation of testMul took 65.7ms
-- elaboration took 58.9ms
```
Performance is slower on `testMul` than `testMod` because `whnf` ends up
evaluateing `128 * 1` using Peano arithmetic while `128 % 1024` is able
to avoid that treatment since `128 < 1024`.
This makes hover info, go to definition, etc work for the `h` in `cases
h : e`. The implementation is similar to that used for the `generalize h
: e = x` tactic.
#2966 was the `@[extern]` bug that prompted development of the
`test_extern` command, but then we merged the fix to #2966 without
updating the tests to use `test_extern`.
# 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>
This PR fixes the documentation error in "Extended Setup Notes", where
the path of builded binary is pointed to
`./build/bin/foo`, but the truly path is `./lake/build/bin/foo`.
---
Closes#3094 (`RFC` or `bug` issue number fixed by this PR, if any)
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.
given that we now use the PR description as the commit message, the PR
template should point that out. Also, a `# Summary` is relatively
strange in a commit message, so removed it.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
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>
Getting the original PR number from a `workflow_run` cleanly and
reliably seems to be
basically impossible. See
<https://github.com/orgs/community/discussions/25220> for a discussion.
So for now let’s go back to the working state, even though it’s
deprecated and throws warnings.
This prompts users opening the workspace (on a new device) for the first
time to install the lean extension
# Summary
Link to `RFC` or `bug` issue: N/A
#3066 is causing CI failures, e.g.
[here](https://github.com/leanprover/lean4/actions/runs/7202184616/job/19619827364).
Although there are plenty of examples of using `await` in a Github
workflow script block, the error *seems* to be about this. This refactor
hopefully works around that, but I'm still uncertain of a root cause.
This fixe a surprisingly embarrassing bug introduced by me in
fa26d222cb (maybe while testing).
Enable more debug output while we are at it, to find out why sometimes
`context.payload.workflow_run.pull_requests[0]` is undefined.
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.
the workflow is triggered not only by pull-request-CI-runs but also by
others. These should be skipped.
Also, no need to query the Github API to get the pull request number and
head sha, they are part of the payload, it seems.
Since the vscode-lean4 setup guide allows us to provide information on
setting up Lean 4 tailored to the user's operating system, this PR
adjusts the quickstart guide to reference the vscode-lean4 setup guide
instead.
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.)
In particular:
* Do not use deprecated `potiuk/get-workflow-origin`.
* Use a bare checkout to push PR to `pr-releases`
* Replace `script/most-recent-nightly-tag.sh` by a one-liner inside the
workflow, so that th workflow is self-contained
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?`.
This Github action automatically updates `stage0` on `master` if
`src/stdlib_flags.h` and `stage0/src/stdlib_flags.h`
are out of sync there.
It bypasses the merge queue to be quick, this way, an out-of-date stage0
on on
master should only exist for a few minutes.
Needs access to a _deploy SSH key_ with write permission.
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.
This sets the build directory to `build/release` for the "CMake Tools
for Visual Studio Code" extension documented at
https://vector-of-bool.github.io/docs/vscode-cmake-tools/settings.html#cmake-builddirectory.
It also sets the generator to `make`, since otherwise it tries `Ninja`
which doesn't work.
Without these settings, the extension runs configure in a bad place at
startup.
This does *not* add the cmake tools extension to the default workspace
configuration; the goal is simply to prevent bad behavior for users who
already have the extension enabled.
# Summary
Screenshot of this in action:
Link to `RFC` or `bug` issue: N/A, this is not a bug nor a user-visible
feature.
Now that we're, at least temporarily, relying more on the Nix CI,
replace some old hacks of mine with better solutions people have figured
out in the meantime.
Cachix support could probably be dropped at this point but it doesn't
really hurt.
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
CI will now run on _any_ manually added label; hard to avoid.
Fun fact: Because the `toolchain-available` label is added by a github
action with the default token, it will _not_ trigger the workflow. Lucky
coincidence.
Following up on #2986, stop running the test suite in ci.yml in quick
mode; the test suite is run in the Nix job, and we do not need to run it
twice.
With a cold nix cache, when `lean` is rebuilt, not much changes, as both
jobs take ~20mins. But when `lean` is unchanged, the nix build should
be faster, and shaving off the (currently) 4mins in the CI.yaml run
should get us to a green PR sooner.
Another benefit is that we get the PR release sooner and even get it
when the test suite fails, which can be useful if you want to test
mathlib or other things before fixing the lean test suite.
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.
The goal of this change is to run a trimmed-down CI on PRs by default,
but allows opt-in the full CI as necessary.
### Specification
The CI workflow runs in “quick” mode if it was triggered from a pull
request, and that pull request does not have the `full-ci` label set.
In “quick” mode the build matrix contains fewer jobs. At the moment
only:
* Linux-release, to get the PR releases.
In non-quick mode everything should be as before.
### Implementation notes
I created a `configure` job that combines all the previous `set-` jobs,
I guess this is faster than firing up separate jobs.
The matrix is calculated in this job; this seems to be the cleanest way
to get a dynamic matrix going (experiments using `exclude` failed). The
downside is that the matrix is now in JSON rather than Yaml syntax. The
upside is that we can (later) make it’s calculation simpler, e.g. set
default `shell` values etc.
I was not able to make it so that CI runs when the `full-ci` label is
added, but don’t do anything otherwise. I think it can be done with
another workflow listening to `labeled` and then triggering this one,
but let’s do that separately. For now, add the label and then push (or
close and reopen).
The checks
```
if: matrix.build-stage2 || matrix.check-stage3
if: matrix.check-stage3
```
were dead code, we did not have these fields in the matrix anymore, so I
replaced them with
```
if: matrix.test-speedcenter
```
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.
there is a little dance with `if: success()` because otherwise a failed
`build` job would make this new job skipped, not failed, and I fear
skipped means ok when it is a required job.
So let’s make sure this job actually fails.
Also turn this into a proper check, run when a PR is opened or edited.
I took the liberty to rename the workflow file and name, so that one
doesn't have to look inside to guess what the workflow is doing.
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.
This is an additional safety net on top of #2749: it protects users that
circumvent the build system (e.g. with `lake env`) as well as obviates
the need for TOCTOU-like race condition checks in the build system.
The check is activated by `CHECK_OLEAN_VERSION=ON`, which now defaults
to `OFF` as the sensible default for local development. When activated,
`USE_GITHASH=ON` is also force-enabled for stage 0 in order to make sure
that stage 1 can load its own core library.
This PR adds per-package server options to resolve#2455. It is based on
the previous work in #2456, but takes a different approach: options are
loaded for the specific file in the file worker when `print-paths` is
called, instead of loading them in the watchdog with a separate Lake
command. This change addresses review comments made in #2456.
In doing so, it introduces two new Lake config fields:
- `leanOptions`: `-D` flag options that are passed to both the language
server and `lean` when building.
- `moreServerOptions`: `-D` flag options that are passed to the language
server.
Since `print-paths` must also accept a file path to compute the options
for that file, this PR is changing the API for `print-paths`. As there
have been numerous complaints about the name `print-paths`, I also
decided to change it to `setup-file` in this PR, since it would break
compatibility with the old Lake API anyways.
This PR deprecates the Lakefile field `moreServerArgs` in favor of
`moreGlobalServerArgs`, as suggested in the review for #2456.
Fixes#2455
---------
Co-authored-by: digama0 <mcarneir@andrew.cmu.edu>
This was a Lean 3 pretty printer option. While this pretty printer
option tends to lead to confusing situations when set, it has been
frequently requested. [It is
possible](https://github.com/leanprover-community/mathlib4/pull/7910) to
implement this pretty printer option as a user, but it comes with some
artifacts -- for instance, expressions in hovers are not beta reduced.
Adding this as a core pp option is cleanest.
(We should consider having hooks into the tactic evaluator to allow
users to transform the tactic state between tactics. This would enable
beta reducing the entire local context for real, which would be useful
for teaching.)
Closes#715
We noticed at
https://github.com/leanprover/lean4/pull/2923#discussion_r1400468371
that this instance is not used. It's arguably also incorrect (as it
doesn't backtrack the `usedTheorems` field).
Seems better to just remove to avoid confusion.
Evidence that this is dead code:
* After deleting the instance, calling `saveState` in the `SimpM` monad
raises an error `failed to synthesize instance MonadBacktrack PUnit
SimpM`.
* Understanding the `MonadBacktrack` monad leads one to believe that
would have happened, via the fact that the only instances for
`MonadBacktrack` are either concrete instances (e.g. for `MetaM`,
`TacticM`, etc), or a single lifting instance `instance [MonadBacktrack
s m] [Monad m] : MonadBacktrack s (ExceptT ε m)`. (This is good and
correct behaviour: lifting instances for `MonadBacktrack` would be hard
to model.)
* Mathlib builds after the instance is removed.
Potential evidence that I have not sought, because we don't have
sufficient tooling:
* Compiling Lean/Std/Mathlib with a debugger, breaking on entering this
code.
This PR adds basic auto-completion support for imports. Since it still
lacks Lake support for accurate completion suggestions (cc @tydeu - we
already know what needs to be done), it falls back to traversing the
`LEAN_SRC_PATH` for available imports.
Three kinds of import completion requests are supported:
- Completion of the full `import` command. Triggered when requesting
completions in an empty space within the header.
- Known issue: It is possible to trigger this completion within a
comment in the header. Fixing this would require architecture for
parsing some kind of sub-syntax between individual commands.
- Completion of the full module name after an incomplete `import`
command.
- Completion of a partial module name with a trailing dot.
Since the set of imports is potentially expensive to compute, they are
cached for 10 seconds after the last import auto-completion request.
Closes#2655.
### Changes
This PR also makes the following changes:
- To support completions on the trailing dot, the `import` syntax was
adjusted to provide partial syntax when a trailing dot is used.
- `FileWorker.lean` was refactored lightly with some larger definitions
being broken apart.
- The `WorkerState` gained two new fields:
- `currHeaderStx` tracks the current header syntax, as opposed to
tracking only the initial header syntax in `initHeaderStx`. When the
header syntax changes, a task is launched that restarts the file worker
after a certain delay to avoid constant restarts while editing the
header. During this time period, we may still want to serve import
auto-completion requests, so we need to know the up-to-date header
syntax.
- `importCachingTask?` contains a task that computes the set of
available imports.
- `determineLakePath` has moved to a new file `Lean/Util/LakePath.lean`
as it is now needed both in `ImportCompletion.lean` and
`FileWorker.lean`.
- `forEachModuleIn` from `Lake/Config/Blob.lean` has moved to
`Lean/Util/Path.lean` as it is a generally useful utility function that
was useful for traversing the `LEAN_SRC_PATH` as well.
### Tests
Unfortunately, this PR lacks tests since the set of imports available in
`tests/lean/interactive` will not be stable. In the future, I will add
support for testing LSP requests in full project setups, which is when
tests for import auto-completion will be added as well.
there were wrong italics, missing backticks, missing indentation and I
took the liberty to replace `[here]` links with link targets that better
tell the reader what to expect when clicking there.
The `packMutual` code ought to reliably replace all recursive calls to
the functions in `preDefs`, even when they are under- or over-applied.
Therefore eta-expand if need rsp. keep extra arguments around.
Needs a tweak to `Meta.transform` to avoid mistaking the `f` in
`f x1 x2` as a zero-arity application.
Includes a test case.
This fixes#2628 and #2883.
This didn't work before
```
def f (n : Nat) : Nat :=
match n with
| 0 => 0
| n + 1 => (f) n
```
because the `RecApp` metadata marker gets in the way. More practically
relevant, such code is to be produced when using `rw` or `simp` in
recursive theorems (see included test case).
We can fix this by preprocessing the definitions and floating the
`.mdata` marker out of applications.
For structural recursion, there already exists a `preprocess` function;
this now also floats out `.mdata` markers.
For well-founded recursion, this introduces an analogous `preprocess`
function.
Fixes#2810.
One test case output changes: With the `.mdata` out of the way, we get a
different error message. Seems fine.
Alternative approaches are:
* Leaving the `.mdata` marker where it is, and looking around it.
Tried in #2813, but not nice (many many places where `withApp` etc.
need to be adjusted).
* Moving the `.mdata` _inside_ the application, so that `withApp` still
works. Tried in #2814. Also not nice, the invariant that the `.mdata`
is around the `.const` is tedious to maintain.
the code stumbled over recursive functions whose type doesn’t have
enough manifest foralls, like:
```
def FunType := Nat → Nat
mutual
def foo : FunType
| .zero => 0
| .succ n => bar n
def bar : FunType
| .zero => 0
| .succ n => foo n
end
termination_by foo n => n; bar n => n
```
This can be fixed by using `whnf` in appropriate places, to expose the
`.forall` constructor.
Fixes#2925, comes with test case.
`script/most-recent-nightly-tag.sh` determines the most recent nightly
release in your current git history.
Previously it was assuming that you had a `nightly` remote, to pull tags
from. Now it just pulls directly from the repository by URL.
This only really shows up when the `decreasing_tactic` fails with
multiple goals, as in
```
macro_rules
| `(tactic|decreasing_tactic) => `(tactic| by_cases (2 > 1))
def foo (n : Nat) : Nat := foo (n - 1)
termination_by foo n => n
```
where we now get
```
unsolved goals
case inl
n: Nat
h✝: 2 > 1
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n - 1) n
case inr
n: Nat
h✝: ¬2 > 1
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n - 1) n
```
rather than
```
LeanProject.lean:3:27
unsolved goals
case inl
n: Nat
h✝: 2 > 1
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n - 1) n
LeanProject.lean:3:27
unsolved goals
case inr
n: Nat
h✝: ¬2 > 1
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n - 1) n
```
The effect is neglectible, but the code is a bit nicer, so why not,
before someone looks at it again and wonders whether the goals are
reported separately for a reason.
Some beginners have trouble finding the `if h : c then t else e`
(`dite`) version of `ite`. This augments `ite`'s docstring to mention
the dependent version.
This implements a request handler for the `textDocument/rename` LSP
request, enabling renames via F2. It handles both local renames (e.g.
`let x := 1; x` to `let y := 1; y`) as well as global renames
(definitions).
Unfortunately it does not work for "orphan" files outside a project, as
it uses ilean data for the current file and this does not seem to be
saved for orphan files. As a result, the test file does not work,
although one can manually test the implementation against a project such
as mathlib. (This issue already exists for the "references" request,
e.g. ctrl click on the first `x` in `let x := 1; x` takes you to the
second one only if you are not in an orphan file.)
* Fixesleanprover-community/mathlib4#7124
Modifies `cleanup` so that it takes (1) an array of additional fvarids
to preserve and (2) a flag to control whether to include indirect
propositions.
(This is wanted in mathlib for the `extract_goal` tactic.)
previously, it would ignore a recursive call that has extra arguments,
which can happen when the recursive functions return something of
function type. Therefore just leave them extra arguments in place.
Fixes#2883.
In the previous doc-string, the sentence
> "If any of the selected tactic applications fail, it will call
`failed` with the main goal mvar."
was false both for `Location.wildcard` (where it should have said "If
all", not "If any") or for `Location.targets` (where `failed` is never
called).
Add documentation comments with examples to `universe`, `open`,
`export`, and `variable`.
The documentation shows up when hovering over keywords, hopefully
improving the experience for beginners.
Because `Decidable` carries data,
when writing `@[simp]` lemmas which include a `Decidable` instance on the LHS,
it is best to use `{_ : Decidable p}` rather than `[Decidable p]`
so that non-canonical instances can be found via unification rather than
typeclass search.
(Previously this behaviour was often being hidden by the default `decide :=
true` in `simp`.)
We were checking out the synthetic merge commit between the PR `HEAD`
and `master`, and this was then breaking the logic to determine which
nightly-testing branches to use in Mathlib and Std.
* Ensure your PR follows the [External Contribution Guidelines](https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md).
* Please make sure the PR has excellent documentation and tests. If we label it `missing documentation` or `missing tests` then it needs fixing!
*Add the link to your `RFC` or `bug` issue below.
*Include the link to your `RFC` or `bug` issue in the description.
* If the issue does not already have approval from a developer, submit the PR as draft.
*Remove this section before submitting.
*The PR title/description will become the commit message. Keep it up-to-date as the PR evolves.
* If you rebase your PR onto `nightly-with-mathlib` then CI will test Mathlib against your PR.
* You can manage the `awaiting-review`, `awaiting-author`, and `WIP` labels yourself, by writing a comment containing one of these labels on its own line.
* Remove this section, up to and including the `---` before submitting.
You can manage the `awaiting-review`, `awaiting-author`, and `WIP` labels yourself, by writing a comment containing one of these labels on its own line.
---
# Summary
Link to `RFC` or `bug` issue:
Closes #0000 (`RFC` or `bug` issue number fixed by this PR, if any)
echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' branch."
if [[ -n "$BATTERIES_REMOTE_TAGS" ]]; then
echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE=""
if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
else
echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
fi
else
echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' branch."
MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-$MOST_RECENT_NIGHTLY' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow."
echo "... but Batteries does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Batteries CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Batteries CI should run now."
fi
else
echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA"
MESSAGE="- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
fi
if [[ -n "$MESSAGE" ]]; then
echo "Checking existing messages"
# The code for updating comments is duplicated in mathlib's
# scripts/lean-pr-testing-comments.sh
# so keep in sync
# Use GitHub API to check if a comment already exists
// check first commit only (and only once) since later commits might be intended to be squashed away
if (!/^(feat|fix|doc|style|refactor|test|chore|perf): .*[^.]($|\n\n)/.test(commits[0].commit.message)) {
await github.rest.issues.createComment({
owner: context.repo.owner,
repo: context.repo.repo,
issue_number: context.issue.number,
body: 'Thanks for your contribution! Please make sure to follow our [Commit Convention](https://leanprover.github.io/lean4/doc/dev/commit_convention.html).',
**Descriptive Title and Summary**: The PR title should briefly explain the purpose of the PR. The summary should give more detailed information on what changes are made and why. Links to Zulip threads are not acceptable as a summary. You are responsible for summarizing the discussion, and getting support for it.
**Follow the commit convention**: Pull requests are squash merged, and the
commit message is taken from the pull request title and body, so make sure they adhere to the [commit convention](https://github.com/leanprover/lean4/blob/master/doc/dev/commit_convention.md). Put questions and extra information, which should not be part of the final commit message, into a first comment rather than the Pull Request description.
Because the change will be squashed, there is no need to polish the commit messages and history on the branch.
**Link to Relevant Issues**: Reference any issues that your PR addresses to provide context.
**Stay Responsive**: Once the PR is submitted, stay responsive to feedback and be prepared to make necessary revisions. We will close any PR that has been inactive (no response or updates from the submitter) for more than a month.
A value of type `Char`, also known as a character, is a [Unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value). It is represented using an unsigned 32-bit integer and is statically guaranteed to be a valid Unicode scalar value.
Syntactically, character literals are enclosed in single quotes.
```lean
#eval'a'-- 'a'
#eval'∀'-- '∀'
```
Characters are ordered and can be decidably compared using the relational operators `=`, `<`, `≤`, `>`, `≥`.
If any of the terms ``tᵢ`` in the template above contain a recursive call to ``foo``, the equation compiler tries to interpret the definition as a structural recursion. In order for that to succeed, the recursive arguments must be subterms of the corresponding arguments on the left-hand side. The function is then defined using a *course of values* recursion, using automatically generated functions ``below`` and ``brec`` in the namespace corresponding to the inductive type of the recursive argument. In this case the defining equations hold definitionally, possibly with additional case splits.
The case where patterns are matched against an argument whose type is an inductive family is known as *dependent pattern matching*. This is more complicated, because the type of the function being defined can impose constraints on the patterns that are matched. In this case, the equation compiler will detect inconsistent cases and rule them out.
```lean
universe u
inductive Vector (α : Type u) : Nat → Type u
| nil : Vector α 0
| cons : α → Vector α n → Vector α (n+1)
namespace Vector
def head : Vector α (n+1) → α
| cons h t => h
def tail : Vector α (n+1) → Vector α n
| cons h t => t
def map (f : α → β → γ) : Vector α n → Vector β n → Vector γ n
| nil, nil => nil
| cons a va, cons b vb => cons (f a b) (map f va vb)
end Vector
```
.. _recursive_functions:
Recursive functions
===================
Lean must ensure that a recursive function terminates, for which there are two strategies: _structural recursion_, in which all recursive calls are made on smaller parts of the input data, and _well-founded recursion_, in which recursive calls are justified by showing that arguments to recursive calls are smaller according to some other measure.
Structural recursion
--------------------
If the definition of a function contains recursive calls, Lean first tries to interpret the definition as a structural recursion. In order for that to succeed, the recursive arguments must be subterms of the corresponding arguments on the left-hand side.
The function is then defined using a *course of values* recursion, using automatically generated functions ``below`` and ``brec`` in the namespace corresponding to the inductive type of the recursive argument. In this case the defining equations hold definitionally, possibly with additional case splits.
If structural recursion fails, the equation compiler falls back on well-founded recursion. It tries to infer an instance of ``SizeOf`` for the type of each argument, and then show that each recursive call is decreasing under the lexicographic order of the arguments with respect to ``sizeOf`` measure. If it fails, the error message provides information as to the goal that Lean tried to prove. Lean uses information in the local context, so you can often provide the relevant proof manually using ``have`` in the body of the definition. In this case of well-founded recursion, the defining equations hold only propositionally, and can be accessed using ``simp`` and ``rewrite`` with the name ``foo``.
Well-founded recursion
---------------------
If structural recursion fails, the equation compiler falls back on well-founded recursion. It tries to infer an instance of ``SizeOf`` for the type of each argument, and then tries to find a permutation of the arguments such that each recursive call is decreasing under the lexicographic order with respect to ``sizeOf`` measures. Lean uses information in the local context, so you can often provide the relevant proof manually using ``have`` in the body of the definition.
In the case of well-founded recursion, the equation used to declare the function holds only propositionally, but not definitionally, and can be accessed using ``unfold``, ``simp`` and ``rewrite`` with the function name (for example ``unfold foo`` or ``simp [foo]``, where ``foo`` is the function defined with well-founded recursion).
```lean
namespace Hide
@@ -528,9 +569,53 @@ by rw [div]; rfl
end Hide
```
If Lean cannot find a permutation of the arguments for which all recursive calls are decreasing, it will print a table that contains, for every recursive call, which arguments Lean could prove to be decreasing. For example, a function with three recursive calls and four parameters might cause the following message to be printed
```
example.lean:37:0-43: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 x4
1) 39:6-27 = = _ =
2) 40:6-25 = ? _ <
3) 41:6-25 < _ _ _
Please use `termination_by` to specify a decreasing measure.
```
This table should be read as follows:
* In the first recursive call, in line 39, arguments 1, 2 and 4 are equal to the function's parameters.
* The second recursive call, in line 40, has an equal first argument, a smaller fourth argument, and nothing could be inferred for the second argument.
* The third recursive call, in line 41, has a decreasing first argument.
* No other proofs were attempted, either because the parameter has a type without a non-trivial ``WellFounded`` instance (parameter 3), or because it is already clear that no decreasing measure can be found.
Lean will print the termination argument it found if ``set_option showInferredTerminationBy true`` is set.
If Lean does not find the termination argument, or if you want to be explicit, you can append a `termination_by` clause to the function definition, after the function's body, but before the `where` clause if present. It is of the form
```
termination_by e
```
where ``e`` is an expression that depends on the parameters of the function and should be decreasing at each recursive call. The type of `e` should be an instance of the class ``WellFoundedRelation``, which determines how to compare two values of that type.
If ``f`` has parameters “after the ``:``” (for example when defining functions via patterns using `|`), then these can be brought into scope using the syntax
```
termination_by a₁ … aₙ => e
```
By default, Lean uses the tactic ``decreasing_tactic`` when proving that an argument is decreasing; see its documentation for how to globally extend it. You can also choose to use a different tactic for a given function definition with the clause
```
decreasing_by <tac>
```
which should come after ``termination_by`, if present.
Note that recursive definitions can in general require nested recursions, that is, recursion on different arguments of ``foo`` in the template above. The equation compiler handles this by abstracting later arguments, and recursively defining higher-order functions to meet the specification.
The equation compiler also allows mutual recursive definitions, with a syntax similar to that of [Mutual and Nested Inductive Definitions](#mutual-and-nested-inductive-definitions). They are compiled using well-founded recursion, and so once again the defining equations hold only propositionally.
Mutual recursion
----------------
The equation compiler also allows mutual recursive definitions, with a syntax similar to that of [Mutual and Nested Inductive Definitions](#mutual-and-nested-inductive-definitions). Mutual definitions are always compiled using well-founded recursion, and so once again the defining equations hold only propositionally.
```lean
mutual
@@ -587,29 +672,31 @@ def num_consts_lst : List Term → Nat
end
```
The case where patterns are matched against an argument whose type is an inductive family is known as *dependent pattern matching*. This is more complicated, because the type of the function being defined can impose constraints on the patterns that are matched. In this case, the equation compiler will detect inconsistent cases and rule them out.
In a set of mutually recursive function, either all or no functions must have an explicit termination argument (``termination_by``). A change of the default termination tactic (``decreasing_by``) only affects the proofs about the recursive calls of that function, not the other functions in the group.
```lean
universe u
```
mutual
theorem even_of_odd_succ : ∀ n, Odd (n + 1) → Even n
| _, odd_succ n h => h
termination_by n h => h
decreasing_by decreasing_tactic
inductive Vector (α : Type u) : Nat → Type u
| nil : Vector α 0
| cons : α → Vector α n → Vector α (n+1)
theorem odd_of_even_succ : ∀ n, Even (n + 1) → Odd n
| _, even_succ n h => h
termination_by n h => h
end
```
namespace Vector
Another way to express mutual recursion is using local function definitions in ``where`` or ``let rec`` clauses: these can be mutually recursive with each other and their containing function:
def head {α : Type} : Vector α (n+1) → α
| cons h t => h
def tail {α : Type} : Vector α (n+1) → Vector α n
| cons h t => t
def map {α β γ : Type} (f : α → β → γ) :
∀ {n}, Vector α n → Vector β n → Vector γ n
| 0, nil, nil => nil
| n+1, cons a va, cons b vb => cons (f a b) (map f va vb)
end Vector
```
theorem even_of_odd_succ : ∀ n, Odd (n + 1) → Even n
| _, odd_succ n h => h
termination_by n h => h
where
theorem odd_of_even_succ : ∀ n, Even (n + 1) → Odd n
@@ -53,10 +53,59 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
Its runtime value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`).
* A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
* Any other type is represented by `lean_object *`.
Its runtime value is a pointer to an object of a subtype of `lean_object` (see respective declarations in `lean.h`) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
Example: the runtime value of `u : Unit` is always `lean_box(0)`.
#### Inductive types
For inductive types which are in the fallback `lean_object *` case above and not trivial constructors, the type is stored as a `lean_ctor_object`, and `lean_is_ctor` will return true. A `lean_ctor_object` stores the constructor index in the header, and the fields are stored in the `m_objs` portion of the object.
The memory order of the fields is derived from the types and order of the fields in the declaration. They are ordered as follows:
* Non-scalar fields stored as `lean_object *`
* Fields of type `USize`
* Other scalar fields, in decreasing order by size
Within each group the fields are ordered in declaration order. **Warning**: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose.
* To access fields of the first kind, use `lean_ctor_get(val, i)` to get the `i`th non-scalar field.
* To access `USize` fields, use `lean_ctor_get_usize(val, n+i)` to get the `i`th usize field and `n` is the total number of fields of the first kind.
* To access other scalar fields, use `lean_ctor_get_uintN(val, off)` or `lean_ctor_get_usize(val, off)` as appropriate. Here `off` is the byte offset of the field in the structure, starting at `n*sizeof(void*)` where `n` is the number of fields of the first two kinds.
For example, a structure such as
```lean
structure S where
ptr_1 : Array Nat
usize_1 : USize
sc64_1 : UInt64
ptr_2 : { x : UInt64 // x > 0 } -- wrappers don't count as scalars
sc64_2 : Float -- `Float` is 64 bit
sc8_1 : Bool
sc16_1 : UInt16
sc8_2 : UInt8
sc64_3 : UInt64
usize_2 : USize
ptr_3 : Char -- trivial wrapper around `UInt32`
sc32_1 : UInt32
sc16_2 : UInt16
```
would get re-sorted into the following memory order:
By default, all `lean_object *` parameters of an `@[extern]` function are considered *owned*, i.e. the external code is passed a "virtual RC token" and is responsible for passing this token along to another consuming function (exactly once) or freeing it via `lean_dec`.
@@ -111,6 +160,15 @@ if (lean_io_result_is_ok(res)) {
lean_io_mark_end_initialization();
```
In addition, any other thread not spawned by the Lean runtime itself must be initialized for Lean use by calling
```c
void lean_initialize_thread();
```
and should be finalized in order to free all thread-local resources by calling
```c
void lean_finalize_thread();
```
## `@[extern]` in the Interpreter
The interpreter can run Lean declarations for which symbols are available in loaded shared libraries, which includes `@[extern]` declarations.
@@ -121,4 +179,4 @@ Thus to e.g. run `#eval` on such a declaration, you need to
Note that it is not sufficient to load the foreign library containing the external symbol because the interpreter depends on code that is emitted for each `@[extern]` declaration.
Thus it is not possible to interpret an `@[extern]` declaration in the same file.
See `tests/compiler/foreign` for an example.
See [`tests/compiler/foreign`](https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign/) for an example.
You can use `elantoolchain link` to give a specific stage build
directory a reference name, then use `elan override set` to associate
such a name to the current directory. We usually want to use `stage0`
for editing files in `src` and `stage1`for everything else (e.g.
tests).
The `lean-toolchain` files in the Lean 4 repository are set up to use the `lean4-stage0`
toolchain for editing files in `src` and the `lean4` toolchain for editing files in `tests`.
Run the following commands to make `lean4` point at `stage1` and `lean4-stage0`point at `stage0`:
```bash
# in the Lean rootdir
elan toolchain link lean4 build/release/stage1
elan toolchain link lean4-stage0 build/release/stage0
# make `lean` etc. point to stage1 in the rootdir and subdirs
elan override set lean4
cd src
# make `lean` etc. point to stage0 anywhere inside `src`
elan override set lean4-stage0
```
You can also use the `+toolchain` shorthand (e.g. `lean +lean4-debug`) to switch
@@ -65,9 +59,24 @@ If you push `my-tag` to a fork in your github account `my_name`,
you can then put `my_name/lean4:my-tag` in your `lean-toolchain` file in a project using `lake`.
(You must use a tag name that does not start with a numeral, or contain `_`).
### VS Code
There is a `lean.code-workspace` file that correctly sets up VS Code with workspace roots for the stage0/stage1 setup described above as well as with other settings.
You should always load it when working on Lean, such as by invoking
```
code lean.code-workspace
```
on the command line.
### `ccache`
Lean's build process uses [`ccache`](https://ccache.dev/) if it is
installed to speed up recompilation of the generated C code. Without
`ccache`, you'll likely spend more time than necessary waiting on
rebuilds - it's a good idea to make sure it's installed.
### `prelude`
Unlike most Lean projects, all submodules of the `Lean` module begin with the
`prelude` keyword. This disables the automated import of `Init`, meaning that
developers need to figure out their own subset of `Init` to import. This is done
such that changing files in `Init` doesn't force a full rebuild of `Lean`.
This checklist walks you through releasing a stable version.
See below for the checklist for release candidates.
We'll use `v4.6.0` as the intended release version as a running example.
- One week before the planned release, ensure that (1) someone has written the release notes and (2) someone has written the first draft of the release blog post.
If there is any material in `./releases_drafts/`, then the release notes are not done. (See the section "Writing the release notes".)
-`git checkout releases/v4.6.0`
(This branch should already exist, from the release candidates.)
-`git pull`
- In `src/CMakeLists.txt`, verify you see
-`set(LEAN_VERSION_MINOR 6)` (for whichever `6` is appropriate)
-`set(LEAN_VERSION_IS_RELEASE 1)`
- (both of these should already be in place from the release candidates)
-`git tag v4.6.0`
-`git push $REMOTE v4.6.0`, where `$REMOTE` is the upstream Lean repository (e.g., `origin`, `upstream`)
- Now wait, while CI runs.
- You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`,
looking for the `v4.6.0` tag.
- This step can take up to an hour.
- If you are intending to cut the next release candidate on the same day,
you may want to start on the release candidate checklist now.
- Go to https://github.com/leanprover/lean4/releases and verify that the `v4.6.0` release appears.
- Edit the release notes on Github to select the "Set as the latest release".
- Follow the instructions in creating a release candidate for the "GitHub release notes" step,
now that we have a written `RELEASES.md` section.
Do a quick sanity check.
- Next, we will move a curated list of downstream repos to the latest stable release.
- For each of the repositories listed below:
- Make a PR to `master`/`main` changing the toolchain to `v4.6.0`
- Update the toolchain file
- In the Lakefile, if there are dependencies on specific version tags of dependencies that you've already pushed as part of this process, update them to the new tag.
If they depend on `main` or `master`, don't change this; you've just updated the dependency, so it will work and be saved in the manifest
- Run `lake update`
- The PR title should be "chore: bump toolchain to v4.6.0".
- Merge the PR once CI completes.
- Create the tag `v4.6.0` from `master`/`main` and push it.
- Merge the tag `v4.6.0` into the `stable` branch and push it.
- In `RELEASES.md` replace `Development in progress` in the `v4.7.0` section with `Release notes to be written.`
- We will rely on automatically generated release notes for release candidates,
and the written release notes will be used for stable versions only.
It is essential to choose the nightly that will become the release candidate as early as possible, to avoid confusion.
- In `src/CMakeLists.txt`,
- verify that you see `set(LEAN_VERSION_MINOR 7)` (for whichever `7` is appropriate); this should already have been updated when the development cycle began.
- `set(LEAN_VERSION_IS_RELEASE 1)` (this should be a change; on `master` and nightly releases it is always `0`).
- Commit your changes to `src/CMakeLists.txt`, and push.
- `git tag v4.7.0-rc1`
- `git push origin v4.7.0-rc1`
- Ping the FRO Zulip that release notes need to be written. The release notes do not block completing the rest of this checklist.
- Now wait, while CI runs.
- You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`, looking for the `v4.7.0-rc1` tag.
- This step can take up to an hour.
- (GitHub release notes) Once the release appears at https://github.com/leanprover/lean4/releases/
- Edit the release notes on Github to select the "Set as a pre-release box".
- If release notes have been written already, copy the section of `RELEASES.md` for this version into the Github release notes
and use the title "Changes since v4.6.0 (from RELEASES.md)".
- Otherwise, in the "previous tag" dropdown, select `v4.6.0`, and click "Generate release notes".
This will add a list of all the commits since the last stable version.
- Delete anything already mentioned in the hand-written release notes above.
- Delete "update stage0" commits, and anything with a completely inscrutable commit message.
- Briefly rearrange the remaining items by category (e.g. `simp`, `lake`, `bug fixes`),
but for minor items don't put any work in expanding on commit messages.
- (How we want to release notes to look is evolving: please update this section if it looks wrong!)
- Next, we will move a curated list of downstream repos to the release candidate.
- This assumes that there is already a *reviewed* branch `bump/v4.7.0` on each repository
containing the required adaptations (or no adaptations are required).
The preparation of this branch is beyond the scope of this document.
- For each of the target repositories:
- Checkout the `bump/v4.7.0` branch.
- Verify that the `lean-toolchain` is set to the nightly from which the release candidate was created.
- `git merge origin/master`
- Change the `lean-toolchain` to `leanprover/lean4:v4.7.0-rc1`
- In `lakefile.lean`, change any dependencies which were using `nightly-testing` or `bump/v4.7.0` branches
back to `master` or `main`, and run `lake update` for those dependencies.
- Run `lake build` to ensure that dependencies are found (but it's okay to stop it after a moment).
- `git commit`
- `git push`
- Open a PR from `bump/v4.7.0` to `master`, and either merge it yourself after CI, if appropriate,
or notify the maintainers that it is ready to go.
- Once this PR has been merged, tag `master` with `v4.7.0-rc1` and push this tag.
- We do this for the same list of repositories as for stable releases, see above.
As above, there are dependencies between these, and so the process above is iterative.
It greatly helps if you can merge the `bump/v4.7.0` PRs yourself!
It is essential for Mathlib CI that you then create the next `bump/v4.8.0` branch
for the next development cycle.
Set the `lean-toolchain` file on this branch to same `nightly` you used for this release.
- For Batteries/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
`nightly-testing-2024-02-29` with date corresponding to the nightly used for the release
(create it if not), and then on the `nightly-testing` branch `git reset --hard master`, and force push.
- Make an announcement!
This should go in https://leanprover.zulipchat.com/#narrow/stream/113486-announce, with topic `v4.7.0-rc1`.
Please see previous announcements for suggested language.
You will want a few bullet points for main topics from the release notes.
Please also make sure that whoever is handling social media knows the release is out.
- Begin the next development cycle (i.e. for `v4.8.0`) on the Lean repository, by making a PR that:
- Updates `src/CMakeLists.txt` to say `set(LEAN_VERSION_MINOR 8)`
- Replaces the "development in progress" in the `v4.7.0` section of `RELEASES.md` with
```
Release candidate, release notes will be copied from `branch releases/v4.7.0` once completed.
```
and inserts the following section before that section:
```
v4.8.0
----------
Development in progress.
```
- Removes all the entries from the `./releases_drafts/` folder.
## Time estimates:
Slightly longer than the corresponding steps for a stable release.
Similar process, but more things go wrong.
In particular, updating the downstream repositories is significantly more work
(because we need to merge existing `bump/v4.7.0` branches, not just update a toolchain).
# Preparing `bump/v4.7.0` branches
While not part of the release process per se,
this is a brief summary of the work that goes into updating Batteries/Aesop/Mathlib to new versions.
Please remember to push any merges you make to intermediate steps!
# Writing the release notes
We are currently trying a system where release notes are compiled all at once from someone looking through the commit history.
The exact steps are a work in progress.
Here is the general idea:
* The work is done right on the `releases/v4.6.0` branch sometime after it is created but before the stable release is made.
The release notes for `v4.6.0` will be copied to `master`.
* There can be material for release notes entries in commit messages.
* There can also be pre-written entries in `./releases_drafts`, which should be all incorporated in the release notes and then deleted from the branch.
See `./releases_drafts/README.md` for more information.
* The release notes should be written from a downstream expert user's point of view.
This section will be updated when the next release notes are written (for `v4.10.0`).
@@ -5,7 +5,6 @@ After [building Lean](../make/index.md) you can run all the tests using
cd build/release
make test ARGS=-j4
```
Change the 4 to the maximum number of parallel tests you want to
allow. The best choice is the number of CPU cores on your machine as
the tests are mostly CPU bound. You can find the number of processors
@@ -17,6 +16,12 @@ adding the `-C stageN` argument. The default when run as above is stage 1. The
Lean tests will automatically use that stage's corresponding Lean
executables
Running `make test` will not pick up new test files; run
```bash
cmake build/release/stage1
```
to update the list of tests.
You can also use `ctest` directly if you are in the right folder. So
to run stage1 tests with a 300 second timeout run this:
@@ -24,6 +29,9 @@ to run stage1 tests with a 300 second timeout run this:
cd build/release/stage1
ctest -j 4 --output-on-failure --timeout 300
```
Useful `ctest` flags are `-R <name of test>` to run a single test, and
`--rerun-failed` to run all tests that failed during the last run.
You can also pass `ctest` flags via `make test ARGS="--rerun-failed"`.
To get verbose output from ctest pass the `--verbose` command line
option. Test output is normally suppressed and only summary
@@ -33,17 +41,17 @@ information is displayed. This option will show all test output.
All these tests are included by [src/shell/CMakeLists.txt](https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt):
-`tests/lean`: contains tests that come equipped with a
.lean.expected.out file. The driver script `test_single.sh` runs
-[`tests/lean`](https://github.com/leanprover/lean4/tree/master/tests/lean/): contains tests that come equipped with a
.lean.expected.out file. The driver script [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/test_single.sh) runs
each test and checks the actual output (*.produced.out) with the
checked in expected output.
-`tests/lean/run`: contains tests that are run through the lean
-[`tests/lean/run`](https://github.com/leanprover/lean4/tree/master/tests/lean/run/): contains tests that are run through the lean
command line one file at a time. These tests only look for error
codes and do not check the expected output even though output is
produced, it is ignored.
-`tests/lean/interactive`: are designed to test server requests at a
-[`tests/lean/interactive`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/): are designed to test server requests at a
given position in the input file. Each .lean file contains comments
that indicate how to simulate a client request at that position.
using a `--^` point to the line position. Example:
@@ -53,7 +61,7 @@ All these tests are included by [src/shell/CMakeLists.txt](https://github.com/le
Bla.
--^ textDocument/completion
```
In this example, the test driver `test_single.sh` will simulate an
In this example, the test driver [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/test_single.sh) will simulate an
auto-completion request at `Bla.`. The expected output is stored in
a .lean.expected.out in the json format that is part of the
[Language Server
@@ -70,21 +78,21 @@ All these tests are included by [src/shell/CMakeLists.txt](https://github.com/le
--^ collectDiagnostics
```
- `tests/lean/server`: Tests more of the Lean `--server` protocol.
- [`tests/lean/server`](https://github.com/leanprover/lean4/tree/master/tests/lean/server/): Tests more of the Lean `--server` protocol.
There are just a few of them, and it uses .log files containing
JSON.
- `tests/compiler`: contains tests that will run the Lean compiler and
- [`tests/compiler`](https://github.com/leanprover/lean4/tree/master/tests/compiler/): contains tests that will run the Lean compiler and
build an executable that is executed and the output is compared to
the .lean.expected.out file. This test also contains a subfolder
`foreign` which shows how to extend Lean using C++.
[`foreign`](https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign/) which shows how to extend Lean using C++.
- `tests/lean/trust0`: tests that run Lean in a mode that Lean doesn't
- [`tests/lean/trust0`](https://github.com/leanprover/lean4/tree/master/tests/lean/trust0): tests that run Lean in a mode that Lean doesn't
- `tests/plugin`: tests that compiled Lean code can be loaded into
- [`tests/plugin`](https://github.com/leanprover/lean4/tree/master/tests/plugin/): tests that compiled Lean code can be loaded into
`lean` via the `--plugin` command line option.
## Writing Good Tests
@@ -95,7 +103,7 @@ Every test file should contain:
and, if not 100% clear, why that is the desirable behavior
At the time of writing, most tests do not follow these new guidelines yet.
For an example of a conforming test, see `tests/lean/1971.lean`.
For an example of a conforming test, see [`tests/lean/1971.lean`](https://github.com/leanprover/lean4/tree/master/tests/lean/1971.lean).
## Fixing Tests
@@ -111,7 +119,7 @@ First, we must install [meld](http://meldmerge.org/). On Ubuntu, we can do it by
sudo apt-get install meld
```
Now, suppose `bad_class.lean` test is broken. We can see the problem by going to `tests/lean` directory and
Now, suppose `bad_class.lean` test is broken. We can see the problem by going to [`tests/lean`](https://github.com/leanprover/lean4/tree/master/tests/lean) directory and
executing
```
@@ -124,8 +132,3 @@ outputs. `meld` can also be used to repair the problems.
In Emacs, we can also execute `M-x lean4-diff-test-file` to check/diff the file of the current buffer.
To mass-copy all `.produced.out` files to the respective `.expected.out` file, use `tests/lean/copy-produced`.
When using the Nix setup, add `--keep-failed` to the `nix build` call and then call
By default, Lean only accepts total functions. The `partial` keyword should be used when Lean cannot
establish that a function always terminates.
By default, Lean only accepts total functions.
The `partial` keyword may be used to define a recursive function without a termination proof; `partial` functions compute in compiled programs, but are opaque in proofs and during type checking.
These are instructions to set up a working development environment for those who wish to make changes to Lean itself. It is part of the [Development Guide](doc/dev/index.md).
We strongly suggest that new users instead follow the [Quickstart](doc/quickstart.md) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.
Requirements
------------
@@ -10,49 +14,34 @@ Platform-Specific Setup
- [Linux (Ubuntu)](ubuntu.md)
- [Windows (msys2)](msys2.md)
- [Windows (Visual Studio)](msvc.md)
- [Windows (WSL)](wsl.md)
- [macOS (homebrew)](osx-10.9.md)
- Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix-shell` in the project root. That's it.
- There is also an [**experimental** setup based purely on Nix](nix.md) that works fundamentally differently from the
make/CMake setup described on this page.
- Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix develop` in the project root. That's it.
make -C build/release -j$(nproc)# see below for macOS
```
For regular development, we recommend running
```bash
git config submodule.recurse true
```
in the checkout so that `--recurse-submodules` doesn't have to be
specified with `git pull/checkout/...`.
You can replace `$(nproc)`, which is not available on macOS and some alternative shells, with the desired parallelism amount.
The above commands will compile the Lean library and binaries into the
`stage1` subfolder; see below for details. Add `-j N` for an
appropriate `N` to `make` for a parallel build.
`stage1` subfolder; see below for details.
For example, on an AMD Ryzen 9`make` takes 00:04:55, whereas `make -j 10`
takes 00:01:38. Your results may vary depending on the speed of your hard
drive.
You should not usually run `make install` after a successful build.
You should not usually run`cmake --install` after a successful build.
See [Dev setup using elan](../dev/index.md#dev-setup-using-elan) on how to properly set up your editor to use the correct stage depending on the source directory.
Useful CMake Configuration Settings
-----------------------------------
Pass these along with the `cmake ../..` command.
Pass these along with the `cmake --preset release` command.
There are also two alternative presets that combine some of these options you can use instead of `release`: `debug` and `sandebug` (sanitize + debug).
*`-D CMAKE_BUILD_TYPE=`\
Select the build type. Valid values are `RELEASE` (default), `DEBUG`,
While [Nix](https://nixos.org/nix/) can be used to quickly open a shell with all dependencies for the [standard setup](index.md) installed, the user-facing [Nix Setup](../setup.md#nix-setup) can also be used to work *on* Lean.
## Setup
Follow the setup in the link above; to open the Lean shell inside a Lean checkout, you can also use
```bash
# in the Lean root directory
$ nix-shell -A nix
```
On top of the local and remote Nix cache, we do still rely on CCache as well to make C/C++ build steps incremental, which are atomic steps from Nix's point of view.
To enable CCache, add the following line to the config file mentioned in the setup:
```bash
extra-sandbox-paths = /nix/var/cache/ccache
```
Then set up that directory as follows:
```bash
sudo mkdir -m0770 -p /nix/var/cache/ccache
# macOS standard chown doesn't support --reference
From the Lean root directory inside the Lean shell:
```bash
nix build .#stage1 # build this stage's stdlib & executable
nix build .#stage1.test # run all tests
nix run .#stage1.update-stage0 # update ./stage0 from this stage
nix run .#stage1.update-stage0-commit # ...and commit the results
```
The `stage1.` part in each command is optional:
```bash
nix build .#test # run tests for stage 1
nix build . # build stage 1
nix build # ditto
```
## Build Process Description
The Nix build process conceptually works the same as described in [Lean Build Pipeline](index.md#lean-build-pipeline).
However, there are two important differences in practice apart from the standard Nix properties (hermeneutic, reproducible builds stored in a global hash-indexed store etc.):
* Only files tracked by git (using `git add` or at least `git add --intent-to-add`) are compiled.
This is actually a general property of Nix flakes, and has the benefit of making it basically impossible to forget to commit a file (at least in `src/`).
* Only files reachable from `src/Lean.lean` are compiled.
This is because modules are discovered not from a directory listing anymore but by recursively compiling all dependencies of that top module.
## Editor Integration
As in the standard Nix setup.
After adding `src/` as an LSP workspace, it should automatically fall back to using stage 0 in there.
Note that the UX of `{emacs,vscode}-dev` is quite different from the Make-based setup regarding the compilation of dependencies:
there is no mutable directory incrementally filled by the build that we could point the editor at for .olean files.
Instead, `emacs-dev` will gather the individual dependency outputs from the Nix store when checking a file -- and build them on the fly when necessary.
However, it will only ever load changes saved to disk, not ones opened in other buffers.
The absence of a mutable output directory also means that the Lean server will not automatically pick up `.ilean` metadata from newly compiled files.
Instead, you can run `nix run .#link-ilean` to symlink the `.ilean` tree of the stdlib state at that point in time to `src/build/lib`, where the server should automatically find them.
## Other Fun Stuff to Do with Nix
Open Emacs with Lean set up from an arbitrary commit (without even cloning Lean beforehand... if your Nix is new enough):
```bash
nix run github:leanprover/lean4/7e4edeb#emacs-package
```
Open a shell with `lean` and `LEAN_PATH` set up for compiling a specific module (this is exactly what `emacs-dev` is doing internally):
```bash
nix develop .#mods.\"Lean.Parser.Basic\"
# alternatively, directly pass a command to execute:
1. Launch VS Code and install the `lean4` extension.
1. Launch VS Code and install the `lean4` extension by clicking on the "Extensions" sidebar entry and searching for "lean4".
1.Create a new file using "File > New Text File" (`Ctrl+N`). Click the `Select a language` prompt, type in `lean4`, and hit ENTER. You should see the following popup:
1.Open the Lean 4 setup guide by creating a new text file using "File > New Text File" (`Ctrl+N`), clicking on the ∀-symbol in the top right and selecting "Documentation… > Setup: Show Setup Guide".
Click the "Install Lean using Elan" button. You should see some progress output like this:
```
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.0.0
info: downloading component 'lean'
```
If there is no popup, you probably have Elan installed already.
You may want to make sure that your default toolchain is Lean 4 in this case by running `elan default leanprover/lean4:stable` and reopen the file, as the next step will fail otherwise.
1. Follow the Lean 4 setup guide. It will walk you through learning resources for Lean 4, teach you how to set up Lean's dependencies on your platform, install Lean 4 for you at the click of a button and help you set up your first project.
1. While it is installing, you can paste the following Lean program into the new file:
```lean
#eval Lean.versionString
```
When the installation has finished, the Lean Language Server should start automatically and you should get syntax-highlighting and a "Lean Infoview" popping up on the right. You will see the output of the `#eval` statement when
you place your cursor at the end of the statement.
You are set up!
## Create a Lean Project
*If your goal is to contribute to [mathlib4](https://github.com/leanprover-community/mathlib4) or use it as a dependency, please see its readme for specific instructions on how to do that.*
You can now create a Lean project in a new folder. Run `lake init foo` from "View > Terminal" to create a package, followed by `lake build` to get an executable version of your Lean program.
On Linux/macOS, you first have to follow the instructions printed by the Lean installation or log out and in again for the Lean executables to be available in you terminal.
Note: Packages **have** to be opened using "File > Open Folder..." for imports to work.
Saved changes are visible in other files after running "Lean 4: Refresh File Dependencies" (`Ctrl+Shift+X`).
## Troubleshooting
**The InfoView says "Waiting for Lean server to start..." forever.**
Check that the VS Code Terminal is not showing some installation errors from `elan`.
If that doesn't work, try also running the VS Code command `Developer: Reload Window`.
An alternative setup based on Nix provides a perfectly reproducible development environment for your project from the Lean version down to the editor and Lean extension.
However, it is still experimental and subject to change; in particular, it is heavily based on an unreleased version of Nix enabling [Nix Flakes](https://www.tweag.io/blog/2020-05-25-flakes/). The setup has been tested on NixOS, other Linux distributions, and macOS.
After installing (any version of) Nix (<https://nixos.org/download.html>), you can easily open a shell with the particular pre-release version of Nix needed by and tested with our setup (called the "Lean shell" from here on):
```bash
$ nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix
```
While this shell is sufficient for executing the steps below, it is recommended to also set the following options in `/etc/nix/nix.conf` (`nix.extraOptions` in NixOS):
```
max-jobs = auto # Allow building multiple derivations in parallel
keep-outputs = true # Do not garbage-collect build time-only dependencies (e.g. clang)
# Allow fetching build results from the Lean Cachix cache
On a multi-user installation of Nix (the default), you need to restart the Nix daemon afterwards:
```bash
sudo pkill nix-daemon
```
The [Cachix](https://cachix.org/) integration will magically beam any build steps already executed by the CI right onto your machine when calling Nix commands in the shell opened above.
It can be set up analogously as a cache for your own project.
Note: Your system Nix might print warnings about not knowing some of the settings used by the Lean shell Nix, which can be ignored.
## Basic Commands
From a Lean shell, run
```bash
$ nix flake new mypkg -t github:leanprover/lean4
```
to create a new Lean package in directory `mypkg` using the latest commit of Lean 4.
Such packages follow the same directory layout as described in the standard setup, except for a `lakefile.lean` replaced by a `flake.nix` file set up so you can run Nix commands on it, for example:
$ nix run .#emacs-dev # open a pinned version of Emacs with lean4-mode fully set up
$ nix run .#emacs-dev MyPackage.lean # arguments can be passed as well, e.g. the file to open
$ nix run .#vscode-dev MyPackage.lean # ditto, using VS Code
```
Note that if you rename `MyPackage.lean`, you also have to adjust the `name` attribute in `flake.nix` accordingly.
Also note that if you turn the package into a Git repository, only tracked files will be visible to Nix.
As in the standard setup, changes need to be saved to be visible in other files, which have then to be invalidated via an editor command.
If you don't want to or cannot start the pinned editor from Nix, e.g. because you're running Lean inside WSL/a container/on a different machine, you can manually point your editor at the `lean` wrapper script the commands above use internally:
```bash
$ nix build .#lean-dev -o result-lean-dev
```
The resulting `./result-lean-dev/bin/lean` script essentially runs `nix run .#lean` in the current project's root directory when you open a Lean file or use the "refresh dependencies" command such that the correct Lean version for that project is executed.
This includes selecting the correct stage of Lean (which it will compile on the fly, though without progress output) if you are [working on Lean itself](./make/nix.md#editor-integration).
Package dependencies can be added as further input flakes and passed to the `deps` list of `buildLeanPackage`. Example: <https://github.com/Kha/testpkg2/blob/master/flake.nix#L5>
For hacking, it can be useful to temporarily override an input with a local checkout/different version of a dependency:
On a build error, Nix will show the last 10 lines of the output by default. You can pass `-L` to `nix build` to show all lines, or pass the shown `*.drv` path to `nix log` to show the full log after the fact.
Keeping all outputs ever built on a machine alive can accumulate to quite impressive amounts of disk space, so you might want to trigger the Nix GC when `/nix/store/` has grown too large:
```bash
nix-collect-garbage
```
This will remove everything not reachable from "GC roots" such as the `./result` symlink created by `nix build`.
Note that the package information in `flake.nix` is currently completely independent from `lakefile.lean` used in the standard setup.
First [install Pygments](https://pygments.org/download/). Then save [`lean4.py`](https://raw.githubusercontent.com/leanprover/lean4/master/doc/latex/lean4.py), which contains an version of the Lean highlighter updated for Lean 4, and the following sample LaTeX file `test.tex` into the same directory:
First [install Pygments](https://pygments.org/download/) (version 2.18 or newer).
Then save the following sample LaTeX file `test.tex` into the same directory:
```latex
\documentclass{article}
@@ -51,9 +52,8 @@ First [install Pygments](https://pygments.org/download/). Then save [`lean4.py`]
% switch to a monospace font supporting more Unicode characters
- either `xelatex` or `lualatex` is required to handle Unicode characters in the code.
-`--shell-escape` is needed to allow `xelatex` to execute `pygmentize` in a shell.
- If the chosen monospace font is missing some Unicode symbols, you can direct them to be displayed using a fallback font or other replacement LaTeX code.
``` latex
\usepackage{newunicodechar}
\newfontfamily{\freeserif}{DejaVu Sans}
\newunicodechar{✝}{\freeserif{✝}}
\newunicodechar{𝓞}{\ensuremath{\mathcal{O}}}
```
- minted has a "helpful" feature that draws red boxes around characters the chosen lexer doesn't recognize.
Since the Lean lexer cannot encompass all user-defined syntax, it is advisable to [work around](https://tex.stackexchange.com/a/343506/14563) this feature.
``` latex
\usepackage{newunicodechar}
\newfontfamily{\freeserif}{DejaVu Sans}
\newunicodechar{✝}{\freeserif{✝}}
\newunicodechar{𝓞}{\ensuremath{\mathcal{O}}}
```
- If you are using an old version of Pygments, you can copy
[`lean.py`](https://raw.githubusercontent.com/pygments/pygments/master/pygments/lexers/lean.py) into your working directory,
and use `lean4.py:Lean4Lexer -x` instead of `lean4` above.
If your version of `minted` is v2.7 or newer, but before v3.0,
you will additionally need to follow the workaround described in https://github.com/gpoore/minted/issues/360.
A new linter flags situations where a local variable's name is one of
the argumentless constructors of its type. This can arise when a user either
doesn't open a namespace or doesn't add a dot or leading qualifier, as
in the following:
````
inductive Tree (α : Type) where
| leaf
| branch (left : Tree α) (val : α) (right : Tree α)
def depth : Tree α → Nat
| leaf => 0
````
With this linter, the `leaf` pattern is highlighted as a local
variable whose name overlaps with the constructor `Tree.leaf`.
The linter can be disabled with `set_option linter.constructorNameAsVariable false`.
Additionally, the error message that occurs when a name in a pattern that takes arguments isn't valid now suggests similar names that would be valid. This means that the following definition:
```
def length (list : List α) : Nat :=
match list with
| nil => 0
| cons x xs => length xs + 1
```
now results in the following warning:
```
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:
```
invalid pattern, constructor or constant marked with '[match_pattern]' expected
@@ -20,8 +20,29 @@ def Functor.discard {f : Type u → Type v} {α : Type u} [Functor f] (x : f α)
exportFunctor(discard)
/--
An `Alternative` functor is an `Applicative` functor that can "fail" or be "empty"
and a binary operation `<|>` that “collects values” or finds the “left-most success”.
Important instances include
* `Option`, where `failure := none` and `<|>` returns the left-most `some`.
* Parser combinators typically provide an `Applicative` instance for error-handling and
backtracking.
Error recovery and state can interact subtly. For example, the implementation of `Alternative` for `OptionT (StateT σ Id)` keeps modifications made to the state while recovering from failure, while `StateT σ (OptionT Id)` discards them.
-/
-- NB: List instance is in mathlib. Once upstreamed, add
-- * `List`, where `failure` is the empty list and `<|>` concatenates.
Some files were not shown because too many files have changed in this diff
Show More
Reference in New Issue
Block a user
Blocking a user prevents them from interacting with repositories, such as opening or commenting on pull requests or issues. Learn more about blocking a user.
