This PR adjusts the way the pretty printer unresolves names. It used to
make use of all `export`s when pretty printing, but now it only uses
`export`s that put names into parent namespaces (heuristic: these are
"API exports" that are intended by the library author), rather than
"horizontal exports" that put the names into an unrelated namespace,
which the dot notation feature in #6189 now incentivizes.
Closes the already closed#2524
This PR adds `BitVec.[toFin|getMsbD]_setWidth` and
`[getMsb|msb]_signExtend` as well as `ofInt_toInt`.
Also correct renamed the misnamed theorem for
`signExtend_eq_setWidth_of_msb_false`.
---------
Co-authored-by: Siddharth <siddu.druid@gmail.com>
This PR adds docstrings to `Expr.hasLooseBVars` and `Expr.hasLooseBVar`,
to clarify the difference between these functions, and to document that
the former traverses the expression, while the latter is constant-time,
using cached information.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR removes the deprecated aliases `Int.div := Int.tdiv` and
`Int.mod := Int.tmod`. Later we will rename `Int.ediv` to `Int.div` and
`Int.emod` to `Int.mod`.
This PR removes unnecessary parameters from the funcion induction
principles. This is a breaking change; broken code can typically be adjusted
simply by passing fewer parameters.
Part 2, adjusting after stage0 update.
Closes#6320
This PR removes unnecessary parameters from the funcion induction
principles. This is a breaking change; broken code can typically be adjusted
simply by passing fewer parameters.
Part 1, before stage0 update.
Closes#6320
This PR adds `protected` to `Fin.cast` and `BitVec.cast`, to avoid
confusion with `_root_.cast`. These should mostly be used via
dot-notation in any case.
This PR upstreams the `ToLevel` typeclass from mathlib and uses it to
fix the existing `ToExpr` instances so that they are truly universe
polymorphic (previously it generated malformed expressions when the
universe level was nonzero). We improve on the mathlib definition of
`ToLevel` to ensure the class always lives in `Type`, irrespective of
the universe parameter.
This implements part one of the plan to upstream a derive handler for
`ToExpr`, as discussed in #5906 and #5909.
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
This PR adds lemmas simplifying `for` loops over `Option` into
`Option.pelim`, giving parity with lemmas simplifying `for` loops of
`List` into `List.fold`.
This PR removes an unused import in the time library that can yield to
import cycles when building stuff that gets imported by `Std.Internal`
but also wants to import `Std.Time`.
This PR adds `BitVec.[toInt|toFin]_concat` and moves a couple of
theorems into the concat section, as `BitVec.msb_concat` is needed for
the `toInt_concat` proof.
We also add `Bool.toInt`.
This PR adds theorems characterizing the value of the unsigned shift
right of a bitvector in terms of its 2s complement interpretation as an
integer.
Unsigned shift right by at least one bit makes the value of the
bitvector less than or equal to `2^(w-1)`,
makes the interpretation of the bitvector `Int` and `Nat` agree.
In the case when `n = 0`, then the shift right value equals the integer
interpretation.
```lean
theorem toInt_ushiftRight_eq_ite {x : BitVec w} {n : Nat} :
(x >>> n).toInt = if n = 0 then x.toInt else x.toNat >>> n
```
```lean
theorem toFin_uShiftRight {x : BitVec w} {n : Nat} :
(x >>> n).toFin = x.toFin / (Fin.ofNat' (2^w) (2^n))
```
---------
Co-authored-by: Harun Khan <harun19@stanford.edu>
Co-authored-by: Tobias Grosser <github@grosser.es>
This PR changes the implementation of `HashMap.toList`, so the ordering
agrees with `HashMap.toArray`.
Currently there are no verification lemmas about `HashMap.toList`, so no
contract is being broken yet!
This PR moves `IO.Channel` and `IO.Mutex` from `Init` to `Std.Sync` and
renames them to `Std.Channel` and `Std.Mutex`.
Note that the original files are retained and the deprecation is written
manually as we cannot import `Std` from `Init` so this is the only way
to deprecate without a hard breaking change. In particular we do not yet
move `Std.Queue` from `Init` to `Std` both because it needs to be
retained for this deprecation to work but also because it is already
within the `Std` namespace and as such we cannot maintain two copies of
the file at once. After the deprecation period is finished `Std.Queue`
will find a new home in `Std.Data.Queue`.
This PR upstreams `List.length_flatMap`, `countP_flatMap` and
`count_flatMap` from Mathlib. These were not possible to state before we
upstreamed `List.sum`.
This PR makes some proofs more robust so they will still work with
`byAsSorry`. Unfortunately, they are not a complete fix and there are
remaining problems building with `byAsSorry`.
This PR ensures the the log error position is properly preserved when
prepending stray log entries to the job log. It also adds comparison
support for `Log.Pos`.
This PR uses Lean.RArray in bv_decide's reflection proofs. Giving
speedups on problems with lots of variables.
Implement like #6068, speedup:
```
# before
λ hyperfine "lean +nightly-2024-12-02 tests/lean/run/bv_reflection_stress.lean"
Benchmark 1: lean +nightly-2024-12-02 tests/lean/run/bv_reflection_stress.lean
Time (mean ± σ): 1.939 s ± 0.007 s [User: 1.549 s, System: 0.104 s]
Range (min … max): 1.928 s … 1.947 s 10 runs
# after
λ hyperfine "lean tests/lean/run/bv_reflection_stress.lean"
Benchmark 1: lean tests/lean/run/bv_reflection_stress.lean
Time (mean ± σ): 1.409 s ± 0.006 s [User: 1.058 s, System: 0.073 s]
Range (min … max): 1.401 s … 1.419 s 10 runs
```
This PR changes Lake's build process to no longer use `leanc` for
compiling C files or linking shared libraries and executables. Instead,
it directly invokes the bundled compiler (or the native compiler if
none) using the necessary flags.
This PR runs all linters for a single command (together) on a separate
thread from further elaboration, making a first step towards
parallelizing the elaborator.
This PR ensure `bv_decide` uses definitional equality in its reflection
procedure as much as possible. Previously it would build up explicit
congruence proofs for the kernel to check. This reduces the size of
proof terms passed to kernel speeds up checking of large reflection
proofs.
This PR reduces the import closure of `Std.Time` such that it doesn't
have to be rebuilt on every change in `Init.Data`.
Noticed while working on `Init` refactorings.
This PR fixes a bug in structure instance field completion that caused
it to not function correctly for bracketed structure instances written
in Mathlib style.
This PR completes the `toNat` theorems for the bitwise operations
(`and`, `or`, `xor`, `shiftLeft`, `shiftRight`) of the UInt types and
adds `toBitVec` theorems as well. It also renames `and_toNat` to
`toNat_and` to fit with the current naming convention.
This PR fixes a bug that could cause the `injectivity` tactic to fail in
reducible mode, which could cause unfolding lemma generation to fail
(used by tactics such as `unfold`). In particular,
`Lean.Meta.isConstructorApp'?` was not aware that `n + 1` is equivalent
to `Nat.succ n`.
Closes#5064
This PR introduces the basic theory of permutations of `Array`s and
proves `Array.swap_perm`.
The API falls well short of what is available for `List` at this point.
This PR refactors `Array.qsort` to remove runtime array bounds checks,
and avoids the use of `partial`. We use the `Vector` API, along with
auto_params, to avoid having to write any proofs. The new code
benchmarks indistinguishably from the old.
This PR puts code in terms of syntax quotations now that there has been
a stage0 update. Fixes a lingering bug in StructInst where some
intermediate syntax was malformed, but this had no observable effects
outside of some debug messages.
This PR modifies structure instance notation and `where` notation to use
the same notation for fields. Structure instance notation now admits
binders, type ascriptions, and equations, and `where` notation admits
full structure lvals. Examples of these for structure instance notation:
```lean
structure PosFun where
f : Nat → Nat
pos : ∀ n, 0 < f n
def p : PosFun :=
{ f n := n + 1
pos := by simp }
def p' : PosFun :=
{ f | 0 => 1
| n + 1 => n + 1
pos := by rintro (_|_) <;> simp }
```
Just like for the structure `where` notation, a field `f x y z : ty :=
val` expands to `f := fun x y z => (val : ty)`. The type ascription is
optional.
The PR also is setting things up for future expansion. Pending some
discussion, in the future structure/`where` notation could have have
embedded `where` clauses; rather than `{ a := { x := 1, y := z } }` one
could write `{ a where x := 1; y := z }`.
This PR implements `Simp.Config.implicitDefEqsProofs`. When `true`
(default: `true`), `simp` will **not** create a proof term for a
rewriting rule associated with an `rfl`-theorem. Rewriting rules are
provided by users by annotating theorems with the attribute `@[simp]`.
If the proof of the theorem is just `rfl` (reflexivity), and
`implicitDefEqProofs := true`, `simp` will **not** create a proof term
which is an application of the annotated theorem.
The default setting does change the existing behavior. Users can use
`simp -implicitDefEqProofs` to force `simp` to create a proof term for
`rfl`-theorems. This can positively impact proof checking time in the
kernel.
This PR also fixes an issue in the `split` tactic that has been exposed
by this feature. It was looking for `split` candidates in proofs and
implicit arguments. See new test for issue exposed by the previous
feature.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR fixes a performance issue where the Lean language server would
walk the full project file tree every time a file was saved, blocking
the processing of all other requests and notifications and significantly
increasing overall language server latency after saving.
This issue was originally reported at
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Compiling.20too.20slow/near/484386515
and uncovered in a lengthy investigation. The performance bug that
causes the Lean language server to walk the full project file tree when
the file watcher for .ilean files is triggered was introduced when the
.ileans were first introduced, whereas the specific issue of file saving
also triggering the walk was introduced by #3247 in 4.8.0 and the use of
the file watcher for .lean files, which would then also trigger the
directory walk. Combining this with VS Code's auto-save feature causes
the language server to walk the full project file tree on every change
of the document.
It somehow hasn't really been much of an issue until now, but we still
do way too much work in the watchdog main loop. I'll look into resolving
that more general issue in the future.
This PR ensures that nesting trace nodes are annotated with timing
information iff `trace.profiler` is active.
The previous connection to the otherwise unrelated `profiler` option was
a remnant from before `trace.profiler` existed; if users want to
annotate explicitly activated trace classes only, they can instead
increase `trace.profiler.threshold`.
This PR adds the builtin simproc `USize.reduceToNat` which reduces the
`USize.toNat` operation on literals less than `UInt32.size` (i.e.,
`4294967296`).
This PR upstreams some UInt theorems from Batteries and adds more
`toNat`-related theorems. It also adds the missing `UInt8` and `UInt16`
to/from `USize` conversions so that the the interface is uniform across
the UInt types.
**Summary of all changes:**
* Upstreamed and added `toNat` constructors lemmas: `toNat_mk`,
`ofNat_toNat`, `toNat_ofNat`, `toNat_ofNatCore`, and
`USize.toNat_ofNat32`
* Upstreamed and added `toNat` canonicalization; `val_val_eq_toNat` and
`toNat_toBitVec_eq_toNat`
* Added injectivity iffs: `toBitVec_inj`, `toNat_inj`, and `val_inj`
* Added inequality iffs: `le_iff_toNat_le` and `lt_iff_toNat_lt`
* Upstreamed antisymmetry lemmas: `le_antisymm` and `le_antisymm_iff`
* Upstreamed missing `toNat` lemmas on arithmetic operations:
`toNat_add`, `toNat_sub`, `toNat_mul`
* Upstreamed and added missing conversion lemmas: `toNat_toUInt*` and
`toNat_USize`
* Added missing `USize` conversions: `USize.toUInt8`, `UInt8.toUSize`,
`USize.toUInt16`, `UInt16.toUSize`
This PR deprecates `Fin.ofNat` in favour of `Fin.ofNat'` (which takes an
`[NeZero]` instance, rather than returning an element of `Fin (n+1)`).
After leaving the deprecation warning in place for some time, we will
then rename `ofNat'` back to `ofNat`.
This PR fixes:
- Problems in other linux distributions that the default `tzdata`
directory is not the same as previously defined by ensuring it with a
fallback behavior when directory is missing.
- Trim unnecessary characters from local time identifier.
This PR adds a cmake knob to allow turning off installing a copy of
`cadical`.
This can be useful for custom builds/installs where cadical is already
available in the system.
Closes: #5603
This PR adds `Lean.loadPlugin` which exposes functionality similar to
the `lean` executable's `--plugin` option to Lean code.
This will allow custom Lean frontends (e.g., Lake, the Lean language
server) to also load plugins.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR improves the errors Lake produces when it fails to fetch a
dependency from Reservoir. If the package is not indexed, it will
produce a suggestion about how to require it from GitHub.
Closes#5330.
This PR upstreams the definition and basic lemmas about `List.finRange`
from Batteries.
Thanks for contributors to Batteries and Mathlib who've previously
worked on this material. Further PRs are welcome here. I'll be adding
more API later.
This PR upstreams lemmas about `Vector` from Batteries.
I'll be adding more soon, and PRs are welcome, particularly from those
who have previously contributed to `Vector` in Batteries.
This PR implements `BitVec.toInt_abs`.
The absolute value of `x : BitVec w` is naively a case split on the sign
of `x`.
However, recall that when `x = intMin w`, `-x = x`.
Thus, the full value of `abs x` is computed by the case split:
- If `x : BitVec w` is `intMin`, then its absolute value is also `intMin
w`, and
thus `toInt` will equal `intMin.toInt`.
- Otherwise, if `x` is negative, then `x.abs.toInt = (-x).toInt`.
- Finally, when `x` is nonnegative, then `x.abs.toInt = x.toInt`.
```lean
theorem toInt_abs {x : BitVec w} :
x.abs.toInt =
if x = intMin w then (intMin w).toInt
else if x.msb then -x.toInt
else x.toInt
```
We also provide a variant of `toInt_abs` that
hides the case split for `x` being positive or negative by using
`natAbs`.
```lean
theorem toInt_abs_eq_natAbs {x : BitVec w} : x.abs.toInt =
if x = intMin w then (intMin w).toInt else x.toInt.natAbs
```
Supercedes https://github.com/leanprover/lean4/pull/5787
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
This PR adds `toNat` theorems for `BitVec.signExtend.`
Sign extending to a larger bitwidth depends on the msb. If the msb is
false, then the result equals the original value. If the msb is true,
then we add a value of `(2^v - 2^w)`, which arises from the sign
extension.
```lean
theorem toNat_signExtend (x : BitVec w) {v : Nat} :
(x.signExtend v).toNat = (x.setWidth v).toNat + if x.msb then 2^v - 2^w else 0
```
Co-authored-by: Harun Khan <harun19@stanford.edu>
This PR adds theorem `mod_eq_sub`, makes theorem
`sub_mul_eq_mod_of_lt_of_le` not private anymore and moves its location
within the `rotate*` section to use it in other proofs.
This PR upstreams `Nat.lt_pow_self` and `Nat.lt_two_pow` from Mathlib
and uses them to prove the simp theorem `Nat.mod_two_pow`.
This simplifies expressions like `System.Platform.numBits % 2 ^
System.Platform.numBits = System.Platform.numBits`, which is needed for
#6188.
This PR adds the theorems `le_usize_size` and `usize_size_le`, which
make proving inequalities about `USize.size` easier.
It also deprecates `usize_size_gt_zero` in favor of `usize_size_pos` (as
that seems more consistent with our naming covention) and adds
`USize.toNat_ofNat_of_lt_32` for dealing with small USize literals.
It also moves `USize.ofNat32` and `USize.toUInt64` to
`Init.Data.UInt.Basic` as neither are used in `Init.Prelude` anymore.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR makes Lake no longer automatically fetch GitHub cloud releases
if the package build directory is already present (mirroring the
behavior of the Reservoir cache). This prevents the cache from
clobbering existing prebuilt artifacts. Users can still manually fetch
the cache and clobber the build directory by running `lake build
<pkg>:release`.
This PR changes the definition of `HashSet.insertMany` and
`HashSet.Raw.insertMany` so that it is equivalent to repeatedly calling
`HashSet.insert`/`HashSet.Raw.insert`. It also clarifies the docstrings
of all the `insert` and `insertMany` functions.
---------
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
This PR makes stricter requirements for the `@[deprecated]` attribute,
requiring either a replacement identifier as `@[deprecated bar]` or
suggestion text `@[deprecated "Past its use by date"]`, and also
requires a `since := "..."` field.
This PR changes how generalized field notation ("dot notation") resolves
the function. The new resolution rule is that if `x : S`, then `x.f`
resolves the name `S.f` relative to the root namespace (hence it now
affected by `export` and `open`). Breaking change: aliases now resolve
differently. Before, if `x : S`, and if `S.f` is an alias for `S'.f`,
then `x.f` would use `S'.f` and look for an argument of type `S'`. Now,
it looks for an argument of type `S`, which is more generally useful
behavior. Code making use of the old behavior should consider defining
`S` or `S'` in terms of the other, since dot notation can unfold
definitions during resolution.
This also fixes a bug in explicit-mode generalized field notation
(`@x.f`) where `x` could be passed as the wrong argument. This was not a
bug for explicit-mode structure projections.
Closes#3031. Addresses the `Function` namespace issue in #1629.
This PR makes it possible to write `rw (occs := [1,2]) ...` instead of
`rw (occs := .pos [1,2]) ...` by adding a coercion from `List.Nat` to
`Lean.Meta.Occurrences`.
This PR makes `USize.toUInt64` a regular non-opaque definition.
It also moves it to `Init.Data.UInt.Basic`, as it is not actually used
in `Init.Prelude` anymore.
This PR changes the signature of `Array.swap`, so it takes `Nat`
arguments with tactic provided bounds checking. It also renames
`Array.swap!` to `Array.swapIfInBounds`.
This PR completes the TODO in `Init.Data.Array.BinSearch`, removing the
`partial` keyword and converting runtime bounds checks to compile time
bounds checks.
This PR fixes a bug with the `structure`/`class` command where if there
are parents that are not represented as subobjects but which used other
parents as instances, then there would be a kernel error. Closes#2611.
Note: there is still the limitation that parents that are not
represented as subobjects do not themselves provide instances to other
parents.
This PR adds toInt theorems for BitVec.signExtend.
If the current width `w` is larger than the extended width `v`,
then the value when interpreted as an integer is truncated,
and we compute a modulo by `2^v`.
```lean
theorem toInt_signExtend_of_le (x : BitVec w) (hv : v ≤ w) :
(x.signExtend v).toInt = Int.bmod (x.toNat) (2^v)
```
Co-authored-by: Siddharth Bhat <siddu.druid@gmail.com>
Co-authored-by: Harun Khan <harun19@stanford.edu>
Stacked on top of #6155
---------
Co-authored-by: Harun Khan <harun19@stanford.edu>
This PR uses `Array.findFinIdx?` in preference to `Array.findIdx?` where
it allows converting a runtime bounds check to a compile time bounds
check.
(and some other minor cleanup)
This PR fixes a bug where the signature pretty printer would ignore the
current setting of `pp.raw`. This fixes an issue where `#check ident`
would not heed `pp.raw`. Closes#6090.
This PR fixes a non-termination bug that occurred when generating the
match-expression equation theorems. The bug was triggered when the proof
automation for the equation theorem repeatedly applied `injection(` to
the same local declaration, as it could not be removed due to forward
dependencies. See issue #6067 for an example that reproduces this issue.
closes#6067
This PR adds core metaprogramming functions for forking off background
tasks from elaboration such that their results are visible to reporting
and the language server
This PR adds support for `structure` in `mutual` blocks, allowing
inductive types defined by `inductive` and `structure` to be mutually
recursive. The limitations are (1) that the parents in the `extends`
clause must be defined before the `mutual` block and (2) mutually
recursive classes are not allowed (a limitation shared by `class
inductive`). There are also improvements to universe level inference for
inductive types and structures. Breaking change: structure parents now
elaborate with the structure in scope (fix: use qualified names or
rename the structure to avoid shadowing), and structure parents no
longer elaborate with autoimplicits enabled.
Internally, this is a large refactor of both the `inductive` and
`structure` commands. Common material is now in
`Lean.Elab.MutualInductive`, and each command plugs into this mutual
inductive elaboration framework with the logic specific to the
respective command. For example, `structure` has code to add projections
after the inductive types are added to the environment.
Closes#4182
This PR modifies the signature of the functions `Nat.fold`,
`Nat.foldRev`, `Nat.any`, `Nat.all`, so that the function is passed the
upper bound. This allows us to change runtime array bounds checks to
compile time checks in many places.
This file was upstreamed from batteries; I just got bitten by the
invalid reference and it took quite a while to figure out that this one
had been moved!
This PR adds a slight performance improvement to reflection of `if`
statements that I noticed by profiling Leanwuzla against SMTCOMP's
`non-incremental/QF_BV/fft/Sz256_6616.smt2`.
In particular:
1. The profile showed about 4 percent of the total run time were spent
constructing these decidable instances in reflection of `if` statements.
We can construct them much quicker by hand as they always have the same
structure
2. This delays construction of these statements until we actually
generate the reflection proof that we wish to submit to the kernel. Thus
if we encounter a SAT instad of an UNSAT problem we will not spend time
generating these expressions anymore.
```
baseline
Time (mean ± σ): 31.236 s ± 0.258 s
Range (min … max): 30.899 s … 31.661 s 10 runs
after
Time (mean ± σ): 30.671 s ± 0.288 s
Range (min … max): 30.350 s … 31.156 s 10 runs
```
This PR fixes a non-termination bug that occurred when generating the
match-expression splitter theorem. The bug was triggered when the proof
automation for the splitter theorem repeatedly applied `injection` to
the same local declaration, as it could not be removed due to forward
dependencies. See issue #6065 for an example that reproduces this issue.
closes#6065
This PR adds lemmas for extracting a given bit of a `BitVec` obtained
via `sub`/`neg`/`sshiftRight'`/`abs`.
---------
Co-authored-by: Kim Morrison <scott@tqft.net>
This PR avoids runtime array bounds checks in places where it can
trivially be done at compile time.
None of these changes are of particular consequence: I mostly wanted to
learn how much we do this, and what the obstacles are to doing it less.
This PR does the same fix as #6104, but such that it doesn't break the
test/the file in `Plausible`. This is done by not creating unused let
binders in metavariable types that are made by `elimMVar`. (This is also
a positive thing for users looking at metavariable types, for example in
error messages)
We get rid of `skipAtMostNumBinders`. This function was originally
defined for the purpose of making this test work, but it is a hack
because it allows cycles in the metavariable context.
It would make sense to split these changes into 2 PRs, but I combined
them here to show that the combination of them closes#6013 without
breaking anything
Closes#6013
This PR adds support for displaying multiple threads in the trace
profiler output.
`TraceState.tid` needs to be adjusted for this purpose, which is not
done yet by the Lean elaborator as it is still single-threaded.
This PR replaces `Array.feraseIdx` and `Array.insertAt` with
`Array.eraseIdx` and `Array.insertIdx`, both of which take a `Nat`
argument and a tactic-provided proof that it is in bounds. We also have
`eraseIdxIfInBounds` and `insertIdxIfInBounds` which are noops if the
index is out of bounds. We also provide a `Fin` valued version of
`Array.findIdx?`. Together, these quite ergonomically improve the array
indexing safety at a number of places in the compiler/elaborator.
This PR adds theorems `BitVec.(getMsbD, msb)_(rotateLeft, rotateRight)`.
We follow the same strategy taken for `getLsbD`, constructing the
necessary auxilliary theorems first (relying on different hypotheses)
and then generalizing.
---------
Co-authored-by: Siddharth <siddu.druid@gmail.com>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
This PR improves the `#print` command for structures to show all fields
and which parents the fields were inherited from, hiding internal
details such as which parents are represented as subobjects. This
information is still present in the constructor if needed. The pretty
printer for private constants is also improved, and it now handles
private names from the current module like any other name; private names
from other modules are made hygienic.
Example output for `#print Monad`:
```
class Monad.{u, v} (m : Type u → Type v) : Type (max (u + 1) v)
number of parameters: 1
parents:
Monad.toApplicative : Applicative m
Monad.toBind : Bind m
fields:
Functor.map : {α β : Type u} → (α → β) → m α → m β
Functor.mapConst : {α β : Type u} → α → m β → m α
Pure.pure : {α : Type u} → α → m α
Seq.seq : {α β : Type u} → m (α → β) → (Unit → m α) → m β
SeqLeft.seqLeft : {α β : Type u} → m α → (Unit → m β) → m α
SeqRight.seqRight : {α β : Type u} → m α → (Unit → m β) → m β
Bind.bind : {α β : Type u} → m α → (α → m β) → m β
constructor:
Monad.mk.{u, v} {m : Type u → Type v} [toApplicative : Applicative m] [toBind : Bind m] : Monad m
resolution order:
Monad, Applicative, Bind, Functor, Pure, Seq, SeqLeft, SeqRight
```
Suggested by Floris van Doorn [on
Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.23print.20command.20for.20structures/near/482503637).
This PR fixes a bug at the definitional equality test (`isDefEq`). At
unification constraints of the form `c.{u} =?= c.{v}`, it was not trying
to unfold `c`. This bug did not affect the kernel.
closes#6117
This PR adds a case to `Level.geq` that is present in the kernel's level
`is_geq` procedure, making them consistent with one another.
This came up during testing of `lean4lean`. Currently `Level.geq`
differs from `level::is_geq` in the case of `max u v >= imax u v`. The
elaborator function is overly pessimistic and yields `false` on this
while the kernel function yields true. This comes up concretely in the
`Trans` class:
```lean
class Trans (r : α → β → Sort u) (s : β → γ → Sort v) (t : outParam (α → γ → Sort w)) where
trans : r a b → s b c → t a c
```
The type of this class is `Sort (max (max (max (max (max (max 1 u) u_1)
u_2) u_3) v) w)` (where `u_1 u_2 u_3` are the levels of `α β γ`), but if
you try writing that type explicitly then the `class` command fails.
Omitting the type leaves the `class` to infer the universe level (the
command assumes the level is correct, and the kernel agrees it is), but
including the type then the elaborator checks the level inequality with
`Level.geq` and fails.
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
This PR changes `lean_sharecommon_{eq,hash}` to only consider the
salient bytes of an object, and not any bytes of any
unspecified/uninitialized unused capacity.
Accessing uninitialized storage results in undefined behaviour.
This does not seem to have any semantics disadvantages: If objects
compare equal after this change, their salient bytes are still equal. By
contrast, if the actual identity of allocations needs to be
distinguished, that can be done by just comparing pointers to the
storage.
If we wanted to retain the current logic, we would need initialize the
otherwise unused parts to some specific value to avoid the undefined
behaviour.
Closes#5831
This PR fixes a bug where structural recursion did not work when indices
of the recursive argument appeared as function parameters in a different
order than in the argument's type's definition.
Fixes#6015.
This PR liberalizes atom rules by allowing `''` to be a prefix of an
atom, after #6012 only added an exception for `''` alone, and also adds
some unit tests for atom validation.
This PR fixes an issue in the `injection` tactic. This tactic may
execute multiple sub-tactics. If any of them fail, we must backtrack the
partial assignment. This issue was causing the error: "`mvarId` is
already assigned" in issue #6066. The issue is not yet resolved, as the
equation generator for the match expressions is failing in the example
provided in this issue.
This PR fixes the caching infrastructure for `whnf` and `isDefEq`,
ensuring the cache accounts for all relevant configuration flags. It
also cleans up the `WHNF.lean` module and improves the configuration of
`whnf`.
This PR fixes a stack overflow caused by a cyclic assignment in the
metavariable context. The cycle is unintentionally introduced by the
structure instance elaborator.
closes#3150
This PR makes the `change` tactic and conv tactic use the same
elaboration strategy. It works uniformly for both the target and local
hypotheses. Now `change` can assign metavariables, for example:
```lean
example (x y z : Nat) : x + y = z := by
change ?a = _
let w := ?a
-- now `w : Nat := x + y`
```
This PR modifies `Lean.MVarId.replaceTargetDefEq` and
`Lean.MVarId.replaceLocalDeclDefEq` to use `Expr.equal` instead of
`Expr.eqv` when determining whether the expression has changed. This is
justified on the grounds that binder names and binder infos are
user-visible and affect elaboration.
This PR adds raw transmutation of floating-point numbers to and from
`UInt64`. Floats and UInts share the same endianness across all
supported platforms. The IEEE 754 standard precisely specifies the bit
layout of floats. Note that `Float.toBits` is distinct from
`Float.toUInt64`, which attempts to preserve the numeric value rather
than the bitwise value.
closes#6071
This PR adds the option `pp.parens` (default: false) that causes the
pretty printer to eagerly insert parentheses, which can be useful for
teaching and for understanding the structure of expressions. For
example, it causes `p → q → r` to pretty print as `p → (q → r)`.
Any notations with precedence greater than or equal to `maxPrec` do not
receive such discretionary parentheses, since this precedence level is
considered to be infinity.
This option was a feature in the Lean 3 community edition.
This PR fixes a bug in the constant folding for the `Nat.ble` and
`Nat.blt` function in the old code generator, leading to a
miscompilation.
Closes#6086
This PR improves the term info for coercions marked with
`CoeFnType.coeFun` (such as `DFunLike.coe` in Mathlib), making "go to
definition" on the function name work. Hovering over such a coerced
function will show the coercee rather than the coercion expression. The
coercion expression can still be seen by hovering over the whitespace in
the function application.
This PR introduces date and time functionality to the Lean 4 Std.
Breaking Changes:
- `Lean.Data.Rat` is now `Std.Internal.Rat` because it's used by the
DateTime library.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
This PR prepares #6068 by using the `RArray` data structure in
`simp_arith` the simp-arith meta code.
After the subsequent stage0 we can change the simp-arith theorems in
`Init`.
This PR adds the Lean.RArray data structure.
This data structure is equivalent to `Fin n → α` or `Array α`, but
optimized for a fast kernel-reduction `get` operation.
It is not suitable as a general-purpose data structure. The primary
intended use case is the “denote” function of a typical proof by
reflection proof, where only the `get` operation is necessary, and where
using `List.get` unnecessarily slows down proofs with more than a
hand-full of atomic expressions.
There is no well-formedness invariant attached to this data structure,
to keep it concise; it's semantics is given through `RArray.get`. In
that way one can also view an `RArray` as a decision tree implementing
`Nat → α`.
In #6068 this data structure is used in `simp_arith`.
This PR improves the validation of new syntactic tokens. Previously, the
validation code had inconsistencies: some atoms would be accepted only
if they had a leading space as a pretty printer hint. Additionally,
atoms with internal whitespace are no longer allowed.
Closes#6011
This PR adds a newline at end of each Lean file generated by `lake new`
templates.
I have tested it with a locally compiled Lean with this commit. I hope
these changes make `lake new`'s behavior more consistent with the Lean 4
plugins and libraries newlines convention.
This PR adds a new definition `Message.kind` which returns the top-level
tag of a message. This is serialized as the new field `kind` in
`SerialMessaege` so that i can be used by external consumers (e.g.,
Lake) to identify messages via `lean --json`.
The tag of trace messages has also been changed from `_traceMsg` to the
more friendly `trace`.
Not a huge benefit, but actually reduces the code complexity (no need
for the `.fuse` function), and can help with problems with many repeated
varibles.
This PR fixes a bug where the monad lift coercion elaborator would
partially unify expressions even if they were not monads. This could be
taken advantage of to propagate information that could help elaboration
make progress, for example the first `change` worked because the monad
lift coercion elaborator was unifying `@Eq _ _` with `@Eq (Nat × Nat)
p`:
```lean
example (p : Nat × Nat) : p = p := by
change _ = ⟨_, _⟩ -- used to work (yielding `p = (p.fst, p.snd)`), now it doesn't
change ⟨_, _⟩ = _ -- never worked
```
As such, this is a breaking change; you may need to adjust expressions
to include additional implicit arguments.
This PR implements conversion functions from `Bool` to all `UIntX` and
`IntX` types.
Note that `Bool.toUInt64` already existed in previous versions of Lean.
This PR simplifies the implementation of `omega`.
When constructing the proof, `omega` is using MVars only for the purpose
of doing case analysis on `Or`. We can simplify the implementation a
fair bit if we just produce the proof directly using `Or.elim`.
While it didn’t yield the performance benefits I was hoping for, this
still seems a worthwhile simplification, now that we already have it.
This PR modifies the order of arguments for higher-order `Array`
functions, preferring to put the `Array` last (besides positional
arguments with defaults). This is more consistent with the `List` API,
and is more flexible, as dot notation allows two different partially
applied versions.
This PR changes the signature of `Array.get` to take a Nat and a proof,
rather than a `Fin`, for consistency with the rest of the (planned)
Array API. Note that because of bootstrapping issues we can't provide
`get_elem_tactic` as an autoparameter for the proof. As users will
mostly use the `xs[i]` notation provided by `GetElem`, this hopefully
isn't a problem.
We may restore `Fin` based versions, either here or downstream, as
needed, but they won't be the "main" functions.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
This PR changes the rule for which projections become instances. Before,
all parents along with all indirect ancestors that were represented as
subobject fields would have their projections become instances. Now only
projections for direct parents become instances.
Features:
- Only parents that are not ancestors of other parents get instances.
This allows "discretionary" indirect parents to be inserted for the
purpose of computing strict resolution orders when
`structure.strictResolutionOrder` is enabled, without having an impact
on typeclass synthesis.
- Non-subobject projections are now theorems if the parent is a
proposition. These are also no longer `@[reducible]`.
Closes#2905
This PR fixes `bv_decide`'s embedded constraint substitution to generate
correct counter examples in the corner case where duplicate theorems are
in the local context.
This PR introduces the and flattening pre processing pass from Bitwuzla
to `bv_decide`. It splits hypotheses of the form `(a && b) = true` into
`a = true` and `b = true` which has synergy potential with the already
existing embedded constraint substitution pass.
Beyond this I also added some profiling infra structure for the passes.
This PR adds a normalization rule to `bv_normalize` (which is used by
`bv_decide`) that converts `x / 2^k` into `x >>> k` under suitable
conditions. This allows us to simplify the expensive division circuits
that are used for bitblasting into much cheaper shifting circuits.
Concretely, it allows for the following canonicalization:
```lean
example {x : BitVec 16} : x / (BitVec.twoPow 16 2) = x >>> 2 := by bv_normalize
example {x : BitVec 16} : x / (BitVec.ofNat 16 8) = x >>> 3 := by bv_normalize
```
This PR changes the signature of `Array.set` to take a `Nat`, and a
tactic-provided bound, rather than a `Fin`.
Corresponding changes (but without the auto-param) for `Array.get` will
arrive shortly, after which I'll go more pervasively through the Array
API.
This PR is a follow-up to https://github.com/leanprover/lean4/pull/5609,
where we add lemmas characterizing `smtUDiv` and `smtSDiv`'s behavior
when the denominator is zero.
We build some `slt` theory, connecting it to `msb` for a clean proof. I
chose not to characterize `slt` in terms of `msb` a `simp` lemma, since
I anticipate use cases where we want to keep the arithmetic
interpretation of `slt`.
This PR removes
- a duplicate `MonadMCtx` instance in `MetavarContext.lean`
- `:= return ←` that I had left there accidentally in a previous PR.
- the unnecessary application of `mapMetaM` in `withTransparency`.
This PR adds a feature to the the mutual def elaborator where the
`instance` command yields theorems instead of definitions when the class
is a `Prop`.
Closes#5672
This PR adds configuration options for
`decide`/`decide!`/`native_decide` and refactors the tactics to be
frontends to the same backend. Adds a `+revert` option that cleans up
the local context and reverts all local variables the goal depends on,
along with indirect propositional hypotheses. Makes `native_decide` fail
at elaboration time on failure without sacrificing performance (the
decision procedure is still evaluated just once). Now `native_decide`
supports universe polymorphism.
Closes#2072
This now occurs for some large completions downstream of `import
Mathlib`. I'd like to get rid of this `whnf` call entirely in the
future, but this is a decent quick mitigation.
We add a new `Meta.instantiateMVars` trace node to the
`instantiateMVarsProfiling` definition used in `elabMutualDef`, and we
replace various uses of plain `instantiateMVars` with the profiled
version (which necessitated pulling up the definition to be higher in
the file).
This fixes a "time leak" when profiling large proofs, where
instantiating the goal metavariable can take a significant amount of
time, that previously would not be accounted for when using the trace
profiler.
This PR changes `bv_decide`'s configuration from lots of `set_option` to
an elaborated config like `simp` or `omega`. The notable exception is
`sat.solver` which is still a `set_option` such that users can configure
a custom SAT solver globally for an entire project or file. Additionally
it introduces the ability to set `maxSteps` for the simp preprocessing
run through the new config.
The latter feature was requested by people using `bv_decide` on SMTLIB
which has ginormous terms that exceed the default.
This PR verifies the `keys` function on `Std.HashMap`.
---
Initial discussions have already happend with @TwoFX and we are
collaborating on this matter.
This will remain a draft as long as not all desired results have been
added.
If we should still create an issue for the topic of this PR, let us
know.
Of course, any other feedback is appreciated as well :)
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: monsterkrampe <monsterkrampe@users.noreply.github.com>
Co-authored-by: jt0202 <johannes.tantow@gmail.com>
Enables us to auto-generate the changelog from the list of PRs for a
modicum of summarizing/categorizing work on PR creation.
Does not (yet) allow external contributors to set category labels by
themselves as this creates issues with triggering one workflow from
another, it is not clear whether they should be allowed to create new
categories, and the reviewer/triage team likely is in a better position
to do the categorization anyway.
This PR names the default SizeOf instance `instSizeOfDefault`
I regularly have to debug termination checking failures where I end up
hovering over some termination measure, and seeing `instSizeOfDefault`
is more likely to tell me that the default instance is used than
`instSizeOf`.
This PR relates the operations `findSomeM?`, `findM?`, `findSome?`, and
`find?` on `Array` with the corresponding operations on `List`, and also
provides simp lemmas for the `Array` operations `findSomeRevM?`,
`findRevM?`, `findSomeRev?`, `findRev?` (in terms of `reverse` and the
usual forward find operations).
Bumps
[mymindstorm/setup-emsdk](https://github.com/mymindstorm/setup-emsdk)
from 12 to 14.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/mymindstorm/setup-emsdk/releases">mymindstorm/setup-emsdk's
releases</a>.</em></p>
<blockquote>
<h2>Version 14</h2>
<h1>Breaking Changes</h1>
<p>The default cache key naming scheme was changed from
<code>{Emscripten version}-{OS type}-${CPU architecture}-master</code>
to <code>{Github workflow name}-{Emscripten version}-{OS type}-${CPU
architecture}</code>. If <code>actions-cache-folder</code> is defined,
ensure that there are no conflicts with other caches to prevent
issues.</p>
<h1>Changelog</h1>
<ul>
<li>Add option to override cache key naming scheme (<a
href="https://redirect.github.com/mymindstorm/setup-emsdk/issues/20">#20</a>)</li>
<li>Add workflow name to cache key naming scheme (<a
href="https://redirect.github.com/mymindstorm/setup-emsdk/issues/20">#20</a>)</li>
<li>Updated dependencies to latest versions</li>
</ul>
<h2>Version 13</h2>
<ul>
<li>Updated to Node 20</li>
</ul>
</blockquote>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="6ab9eb1bda"><code>6ab9eb1</code></a>
v13 -> v14</li>
<li><a
href="bb630c3bf4"><code>bb630c3</code></a>
Update all dependencies to latest versions</li>
<li><a
href="74881103d0"><code>7488110</code></a>
Add workflow ID to cache key and cache key override option (<a
href="https://redirect.github.com/mymindstorm/setup-emsdk/issues/40">#40</a>)</li>
<li><a
href="d233ac12b0"><code>d233ac1</code></a>
v13</li>
<li><a
href="1749b22b40"><code>1749b22</code></a>
npm audit fix + update runtime to node20</li>
<li>See full diff in <a
href="https://github.com/mymindstorm/setup-emsdk/compare/v12...v14">compare
view</a></li>
</ul>
</details>
<br />
[](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores)
Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.
[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)
---
<details>
<summary>Dependabot commands and options</summary>
<br />
You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot merge` will merge this PR after your CI passes on it
- `@dependabot squash and merge` will squash and merge this PR after
your CI passes on it
- `@dependabot cancel merge` will cancel a previously requested merge
and block automerging
- `@dependabot reopen` will reopen this PR if it is closed
- `@dependabot close` will close this PR and stop Dependabot recreating
it. You can achieve the same result by closing it manually
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)
</details>
Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Bumps
[nwtgck/actions-netlify](https://github.com/nwtgck/actions-netlify) from
2.0 to 3.0.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/nwtgck/actions-netlify/releases">nwtgck/actions-netlify's
releases</a>.</em></p>
<blockquote>
<h2>v3.0.0</h2>
<h3>Changed</h3>
<ul>
<li>Update dependencies</li>
<li>Updates the default runtime to node20</li>
</ul>
<h2>v2.1.0</h2>
<h3>Changed</h3>
<ul>
<li>Update dependencies</li>
</ul>
<h3>Added</h3>
<ul>
<li>Add "enable-github-deployment" input <a
href="https://redirect.github.com/nwtgck/actions-netlify/pull/901">#901</a>
by <a href="https://github.com/a-tokyo"><code>@a-tokyo</code></a></li>
</ul>
</blockquote>
</details>
<details>
<summary>Changelog</summary>
<p><em>Sourced from <a
href="https://github.com/nwtgck/actions-netlify/blob/develop/CHANGELOG.md">nwtgck/actions-netlify's
changelog</a>.</em></p>
<blockquote>
<h1>Changelog</h1>
<p>All notable changes to this project will be documented in this
file.</p>
<p>The format is based on <a
href="https://keepachangelog.com/en/1.0.0/">Keep a Changelog</a></p>
<h2>[Unreleased]</h2>
<h2>[3.0.0] - 2024-03-10</h2>
<h3>Changed</h3>
<ul>
<li>Update dependencies</li>
<li>Updates the default runtime to node20</li>
</ul>
<h2>[2.1.0] - 2023-08-18</h2>
<h3>Changed</h3>
<ul>
<li>Update dependencies</li>
</ul>
<h3>Added</h3>
<ul>
<li>Add "enable-github-deployment" input <a
href="https://redirect.github.com/nwtgck/actions-netlify/pull/901">#901</a>
by <a href="https://github.com/a-tokyo"><code>@a-tokyo</code></a></li>
</ul>
<h2>[2.0.0] - 2022-12-08</h2>
<h3>Changed</h3>
<ul>
<li>Update dependencies</li>
<li>Updates the default runtime to node16</li>
</ul>
<h2>[1.2.4] - 2022-10-14</h2>
<h3>Changed</h3>
<ul>
<li>Update dependencies</li>
</ul>
<h2>[1.2.3] - 2021-12-20</h2>
<h3>Changed</h3>
<ul>
<li>Update dependencies</li>
</ul>
<h2>[1.2.2] - 2021-05-08</h2>
<h3>Fixed</h3>
<ul>
<li>Fix GitHub deployment description</li>
</ul>
<h3>Changed</h3>
<ul>
<li>Update dependencies</li>
</ul>
<h2>[1.2.1] - 2021-05-05</h2>
<h3>Added</h3>
<ul>
<li>Add "fails-without-credentials" input to fail if the
credentials not provided <a
href="https://redirect.github.com/nwtgck/actions-netlify/pull/532">#532</a></li>
</ul>
<h3>Changed</h3>
<ul>
<li>Update dependencies</li>
</ul>
<h2>[1.2.0] - 2021-04-29</h2>
<h3>Changed</h3>
<ul>
<li>Update dependencies</li>
<li>(breaking change for <code>overwrites-pull-request-comment:
true</code>): Support multiple app deploys in a single PR <a
href="https://redirect.github.com/nwtgck/actions-netlify/pull/484">#484</a>
by <a
href="https://github.com/kaisermann"><code>@kaisermann</code></a></li>
</ul>
<!-- raw HTML omitted -->
</blockquote>
<p>... (truncated)</p>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="4cbaf4c08f"><code>4cbaf4c</code></a>
Merge branch 'release/3.0.0'</li>
<li><a
href="6b45669baf"><code>6b45669</code></a>
bump: 3.0.0</li>
<li><a
href="8d5d80bf73"><code>8d5d80b</code></a>
Merge pull request <a
href="https://redirect.github.com/nwtgck/actions-netlify/issues/1151">#1151</a>
from nwtgck/actions-build/nwtgck-dependabot/npm_and_...</li>
<li><a
href="85c2e8e35a"><code>85c2e8e</code></a>
build</li>
<li><a
href="ea3c314fcd"><code>ea3c314</code></a>
Build(deps): bump <code>@actions/github</code> from 5.1.1 to 6.0.0</li>
<li><a
href="333815eadd"><code>333815e</code></a>
updates the default runtime to node20</li>
<li><a
href="06de7de77b"><code>06de7de</code></a>
Build(deps-dev): bump <code>@vercel/ncc</code> from 0.36.1 to 0.38.1
(<a
href="https://redirect.github.com/nwtgck/actions-netlify/issues/1121">#1121</a>)</li>
<li><a
href="a7f64ad4e2"><code>a7f64ad</code></a>
deps: update</li>
<li><a
href="fee801f039"><code>fee801f</code></a>
Build(deps): bump actions/setup-node from 3 to 4 (<a
href="https://redirect.github.com/nwtgck/actions-netlify/issues/1124">#1124</a>)</li>
<li><a
href="e4998d22a0"><code>e4998d2</code></a>
README.md, sample workflow: bump to latest action versions (<a
href="https://redirect.github.com/nwtgck/actions-netlify/issues/1149">#1149</a>)</li>
<li>Additional commits viewable in <a
href="https://github.com/nwtgck/actions-netlify/compare/v2.0...v3.0">compare
view</a></li>
</ul>
</details>
<br />
[](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores)
Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.
[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)
---
<details>
<summary>Dependabot commands and options</summary>
<br />
You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot merge` will merge this PR after your CI passes on it
- `@dependabot squash and merge` will squash and merge this PR after
your CI passes on it
- `@dependabot cancel merge` will cancel a previously requested merge
and block automerging
- `@dependabot reopen` will reopen this PR if it is closed
- `@dependabot close` will close this PR and stop Dependabot recreating
it. You can achieve the same result by closing it manually
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)
</details>
Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
New behavior: when in recovery mode, if any tactic fails in `all_goals`
then the metacontext is restored and all goals are admitted.
Without this, it can leave partially-solved metavariables and incomplete
goal lists.
Lake will now update a package's `lean-toolchain` file on `lake update`
if it finds the package's direct dependencies use a newer compatible
toolchain. To skip this step, use the `--keep-toolchain` CLI option.
Closes#2582. Closes#2752. Closes#5615.
### Toolchain update details
To determine "newest compatible" toolchain, Lake parses the toolchain
listed in the packages' `lean-toolchain` files into four categories:
release , nightly, PR, and other. For newness, release toolchains are
compared by semantic version (e.g., `"v4.4.0" < "v4.8.0"` and
`"v4.6.0-rc1" < "v4.6.0"`) and nightlies are compared by date (e.g.,
`"nightly-2024-01-10" < "nightly-2014-10-01"`). All other toolchain
types and mixtures are incompatible. If there is not a single newest
toolchain, Lake will print a warning and continue updating without
changing the toolchain.
If Lake does find a new toolchain, Lake updates the workspace's
`lean-toolchain` file accordingly and restarts the update process on the
new Lake. If Elan is detected, it will spawn the new Lake process via
`elan run` with the same arguments Lake was initially run with. If Elan
is missing, it will prompt the user to restart Lake manually and exit
with a special error code (4).
### Other changes
To implement this new logic, various other refactors were needed. Here
are some key highlights:
* Logs emitted during package and workspace loading are now eagerly
printed.
* The Elan executable used by Lake is now configurable by the `ELAN`
environment variable.
* The `--lean` CLI option was removed. Use the `LEAN` environment
variable instead.
* `Package.deps` / `Package.opaqueDeps` have been removed. Use
`findPackage?` with a dependency's name instead.
* The dependency resolver now uses a pure breadth-first traversal to
resolve dependencies. It also resolves dependencies in reverse order,
which is done for consistency with targets. Latter targets shadow
earlier ones and latter dependencies take precedence over earlier ones.
**These changes mean the order of dependencies in a Lake manifest will
change after the first `lake update` on this version of Lake.**
This introduces a notion of synthetic atoms into `bv_decide`'s
reflection framework. An atom can be declared synthetic if its behavior
is fully specified by additional lemmas that are added in the process of
creating it. This is for example useful in the code that handles `if` as
the entire `if` block is abstracted as an atom and then two lemmas to
describe either branch are added. Previously this had the effect of
creating error messages about potentially unsound counterexamples, now
the synthetic atoms get filtered from the counter example generation.
In patterns, ellipsis should always fill in each remaining argument as
an implicit argument, even if it is an optparam or autoparam. This
prevents examples such as the one in #4555 from failing:
```lean
match e with
| .internal .. => sorry
| .error .. => sorry
```
The `internal` constructor has an optparam (`| internal (id :
InternalExceptionId) (extra : KVMap := {})`).
We may consider having ellipsis suppress optparams and autoparams in
general. We avoid doing so for now since it's possible to opt-out of
them individually (for example with `.internal (extra := _) ..`) but
it's not possible to opt-in, and it is plausible that `..` with
optparams is useful in contexts such as the `refine` tactic. With
patterns however, it is hard to imagine a use case that offsets the
inconvenience of optparams being eagerly supplied.
Closes#4555
Following up #5928, updates the syntax for `omega` and `solve_by_elim`
and restores the syntax quotations in their implementations.
Following up #5898, uses the new tactic syntax in the library, replacing
all uses of `(config := ...)`.
The tactic elaborators match a too-restrictive syntax for the migration
to the new configuration syntax. This generalizes what they accept, and
the code will return to using quotations after a stage0 update and
syntax change.
Adds an optional `text` argument to the `fetchFile*` and `buildFile*`
definitions that can be used to hash built files as text files (with
normalized line endings) instead of as binary files (the previous
default).
Separately, this change also significantly expands the documentation in
the `Lake.Build.Trace` module and preforms minor touchups of some build
job signatures.
Simplifies the definition of `MapDeclarationExtension` so that it only
contains a `NameMap` without an additional `List (Name × α)`. Uses the
`NameMap`'s natural ordering during export rather than sorting.
This fixes issues from inserting into a `MapDeclarationExtension`
multiple times with the same key. Inside a module it appears that each
insertion overwrites the data, since those queries access the `NameMap`.
But across modules, only the first insertion is accessible, since each
insertion was actually pushed to the front of a `List`.
Mathlib needs this for a documentation extension feature, and [they are
considering a PR with a
workaround](https://github.com/leanprover-community/mathlib4/pull/17043)
that digs into the `MapDeclarationExtension` data structures.
As far as I can tell, the ability to pass a structure instance to a
deriving handler is not actually used in practice. It didn't seem to be
used in the test suite, at least.
Do we want to remove this, or do we want to use and document it? This PR
removes it, but that's not something I feel strongly about - but seeing
if it breaks Mathlib is a useful data point.
Example: Normally subtype notation pretty prints as `{ x // x > 0 }`,
but now the difference in domains is exposed:
```lean
example (h : {x : Int // x > 0}) : {x : Nat // x > 0} := h
/-
error: type mismatch
h
has type
{ x : Int // x > 0 } : Type
but is expected to have type
{ x : Nat // x > 0 } : Type
-/
```
Example:
```lean
example : 0 = (0 : Nat) := by
exact Eq.refl (0 : Int)
/-
error: type mismatch
Eq.refl 0
has type
(0 : Int) = 0 : Prop
but is expected to have type
(0 : Nat) = 0 : Prop
-/
```
`bv_normalize` would just silently drop other goals if called while not
focused on a singular goal, for example:
```lean
theorem mvarid (x y : Bool) (h : x ∨ y) : y ∨ x := by
cases h
bv_normalize
-- we want to write another bv_normalize here but all goals are gone
```
Would make the second subgoal disappear and then throw an error about
meta variables in the kernel.
There are many more lemmas about `foldlM`, so this may be useful for
reasoning about for loops by transforming them into folds.
The transformation includes accounting for monad effects, but does have
a mild performance difference in that short-circuiting on
`ForInStep.done` is replaced by traversing the rest of the list with a
noop.
Specializes the congr lemma generated for the `arg` conv tactic to only
rewrite the chosen argument. This makes it much more likely that the
chosen argument is able to be accessed.
Lets `arg` access the domain and codomain of pi types via `arg 1` and
`arg 2` in more situations. Upstreams `pi_congr` for this from mathlib.
Adds a negative indexing option, where `arg -2` accesses the
second-to-last argument for example, making the behavior of `lhs`
available to `arg`. This works for `enter` as well.
Other improvement: when there is an error in the `enter [...]` tactic,
individual locations get underlined with the error. The tactic info now
also is like `rw`, so you can see the intermediate conv states.
Closes#5871
PR #5883 added a new syntax for tactic configuration, and this PR
enables it in most tactics. Example: `simp +contextual`.
There will be followup PRs to modify the remaining ones.
Breaking change: Tactics that are macros for `simp` or other core
tactics need to adapt. The easiest way is to replace `(config)?` with
`optConfig` and then in the syntax quotations replace `$[$cfg]?` by
`$cfg:optConfig`. For tactics that manipulate the configuration, see
`erw` for an example:
```lean
macro "erw" c:optConfig s:rwRuleSeq loc:(location)? : tactic => do
`(tactic| rw $[$(getConfigItems c)]* (transparency := .default) $s:rwRuleSeq $(loc)?)
```
Configuration options are processed left-to-right, so this forces the
`transparency` to always be `.default`.
These implementations could be made more efficient by promoting them to
primitive operations, but I propose installing these in the meantime to
encourage users to avoid non-linearity problems.
* Now `getPathToBaseStructure?` can navigate to all parent structures,
not just through subobjects.
* Adds a "resolution order" for methods. This is the order that
generalized field notation visits parent structures when trying to
resolve names. The algorithm to compute a resolution order is the
commonly used C3 (used for instance by Python). By default we use a
relaxed version of the algorithm that tolerates inconsistencies. Using
`set_option structure.strictResolutionOrder true` makes inconsistent
parent orderings into warnings.
* This makes generalized field notation be able to resolve names for all
parent structures, not just those that are embedded as subobjects.
Closes#3467. (And addresses side note in #1881.)
* Modifies `getAllParentStructures` to return *all* parents. This
improves dot completion in the editor.
I'd previously added an instance from `ForIn'` to `ForIn`, but this then
caused some non-defeq duplication. It seems fine to just remove the
concrete `ForIn` instances in cases where the `ForIn'` instance exists
too. We can even remove a number of type-specific lemmas in favour of
the general ones.
Now that the elaborator supports primitive projections for recursive
inductive types (#5822), enable defining recursive inductive types with
the `structure` command, which was set up in #5842.
Example:
```lean
structure Tree where
n : Nat
children : Fin n → Tree
def Tree.size : Tree → Nat
| {n, children} => Id.run do
let mut s := 0
for h : i in [0 : n] do
s := s + (children ⟨i, h.2⟩).size
pure s
```
Note for kernel re-implementors: recursive structures are exercising the
kernel feature where primitive projections are valid for one-constructor
inductive types in general, so long as the structure isn't a `Prop` and
doesn't have any non-`Prop` fields, not just ones that are non-indexed
and non-recursive.
Closes#2512
The kernel supports primitive projections for all inductive types with
one construtor. The elaborator was assuming primitive projections only
work for "structure-likes", non-recursive inductive types with no
indices.
Enables numeric projection notation for general one-constructor
inductives.
Extracted from #5783.
Modifies the `structureExt` from being a `SimplePersistentEnvExtension`
to a `PersistentEnvExtension`. The simple version contains a `List` of
all added entries, which we do not need since we already have a
`PersistentHashMap` of them in the state. The oversight was that this
`List` contained duplicate entries due to `setStructureParents`
re-adding entries.
This hasn't affected release candidates or stables, but I realised that
I haven't been updating `LEAN_VERSION_MINOR` on `master` the last two
months, so it still says v4.12.0. This advances it to v4.14.0.
This PR adds a new syntax for tactic and command configurations. It also
updates the elaborator construction command to be able to process this
new syntax.
We do not update core tactics yet. Once tactics switch over to it,
rather than (for example) writing `simp (config := { contextual := true,
maxSteps := 22})`, one can write `simp +contextual (maxSteps := 22)`.
The new syntax is reverse compatible in the sense that `(config := ...)`
still sets the entire configuration.
Note to metaprogrammers: Use `optConfig` instead of `(config)?`. The
elaborator generated by `declare_config_elab` accepts both old and new
configurations. The elaborator has also been written to be tolerant to
null nodes, so adapting to `optConfig` should be as easy as changing
just the syntax for your tactics and deleting `mkOptionalNode`.
Breaking change: The new system is mostly reverse compatible, however
the type of the generated elaborator now lands in `TacticM` to make use
of the current recovery state. Commands that wish to elaborate
configurations should now use `declare_command_config_elab` instead of
`declare_config_elab` to get an elaborator landing in `CommandElabM`.
This command comes from Lean 3, which I had previously ported and
contributed to Batteries (née Std). In this new version, `#where`
produces actual command Syntax for all features of a top-level scope
(rather than splicing together strings), and it also now reports
included variables.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This adds the embedded constraint substitution preprocessing pass from
Bitwuzla to `bv_decide`.
It looks for hypotheses of the form `h : x = true` and then attempts to
find occurrences of
`x` within other hypotheses to replace them with true.
Fixes a serious issue where Lake would delete path dependencies when
attempting to cleanup a dependency required with an incorrect name.
Closes#5876. Originally part of #5684, but also independently
discovered by François.
Makes `MessageData.ofConstName` available without needing to import the
pretty printer. Any code making use of `MessageData` can write `m!" ...
{.ofConstName n} ... "` to have the name print with hover information.
More error messages now have hover information.
* Now `.ofConstName` also has a boolean flag to make names print fully
qualified. Default: false.
* Now `.ofConstName` will sanitize names that aren't constants. It is OK
to use it in `"unknown constant '{.ofConstName constName}'"` errors.
Usability note: it is more user-friendly to have "has already been
declared" errors report the fully qualified name. For this, write
`m!"{.ofConstName n true} has already been declared"`.
An important part of the interface of a function is the parameter names,
for making used of named arguments. This PR makes the parameter names
print in a reliable way. The parameters of the type now appear as
hygienic names if they cannot be used as named arguments.
Modifies the heuristic for how parameters are chosen to appear before or
after the colon. The rule is now that parameters start appearing after
the colon at the first non-dependent non-instance-implicit parameter
that has a name unusable as a named argument. This is a refinement of
#2846.
Fixes the issue where consecutive hygienic names pretty print without a
space separating them, so we now have `(x✝ y✝ : Nat)` rather than `(x✝y✝
: Nat)`.
Breaking change: `Lean.PrettyPrinter.Formatter.pushToken` now takes an
additional boolean `ident` argument, which should be `true` for
identifiers. Used to insert discretionary space between consecutive
identifiers.
Closes#5810
This adds the ability to add the converse direction of a rewrite rule
not just in simp arguments `simp [← thm]`, but also as a global
attribute
```lean
attribute [simp ←] thm
```
This fixes#5828.
This can be undone with `attribute [-simp]`, although note that
`[-simp]` wins and cannot be undone at the moment (#5868).
Like `simp [← thm]` (see #4290), this will do an implicit `attribute
[-simp] thm` if the other direction is already defined.
Type mismatch errors have a nice feature where expressions are annotated
with `pp.explicit` to expose differences via `isDefEq` checking.
However, this procedure has side effects since `isDefEq` may assign
metavariables. This PR wraps the procedure with `withoutModifyingState`
to prevent assignments from escaping.
Assignments can lead to confusing behavior. For example, in the
following a higher-order unification fails, but the difference-finding
procedure unifies metavariables in a naive way, producing a baffling
error message:
```lean
theorem test {f g : Nat → Nat} (n : Nat) (hfg : ∀a, f (g a) = a) :
f (g n) = n := hfg n
example {g2 : ℕ → ℕ} (n2 : ℕ) : (λx => x * 2) (g2 n2) = n2 := by
with_reducible refine test n2 ?_
/-
type mismatch
test n2 ?m.648
has type
(fun x ↦ x * 2) (g2 n2) = n2 : Prop
but is expected to have type
(fun x ↦ x * 2) (g2 n2) = n2 : Prop
-/
```
With the change, it now says `has type ?m.153 (?m.154 n2) = n2`.
Note: this uses `withoutModifyingState` instead of `withNewMCtxDepth`
because we want to know something about where `isDefEq` failed — we are
trying to simulate a very basic version of `isDefEq` for function
applications, and we want the state at the point of failure to know
which argument is "at fault".
Modifies `simp` to elaborate all simp arguments without disabling error
recovery. Like in #4177, simp arguments with elaboration errors are not
added to the simp set. Error recovery is still disabled when `simp` is
used in combinators such as `first`.
This enables better term info and features like tab completion when
there are elaboration errors.
Also included is a fix to the `all_goals` and `<;>` tactic combinators.
Recall that `try`/`catch` for the Tactic monad restores the state on
failure. This meant that all messages were being cleared on tactic
failure. The fix is to use `Tactic.tryCatch` instead, which doesn't
restore state.
Part of addressing #3831Closes#4888
The assumptions behind disabling error recovery for the `apply` tactic
no longer seem to hold, since tactic combinators like `first` themselves
disable error recovery when it makes sense.
This addresses part of #3831
Breaking change: `elabTermForApply` no longer uses `withoutRecover`.
Tactics using `elabTermForApply` should evaluate whether it makes sense
to wrap it with `withoutRecover`, which is generally speaking when it's
used to elaborate identifiers.
Makes the error messages report on RHSs and LHSs that do not match the
expected values when the relations are defeq. If the relations are not
defeq, the error message now no longer mentions the value of the whole
`calc` expression.
Adds a field to `mkCoe` with an optional callback to use to generate
error messages.
Note: it is tempting to try to make use of expected types when
elaborating the `calc` expression, but this runs into issue #2073.
Closes#4318
Adds ability to chain congruence lemmas when a function's arity is less
than the number of supplied arguments. This improves `congr` as well as
all conv tactics implemented using `congr`, like `arg` and `enter`.
(The non-conv `congr` tactic still needs to be fixed.)
Toward #2942.
Followup to #5841. Makes the `structure` command populate the new
`parentInfo` field with all the structures in the `extends` clause.
This will require a stage0 update to fully take effect.
Breaking change: now it's a warning if a structure extends a parent
multiple times.
Breaking change: now `getParentStructures` is `getStructureSubobjects`.
Adds `getStructureParentInfo` for getting all the immediate parents.
Note that the set of subobjects is neither a subset nor a superset of
the immediate parents.
Closes#1881
This default instance makes it possible to write things like `m!"the
constant is {.ofConstName n}"`.
Breaking change: This weakly causes terms to have a type of
`MessageData` if their type is otherwise unknown. For example:
* `m!"... {x} ..."` can cause `x` to have type `MessageData`, causing
the `let` definition of `x` to fail to elaborate. Fix: give `x` an
explicit type.
* Arithmetic expressions in `m!` strings may need a type ascription. For
example, if the type of `i` is unknown at the time the arithmetic
expression is elaborated, then `m!"... {i + 1} ..."` can fail saying
that it cannot find an `HAdd Nat Nat MessageData` instance. Two fixes:
either ensure that the type of `i` is known, or add a type ascription to
guide the `MessageData` coercion, like `m!"... {(i + 1 : Nat)} ..."`.
Using the same strategy as #5852 this provides `bv_decide` support for
`Bool` and `BitVec` ifs
this in turn instantly enables support for:
- `sdiv`
- `smod`
- `abs`
and thus closes our last discrepancies to QF_BV!
This is the first step towards fixing the issue of not having mutual
recursion between the `Bool` and `BitVec` fragment of `QF_BV` in
`bv_decide`. This PR adds support for `BitVec.ofBool` by doing the
following:
1. Introduce a new mechanism into the reification engine that allows us
to add additional lemmas to the top level on the fly as we are
traversing the expression tree.
2. If we encounter an expression `BitVec.ofBool boolExpr` we reify
`boolExpr` and then abstract `BitVec.ofBool boolExpr` as some atom `a`
3. We add two lemmas `boolExpr = true -> a = 1#1` and `boolExpr = false
-> a = 0#1`. This mirrors the full behavior of `BitVec.ofBool` and thus
makes our atom `a` correctly interpreted again.
In order to do the reification in step 2 mutual recursion in the
reification engine is required. For this reason I started pulling out
logic from the, now rather large, mutual block into other files and
document the invariants that they assume explicitly.
A step of expanding structure instances is to determine all the default
values, and part of this is reducing projections that appear in the
default values so that they get replaced with the user-provided values.
Binder types in foralls, lambdas, and lets have to be reduced too.
Closes#2186
Refactors the `structure` command to support recursive structures. These
are disabled for now, pending additional elaborator support in #5822.
This refactor is also a step toward `structure` appearing in `mutual`
blocks.
Error reporting is now more precise, and this fixes an issue where
general errors could appear on the last field. Adds "don't know how to
synthesize placeholder" errors for default values.
Closes#2512
This adds a `parentInfo` field to the `StructureInfo`, which will
eventually be populated with the actual parents of a structure. This is
work toward #1881. Also documents fields of the structure info data
structures.
Requires a stage0 update before the next steps.
`generalize ... at *` sometimes will try to modify the recursive
hypothesis corresponding to the current theorem being defined, which may
not be the expected behaviour. It should only try to `generalize`
hypotheses that it can actually modify and are visible, not
implementation details. Otherwise this means that there are
discrepancies between `generalize ... at *` and `generalize ... at H`,
even though `H` is the only hypothesis in the context.
This commit uses `getLocalHyps` instead of `getFVarIds` to get the
current valid `FVarIds` in the context. This uses
`isImplementationDetail` to filter out `FVarIds` that are implementation
details in the context and are not visible to the user and should not be
manipulated by `generalize`.
Closes#4845
Closes#3146
Reduction doesn't trigger correctly on the bodies of `let`-expressions
in `StructInst`, leading some meta-variables to linger in the terms of
some fields. Because of this, default fields may try multiple times (and
fail) to be generated, leading to an unexpected error.
The solution implemented here is to modify the values of the introduced
variables in the local context so as to reduce them correctly.
The `liftCommandElabM : CommandElabM α -> CoreM α` function now carries
over macro scopes, the name generator, info trees, and messages.
Adds a flag `throwOnError`, which is true by default. When it is true,
then if the messages contain an error message, it is converted into an
exception. In this case, the infotrees and messages are not carried
over; the motivation is that `throwOnError` is likely used for synthetic
syntax, and so the info and messages on errors will just be noise.
Cleanup of #5650
* default `Modifiers.stx` to missing
* rename and clarify `addDeclarationRangesFromSyntax` as the main
convenience function for user metaprograms
Add an example Lean file that includes an unusually large definition
that takes a long time to elaborate.
It may be that it's difficult to process it more efficiently, but
perhaps someone will discover a way to improve it if it's in the
benchmark suite. Improved performance on this benchmark will likely make
some program analysis and verification tasks within Lean more feasible.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Example new output:
```text
failed to compile 'partial' definition 'checkMyList', could not prove that the type
ListNode → Bool × ListNode
is nonempty.
This process uses multiple strategies:
- It looks for a parameter that matches the return type.
- It tries synthesizing 'Inhabited' and 'Nonempty' instances for the return type.
- It tries unfolding the return type.
If the return type is defined using the 'structure' or 'inductive' command, you can try
adding a 'deriving Nonempty' clause to it.
```
The inhabitation prover now also unfolds definitions when trying to
prove inhabitation. For example,
```lean
def T (α : Type) := α × α
partial def f (n : Nat) : T Nat := f n
```
Motivated [by
Zulip](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Why.20return.20type.20of.20partial.20function.20MUST.20.60inhabited.60.3F/near/477905312)
Refactors `inductive` elaborator to keep track of universe level
parameters created during elaboration of `variable`s and binders. This
fixes an issue in Mathlib where its `Type*` elaborator can result in
unexpected universe levels.
For example, in
```lean4
variable {F : Type*}
inductive I1 (A B : Type*) (x : F) : Type
```
before this change the signature would be
```
I1.{u_1, u_2} {F : Type u_1} (A : Type u_1) (B : Type u_2) (x : F) : Type
```
but now it is
```
I1.{u_1, u_2, u_3} {F : Type u_1} (A : Type u_2) (B : Type u_3) (x : F) : Type
```
Fixes this for the `axiom` elaborator too.
Adds more accurate universe level validation for mutual inductives.
Breaking change: removes `Lean.Elab.Command.expandDeclId`. Use
`Lean.Elab.Term.expandDeclId` from within `runCommandElabM`.
Breaking changes:
To build Lean from source on Windows, it is now necessary to install the
[Windows
SDK](https://developer.microsoft.com/en-us/windows/downloads/windows-sdk/).
The build instructions have been updated to reflect this. Note that the
Windows SDK is **not** needed to compile Lean programs using a Lean
toolchain obtained using `elan`. The Windows SDK is only needed to build
Lean itself from source.
Furthermore, we are dropping support for Windows versions older than
Windows 10 1903 (released in May 2019).
No Windows version that is still supported by Microsoft as part of
mainstream support is affected by this.
The following Windows versions are still supported by Microsoft as part
of commercial extended support but are no longer supported by Lean:
- Windows 10 Enterprise LTSC 2015
- Windows 10 Enterprise LTSC 2016
- Windows 10 Enterprise LTSC 2019
- Windows Server 2019
It's difficult to distinguish theorems from regular definitions in the
completion menu, which is annoying when using completion for searching
one or the other. This PR makes theorem completions use the "Eureka!"
icon ()
to distinguish them more clearly from other completions.
NB: We are very limited in terms of which icons we can pick here since
[the completion kinds provided by LSP / VS
Code](https://code.visualstudio.com/docs/editor/intellisense#_types-of-completions)
are optimized for object-oriented programming languages, but I think
this choice strikes a nice balance between being easy to identify,
having some visual connection to theorem proving and not being used a
lot in other languages and thus not clashing with pre-existing
associations.
Between #3106 and this, it was possible that reparsing the file up to
the current position was stuck waiting in the threadpool queue,
displaying a yellow bar and not displaying any info on the unchanged
prefix.
`instantiate_mvars` is now implemented in C/C++, and makes many calls to
`has_fvar`, `has_mvar`. The new C/C++ implementations are inlined and
avoid unnecessary RC inc/decs.
Previously `RecursorVal.getInduct` would return the prefix of the
recursor’s name, which is unlikely the right value for the “derived”
recursors in nested recursion. The code using `RecursorVal.getInduct`
seems to expect the name of the inductive type of major argument here.
If we return that name, this fixes#5661.
This bug becomes more visible now that we have structural mutual
recursion.
Also, to avoid confusion, renames the function to ``getMajorInduct`.
This PR simplifies the signature of `Array.mapIdx`, to take a function
`f : Nat \to \a \to \b` rather than a function `f : Fin as.size \to \a
\to \b`.
Lean doesn't actually use the extra generality anywhere (so in fact this
change *simplifies* all the call sites of `Array.mapIdx`, since we no
longer need to throw away the proof).
This change would make the function signature equivalent to
`List.mapIdx`, hence making it easier to write verification lemmas.
We keep the original behaviour as `Array.mapFinIdx`.
This replaces `export Lean (Name NameMap)` and `export System
(SearchPath FilePath)` with the relevant `open` commands. This fixes
docgen output so that it can refer to, for example, `Lean.Name` instead
of `Lake.Name`.
The reason for these `export`s was convenience: by doing `open Lake` you
could get these aliases for free. However, aliases affect pretty
printing, and the Lake aliases took precedence. We don't want to disable
pretty printing re-exported names because this can be a valid pattern
(names could incrementally get re-exported from namespace to parent
namespace).
In the future we might implement a feature to be able to `scoped open`
some names.
Breaking change: Lakefiles that refer to `FilePath` may need to change
this to `System.FilePath` or otherwise add `open System (FilePath)`.
Closes#2524
This PR resolves the following issues related to goal state display:
1. In a new line after a `case` tactic with a completed proof, the state
of the proof in the `case` would be displayed, not the proof state after
the `case`
1. In the range of `next =>` / `case' ... =>`, the state of the proof in
the corresponding case would not be displayed, whereas this is true for
`case`
1. In the `suffices ... by` tactic, the tactic state of the `by` block
was not displayed after the `by` and before the first tactic
The incorrect goal state after `case` was caused by `evalCase` adding a
`TacticInfo` with the full block proof state for the full range of the
`case` block that the goal state selection has no means of
distinguishing from the `TacticInfo` with the same range that contains
the state after the whole `case` block. Narrowing the range of this
`TacticInfo` to `case ... =>` fixed this issue.
The lack of a case proof state on `next =>` was caused by the `case`
syntax that `next` expands to receiving noncanonical synthetic
`SourceInfo`, which is usually ignored by the language server. Adding a
token antiquotation for `next` fixed this issue.
The lack of a case proof state on `case' ... =>` was caused by
`evalCase'` not adding a `TacticInfo` with the full block state to the
range of `case' ... =>`. Adding this `TacticInfo` fixed this issue.
The tactic state of the block not being displayed after the `by` was
caused by the macro expansion of `suffices` to `have` not transferring
the trailing whitespace of the `by`. Ensuring that this trailing
whitespace information is transferred fixed this issue.
Fixes#2881.
Should ensure we visit at most as many expr nodes as in the final expr
instead of many possibly overlapping mvar assignments. This is likely
the only way we can ensure acceptable performance in all cases.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
this option was added in fb97275dcb to
prepare for #4595, due to boostrapping issues, but #4595 has not landed
yet. This is be very confusing when people discover this option and try
to use it (as I did).
So let's clearly mark this as not yet implemented on `master`, and add
the
docstring only with #4595.
Since `getMsbD_add`, `getMsbD_sub`, `getLsbD_sub`, `msb_sub` , `msb_add`
depend on `getLsbD_add` (which lives in`BitBlast.lean`) and on each
other, I put all of these in `BitBlast.lean`.
It bothered me that inferring instances of the shape `Decidable (∀ (x : Fin _), _)`
will go linearly through all instances of that shape, even those that are
about `∀ (x : Nat), …`. And that `Decidable (∃ (x : Fin _), _)` gets better
indexing than `Decidable (∀ (x : Fin _), _)`.
Judging from code comments, the discr tree used to index arrow types
with two arguments (domain and body), and that led to bugs due to the
dependency, so the arguments were removed. But it seems that indexing
the domain is completely simple and innocent.
So let’s see what happens…
Mostly only insignificant perf improvements, unfortunately (~Mathlib.Data.Matroid.IndepAxioms — instructions -11.4B, overall build instructions -0.097 %):
http://speed.lean-fro.org/mathlib4/compare/dd333cc1-fa26-42f2-96c6-b0e66047d0b6/to/6875ff8f-a17c-431d-8b8b-2f00799be794
This is just a small baby step compared to the more invasive improvements
done in the [`RefinedDiscrTree` by J. W. Gerbscheid](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/FunProp/RefinedDiscrTree.html) in mathlib.
I made a few choices so far that can probably be discussed:
- got rid of `modn` on `UInt`, nobody seems to use it apart from the
definition of `shift` which can use normal `mod`
- removed the previous defeq optimized definition of `USize.size` in
favor for a normal one. The motivation was to allow `OfNat` to work
which doesn't seem to be necessary anymore afaict.
- Minimized uses of `.val`, should we maybe mark it deprecated?
- Mostly got rid of `.val` in basically all theorems as the proper next
level of API would now be `.toBitVec`. We could probably re-prove them
but it would be more annoying given the change of definition.
- Did not yet redefine `log2` in terms of `BitVec` as this would require
a `log2` in `BitVec` as well, do we want this?
- I added a couple of theorems around the relation of `<` on `UInt` and
`Nat`. These were previously not needed because defeq was used all over
the place to save us. I did not yet generalize these to all types as I
wasn't sure if they are the appropriate lemma that we want to have.
Adds `pushGoal`/`pushGoals` and `popGoal` for manipulating the goal
state. These are an alternative to `replaceMainGoal` and `getMainGoal`,
and with them you don't need to worry about making sure nothing clears
assigned metavariables from the goal list between assigning the main
goal and using `replaceMainGoal`.
Modifies `closeMainGoalUsing`, which is like a `TacticM` version of
`liftMetaTactic`. Now the callback is run in a context where the main
goal is removed from the goal list, and the callback is free to modify
the goal list. Furthermore, the `checkUnassigned` argument has been
replaced with `checkNewUnassigned`, which checks whether the value
assigned to the goal has any *new* metavariables, relative to the start
of execution of the callback. This API is sufficient for the `exact`
tactic for example.
Modifies `withCollectingNewGoalsFrom` to take the `parentTag` argument
explicitly rather than indirectly via `getMainTag`. This is needed when
used under `closeMainGoalUsing`.
Modifies `elabTermWithHoles` to optionally take `parentTag?`. It
defaults to `getMainTag` if it is `none`.
Renames `Tactic.tryCatch` to `Tactic.tryCatchRestore`, and adds a
`Tactic.tryCatch` that doesn't do backtracking.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
`getNumHeadForalls` and `getNumHeadLambdas` were both duplicated
downstream with different names; I'll clean up those next.
Also adds `getAppNumArgs'`.
it seems to be unused, arguably even for kernel recursors their type
should be usable with `mkRecursorInfo`, and removing this will help
understand the impact of #5679.
Mathlib has a duplicate of this instance as `Quotient.decidableEq` (with
the same implementation) and refers to it by name a few times, so let's
just rename our version to the mathlib name so that the copy in mathlib
can be dropped.
This takes a few standalone bitvector problems, about inequalties, from
LNSym, and adds them as a benchmark to prevent further regressions with
bv_decide.
These problems are particularly interesting, because they've previously
had a bad interaction with bv_decides normalization pass, see
https://github.com/leanprover/lean4/issues/5664.
---------
Co-authored-by: Henrik Böving <hargonix@gmail.com>
Projects like mathlib like to define projection functions with extra
structure, for example one could imagine defining `Multiset.card :
Multiset α →+ Nat`, which bundles the fact that `Multiset.card (m1 + m2)
= Multiset.card m1 + Multiset.card m2` for all `m1 m2 : Multiset α`. A
problem though is that so far this has prevented dot notation from
working: you can't write `(m1 + m2).card = m1.card + m2.card`.
With this PR, now you can. The way it works is that "LValue resolution"
will apply CoeFun instances when trying to resolve which argument should
receive the object of dot notation.
A contrived-yet-representative example:
```lean
structure Equiv (α β : Sort _) where
toFun : α → β
invFun : β → α
infixl:25 " ≃ " => Equiv
instance: CoeFun (α ≃ β) fun _ => α → β where
coe := Equiv.toFun
structure Foo where
n : Nat
def Foo.n' : Foo ≃ Nat := ⟨Foo.n, Foo.mk⟩
variable (f : Foo)
#check f.n'
-- Foo.n'.toFun f : Nat
```
Design note 1: While LValue resolution attempts to make use of named
arguments when positional arguments cannot be used, when we apply CoeFun
instances we disallow making use of named arguments. The rationale is
that argument names for CoeFun instances tend to be random, which could
lead dot notation randomly succeeding or failing. It is better to be
uniform, and so it uniformly fails in this case.
Design note 2: There is a limitation in that this will *not* make use of
the values of any of the provided arguments when synthesizing the CoeFun
instances (see the tests for an example), since argument elaboration
takes place after LValue resolution. However, we make sure that
synthesis will fail rather than choose the wrong CoeFun instance.
Performance note: Such instances will be synthesized twice, once during
LValue resolution, and again when applying arguments.
This also adds in a small optimization to the parameter list computation
in LValue resolution so that it lazily reduces when a relevant parameter
hasn't been found yet, rather than using `forallTelescopeReducing`. It
also switches to using `forallMetaTelescope` to make sure the CoeFun
synthesis will fail if multiple instances could apply.
Getting this to pretty print will be deferred to future work.
Closes#1910
Gives more control over pretty printing metavariables.
- When `pp.mvars.levels` is false, then universe level metavariables
pretty print as `_` rather than `?u.22`
- When `pp.mvars.anonymous` is false, then anonymous metavariables
pretty print as `?_` rather than `?m.22`. Named metavariables still
pretty print with their names. When this is false, it also sets
`pp.mvars.levels` to false, since every level metavariable is anonymous.
- When `pp.mvars` is false, then all metavariables pretty print as `?_`
or `_`.
Modifies TryThis to use `pp.mvars.anonymous` rather than doing a
post-delaboration modification. This incidentally improves TryThis since
it now prints universe level metavariables as `_` rather than `?u.22`.
We trust that the users read the error messages or tactic docs to
discover the option.
AWS problems have shown that this can be too eager of an operation to
do.
Given that we have the luxury of interactivity let's go for an approach
where the users
can optionally enable it.
This PR ensures that deprecated declarations are displayed with a
strikethrough markup in the completion popup of VS Code and that the
docstring of a completion item denotes the meta-data of the deprecation.
These lemmas are peeled from `leanprover/lnsym`.
Moreover, note that these lemmas only hold when we do not have overflow
in their operands, and thus, we are able to treat the operands as if
they were 'regular' natural numbers.
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Kim Morrison <scott@tqft.net>
Divison proofs are more likely to depend on add/sub/mul proofs than the
other way around. This cleans up
https://github.com/leanprover/lean4/pull/5609, which added division
proofs that rely on negation to already be defined.
Closes#5682
- Removes the broken `-f` flag from the help message which doesn't
behave as expected as an alternative to `--features`.
- Adds the `-g` flag to the help message which is a working alternative
to the `--githash` flag.
Lake will now only automatically fetch Reservoir build caches for
package in the the `leanprover` and `leanprover-community`
organizations. We are not planning to expand the Reservoir build cache
to other packages until farther in the future.
Makes `#eval` use the `elabMutualDef` machinery to process all the `let
rec`s that might appear in the expression. This now works:
```lean
#eval
let rec fact (n : Nat) : Nat :=
match n with
| 0 => 1
| n' + 1 => n * fact n'
fact 5
```
Closes#2374
The `decide!` tactic is like `decide`, but when it tries reducing the
`Decidable` instance it uses kernel reduction rather than the
elaborator's reduction.
The kernel ignores transparency, so it can unfold all definitions (for
better or for worse). Furthermore, by using kernel reduction we can
cache the result as an auxiliary lemma — this is more efficient than
`decide`, which needs to reduce the instance twice: once in the
elaborator to check whether the tactic succeeds, and once again in the
kernel during final typechecking.
While RFC #5629 proposes a `decide!` that skips checking altogether
during elaboration, with this PR's `decide!` we can use `decide!` as
more-or-less a drop-in replacement for `decide`, since the tactic will
fail if kernel reduction fails.
This PR also includes two small fixes:
- `blameDecideReductionFailure` now uses `withIncRecDepth`.
- `Lean.Meta.zetaReduce` now instantiates metavariables while zeta
reducing.
Some profiling:
```lean
set_option maxRecDepth 2000
set_option trace.profiler true
set_option trace.profiler.threshold 0
theorem thm1 : 0 < 1 := by decide!
theorem thm1' : 0 < 1 := by decide
theorem thm2 : ∀ x < 400, x * x ≤ 160000 := by decide!
theorem thm2' : ∀ x < 400, x * x ≤ 160000 := by decide
/-
[Elab.command] [0.003655] theorem thm1 : 0 < 1 := by decide!
[Elab.command] [0.003164] theorem thm1' : 0 < 1 := by decide
[Elab.command] [0.133223] theorem thm2 : ∀ x < 400, x * x ≤ 160000 := by decide!
[Elab.command] [0.252310] theorem thm2' : ∀ x < 400, x * x ≤ 160000 := by decide
-/
```
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Deprecates `inductive ... :=`, `structure ... :=`, and `class ... :=` in
favor of the `... where` variant. Currently this syntax produces a
warning, controlled by the `linter.deprecated` option.
Breaking change: modifies `Lean.Linter.logLintIf` to use
`Lean.Linter.getLinterValue` to determine if a linter value is set. This
means that the `linter.all` option now is taken into account when the
linter option is not set.
Part of #5236
This PR enables tactic completion in the whitespace of a tactic proof
and adds tactic docstrings to the completion menu.
Future work:
- A couple of broken tactic completions: This is due to tactic
completion now using @david-christiansen's `Tactic.Doc.allTacticDocs` to
obtain the tactic docstrings and should be fixed soon.
- Whitespace tactic completion in tactic combinators: This requires
changing the syntax of tactic combinators to produce a syntax node that
makes it clear that a tactic is expected at the given position.
Closes#1651.
When named arguments introduce eta arguments, the full application
contains fvars for these eta arguments, so `MVarErrorKind.implicitArg`
needs to keep a local context for its error messages. This is because
the local context of the mvar associated to the `MVarErrorKind` is not
sufficient, since when an eta argument come after an implicit argument,
the implicit argument's mvar doesn't contain the eta argument's fvar in
its local context.
Closes#5475
Now one can write `@x.f`, `@(x).f`, `@x.1`, `@(x).1`, and so on.
This fixes an issue where structure instance update notation (like `{x
with a := a'}`) could fail if the field `a` had a type with implicit,
optional, or auto parameters.
Closes#5406
Fixes#5565, by using tags instead of trying to string match on a
`MessageData`. This ends up reverting some unwanted test output changes
from #4781 too.
This changes `isMaxRecDepth` for good measure too.
This was a regression in Lean 4.11.0, so may be worth backporting to
4.12.x, if not also 4.11.x.
A Lake build of target within a a package will no longer build a
package's dependencies package-level extra targets dependencies. At the
technical level, a package's `extraDep` facet no longer transitively
builds its dependencies' `extraDep` facet.
Closes#5633.
Closes#5634. Before assigning the simplified `using` clause expression
to the goal, this adds a check that the expression has no new
metavariables. It also adjusts how new hypotheses are added to the goal
to prevent spurious "don't know how to synthesize placeholder" errors on
that goal metavariable. We also throw in an occurs check immediately
after elaboration to avoid some counterintuitive behavior when
simplifying such a term closes the goal.
Closes#4101. This also improves the type mismatch error message,
showing the elaborated `using` clause rather than `h✝`:
```lean
example : False := by
simpa using (fun x : True => x)
/-
error: type mismatch, term
fun x => x
after simplification has type
True : Prop
but is expected to have type
False : Prop
-/
```
A `Prop`-valued inductive type is a syntactic subsingleton if it has at
most one constructor and all the arguments to the constructor are in
`Prop`. Such types have large elimination, so they could be defined in
`Type` or `Prop` without any trouble, though users tend to expect that
such types define a `Prop` and need to learn to insert `: Prop`.
Currently, the default universe for types is `Type`. This PR adds a
heuristic: if a type is a syntactic subsingleton with exactly one
constructor, and the constructor has at least one parameter, then the
`inductive` command will prefer creating a `Prop` instead of a `Type`.
For `structure`, we ask for at least one field.
More generally, for mutual inductives, each type needs to be a syntactic
subsingleton, at least one type must have one constructor, and at least
one constructor must have at least one parameter. The motivation for
this restriction is that every inductive type starts with a zero
constructors and each constructor starts with zero fields, and
stubbed-out types shouldn't be `Prop`.
Thanks to @arthur-adjedj for the investigation in #2695 and to @digama0
for formulating the heuristic.
Closes#2690
This refactors and improves the `#eval` command, introducing some new
features.
* Now evaluated results can be represented using `ToExpr` and pretty
printing. This means **hoverable output**. If `ToExpr` fails, it then
tries `Repr` and then `ToString`. The `eval.pp` option controls whether
or not to try `ToExpr`.
* There is now **auto-derivation** of `Repr` instances, enabled with the
`pp.derive.repr` option (default to **true**). For example:
```lean
inductive Baz
| a | b
#eval Baz.a
-- Baz.a
```
It simply does `deriving instance Repr for Baz` when there's no way to
represent `Baz`. If core Lean gets `ToExpr` derive handlers, they could
be used here as well.
* The option `eval.type` controls whether or not to include the type in
the output. For now the default is false.
* Now things like `#eval do return 2` work. It tries using
`CommandElabM`, `TermElabM`, or `IO` when the monad is unknown.
* Now there is no longer `Lean.Eval` or `Lean.MetaEval`. These each used
to be responsible for both adapting monads and printing results. The
concerns have been split into two. (1) The `MonadEval` class is
responsible for adapting monads for evaluation (it is similar to
`MonadLift`, but instances are allowed to use default data when
initializing state) and (2) finding a way to represent results is
handled separately.
* Error messages about failed instance synthesis are now more precise.
Once it detects that a `MonadEval` class applies, then the error message
will be specific about missing `ToExpr`/`Repr`/`ToString` instances.
* Fixes a bug where `Repr`/`ToString` instances can't be found by
unfolding types "under the monad". For example, this works now:
```lean
def Foo := List Nat
def Foo.mk (l : List Nat) : Foo := l
#eval show Lean.CoreM Foo from do return Foo.mk [1,2,3]
```
* Elaboration errors now abort evaluation. This eliminates some
not-so-relevant error messages.
* Now evaluating a value of type `m Unit` never prints a blank message.
* Fixes bugs where evaluating `MetaM` and `CoreM` wouldn't collect log
messages.
The `run_cmd`, `run_elab`, and `run_meta` commands are now frontends for
`#eval`.
This verifies a bit hack from here:
https://en.wikipedia.org/wiki/Lehmer_random_number_generator#Sample_C99_code
I previously ran the SMTLIB equivalent this with Bitwuzla in my crypto
class and got the following numbers:
- 22s with Bitwuzla
- Z3 and CVC5 don't yet terminate after > 2min
Now with`bv_decide` the overall timing is 33.7s, consisting of:
- 5s of checking the LRAT cert
- 5s of trimming the LRAT cert from 800k to 300k proof steps
- remainder actual solving time
So running `bv_decide` like a normal SMT solver without verifying the
result of the SAT solver would yield approximately ~24s.
Where before we had
```lean
#check fun x : Nat => ?a
-- fun x ↦ ?m.7 x : (x : Nat) → ?m.6 x
```
Now by default we have
```lean
#check fun x : Nat => ?a
-- fun x => ?a : (x : Nat) → ?m.6 x
```
In particular, delayed assignment metavariables such as `?m.7` pretty
print using the name of the metavariable they are delayed assigned to,
suppressing the bound variables used in the delayed assignment (hence
`?a` rather than `?a x`). Hovering over `?a` shows `?m.7 x`.
The benefit is that users can see the user-provided name in local
contexts. A justification for this pretty printing choice is that `?m.7
x` is supposed to stand for `?a`, and furthermore it is just as opaque
to assignment in defeq as `?a` is (however, when synthetic opaque
metavariables are made assignable, delayed assignments can be a little
less assignable than true synthetic opaque metavariables).
The original pretty printing behavior can be recovered using `set_option
pp.mvars.delayed true`.
This PR also extends the documentation for holes and synthetic holes,
with some technical details about what delayed assignments are. This
likely should be moved to the reference manual, but for now it is
included in this docstring.
(This PR is a simplified version of #3494, which has a round-trippable
notation for delayed assignments. The pretty printing in this PR is
unlikely to round trip, but it is better than the current situation,
which is that delayed assignment metavariables never round trip, and
plus it does not require introducing a new notation.)
The app unexpanders for `Name.mkStr1` through `Name.mkStr8` weren't
respecting the escaping rules for names. For example, ``#check `«a.b»``
would show `` `a.b``.
This PR folds the unexpanders into the name literal delaborator, where
escaping is already handled.
The `#guard_msgs` command runs the command it is attached to as if it
were a top-level command. This is because the top-level command
elaborator runs linters, and we are interested in capturing linter
warnings using `#guard_msgs`. However, the linters will run on
`#guard_msgs` itself, leading sometimes to duplicate warnings (like for
the unused variable linter).
Rather than special-casing `#guard_msgs` in every affected linter, this
PR special-cases it in the top-level command elaborator itself. **Now
linters are only run if the command doesn't contain `#guard_msgs`.**
This way, the linters are only run on the sub-command that `#guard_msgs`
runs itself. This rule also keeps linters from running multiple times in
cases such as `set_option pp.mvars false in /-- ... -/ #guard_msgs in
...`.
This follows the norm for all other Bitvector operations, and makes the
symbols `/` and `%` the simp normal form.
I'd imagine that @hargonix would prefer that this be merged after
https://github.com/leanprover/lean4/pull/5628, so as to prevent churn
for his PR. I'm happy to rebase the PR once the other PR lands.
---------
Co-authored-by: Henrik Böving <hargonix@gmail.com>
These lemmas explain what happens when the denominator is zero with
`udiv`, `umod`, `sdiv`, `smod`. A follow-up PR will show what happens
with `smtUDiv` and `smtSMod`, since these need some more bitvector
theory.
These lemmas will be used by `bv_decide` for bitblasting.
The theorems `{sdiv, smod}_zero` are located after `neg` theory has been
built for the purpose of writing terse proofs.
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
This PR fixes three problems:
- When the language server is being stopped in a non-normal way without
going through the regular LSP shutdown protocol (e.g. by closing VS
Code), it could sometimes happen that both the watchdog and the file
worker were not properly terminated and lingered around forever,
resulting in zombie processes (#5296)
- When the file worker crashes and the user restarts it by making a
change to the document, the file worker would produce incorrect
diagnostics for the document until the file is restarted.
- (Minor) When the file worker would crash during initialization, the
error diagnostic would be reported on stderr instead of stdout
The deadlock-induced termination issue from #5296 should be resolved by
the following measures:
- The watchdog main task is always terminated with `IO.Process.exit` to
ensure that it terminates even if some other tasks in the process are
still running.
- The file worker communication task in the watchdog no longer waits for
the file worker process to terminate when writing to the client fails,
only when reading from the file worker fails.
- When the watchdog shuts down (either as a result of an orderly or a
non-normal shutdown), instead of waiting for the file worker
communication tasks to complete, it kills the file worker process. The
rationale behind this is that the file worker currently should have no
essential work to complete if the server is being stopped anyways, and
so waiting for the communication task is not necessary.
The file worker diagnostic desync after a crash was caused by us
tracking changes to the document of a crashed file worker twice: Once as
part of the document, and once as part of the queued messages to the
file worker. This meant that when the file worker was restarted, it
would receive the changes made to the document while the file worker was
crashed twice, leading to a desynced document state.
(Probably) fixes#5296.
... while at it also call `trivial` to close goals that can be trivially
closed.
---------
Co-authored-by: Siddharth <siddu.druid@gmail.com>
Co-authored-by: Henrik Böving <hargonix@gmail.com>
when the transparency mode is `.all`, then one expects `getFunInfo` and
`inferType` to also work with that transparency mode.
Fixes#5562Fixes#2975Fixes#2194
While `initialize` pretended it had the declaration name of the constant
to be initialized, missing declaration ranges for the latter led call
hierarchy etc. to ignore the definition
Lake no longer attempts to fetch the Reservoir build cache if the build
directory is already present. Plus, failure of the automatic fetch now
only produces a trace message, not a warning.
@kim-em, I'm happy to keep any subset of `foldl_min`, `foldl_min_right`,
`foldl_min_le`, `foldl_min_min_of_le` (should that one have been called
`foldl_min_le_of_le`?). Which ones do you like?
I think the overhead (runtime/later proving) of using `for` is paid off
by being able to short-circuit.
These functions are needed downstream to switch over the Std.HashSet.
On Windows, shared libraries must be removed before linking. Otherwise,
linking can fail with "Permission denied" when the libraries are in use.
This ensures such removal is done for the new `libLake_shared.dll` and
both parts of `libleanshared`.
Lake no longer attempts to fetch Reservoir build caches (barrels) for
non-Reservoir dependencies, and it will only fetch them for Reservoir
dependencies in the presence of a known toolchain.
Also, optional build job failures are now only displayed in verbose
mode.
In C, these are supported only as a vendor extension; they should
instead use proper C99 flexible array members.
In C++, both `[]` and `[0]` are vendor extensions.
Co-authored-by: Thomas Köppe <tkoeppe@google.com>
The constructor `AttributeExtensionOLeanEntry.decl` and related code
seems to be unused, and has been unused since its introduction in
a77598f7cf three years ago. Probably worth
removing (and changing the now one-constructor inductive into a
structure).
ac_nf is a counterpart to ac_rfl, which normalizes bitvector expressions
with respect to associativity and commutativity.
While there, also add test coverage for ac_rfl and ac_nf for BitVec,
complementing the existing test coverage.
The lemma `exists_const` already handles all real cases of `(∃ _ : α, p)
↔ p` for general types `α`. If there are no `Nonempty` instances and
this lemma cannot apply, it seems unlikely that simp could make more
progress with `(∃ _ : α, p) ↔ Nonempty α ∧ p`.
However, it is still worth simplifying `(∃ _ : p, q)` to `p ∧ q`.
Also adds a `Nonempty (Decidable a)` instance, which is used by Mathlib.
…|twoPow|one|replicate]
... and mark `getElem_setWidth` as `@[simp]`.
`getElem_rotateLeft` and `getElem_rotateRight` have a non-trivial rhs
but we follow `getLsbD_[rotateLeft|rotateRight]`for consistency.
---------
Co-authored-by: Kim Morrison <scott@tqft.net>
Adds Reservoir as another possible source of build caches in addition to
GitHub releases. If a GitHub release is not configured for a Reservoir
dependency, it will attempt download a build cache from Reservoir. Like
with GitHub releases, failure will not stop the build and instead issue
a warning. Many of the Lake API calls related to these build caches were
refactored and renamed, with the old names remaining around as
deprecated aliases.
Build cache downloads (from Reservoir or GitHub) can now be disabled via
the `--no-cache` CLI option or the `LAKE_NO_CACHE` environment variable.
A disabled cache can be re-enable with the `--try-cache` CLI option.
Macros sometimes create auxiliary types and instances about them, and
they rely on the instance name generate to create unique names in that
case.
This modifies the automatic name generator to add a fresh macro scope to
the generated name if any of the constants in the type of the instance
themselves have macro scopes.
Closes#2044
Generally works best to pick up the proofs by unification with the lhs.
pinging @hargoniX as this goes by, as it changes some proofs in
bv_decide (nothing interesting, just a bit simpler)
@bollu, it would be good to have confirmation from you, but presumably
this was not meant to be `@[simp]`? It competes with `divRec_succ`, and
has a terrible RHS.
after this change, `simp` will be able to discharge side-goals that,
after simplification, are of the form `∀ …, a = b` with `a =?= b`.
Usually these side-goals are solved by simplification using `eq_self`,
but that does not work when there are metavariables involved.
This enables us to have rewrite rules like
```
theorem List.foldl_subtype (p : α → Prop) (l : List (Subtype p)) (f : β → Subtype p → β)
(g : β → α → β) (b : β)
(hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
l.foldl f b = (l.map (·.val)).foldl g b := by
```
where the parameter `g` does not appear on the lhs, but can be solved
for using the `hf` equation. See `tests/lean/run/simpHigherOrder.lean`
for more examples.
The motivating use-case is that `simp` should be able to clean up the
usual
```
l.attach.map (fun <x, _> => x)
```
idiom often seen in well-founded recursive functions with nested
recursion.
Care needs to be taken with adding such rules to the default simp set if
the lhs is very general, and thus causes them to be tried everywhere.
Performance impact of just this PR (no additional simp rules) on mathlib
is unsuspicious:
http://speed.lean-fro.org/mathlib4/compare/b5bc44c7-e53c-4b6c-9184-bbfea54c4f80/to/ae1d769b-2ff2-4894-940c-042d5a698353
I tried a few alternatives, e.g. letting `simp` apply `eq_self` without
bumping the mvar depth, or just solve equalities directly, but that
broke too much things, and adding code to the default discharger seemed
simpler.
The formatter was using `tk ++ " "` to separate tokens from tokens they
would merge with, but `" "` is not whitespace that could merge. This
affected large binder lists, which wouldn't pretty print with any line
breaks. Now they can be flowed across multiple lines.
Closes#5424
Just an `Array` version of `List.eraseReps`. These functions are for now
outside of scope for verification, so there's just a simple `example` in
the tests.
Now the elab-as-elim procedure allows eliminators whose result is an
arbitrary application of the motive. For example, the following is now
accepted. It will generalize `Int.natAbs _` from the expected type.
```lean
@[elab_as_elim]
theorem natAbs_elim {motive : Nat → Prop} (i : Int)
(hpos : ∀ (n : Nat), i = n → motive n)
(hneg : ∀ (n : Nat), i = -↑n → motive n) :
motive (Int.natAbs i) := by sorry
```
This change simplifies the elaborator, since it no longer needs to keep
track of discriminants (which can easily be read off from the return
type of the eliminator) or the difference between "targets" and "extra
arguments" (which are now both "major arguments" that should be eagerly
elaborated).
Closes#4086
`BitVec.Lemmas` contained a couple of non-terminal simps. We turn
non-terminal `simp$`, `simp [`, and `simp at` expressions into `simp
only` to improve code maintainability.
This was upstreamed from Mathlib in #5478, but leaving off the `@[simp]`
attribute, thereby breaking Mathlib. (We could of course add the simp
attribute back in Mathlib, but wherever it lives it should have been in
place at the time we merged -- this way I have to add it temporarily in
Mathlib and then remove it again once it is redundant.)
Recall that currently named arguments suppress all explicit parameters
that are dependencies. This PR limits this feature to only apply to true
structure projections, except in the case where it is triggered when
there are no more positional arguments. This preserves the primary
reason for generalizing this feature (issue #1851), while removing the
generalized feature, which has led to numerous confusions (issue #1867).
This also fixes a bug pointed out [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.40foo.20.28A.20.3A.3D.20bar.29.20_.20_/near/468564862)
where in `@` mode, instance implicit parameter dependencies to named
arguments would be suppressed unless the next positional argument was
`_`.
More detail:
* The `NamedArg` structure now has a `suppressDeps : Bool` field. It is
set to `true` for the `self` argument in structure projections. If there
is such a `NamedArg`, explicit parameters that are dependencies to the
named argument are turned into implicit arguments. The consequence is
that *all* structure projections are treated as if their type parameters
are implicit, even for class projections. This flag is *not* used for
generalized field notation.
* We preserve the suppression feature when there are no positional
arguments remaining. This feature pre-dates the fix to issue #1851, and
it is useful when combining named arguments and the eta expansion
feature, since dependencies of named arguments cannot be turned into eta
arguments. Plus, there are examples of the form `rw [lem (h := foo)]`
where `lem` has explicit arguments that `h` depends on.
* For instance implicit parameters in explicit mode, now `_` arguments
register terminfo and are hoverable.
* Now `..` is respected in explicit mode.
This implements RFC #5397. The `suppressDeps` flag suggests a future
possibility of a named argument syntax that can suppress dependencies.
Adds a mechanism where when an autoparam tactic fails to synthesize a
parameter, the associated parameter name or field name for the autoparam
is reported in an error.
Examples:
```text
could not synthesize default value for parameter 'h' using tactics
could not synthesize default value for field 'inv' of 'S' using tactics
```
Notes:
* Autoparams now run their tactics without any error recovery or
error-to-sorry enabled. This enables catching the error and reporting
the contextual information. This is justified on the grounds that
autoparams are not interactive.
* Autoparams for applications now cleanup the autoParam annotation,
bringing it in line with autoparams for structure fields.
* This preserves the old behavior that autoparams leave terminfo, but we
will revisit this after some imminent improvements to the unused
variable linter.
Closes#2950
`elabEvalUnsafe` already does something similar: it also instantiates
universe metavariables, but it is not clear to me whether that is
sensible here.
To be conservative, I leave it out of this PR.
See https://github.com/leanprover/lean4/pull/3090#discussion_r1432007590
for a comparison between `#eval` and `Meta.evalExpr`. This PR is not
trying to fully align them, but just to fix one particular misalignment
that I am impacted by.
Closes#3091
This PR adds the theorems
```
@[simp]
theorem divRec_zero (qr : DivModState w) :
divRec w w 0 n d qr = qr
@[simp]
theorem divRec_succ' (wn : Nat) (qr : DivModState w) :
divRec w wr (wn + 1) n d qr =
let r' := shiftConcat qr.r (n.getLsbD wn)
let input : DivModState w :=
if r' < d then ⟨qr.q.shiftConcat false, r'⟩ else ⟨qr.q.shiftConcat true, r' - d⟩
divRec w (wr + 1) wn n d input
```
The final statements may need some masasging to interoperate with
`bv_decide`. We prove the recurrence for unsigned division by building a
shift-subtract circuit, and then showing that this circuit obeys the
division algorithm's invariant.
---
A `DivModState` is lawful if the remainder width `wr` plus the dividend
width `wn` equals `w`,
and the bitvectors `r` and `n` have values in the bounds given by
bitwidths `wr`, resp. `wn`.
This is a proof engineering choice: An alternative world could have
`r : BitVec wr` and `n : BitVec wn`, but this required much more
dependent typing coercions.
Instead, we choose to declare all involved bitvectors as length `w`, and
then prove that
the values are within their respective bounds.
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Kim Morrison <scott@tqft.net>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
There's a comment on `withHeartbeats` that says "See also
Lean.withSeconds", but his definition does not seem to actually exist.
Hence, I've removed the comment.
Add iff version of `List.IsPrefix.getElem`, and `eq_of_length_le`
variants of `List.IsInfix.eq_of_length, List.IsPrefix.eq_of_length,
List.IsSuffix.eq_of_length`
We make sure that we can pull `List.toArray` out through all operations
(well, for now "most" rather than "all"). As we also push `Array.toList`
inwards, this hopefully has the effect of them cancelling as they meet,
and `simp` naturally rewriting Array operations into List operations
wherever possible.
This is not at all complete yet.
building upon #3714, this (almost) implements the second half of #3302.
The main effect is that we now get a better error message when `rfl`
fails. For
```lean
example : n+1+m = n + (1+m) := by rfl
```
instead of the wall of text
```
The rfl tactic failed. Possible reasons:
- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
- The arguments of the relation are not equal.
Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
`exact HEq.rfl` etc.
n m : Nat
⊢ n + 1 + m = n + (1 + m)
```
we now get
```
error: tactic 'rfl' failed, the left-hand side
n + 1 + m
is not definitionally equal to the right-hand side
n + (1 + m)
n m : Nat
⊢ n + 1 + m = n + (1 + m)
```
Unfortunately, because of very subtle differences in semantics (which
transparency setting is used when reducing the goal and whether the
“implicit lambda” feature applies) I could not make this simply the only
`rfl` implementation. So `rfl` remains a macro and is still expanded to
`eq_refl` (difference transparency setting) and `exact Iff.rfl` and
`exact HEq.rfl` (implicit lambda) to not break existing code. This can
be revised later, so this still closes: #3302.
A user might still be puzzled *why* to terms are not defeq. Explaining
that better (“reduced to… and reduces to… etc.”) would also be great,
but that’s not specific to `rfl`, so better left for some other time.
Previously the formatter was using the builtin token table rather that
the one in the current environment. This could lead to round-tripping
failures for user-defined notations.
For an illustrative example, given the following notation
```lean
infixl:65 "+'" => Int.add
notation:65 a:65 "+'-" b:66 => Int.add a (id b)
```
then `5 +' -1` would parse as `Int.add 5 (-1)` and incorrectly pretty
print as `5+'-1`, which in turn would parse as `Int.add 5 (id 1)`. Now
it pretty prints as `5+' -1`.
Modifies how the declaration command elaborator reports when there are
unassigned metavariables. The visible effects are that (1) now errors
like "don't know how to synthesize implicit argument" and "failed to
infer 'let' declaration type" take precedence over universe level
issues, (2) universe level metavariables are reported as metavariables
(rather than as `u_1`, `u_2`, etc.), and (3) if the universe level
metavariables appear in `let` binding types or `fun` binder types, the
error is localized there.
Motivation: Reporting unsolved expression metavariables is more
important than universe level issues (typically universe issues are from
unsolved expression metavariables). Furthermore, `let` and `fun` binders
can't introduce universe polymorphism, so we can "blame" such bindings
for universe metavariables, if possible.
Example 1: Now the errors are on `x` and `none` (reporting expression
metavariables) rather than on `example` (which reported universe level
metavariables).
```lean
example : IO Unit := do
let x := none
pure ()
```
Example 2: Now there is a "failed to infer universe levels in 'let'
declaration type" error on `PUnit`.
```lean
def foo : IO Unit := do
let x : PUnit := PUnit.unit
pure ()
```
In more detail:
* `elabMutualDef` used to turn all level mvars into fresh level
parameters before doing an analysis for "hidden levels". This analysis
turns out to be exactly the same as instead creating fresh parameters
for level mvars in only pre-definitions' types and then looking for
level metavariables in their bodies. With this PR, error messages refer
to the same level metavariables in the Infoview, rather than obscure
generated `u_1`, `u_2`, ... level parameters.
* This PR made it possible to push the "hidden levels" check into
`addPreDefinitions`, after the checks for unassigned expression mvars.
It used to be that if the "hidden levels" check produced an "invalid
occurrence of universe level" error it would suppress errors for
unassigned expression mvars, and now it is the other way around.
* There is now a list of `LevelMVarErrorInfo` objects in the `TermElabM`
state. These record expressions that should receive a localized error if
they still contain level metavariables. Currently `let` expressions and
binder types in general register such info. Error messages make use of a
new `exposeLevelMVars` function that adds pretty printer annotations
that try to expose all universe level metavariables.
* When there are universe level metavariables, for error recovery the
definition is still added to the environment after assigning each
metavariable to level 0.
* There's a new `Lean.Util.CollectLevelMVars` module for collecting
level metavariables from expressions.
Closes#2058
These theorems are useful when one wants to simplify the goal state,
under knowledge that the bitvector operations don't overflow. This can
produce much smaller goal states that eventually allows `bv_omega` to
quickly close the goal.
Note that the LHS of the theorem is *not* in `simp` normal form, since
e.g. `(x + y).toNat` is normalized to `(x.toNat + y.toNat) % 2^w`. It's
not immediately clear to me what should be done about this.
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
Resolve cases when the `To/FromJSON` type classes are used with `Empty`,
e.g. in the following motivating example.
```
import Lean
structure Foo (α : Type) where
y : Option α
deriving Lean.ToJson
#eval Lean.toJson (⟨none⟩ : Foo Empty) -- fails
```
This is a follow-up to this PR
https://github.com/leanprover/lean4/pull/5415, as suggested by
@eric-wieser. It expands on the original suggestion by also handling
`FromJSON`.
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
---
Correct some stray spelling mistakes. I think the typo count is
asymptotically approaching zero.
Co-authored-by: euprunin <euprunin@users.noreply.github.com>
The problem here was that in Mathlib's `lean-pr-testing-NNNN` branches,
we were setting Batteries to a `nightly-testing-YYYY-MM-DD` branch. This
means that when we merge or rebase a new `nightly-with-mathlib` into a
Lean PR, the corresponding Mathlib testing branch would keep using an
old version of Batteries.
We also make sure to bump Batteries if Mathlib's `lean-pr-testing-NNNN`
branch already exists.
On a document edit, it may be the case that the first nontrivial
snapshot is e.g. for a macro-generated tactic call that does not have
range information. In that case, instead of just displaying nothing, we
should fall back to a previous range, in this case of the original
tactic macro.
Previously, it was not possible to use `decide` with most Array
functions (including `==`).
Later, we may replace some of these functions with defeqs that go via
the `List` operations, and use `csimp` lemmas for fast runtime
behaviour. In the meantime, this allows using `decide`.
Given the derived `Repr` instance for types with parameters, the absence
of `Repr Empty` can cause `Repr` instance synthesis to fail. For
example, given
```lean
inductive Prim (special : Type) where
| plus
| other : special → Prim special
deriving Repr
```
this works:
```lean
#eval (Prim.plus : Prim Int)
```
but this fails:
```lean
#eval (Prim.plus : Prim Empty)
```
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This implements the first half of #3302: It improves the extensible
`apply_rfl` tactic (the one that looks at `refl` attributes, part of
the `rfl` macro) to
* Check itself and ahead of time that the lhs and rhs are defEq, and
give
a nice consistent error message when they don't (instead of just passing
on
the less helpful error message from `apply Foo.refl`), and using the
machinery that `apply` uses to elaborate expressions to highlight diffs
in implicit arguments.
* Also handle `Eq` and `HEq` (built in) and `Iff` (using the attribute)
Care is taken that, as before, the current transparency setting affects
comparing the lhs and rhs, but not the reduction of the relation
So before we had
```lean
opaque P : Nat → Nat → Prop
@[refl] axiom P.refl (n : Nat) : P n n
/--
error: tactic 'apply' failed, failed to unify
P ?n ?n
with
P 42 23
⊢ P 42 23
-/
#guard_msgs in
example : P 42 23 := by apply_rfl
opaque withImplicitNat {n : Nat} : Nat
/--
error: tactic 'apply' failed, failed to unify
P ?n ?n
with
P withImplicitNat withImplicitNat
⊢ P withImplicitNat withImplicitNat
-/
#guard_msgs in
example : P (@withImplicitNat 42) (@withImplicitNat 23) := by apply_rfl
```
and with this PR the messages we get are
```
error: tactic 'apply_rfl' failed, The lhs
42
is not definitionally equal to rhs
23
⊢ P 42 23
```
resp.
```
error: tactic 'apply_rfl' failed, The lhs
@withImplicitNat 42
is not definitionally equal to rhs
@withImplicitNat 23
⊢ P withImplicitNat withImplicitNat
```
A test file checks the various failure modes and error messages.
I believe this `apply_rfl` can serve as the only implementation of
`rfl`, which would then complete #3302, and actually expose these
improved
error messages to the user. But as that seems to require a
non-trivial bootstrapping dance, it’ll be separate.
Provide an instance `Inhabited (TacticM α)`, even when `α` is not known
to be inhabited.
The default value is just the default value of `TermElabM α`, which
already has a similar instance.
closes#5333
This PR tries to address issue #5333.
My conjecture is that the binder annotations for `C.toB` and
`Algebra.toSMul` are not ideal. `Algebra.toSMul` is one of declarations
where the new command `set_synth_order` was used. Both classes, `C` and
`Algebra`, are parametric over instances, and in both cases, the issue
arises due to projection instances: `C.toB` and `Algebra.toSMul`. Let's
focus on the binder annotations for `C.toB`. They are as follows:
```
C.toB [inst : A 20000] [self : @C inst] : @B ...
```
As a projection, it seems odd that `inst` is an instance-implicit
argument instead of an implicit one, given that its value is fixed by
`self`. We observe the same issue in `Algebra.toSMul`:
```
Algebra.toSMul {R : Type u} {A : Type v} [inst1 : CommSemiring R] [inst2 : Semiring A]
[self : @Algebra R A inst1 inst2] : SMul R A
```
The PR changes the binder annotations as follows:
```
C.toB {inst : A 20000} [self : @C inst] : @B ...
```
and
```
Algebra.toSMul {R : Type u} {A : Type v} {inst1 : CommSemiring R} {inst2 : Semiring A}
[self : @Algebra R A inst1 inst2] : SMul R A
```
In both cases, the `set_synth_order` is used to force `self` to be
processed first.
In the MWE, there is no instance for `C ...`, and `C.toB` is quickly
discarded. I suspect a similar issue occurs when trying to use
`Algebra.toSMul`, where there is no `@Algebra R A ... ...`, but Lean
spends unnecessary time trying to synthesize `CommSemiring R` and
`Semiring A` instances. I believe the new binder annotations make sense,
as if there is a way to synthesize `Algebra R A ... ...`, it will tell
us how to retrieve the instance-implicit arguments.
TODO:
- Impact on Mathlib.
- Document changes.
---------
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
We need to follow the fvar aliases registered by `match` in both
directions
Fixes#4714, fixes#2837
---------
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
After #5270, `partial` functions that use products of sums no longer
compile with only `Nonempty` constraints on their arguments. These
instances allow the compilation to work.
In LNSym we often use the pattern `ofBool (a.getLsbD i)` to pick out a
specific bit (`i`) from a bitvector (`a`).
By adding a rewrite to `extractLsb` to `bv_decide`s normalization set,
we can still automatically close goals that have this pattern. In the
process, I also added a simp-lemma about the value of a `Fin 1`.
Obviously a link to the web docs isn't ideal, but having hovers
available on the symbol is much better than nothing.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
A round of clean-up for the context of the functional induction
principle cases.
* Already previously, with `match e with | p => …`, functional induction
would ensure that `h : e = p` is in scope, but it wouldn’t work in
dependent cases. Now it introduces heterogeneous equality where needed
(fixes#4146)
* These equalities are now added always (previously we omitted them when
the discriminant was a variable that occurred in the goal, on the
grounds that the goal gets refined through the match, but it’s more
consistent to introduce the equality in any case)
* We no longer use `MVarId.cleanup` to clean up the goal; it was
sometimes too aggressive (fixes#5347)
* Instead, we clean up more carefully and with a custom strategy:
* First, we substitute all variables without a user-accessible name, if
we can.
* Then, we substitute all variable, if we can, outside in.
* As we do that, we look for `HEq`s that we can turn into `Eq`s to
substitute some more
* We substitute unused `let`s.
**Breaking change**: In some cases leads to a different functional
induction principle (different names and order of assumptions, for
example).
Fixes a workflow bug where the `check-level` was not always set
correctly. Arguments to a `gh` call used to determine the `check_level`
were accidentally outside of the relevant command substitution (`$(gh
...)`).
-----
This can be observed in [these
logs](https://github.com/leanprover/lean4/actions/runs/10859763037/job/30139540920),
where the check level (shown first under "configure build matrix") is
`2`, but the PR does not have the `release-ci` tag. As a "test", run the
script for "set check level" printed in those logs (with some lines
omitted):
```
check_level=0
labels="$(gh api repos/leanprover/lean4/pulls/5343) --jq '.labels'"
if echo "$labels" | grep -q "release-ci"; then
check_level=2
elif echo "$labels" | grep -q "merge-ci"; then
check_level=1
fi
echo "check_level=$check_level"
```
Note that this prints `check_level=2`, but changing `labels` to
`labels="$(gh api repos/leanprover/lean4/pulls/5343 --jq '.labels')"`
prints `check_level=0`.
This PR fixes an issue reported a while ago at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60Monad.2Emap.60.20is.20a.20namespace.3F/near/425662846
where `Monad.map` was incorrectly reported by the autocompletion as a
namespace.
The underlying issue is that `Monad.map` contains an internal
declaration `_default`. This PR ensures that no namespaces are
registered that only contain internal declarations.
This also means that `open`ing namespaces that only contain internal
declarations will now fail.
The Mathlib adaption for this is a minor change where a declaration
(i.e. a namespace that only contains internal declarations) was `open`ed
by accident.
This solves the issue where certain subexpressions are lacking syntax
hovers because the hover text is not "builtin" - it only shows up if the
`Parser` constant is imported in the environment. For top level syntaxes
this is not a problem because `builtin_term_parser` will automatically
add this doc information, but nested syntaxes don't get the same
treatment.
We could walk the expression and add builtin docs recursively, but this
is somewhat expensive and unnecessary given that it's a fixed list of
declarations in lean core. Moreover, there are reasons to want to
control which syntax nodes actually get hovers, and while a better
system for that is forthcoming, for now it can be achieved by
strategically not applying the `@[builtin_doc]` attribute.
Fixes#3842
When the elaborator doesn't provide us with any `CompletionInfo`, we
currently provide no completions whatsoever. But in many cases, we can
still provide some helpful identifier completions without elaborator
information. This PR adds a fallback mode for this situation.
There is more potential here, but this should be a good start.
In principle, this issue alleviates #5172 (since we now provide
completions in these contexts). I'll leave it up to an elaboration
maintainer whether we also want to ensure that the completion infos are
provided correctly in these cases.
This adds a simplification lemma for `(x - y).toNat` when the
subtraction is known to not overflow (i.e., `y ≤ x`).
We make a new section for this for two reasons:
1. Definitions of subtraction occur before the definition of
`BitVec.le_def`, so we cannot directly place this lemma at `sub`.
2. There are other theorems of this kind, for addition and
multiplication, which can morally live in the same section.
The theorem
```lean
namespace Int
theorem ediv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a / b := by
match a, b with
| ofNat a, b =>
match Int.le_antisymm Ha (ofNat_zero_le a) with
| h1 =>
rw [h1, zero_ediv,]
exact Int.le_refl 0
| a, ofNat b =>
match Int.le_antisymm Hb (ofNat_zero_le b) with
| h1 =>
rw [h1, Int.ediv_zero]
exact Int.le_refl 0
| negSucc a, negSucc b =>
rw [Int.div_def, ediv]
have le_succ {a: Int} : a ≤ a+1 := (le_add_one (Int.le_refl a))
have h2: 0 ≤ ((↑b:Int) + 1) := Int.le_trans (ofNat_zero_le b) le_succ
have h3: (0:Int) ≤ ↑a / (↑b + 1) := (ediv_nonneg (ofNat_zero_le a) h2)
exact Int.le_trans h3 le_succ
```
is nontrivial to prove from existing theorems and would be nice to add
as standard theorem in DivModLemmas.
See the zullip conversation
[here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Adding.20theorem.20theorem.20ediv_nonneg'.20for.20negative.20a.20and.20b)
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
From the new doc-string:
```quote
In early versions of Lean, the typeclasses provided by `/` and `%`
were defined in terms of `tdiv` and `tmod`, and these were named simply as `div` and `mod`.
However we decided it was better to use `ediv` and `emod`,
as they are consistent with the conventions used in SMTLib, Mathlib,
and often mathematical reasoning is easier with these conventions.
At that time, we did not rename `div` and `mod` to `tdiv` and `tmod` (along with all their lemma).
In September 2024, we decided to do this rename (with deprecations in place),
and later we intend to rename `ediv` and `emod` to `div` and `mod`, as nearly all users will only
ever need to use these functions and their associated lemmas.
```
Proves that `<` and `<=` on `BitVec` are (strict) (total) partial
orders. This is required for the `UInt` as `BitVec` refactor.
This does open the question how to state these theorems "correctly" for
`BitVec`, we have both `<` living in `Prop` and `BitVec.ult` living in
`Bool`. We might of course say to always use `<` but: Once we start
adding `IntX` we need to prove the same results for `BitVec.slt` to
provide an equivalent API. So it would appear that it is unavoidable to
have a `= true` variant of these theorems there?
Question answered: Use `<` and `slt`.
Refactors the derive handlers for `ToJson` and `FromJson` in preparation
for #3160.
This splits up the different parts of the handler according to how other
similar handlers are implemented while keeping the original logic
intact. This makes the changes necessary to adapt the file in #3160 much
easier.
Fixes#4455, fixes#4705, fixes#5219
Also fixes a minor bug where a dot in brackets would report incorrect
completions instead of no completions.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
I found that the kernel has special support for `e =?= true`, and will
in this case aggressively whnf `e`. This explains the following behavior
(for a `sqrt` function with fuel):
```lean
theorem foo : sqrt 100000000000000000002 == 10000000000 := rfl -- fast
theorem foo : sqrt 100000000000000000002 = 10000000000 := rfl -- slow
theorem foo : sqrt 100000000000000000002 = 10000000000 := by decide -- fast
```
The special support in the kernel only applies for closed `e` and `true`
on the RHS. It could be generlized (also open terms, also `false`, other
data type's constructors, different orientation). But maybe I should
wait for evidence that this generaziation really matters, or whether
all applications (proof by reflection) can be made to have this form.
This PR enables the use of incrementality for completion in tactic
blocks. Consider the following example:
```lean
example : True := by
have : True := T
sleep 10000
```
Before this PR, in order to respond to a completion request after `T`,
`sleep 10000` has to complete first since the command must be fully
elaborated. After this PR, the completion request is responded to
immediately.
Currently, `ll_infer_type` is responsible for telling the user about
`noncomputable` when a definition depends on one without executable
code. However, this is imperfect because type inference does not check
every subexpression. This leads to errors later on that users find to be
hard to interpret.
Now, `Lean.IR.checkDecls` has a friendlier error message when it
encounters constants without compiled definitions, suggesting to
consider using `noncomputable`. While this function is an internal IR
consistency check, it is also reasonable to have it give an informative
error message in this particular case. The suggestion to use
`noncomputable` is limited to just unknown constants.
Some alternatives would be to either (1) create another checker just for
missing constants, (2) change `ll_infer_type` to always visit every
subexpression no matter if they are necessary for inferring the type, or
(3) investigate whether `tests/lean/run/1785.lean` is due to a deeper
issue.
Closes#1785
This is "upstreaming" mathlib's `unfold_let` tactic by incorporating its
functionality into `unfold`. Now `unfold` can, in addition to unfolding
global definitions, unfold local definitions. The PR also updates the
`conv` version of the tactic.
An improvement over `unfold_let` is that it beta reduces unfolded local
functions.
Two features not present in `unfold` are that (1) `unfold_let` with no
arguments does zeta delta reduction of *all* local definitions, and also
(2) `unfold_let` can interleave unfoldings (in contrast, `unfold a b c`
is exactly the same as `unfold a; unfold b; unfold c`).
Closes RFC #4090
When an eliminator was overapplied with more than one additional
argument, elaboration produced an incorrect term because the list of
processed arguments was being reversed. Now these arguments are not
reversed.
1. Remove the need to allocate an intermediate `String` for literally
every character in a JSON `String`.
2. Use a single `String` buffer in the entire `Json.compress` machinery.
3. Use `toListAppend`
Number 1 is doing most of the lifting in the perf diff, the rest are
some minor but measurable improvements.
We change the `bv_decide` to understand `BitVec.extractLsb'` as a
primitive, and add a normalization lemma for `extractLsb`.
It's important to pick the primed version as a primitive, because it is
not always possible to rewrite `extractLsb'` back into `extractLsb` (see
#5007 for that direction, and the relevant side-conditions).
That is, with this PR, `bv_decide` is able to bitblast both versions of
extracting bits.
I don't think we gain anything from having them as `abbrev` here, and
the simpNF linter complains:
```
-- Init.Data.BitVec.Lemmas
#check @BitVec.toNat_intMin /- simp can prove this:
by simp only [BitVec.toNat_twoPow]
One of the lemmas above could be a duplicate.
If that's not the case try reordering lemmas or adding @[priority].
-/
#check @BitVec.toNat_intMax /- Left-hand side simplifies from
(BitVec.intMax w).toNat
to
(2 ^ w - 1 % 2 ^ w + 2 ^ (w - 1)) % 2 ^ w
using
simp only [@BitVec.toNat_sub, @BitVec.ofNat_eq_ofNat, BitVec.toNat_ofNat, BitVec.toNat_twoPow, Nat.add_mod_mod]
Try to change the left-hand side to the simplified term!
-/
```
```
#lint only simpNF in all
```
reports (amongst others):
```
-- Init.Data.Int.Order
#check @Int.toNat_of_nonneg /- Left-hand side simplifies from
↑a.toNat
to
max a 0
using
simp only [Int.ofNat_toNat]
Try to change the left-hand side to the simplified term!
-/
#check Int.toNat_sub_toNat_neg /- Left-hand side simplifies from
↑n.toNat - ↑(-n).toNat
to
max n 0 - max (-n) 0
using
simp only [Int.ofNat_toNat]
Try to change the left-hand side to the simplified term!
-/
```
This doesn't completely resolve the danger (only relevant in `prelude`
files) of importing `Init.Data.List.Basic` but not `Init.Data.List.Impl`
and thereby not having `@[csimp]` lemmas installed for some list
operations.
I'm going to address this better while working on `Array`.
Sebastian mentioned that the use of the kernel defeq was to work around
a performance issue that was fixed since. Let's see if we can do
without.
This is also a semantic change: Ground terms (no free vars, no mvars)
are reduced at
“all” transparency even if the the transparency setting is default. This
was the case
even before 03f6b87647 switched to the
kernel defeq
checking for performance. It seems that this is rather surprising
behavior from the user
point of view. The fallout on batteries and mathlib is rather limited,
only a few
`rfl` proofs seem to have (inadvertently or not) have relied on this.
The speedcenter reports no significant regressions on core or mathlib.
Remark: declarations like `sizeWithSharing` must be in `IO` since they
are not functions.
The commit also uses the more efficient `ShareCommon.shareCommon'`.
Adds additional fields to the package configuration which will be used
by Reservoir:
* `version`: The version of the package. Follows Lean's model of
`<major>.<minor>.<patch>[-<specialDescr>]`.
* `versionTags`: A pattern matching the set of Git tags Reservoir should
consider package version revisions.
* `description`: A short description for the package. Takes precedence
over the GitHub's description.
* `keywords`: An array of package keywords that will be used to group
packages into categories on Reservoir. Takes precedence over labels on
the repository.
* `homepage`: A URL to a website for the package. Takes precedence over
GitHub's homepage.
* `license`: An SPFX license identifier for the package's license (not
verified to be well-formed).
* `licenseFiles`: An array of (relative) files the contain license
information (e.g., `#["LICENSE", "NOTICE"]` for Apache 2.0).
* `readmeFile`: Relative path to the package's readme (enables
non-standard README locations).
* `reservoir`: Reservoir will use this setting to determine whether to
include packages in its index.
Also adds two new CLI commands:
* `lake reservoir-config`: Used by Reservoir to extract a package's
configuration.
* `lake check-build`: Determines whether the package has any default
build targets configured.
The Reservoir configuration also makes uses of the exiting `name` and
`platformIndependent` fields.
These commands were trusting that elaboration resulted in type-correct
terms, but users testing custom elaborators have found it to be
surprising that they do not do typechecking. This adds a `Meta.check`
step.
This renames `BitVec.getLsb` to `getLsbD` (`D` for "default" value, i.e.
false), and introduces `getLsb?` and `getLsb'` (which we can rename to
`getLsb` after a deprecation cycle).
(Similarly for `getMsb`.)
Also adds a `GetElem` class so we can use `x[i]` and `x[i]?` notation.
Later, we will turn
```
theorem getLsbD_eq_getElem?_getD (x : BitVec w) (i : Nat) (h : i < w) :
x.getLsbD i = x[i]?.getD false
```
on as a `@[simp]` lemma.
This PR doesn't attempt to demonstrate the benefits, but I think both
arguments are going to get easier, and this will bring the BitVec API
closer in line to List/Array, etc.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
in #4154 and #5129 the rules for equational lemmas have changed, and new
options were introduced that can be used to revert to the pre-4.12
behavior. Hopefully nobody really needs these options besides for
backwards compatibility, therefore we put these options in the
`backward` option name space.
So the previous behavior can be achieved by setting
```lean
set_option backward.eqns.nonrecursive false
set_option backward.eqns.deepRecursiveSplit false
```
With this, lean produces the following zoo of rewrite rules:
```
Option.map.eq_1 : Option.map f none = none
Option.map.eq_2 : Option.map f (some x) = some (f x)
Option.map.eq_def : Option.map f p = match o with | none => none | (some x) => some (f x)
Option.map.eq_unfold : Option.map = fun f p => match o with | none => none | (some x) => some (f x)
```
The `f.eq_unfold` variant is especially useful to rewrite with `rw`
under
binders.
This implements and fixes#5110
This PR propagates the `AttributeKind` to `SimpleScopedEnvExtension.add`
in attributes created with `register_label_attr`.
This also fixes a nearby stale docstring which referenced `Std`.
---
Closes#3697
This PR roughly halves the time needed to load the .ilean files by
optimizing the JSON parser and the conversion from JSON to Lean data
structures.
The code is optimized roughly as follows:
- String operations are inlined more aggressively
- Parsers are changed to use new `String.Iterator` functions `curr'` and
`next'` that receive a proof and hence do not need to perform an
additional check
- The `RefIdent` of .ilean files now uses a `String` instead of a `Name`
to avoid the expensive parse step from `String` to `Name` (despite the
fact that we only very rarely actually need a `Name` in downstream code)
- Instead of `List`s and `Subarray`s, the JSON to Lean conversion now
directly passes around arrays and array indices to avoid redundant
boxing
- Parsec's `peek?` sometimes generates redundant `Option` wrappers
because the generation of basic blocks interferes with the ctor-match
optimization, so it is changed to use an `isEof` check where possible
- Early returns and inline-do-blocks cause the code generator to
generate new functions, which then interfere with optimizations, so they
are now avoided
- Mutual defs are used instead of unspecialized passing of higher-order
functions to generate faster code
- The object parser is made tail-recursive
This PR also fixes a stack overflow in `Lean.Json.compress` that would
occur with long lists and adds a benchmark for the .ilean roundtrip
(compressed pretty-printing -> parsing).
This PR fixes a small bug where over time, "import out of data" messages
would accumulate in files when their size changed before restarting its
file worker.
https://github.com/leanprover/vscode-lean4/pull/521 changed the display
name of the VS Code extension so that it can be found more easily when
searching for "Lean" (before it would appear far down in the list). This
PR updates the quickstart guide to reflect this fact.
This was not a great simp lemma, and hurts simp confluence. Better to
just use it locally where it is useful.
Similarly `List.head_eq_iff_head?_eq_some`.
This PR also pulls in some mathlib theorems on testBit and Nat and establishes facts about 2^w that are needed here and which are generally useful for bitvector reasoning.
The following theorem is not generalized to arbitrary x instead of 2, as this would require a condition to be added for x > 1 which would have to be passed to simp each time this theorem should fire.
chore: derive from testBit_two_pow
chore: convert first to prop and then decide
chore: move intMax down as well
chore: add simp set
Add simp-set into this PR
chore: fix simp extension
Move file to src/Lean to fix build
Add prelude
update date
Add university of cambridge as copyright holder
improve naming
use whitespace uniformly
use decide (n = m)
Drop the 'Nat.' namespace
Update src/Init/Data/BitVec/Lemmas.lean
Co-authored-by: Siddharth <siddu.druid@gmail.com>
Update src/Init/Data/BitVec/Lemmas.lean
Co-authored-by: Siddharth <siddu.druid@gmail.com>
Fix build
add some theorems
Revert "add some theorems"
This reverts commit fb97bc2007e371854b40badb3d6014da034c1f5e.
WIP
Shorten proof
Update src/Init/Data/Nat/Lemmas.lean
finish proofs
Update src/Init/Data/BitVec/Lemmas.lean
Co-authored-by: Kim Morrison <scott@tqft.net>
Update src/Init/Data/Nat/Lemmas.lean
Co-authored-by: Kim Morrison <scott@tqft.net>
chore: move BoolToPropSimps
`simp only` will not apply this simproc anymore. Users must now write
`simp only [reduceCtorEq]`. See RFC #5046 for motivation.
This PR also renames simproc to `reduceCtorEq`.
close#5046
@semorrison A few `simp only ...` tactics will probably break in
Mathlib. Fix: include `reduceCtorEq`.
We use `no_index` to work around special-handling of `OfNat.ofNat` in
`DiscrTree`, which has been reported as an issue in
https://github.com/leanprover/lean4/issues/2867 and is currently in the
process of being fixed in https://github.com/leanprover/lean4/pull/3684.
As the potential fix seems non-trivial and might need some time to
arrive in-tree, we meanwhile add the `no_index` keyword to the
problematic subterm.
---------
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
We swap the arguments for `Membership.mem` so that when proceeded by a
`SetLike` coercion, as is often the case in Mathlib, the resulting
expression is recognized as eta expanded and reduce for many
computations. The most beneficial outcome is that the discrimination
tree keys for instances and simp lemmas concerning subsets become more
robust resulting in more efficient searches.
Closes `RFC` #4932
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Henrik Böving <hargonix@gmail.com>
This is part of #3983.
After #4154 introduced equational lemmas for non-recursive functions and
#5055
unififed the lemmas for structural and wf recursive funcitons, this now
disables the special handling of recursive functions in
`findMatchToSplit?`, so that the equational lemmas should be the same no
matter how the function was defined.
The new option `eqns.deepRecursiveSplit` can be disabled to get the old
behavior.
### Breaking change
This can break existing code, as there now can be extra equational
lemmas:
* Explicit uses of `f.eq_2` might have to be adjusted if the numbering
changed.
* Uses of `rw [f]` or `simp [f]` may no longer apply if they previously
matched (and introduced a `match` statement), when the equational
lemmas got more fine-grained.
In this case either case analysis on the parameters before rewriting
helps, or setting the option `opt.deepRecursiveSplit false` while
defining the function
Updates the user widget manual to account for more recent changes. One
issue is that the samples no longer work on https://live.lean-lang.org/
because it uses an outdated version of the `@leanprover/infoview` NPM
package. They work on https://lean.math.hhu.de/ and in recent versions
of the VSCode extension.
This is part of #3983.
Fine-grained equational lemmas are useful even for non-recursive
functions, so this adds them.
The new option `eqns.nonrecursive` can be set to `false` to have the old
behavior.
### Breaking channge
This is a breaking change: Previously, `rw [Option.map]` would rewrite
`Option.map f o` to `match o with … `. Now this rewrite will fail
because the equational lemmas require constructors here (like they do
for, say, `List.map`).
Remedies:
* Split on `o` before rewriting.
* Use `rw [Option.map.eq_def]`, which rewrites any (saturated)
application of `Option.map`
* Use `set_option eqns.nonrecursive false` when *defining* the function
in question.
### Interaction with simp
The `simp` tactic so far had a special provision for non-recursive
functions so that `simp [f]` will try to use the equational lemmas, but
will also unfold `f` else, so less breakage here (but maybe performance
improvements with functions with many cases when applied to a
constructor, as the simplifier will no longer unfold to a large
`match`-statement and then collapse it right away).
For projection functions and functions marked `[reducible]`, `simp [f]`
won’t use the equational theorems, and will only use its internal
unfolding machinery.
### Implementation notes
It uses the same `mkEqnTypes` function as for recursive functions, so we
are close to a consistency here. There is still the wrinkle that for
recursive functions we don't split matches without an interesting
recursive call inside. Unifying that is future work.
in principle we'd like to use the existing parser
```
"?" >> (ident <|> hole)
```
but somehow annotate it so that hovering the `hole` will not show the
hole's hover. But for now it was easier to just change the parser to
```
"?" >> (ident <|> "_")
```
and be done with it.
Fixes#5021
The goal at the crucial step is
```
a : Array Nat
i : Fin ?m.27
⊢ ↑i < a.size
```
and after the `apply Fin.val_lt_of_le;` we have
```
a : Array Nat
i : Fin ?m.27
⊢ ?m.27 ≤ a.size
```
and now `apply Fin.val_lt_of_le` applies again, due to accidential
defeq. Adding `with_reducible` helps here.
fixes#5061
Defines `mergeSort`, a naive stable merge sort algorithm, replaces it
via a `@[csimp]` lemma with something faster at runtime, and proves the
following results:
* `mergeSort_sorted`: `mergeSort` produces a sorted list.
* `mergeSort_perm`: `mergeSort` is a permutation of the input list.
* `mergeSort_of_sorted`: `mergeSort` does not change a sorted list.
* `mergeSort_cons`: proves `mergeSort le (x :: xs) = l₁ ++ x :: l₂` for
some `l₁, l₂`
so that `mergeSort le xs = l₁ ++ l₂`, and no `a ∈ l₁` satisfies `le a
x`.
* `mergeSort_stable`: if `c` is a sorted sublist of `l`, then `c` is
still a sublist of `mergeSort le l`.
@arthur-adjedj was very confused when a mutually recursive definition
didn't work as expected, and the reason was that he used different names
for the fixed parameters.
It seems plausible to simply allow that and calculate the fixed-prefix
up to alpha renaming.
It does mean, though, that, for example, termination proof goals will
mention the names as used by the first function. But probably better
than simply failing. And we could even fix that later (by passing down
the
actual names, and renmaing the variables in the context of the mvar,
depending on the “current function”) should it bother our users.
This PR imports LeanSAT's LRAT module as step 4/~6 (step 7 could go
after I did some refactorings to import this) of the LeanSAT
upstreaming. It is the last large component, after this only the LRAT
parser and the reflection tactic that hooks everything up to the meta
level remains. In particular it is the last component that contains
notable proofs, yay!
Again a few remarks:
1. Why is this not in `Std`? I'm not quite sure whether it should be
there. At the current level of code/proof quality we can certainly not
import the checker itself into `Std` but maybe having the data type as
well as the trimming algorithm there might be of interested? I'm hoping
that as we refactor the checker in the future its quality will be high
enough to be also put into `Std`. At this point we would have a full AIG
-> CNF -> LRAT verification pipeline in `Std` for everyone to use. One
additional blocker in this is that we cannot provide the parsers for the
format in `Std` as of today because `Parsec` is still in `Lean` so that
would also have to change.
2. There do exist two abstraction levels to make sure we can swap out
the LRAT implementation at any time:
- The public interface is just all files in the top level `LRAT`
directory. It basically only contains the LRAT format itself, the
checker + soundness proof and the trimming algorithm. As long as we
don't need to change their API (which we shouldn't have to I think) we
can always swap out the entire `Internal` directory without breaking
anything else in LeanSAT.
- The `Internal` module itself contains another layer of abstraction in
the form of the `Formula` class. This allows us to swap out the most
complex component in `Internal` as well, without having to touch any of
the infrastructure that is built around it either.
3. I mostly performed stylistic cleanups on the `Internal` module. In my
experience over upgrading to many nightlies during the course of LeanSAT
development, I have gotten these proofs cleaned up to the point, where
they only break if we change the `List` or `Array` proof API
significantly. Given that we are currently in the process of stabilizing
it I'm hoping that these proofs do not have to be touched anymore unless
we do something crazy. All of the custom theory that the LRAT component
developed around various basic data types has been upstreamed into Lean
over the course of various other PRs.
4. If there are some simple tricks that we can pull off to increase the
code / proof quality in `Internal` and in particular `Internal.Formula`
(this module is not for the light-hearted Lean reviewer) I'm all for it.
Otherwise the best course of action to provide LeanSAT to our users soon
would probably be to merge it as is and do a cut + rewrite at one of the
two interface points described above.
When elaborating the headers of mutual indexed inductive types, mvars
have to be synthesized and instantiated before replacing the fvars
present there. Otherwise, some fvars present in uninstantiated mvars may
be missed and lead to an error later.
Closes#3242 (again)
As discussed with @semorrison, feel free to do whatever to the branch.
---------
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Previously, the tactic state shown at `decreasing_by` would leak lots of
details about the translation, and mention `invImage`, `PSigma` etc.
This is not nice.
So this introduces `clean_wf`, which is like `simp_wf` but using
`simp`'s `only` mode, and runs this unconditionally. This should clean
up the goal to a reasonable extent.
Previously `simp_wf` was an unrestricted `simp […]` call, but we
probably don’t want arbitrary simplification to happen at this point, so
this now became `simp only` call. For backwards compatibility,
`decreasing_with` begins with `try simp`. The `simp_wf` tactic
is still available to not break too much existing code; it’s docstring
suggests to no longer use it.
With `set_option cleanDecreasingByGoal false` one can disable the use of
`clean_wf`. I hope this is only needed for debugging and understanding.
Migration advise: If your `decreasing_by` proof begins with `simp_wf`,
either remove that (if the proof still goes through), or replace with
`simp`.
I am a bit anxious about running even `simp only` unconditionally here,
as it may do more than some user might want, e.g. because of options
like `zetaDelta := true`. We'll see if we need to reign in this tactic
some more.
I wonder if in corner cases the `simp_wf` tactic might be able to close
the goal, and if that is a problem. If so, we may have to promote simp’s
internal `mayCloseGoal` parameter to a simp configuration option and use
that here.
fixes#4928
Using `Nat.lt_trans` is too restrictive, and using `Nat.lt_of_lt_of_le`
should make this tactic prove more goals.
This fixes a regression probably introduced by #3991; at least in some
cases before that `apply sizeOf_get` would have solved the goal here.
And it’s true that this is now subsumed by `simp`, but because of the
order that `macro_rules` are tried, the too restrictive variant with
`Nat.lt_trans` would be tried before `simp`, without backtracking.
Fixes#5027
Step 3/~7 in upstreaming LeanSAT.
A few thoughts:
- Why is this not in `Std.Sat`? LeanSAT's bitblaster operates on a
limited internal language. For example it has no idea that signed
comparision operators even exist. This is because it relies on a
normalization pass before being given the goal. For this reason I would
not classify the bitblaster as an API that we should publicly advertise
at this abstraction level
- Sometimes I slightly rebuild parts of the LawfulOperator
infrastructure for operators that work non-tail-recursively. This is
because they do not return an `Entrypoint` but instead an
`ExtendingEntrypoint` in order to even be defined in the first place
(casting Ref's and all that). Given the fact that this barely happens
and I never actually commit to rebuilding the full API I'm hoping that
this is indeed a fine decision?
- The single explicit `decreasing_by` that has a simp only which
*almost* looks like `simp_wf` is missing a singular lemma from `simp_wf`
because it doesn't terminate otherwise.
- I am not using functional induction because it basically always fails
at some generalization step, that is also the reason that there is lots
of explicit `generalize` and manually recursive proofs.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
In #4976, I forgot that we do need info trees eventually on the cmdline
for .ilean generation. Unfortunately, not reporting them incrementally
would require an API change, so let's see what the impact of incremental
reporting is
I'm experimenting with changing the signature of `Ord.arrayOrd`; rather
than make a local synonym here, let's make a local instance so it
doesn't interact with the experiments.
Adds a lemma to rewrite `BitVec.extractLsb'` to `extractLsb` plus a
cast.
Note that `extractLsb'` with a length of 0 returns `BitVec 0`, while
`extractLsb` will never return an empty bitvector (because of the `+ 1`
in it `hi - lo + 1`). Hence, this lemma needs a side condition that the
length is non-zero.
Also adds `getLsb_extractLsb'`
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
Since https://github.com/curl/curl/pull/4465 curl adheres to the
`Retry-After` header, so maybe this fixes the issues with
```
jq: error (at <stdin>:5): Cannot index string with string "body"
```
that sometimes make this workflow fail.
#4976 moved resolution of a promise to an earlier point, but that led to
object being marked MT earlier, so we need to move the code that
minimizes those objects earlier too to revert the performance
regression.
For structure projections, the pretty printer assumed that the
expression was type correct. Now it checks that the object being
projected is of the correct type. Such terms appear in type mismatch
errors.
Also, fixes and improves `#print` for structures. The types of
projections now use MessageData (so are now hoverable), and the type of
`self` is now the correct type.
Closes#4670
...unless we are about to kill the process anyway (which is not the
default)
Ensures panics are visible as regular messages in the language server
and properly ordered in relation to other messages on the cmdline
The prior default of 1000000 could not be achieved in practice, because
the stack would overflow after around 5000 recursive invocations. This
meant that a poorly-chosen @[ext] lemma could crash Lean.
Talking to Mathlib users, it seems that 10 would be a very large number
in practice, so a default limit of 100 should not change successful
uses. But it does make it much easier to diagnose and recover from poor
choices of @[ext] lemmas.
Without this change, a stack overflow on Mac OS during tactic execution
can lead to the message:
terminated by signal SIGBUS (Misaligned address error)
This comes from `lean_alloc_small`. With the change, the process instead
terminates with the more accurate and actionable:
Stack overflow detected. Aborting.
After having added already `BitVec.ushiftRight_*_distrib`in
https://github.com/leanprover/lean4/pull/4667 for ushiftRight, this PR
now completes the `*_distrib` theorems for shift.
Adds `@[app_delab ident]` as a macro for `@[delab app.ident]`. Resolves
the identifier when expanding the macro, saving needing to use the fully
qualified identifiers that `@[delab]` requires. Also, unlike `@[delab]`,
throws an error if the identifier cannot be resolved.
Closes#4899
Fixes an issue where each alternative in choice nodes would get their
own arguments. Now cdot function expansion is aware of choice nodes.
Also modifies the variable naming so that multi-argument functions like
`(· + ·)` expand as `fun x1 x2 => x1 + x2` rather than `fun x x_1 => x +
x_1`.
Closes#4832
This restores all of the imports of `Lean.Data.HashMap` and
`Lean.Data.HashSet` so that users actually see the deprecation warnings
instead of a "declaration not found" error.
This implements a naive version of `getline` because Windows does not
have `getline`. Given the fact that `FILE` has buffered IO, calling
`fgetc` in a loop is not as big of a performance hazard as it might seem
at first glance.
The proper solution to this would of course be to have our own buffered
IO so we are fully in charge of the buffer. In this situation we could
check the entire buffer for a newline at once instead of char by char.
However that is not going to happen for the near future so I propose we
stay with this implementation. If reading individual lines of a file
does truly end up being the performance bottle neck we have already
won^^.
Step 1 out of approximately 7 to upstream LeanSAT.
---------
Co-authored-by: Tobias Grosser <tobias@grosser.es>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This change canonicalizes the BitVec variable names to `x y z : BitVec`
instead of alternative namings such as `s t : BitVec` or `a b : BitVec`.
Variable names that carry semantic meaning such as `(msbs : BitVec w)
(lsb : Bool)` remain untouched.
This is purely a naming change to make our bitvector proofs more
consistent and polish the (auto-generated) documentation as a very small
step towards polishing the documentation of the BitVec library in Lean.
---------
Co-authored-by: AnotherAlexHere <153999274+AnotherAlexHere@users.noreply.github.com>
#4917 will expose users of the `Lean` API to the renaming of the hash
map query methods. This PR aims to make the transition easier by adding
deprecated functions with the old names.
With the recent unification of server and cmdline processing,
`IO.Process` tests that previously broke the server because they
directly wrote to stdout are now flaky on the cmdline because
elaboration and reporting are happening in separate threads. By removing
direct writes to stdout, the race condition is removed and the file can
actually be edited in the language server as well again.
This PR:
- changes the implementation of `readBinFile` and `readFile` to only
require two system calls (`stat` + `read`) instead of one `read` per
1024 byte chunk.
- fixes a bug where `Handle.getLine` would get tripped up by a NUL
character in the line and cut the string off. This is caused by the fact
that the original implementation uses `strlen` and `lean_mk_string`
which is the backer of `mk_string` does so as well.
- fixes a bug where `Handle.putStr` and thus by extension `writeFile`
would get tripped up by a NUL char in the line and cut the string off.
Cause here is the use of `fputs` when a NUL char is possible.
Closes: #4891Closes: #3546Closes: #3741
This PR resolves two language server bugs that especially affect Windows
users:
1. Editing the header could result in the watchdog not correctly
restarting the file worker (#3786, #3787), which would lead to the file
seemingly being processed forever.
- The cause of this issue was a race condition in the watchdog that was
accidentally introduced as far back as #1884: In specific circumstances,
the watchdog will attempt forwarding a message to the file worker after
the process has exited due to a changed header, but before the file
worker exiting has been noticed by the watchdog (which will then restart
the file worker). In this case, the watchdog would mark the file worker
as having crashed and not look at its exit code to restart the file
worker, but instead treat it like a crashed file worker that will only
be restarted when editing the file again. Not inspecting the exit code
of the file worker when it crashed from forwarding a message from the
file worker is necessary since we do not restart the file worker until
another notification from the client arrives, and so we would read the
same crash exit code over and over again in the main loop of the
watchdog if we did not remove it from our list of file workers that we
listen to.
- This PR resolves this issue by distinguishing between "crashes when
forwarding messages to the file worker" and "crashes when forwarding
messages from the file worker". In the former case, we still inspect the
exit code of the file worker and potentially restart it if the imports
changed, whereas in the latter case, we stop inspecting the exit code of
the file worker. This is correct because the latter case is exactly the
one where we need to stop inspecting the exit code but where a crash
cannot occur as a result of a changed header, whereas the former case is
exactly the one where we still need to inspect the exit code after a
crash to ensure that we restart the file worker in case it exited
because the header changed.
- At some point in the future, it would be nice to revamp the
concurrency model of the watchdog entirely now that we have all those
fancy concurrency primitives that were not available four years ago when
the watchdog was first written.
2. On an especially slow Windows machine, we found that starting the
language server would sometimes not succeed at all because reading from
the stdin pipe in the watchdog produced an EINVAL error, which was in
turn caused by an NT "pipe empty" error.
- After lots of debugging, @Kha found that Lake accidentally passes its
stdin to Git because it does not explicitly set the `stdin` field to
`null` when spawning the process.
- Changing this fixes the issue, which suggests that Git may mutate the
pipe we pass to it to be non-blocking, which then causes a "pipe empty"
error in the watchdog when we also attempt to read from that same pipe.
- I'm still very uncertain why we only saw this issue on one
particularly slow machine and not across the whole eco system.
This PR also resolves an issue where we would not correctly emit
messages that we received while the file worker is being restarted to
the corresponding file worker after the restart.
Closes#3786, closes#3787.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Autoparam tactic scripts have no source positions, which until recently
made it so that any errors or messages would be logged at the current
ref, which was the application or structure instance being elaborated.
However, with the new incrementality features the ref is now carefully
managed to avoid leakage of outside data. This inhibits the elaborator's
ref from being used for the tactic's ref, causing messages to be placed
at the beginning of the file rather than on the syntax that triggered
the autoparam.
To fix this, now the elaborators insert the ref's source position
everywhere into the autoparam tactic script.
If in the future messages for synthetic tactics appear at the tops of
files in other contexts, we should consider an approach where
`Lean.Elab.Term.withReuseContext` uses something like `replaceRef` to
set the ref while disabling incrementality when the tactic does not
contain source position information.
Closes#4880
Currently, the messages in the diagnostic summaries are created by
appending interpolated strings. We wrap these in `.trace`'s, and the
results are better formatted when expanding child nodes in the info
view. Particularly, the latter diagnostic summaries remain on their own
lines flush to the left instead of on the same line directly adjacent to
the last child node.
For experimentation by @the-sofi-uwu.
I also have an efficient number parser in LeanSAT that I am planning to
upstream after we have sufficiently bikeshed this change.
When `set_option diagnostics true`, for each theorem with size >
`diagnostics.threshold.proofSize`, display proof size, and the number of
applications for each constant symbol.
TODO:
- Support for `zeta := true` at `apply_beta`.
- Investigate test failure.
- Break PR in pieces because of bootstrapping issues. The current PR
updates a stage0 file to workaround the issue.
Motivation: significant performance improvement at
https://github.com/leanprover/LNSym/blob/proof_size_expt/Proofs/SHA512/Experiments/Sym30.lean
With M1 Pro:
- Before: 4.56 secs
- After: 3.16 secs
Successfully built stage2 using this PR
This modification improves the performance of the example in issue
#4861. It no longer times out but is still expensive.
Here is the analysis of the performance issue: Given `(x : Int)`, to
elaborate `x ^ 1`, a few default instances have to be tried.
First, the homogeneous instance is tried and fails since `Int` does not
implement `Pow Int`. Then, the `NatPow` instance is tried, and it also
fails. The same process is performed for each term of the form `p ^ 1`.
There are seveal of them at #4861. After all of these fail, the lower
priority default instance for numerals is tried, and `x ^ 1` becomes `x
^ (1 : Nat)`. Then, `HPow Int Nat Int` can be applied, and the
elaboration succeeds. However, this process has to be repeated for every
single term of the form `p ^ 1`. The elaborator tries all homogeneous
`HPow` and `NatPow` instances for all `p ^ 1` terms before trying the
lower priority default instance `OfNat`.
This commit ensures `Int` has a `NatPow` instance instead of `HPow Int
Nat Int`. This change shortcuts the process, but it still first tries
the homogeneous `HPow` instance, fails, and then tries `NatPow`. The
elaboration can be made much more efficient by writing `p ^ (1 : Nat)`.
Those represent ~13% of the time spent in `save_result`,
even though `r` is a temporary in all cases but one.
See #4698 for details.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
…rators
Right now those constructors result in a copy instead of the desired
move. We've measured that expr copying and assignment by itself uses
around 10% of total runtime on our workloads.
See #4698 for details.
Initial options are now re-parsed and validated after importing. Cmdline
option assignments prefixed with `weak.` are silently discarded if the
option name without the prefix does not exist.
Fixes#3403
This allows bitblasting `BitVec.replicate`.
I changed the definition of `BitVec.replicate` to use `BitVec.cast` in
order to make the proof smoother, since it's an easier time simplifying
away terms with `BitVec.cast`.
---------
Co-authored-by: Tobias Grosser <tobias@grosser.es>
@@ -25,7 +25,7 @@ Please put an X between the brackets as you perform the following steps:
### Context
[Broader context that the issue occured in. If there was any prior discussion on [the Lean Zulip](https://leanprover.zulipchat.com), link it here as well.]
[Broader context that the issue occurred in. If there was any prior discussion on [the Lean Zulip](https://leanprover.zulipchat.com), link it here as well.]
### Steps to Reproduce
@@ -39,7 +39,7 @@ Please put an X between the brackets as you perform the following steps:
### Versions
[Output of `#eval Lean.versionString`]
[Output of `#version` or `#eval Lean.versionString`]
* 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.
* For `feat/fix` PRs, the first paragraph starting with "This PR" must be present and will become a
changelog entry unless the PR is labeled with `no-changelog`. If the PR does not have this label,
it must instead be categorized with one of the `changelog-*` labels (which will be done by a
reviewer for external PRs).
* A toolchain of the form `leanprover/lean4-pr-releases:pr-release-NNNN` for Linux and M-series Macs will be generated upon build. To generate binaries for Windows and Intel-based Macs as well, write a comment containing `release-ci` on its own line.
* 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.
---
Closes #0000 (`RFC` or `bug` issue number fixed by this PR, if any)
This PR <short changelog summary for feat/fix, see above>.
Closes <`RFC` or `bug` issue number fixed by this PR, if any>
# Check that the most recently nightly coincides with 'git merge-base HEAD master'
- name:Check merge-base and nightly-testing-YYYY-MM-DD
@@ -134,7 +134,7 @@ jobs:
MESSAGE=""
if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
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."
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
@@ -163,10 +163,11 @@ jobs:
# so keep in sync
# Use GitHub API to check if a comment already exists
@@ -73,7 +73,7 @@ update the archived C source code of the stage 0 compiler in `stage0/src`.
The github repository will automatically update stage0 on `master` once
`src/stdlib_flags.h` and `stage0/src/stdlib_flags.h` are out of sync.
If you have write access to the lean4 repository, you can also also manually
If you have write access to the lean4 repository, you can also manually
trigger that process, for example to be able to use new features in the compiler itself.
You can do that on <https://github.com/leanprover/lean4/actions/workflows/update-stage0.yml>
or using Github CLI with
@@ -103,10 +103,21 @@ your PR using rebase merge, bypassing the merge queue.
As written above, changes in meta code in the current stage usually will only
affect later stages. This is an issue in two specific cases.
* For the special case of *quotations*, it is desirable to have changes in builtin parsers affect them immediately: when the changes in the parser become active in the next stage, builtin macros implemented via quotations should generate syntax trees compatible with the new parser, and quotation patterns in builtin macros and elaborators should be able to match syntax created by the new parser and macros.
Since quotations capture the syntax tree structure during execution of the current stage and turn it into code for the next stage, we need to run the current stage's builtin parsers in quotations via the interpreter for this to work.
Caveats:
* We activate this behavior by default when building stage 1 by setting `-Dinternal.parseQuotWithCurrentStage=true`.
We force-disable it inside `macro/macro_rules/elab/elab_rules` via `suppressInsideQuot` as they are guaranteed not to run in the next stage and may need to be run in the current one, so the stage 0 parser is the correct one to use for them.
It may be necessary to extend this disabling to functions that contain quotations and are (exclusively) used by one of the mentioned commands. A function using quotations should never be used by both builtin and non-builtin macros/elaborators. Example: https://github.com/leanprover/lean4/blob/f70b7e5722da6101572869d87832494e2f8534b7/src/Lean/Elab/Tactic/Config.lean#L118-L122
* The parser needs to be reachable via an `import` statement, otherwise the version of the previous stage will silently be used.
* Only the parser code (`Parser.fn`) is affected; all metadata such as leading tokens is taken from the previous stage.
For an example, see https://github.com/leanprover/lean4/commit/f9dcbbddc48ccab22c7674ba20c5f409823b4cc1#diff-371387aed38bb02bf7761084fd9460e4168ae16d1ffe5de041b47d3ad2d22422R13
* For *non-builtin* meta code such as `notation`s or `macro`s in
`Notation.lean`, we expect changes to affect the current file and all later
files of the same stage immediately, just like outside the stdlib. To ensure
this, we need to build the stage using `-Dinterpreter.prefer_native=false` -
this, we build stage 1 using `-Dinterpreter.prefer_native=false` -
otherwise, when executing a macro, the interpreter would notice that there is
already a native symbol available for this function and run it instead of the
new IR, but the symbol is from the previous stage!
@@ -124,26 +135,11 @@ affect later stages. This is an issue in two specific cases.
further stages (e.g. after an `update-stage0`) will then need to be compiled
with the flag set to `false` again since they will expect the new signature.
For an example, see https://github.com/leanprover/lean4/commit/da4c46370d85add64ef7ca5e7cc4638b62823fbb.
When enabling `prefer_native`, we usually want to *disable*`parseQuotWithCurrentStage` as it would otherwise make quotations use the interpreter after all.
However, there is a specific case where we want to set both options to `true`: when we make changes to a non-builtin parser like `simp` that has a builtin elaborator, we cannot have the new parser be active outside of quotations in stage 1 as the builtin elaborator from stage 0 would not understand them; on the other hand, we need quotations in e.g. the builtin `simp` elaborator to produce the new syntax in the next stage.
As this issue usually affects only tactics, enabling `debug.byAsSorry` instead of `prefer_native` can be a simpler solution.
* For the special case of *quotations*, it is desirable to have changes in
built-in parsers affect them immediately: when the changes in the parser
become active in the next stage, macros implemented via quotations should
generate syntax trees compatible with the new parser, and quotation patterns
in macro and elaborators should be able to match syntax created by the new
parser and macros. Since quotations capture the syntax tree structure during
execution of the current stage and turn it into code for the next stage, we
need to run the current stage's built-in parsers in quotation via the
interpreter for this to work. Caveats:
* Since interpreting full parsers is not nearly as cheap and we rarely change
built-in syntax, this needs to be opted in using `-Dinternal.parseQuotWithCurrentStage=true`.
* The parser needs to be reachable via an `import` statement, otherwise the
version of the previous stage will silently be used.
* Only the parser code (`Parser.fn`) is affected; all metadata such as leading
tokens is taken from the previous stage.
For an example, see https://github.com/leanprover/lean4/commit/f9dcbbddc48ccab22c7674ba20c5f409823b4cc1#diff-371387aed38bb02bf7761084fd9460e4168ae16d1ffe5de041b47d3ad2d22422
(from before the flag defaulted to `false`).
For a `prefer_native` example, see https://github.com/leanprover/lean4/commit/da4c46370d85add64ef7ca5e7cc4638b62823fbb.
To modify either of these flags both for building and editing the stdlib, adjust
the code in `stage0/src/stdlib_flags.h`. The flags will automatically be reset
@@ -5,7 +5,7 @@ Some notes on how to debug Lean, which may also be applicable to debugging Lean
## Tracing
In `CoreM` and derived monads, we use `trace![traceCls] "msg with {interpolations}"` to fill the structured trace viewable with `set_option trace.traceCls true`.
In `CoreM` and derived monads, we use `trace[traceCls] "msg with {interpolations}"` to fill the structured trace viewable with `set_option trace.traceCls true`.
New trace classes have to be registered using `registerTraceClass` first.
Notable trace classes:
@@ -22,7 +22,9 @@ Notable trace classes:
In pure contexts or when execution is aborted before the messages are finally printed, one can instead use the term `dbg_trace "msg with {interpolations}"; val` (`;` can also be replaced by a newline), which will print the message to stderr before evaluating `val`. `dbgTraceVal val` can be used as a shorthand for `dbg_trace "{val}"; val`.
Note that if the return value is not actually used, the trace code is silently dropped as well.
In the language server, stderr output is buffered and shown as messages after a command has been elaborated, unless the option `server.stderrAsMessages` is deactivated.
By default, such stderr output is buffered and shown as messages after a command has been elaborated, which is necessary to ensure deterministic ordering of messages under parallelism.
If Lean aborts the process before it can finish the command or takes too long to do that, using `-DstderrAsMessages=false` avoids this buffering and shows `dbg_trace` output (but not `trace`s or other diagnostics) immediately.
Now, we prove that if `Expr.typeCheck e` returns `Maybe.unknown`, then forall `ty`, `HasType e ty` does not hold.
The notation `e.typeCheck` is sugar for `Expr.typeCheck e`. Lean can infer this because we explicitly said that `e` has type `Expr`.
The proof is by induction on `e` and case analysis. The tactic `rename_i` is used to to rename "inaccessible" variables.
We say a variable is inaccessible if it is introduced by a tactic (e.g., `cases`) or has been shadowed by another variable introduced
by the user. Note that the tactic `simp [typeCheck]` is applied to all goal generated by the `induction` tactic, and closes
The proof is by induction on `e` and case analysis. Note that the tactic `simp [typeCheck]` is applied to all goal generated by the `induction` tactic, and closes
the cases corresponding to the constructors `Expr.nat` and `Expr.bool`.
Proving and programming are inherently interactive tasks. Lots of mathematical objects and data
structures are visual in nature. *User widgets* let you associate custom interactive UIs with
sections of a Lean document. User widgets are rendered in the Lean infoview.
Proving and programming are inherently interactive tasks.
Lots of mathematical objects and data structures are visual in nature.
*User widgets* let you associate custom interactive UIs
with sections of a Lean document.
User widgets are rendered in the Lean infoview.
## Trying it out
To try it out, simply type in the following code and place your cursor over the `#widget` command.
To try it out, type in the following code and place your cursor over the `#widget` command.
You can also [view this manual entry in the online editor](https://live.lean-lang.org/#url=https%3A%2F%2Fraw.githubusercontent.com%2Fleanprover%2Flean4%2Fmaster%2Fdoc%2Fexamples%2Fwidgets.lean).
-/
@[widget_module]
@@ -21,38 +24,37 @@ def helloWidget : Widget.Module where
import * as React from 'react';
export default function(props) {
const name = props.name || 'world'
return React.createElement('p', {}, name + '!')
return React.createElement('p', {}, 'Hello ' + name + '!')
}"
#widgethelloWidget
/-!
If you want to dive into a full sample right away, check out
@@ -396,7 +396,7 @@ Every expression in Lean has a natural computational interpretation, unless it i
* *β-reduction* : An expression ``(λ x, t) s`` β-reduces to ``t[s/x]``, that is, the result of replacing ``x`` by ``s`` in ``t``.
* *ζ-reduction* : An expression ``let x := s in t`` ζ-reduces to ``t[s/x]``.
* *δ-reduction* : If ``c`` is a defined constant with definition ``t``, then ``c`` δ-reduces to to ``t``.
* *δ-reduction* : If ``c`` is a defined constant with definition ``t``, then ``c`` δ-reduces to ``t``.
* *ι-reduction* : When a function defined by recursion on an inductive type is applied to an element given by an explicit constructor, the result ι-reduces to the specified function value, as described in [Inductive Types](inductive.md).
The reduction relation is transitive, which is to say, is ``s`` reduces to ``s'`` and ``t`` reduces to ``t'``, then ``s t`` reduces to ``s' t'``, ``λ x, s`` reduces to ``λ x, s'``, and so on. If ``s`` and ``t`` reduce to a common term, they are said to be *definitionally equal*. Definitional equality is defined to be the smallest equivalence relation that satisfies all these properties and also includes α-equivalence and the following two relations:
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).
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](../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.
We strongly suggest that new users instead follow the [Quickstart](../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.
1. Launch VS Code and install the `lean4` extension by clicking on the "Extensions" sidebar entry and searching for "lean4".
1. Launch VS Code and install the `Lean4` extension by clicking on the 'Extensions' sidebar entry and searching for 'Lean 4'.
1. Open the Lean 4 setup guide by creating a new text file using "File > New Text File" (`Ctrl+N` / `Cmd+N`), clicking on the ∀-symbol in the top right and selecting "Documentation… > Docs: Show Setup Guide".
1. Open the Lean 4 setup guide by creating a new text file using 'File > New Text File' (`Ctrl+N` / `Cmd+N`), clicking on the ∀-symbol in the top right and selecting 'Documentation… > Docs: Show Setup Guide'.
# glibc: use for linking (so Lean programs don't embed newer symbol versions), but not for running (because libc.so, librt.so, and ld.so must be compatible)!
$CP$GLIBC/lib/libc_nonshared.a stage1/lib/glibc
# libpthread_nonshared.a must be linked in order to be able to use `pthread_atfork(3)`. LibUV uses this function.
* `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
/-- `castAdd m i` embeds `i : Fin n` in `Fin (n+m)`. See also `Fin.natAdd` and `Fin.addNat`. -/
@[inline]defcastAdd(m):Finn→Fin(n+m):=
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.
