this PR reorders the `DiscrTree.Key` constructors to match the order
given in the manually written `DiscrTree.Key.ctorIdx`. This allows us to
use the auto-generated one, and moreover lets this code benefit from
special compiler support for `.ctorIdx`, once that lands.
This PR normalizes the published diagnostics in the test runner so that
messages published out of order (due to parallelism) cannot cause test
failures. Clients can handle out-of-order messages just fine.
This PR generates `.ctorIdx` functions for all inductive types, not just
enumeration types. This can be a building block for other constructions
(`BEq`, `noConfusion`) that are size-efficient even for large
inductives.
It also renames it from `.toCtorIdx` to `.ctorIdx`, which is the more
idiomatic naming.
The old name exists as an alias, with a deprecation attribute to be
added after the next
stage0 update.
These functions can arguably compiled down to a rather efficient tag
lookup, rather than a `case` statement. This is future work (but
hopefully near future).
For a fair number of basic types the compiler is not able to compile a
function using `casesOn` until further definitions have been defined.
This therefore (ab)uses the `genInjectivity` flag and
`gen_injective_theorems%` command to also control the generation of this
construct.
For (slightly) more efficient kernel reduction one could use `.rec`
rather than `.casesOn`. I did not do that yet, also because it
complicates compilation.
This PR fixes a bug that caused the Lean server process tree to survive
the closing of VS Code.
The cause of this issue was that the file worker main task was blocked
on waiting for the result of `lake setup-file` because the blocking call
was lifted outside of the dedicated server task that was supposed to
contain it by the compiler.
This PR upstreams lemmas about `Rat` from `Mathlib.Data.Rat.Defs` and
`Mathlib.Algebra.Order.Ring.Unbundled.Rat`, specifically enough to get
`Lean.Grind.Field Rat` and `Lean.Grind.OrderedRing Rat`. In addition to
the lemmas, instances for `Inv Rat`, `Pow Rat Nat` and `Pow Rat Int`
have been upstreamed.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR adds support for detecting associative operators in `grind`. The
new AC module also detects whether the operator is commutative,
idempotent, and whether it has a neutral element. The information is
cached.
This PR allows for more fine-grained control over what derived instances
have exposed definitions under the module system: handlers should not
expose their implementation unless either the deriving item or a
surrounding section is marked with `@[expose]`. Built-in handlers to be
updated after a stage 0 update.
This PR adds the modules in `Lake.Util` to core's Lake configuration to
ensure all utilities are built. With the module system port, they were
no longer all transitively imported.
Specifically, `Lake.Util.Lock` is unused because Lake does not currently
use a lock file for the build.
This PR allows Lean's parser to run with a final position prior to the
end of the string, so it can be invoked on a sub-region of the input.
This has applications in Verso proper, which parses Lean syntax in
contexts such as code blocks and docstrings, and it is a prerequisite to
parsing the contents of Lean docstrings.
This PR replaces `Std.Internal.Rat` with the new public `Rat` upstreamed
from Batteries.
The time library was depending on some defeqs which are no longer true,
so I have inserted some casts.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Sofia Rodrigues <sofia@algebraic.dev>
This PR contains lemmas about `Int` (minor amendments for BitVec and
Nat) that are being used in preparing the dyadics. This is all work of
@Rob23oba, which I'm pulling out of #9993 early to keep that one
manageable.
This PR fixes the compilation of `noConfusion` by repairing an oversight
made when porting this code from the old compiler. The old compiler only
repeatedly expanded the major for each non-`Prop` field of the inductive
under consideration, mirroring the construction of `noConfusion` itself,
whereas the new compiler erroneously counted all fields.
Fixes#9971.
This PR improves support for `a^n` in `grind cutsat`. For example, if
`cutsat` discovers that `a` and `b` are equal to numerals, it now
propagates the equality. This PR is similar to #9996, but `a^b`.
Example:
```lean
example (n : Nat) : n = 2 → 2 ^ (n+1) = 8 := by
grind
```
With #10022, it also improves the support for `BitVec n` when `n` is not
numeral. Example:
```lean
example {n m : Nat} (x : BitVec n)
: 2 ≤ n → n ≤ m → m = 2 → x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 3 := by
grind
```
This PR refactors the Lake codebase to use the new module system
throughout. Every module in `Lake` is now a `module`.
As this was already a large-scale refactor, a general cleanup of the
code has also been bundled in.
This PR also uses workarounds for currently outstanding module system
issues: #10061, #10062, #10063, #10064, #10065, #10067, and #10068.
**Breaking change:** Since the module system encourages a
`private`-by-default design, the Lake API has switched from its previous
`public`-by-default approach. As such, many definitions that were
previously public are now private. The newly private definitions are not
expected to have had significant user use, Nonetheless, important use
cases could be missed. If a key API is now inaccessible but seems like
it should be public, users are encouraged to report this as an issue on
GitHub.
This PR reverts parts of #10005 that surprisingly turned out to cause a
performance regression in the benchmarks. The slowdown seems to be
related to elaboration, not inefficiencies in the generated code. This
is just a quick fix. I will take a closer look in a week.
This PR adds a stop position field to parser input contexts, allowing
the parser to be instructed to stop parsing prior to the end of a file.
This is step 1, prior to a stage0 update, to make run-time data
structures sufficiently compatible to avoid segfaults. After the update,
the actual code to stop parsing can be merged.
This PR implements the necessary typeclasses so that range notation
works for integers. For example, `((-2)...3).toList = [-2, -1, 0, 1, 2]
: List Int`.
This PR changes macro scope numbering from per-module to per-command,
ensuring that unrelated changes to other commands do not affect macro
scopes generated by a command, which improves `prefer_native` hit rates
on bootstrapping as well as avoids further rebuilds under the module
system.
In detail, instead of always using the current module name as a macro
scope prefix, each command now introduces a new macro scope prefix
(called "context") of the shape `<main module>._hygCtx_<uniq>` where
`uniq` is a `UInt32` derived from the command but automatically
incremented in case of conflicts (which must be local to the current
module). In the current implementation, `uniq` is the hash of the
declaration name, if any, or else the hash of the full command's syntax.
Thus, it is always independent of syntactic changes to other commands
(except in case of hash conflicts, which should only happen in practice
for syntactically identical commands) and, in the case of declarations,
also independent of syntactic changes to any private parts of the
declaration.
This PR replaces the implementation of `Nat.log2` with a version that
reduces faster.
The new version can handle:
```lean-4
example : Nat.log2 (1 <<< 500) = 500 := rfl
```
This PR enables core's `LakeMain` to be a `module` when core is built
without `USE_LAKE`.
This was a problem when porting Lake to the module system (#9749).
This PR shortens the work necessary to make a type compatible with the
polymorphic range notation. In the concrete case of `Nat`, it reduces
the required lines of code from 150 to 70.
This PR adds useful declarations to the `LawfulOrderMin/Max` and
`LawfulOrderLeftLeaningMin/Max` API. In particular, it introduces
`.leftLeaningOfLE` factories for `Min` and `Max`. It also renames
`LawfulOrderMin/Max.of_le` to .of_le_min_iff` and `.of_max_le_iff` and
introduces a second variant with different arguments.
This PR changes the `toMono` pass to replace decls with their `_redArg`
equivalent, which has the consequence of not considering arguments
deemed useless by the `reduceArity` pass for the purposes of the
`noncomputable` check.
This PR adds support for correctly handling computations on fields in
`casesOn` for inductive predicates that support large elimination. In
any such predicate, the only relevant fields allowed are those that are
also used as an index, in which case we can find the supplied index and
use that term instead.
This PR improves support for `Fin n` in `grind cutsat` when `n` is not a
numeral. For example, the following goals can now be solved
automatically:
```lean
example (p d : Nat) (n : Fin (p + 1))
: 2 ≤ p → p ≤ d + 1 → d = 1 → n = 0 ∨ n = 1 ∨ n = 2 := by
grind
example (s : Nat) (i j : Fin (s + 1)) (hn : i ≠ j) (hl : ¬i < j) : j < i := by
grind
example {n : Nat} (j : Fin (n + 1)) : j ≤ j := by
grind
example {n : Nat} (x y : Fin ((n + 1) + 1)) (h₂ : ¬x = y) (h : ¬x < y) : y < x := by
grind
```
This PR adds `@[expose]` to `Lean.ParserState.setPos`. This makes it
possible to prove in-boundedness for a state produced by `setPos` for
functions like `next'` and `get'` without needing to `import all`.
This came up while porting Lake to the module system (#9749).
This PR changes the handling of overapplied constructors when lowering
LCNF to IR from a (slightly implicit) assertion failure to producing
`unreachable`. Transformations on inlined unreachable code can produce
constructor applications with additional arguments.
In the old compiler, these additional arguments were silently ignored,
but it seems more sensible to replace them with `unreachable`, just in
case they arise due to a compiler error.
Fixes#9937.
This PR derives `BEq` and `Hashable` for `Lean.Import`. Lake already did
this later, but it now done when defining `Import`.
Doing this in Lake became problematic when porting it to the module
system (#9749).
This PR exposes the bodies of `Name.append`, `Name.appendCore`, and
`Name.hasMacroScopes`. This enables proof by reflection of the
concatenation of name literals when using the module system.
```lean
example : `foo ++ `bar = `foo.bar := rfl
```
This is necessary for Lake as part of the port to using `module`
(#9749).
This PR make some minor changes to the grind annotation analysis script,
including sorting results and handling errors. Still need to add an
external UI.
This PR changes Lake to not set `LEAN_GITHASH` when in core (i.e.
`bootstrap = true`). This avoids Lake rebuilding modules when the Lake
watchdog is on one build of Lean/Lake and the command line is on a
different one.
The current reuse analysis is greedy in that every function attempts to
reuse a value. However, this means that if the last use is an owned
argument, it will be `inc`'d prior to this last use, in order to prevent
reuse from happening in the callee. In many cases, it makes more sense
to give the callee the chance to reuse it instead. The benchmark results
indicate that this is a much better default.
This PR improves support for nonlinear `/` and `%` in `grind cutsat`.
For example, given `a / b`, if `cutsat` discovers that `b = 2`, it now
propagates that `a / b = b / 2`. This PR is similar to #9996, but for
`/` and `%`. Example:
```lean
example (a b c d : Nat)
: b > 1 → d = 1 → b ≤ d + 1 → a % b = 1 → a = 2 * c → False := by
grind
```
This PR fixes a bug in `#eval` where clicking on the evaluated
expression could show errors in the Infoview. This was caused by `#eval`
not saving the temporary environment that is used when elaborating the
expression.
This PR provides factories that derive order typeclasses in bulk, given
an `Ord` instance. If present, existing instances are preferred over
those derived from `Ord`. It is possible to specify any instance
manually if desired.
This PR reduces the number of `Nat.Bitwise` grind annotations we have
the deal with distributivity. The new smaller set encourages `grind` to
rewrite into DNF. The old behaviour just resulted in saturating up to
the instantiation limits.
This PR improves support for nonlinear monomials in `grind cutsat`. For
example, given a monomial `a * b`, if `cutsat` discovers that `a = 2`,
it now propagates that `a * b = 2 * b`.
Recall that nonlinear monomials like `a * b` are treated as variables in
`cutsat`, a procedure designed for linear integer arithmetic.
Example:
```lean
example (a : Nat) (ha : a < 8) (b c : Nat) : 2 ≤ b → c = 1 → b ≤ c + 1 → a * b < 8 * b := by
grind
example (x y z w : Int) : z * x * y = 4 → x = z + w → z = 1 → w = 2 → False := by
grind
```
This PR registers a parser alias for `Lean.Parser.Command.visibility`.
This avoids having to import `Lean.Parser.Command` in simple command
macros that use visibilities.
This PR provides the means to quickly provide all the order instances
associated with some high-level order structure (preorder, partial
order, linear preorder, linear order). This can be done via the factory
functions `PreorderPackage.ofLE`, `PartialOrderPackage.ofLE`,
`LinearPreorderPackage.ofLE` and `LinearOrderPackage.ofLE`.
This PR makes `IsPreorder`, `IsPartialOrder`, `IsLinearPreorder` and
`IsLinearOrder` extend `BEq` and `Ord` as appropriate, adds the
`LawfulOrderBEq` and `LawfulOrderOrd` typeclasses relating `BEq` and
`Ord` to `LE`, and adds many lemmas and instances.
Note: This PR contains a refactoring where `Init.Data.Ord` is moved to
`Init.Data.Ord.Basic`. If I added `Init.Data.Ord` simply importing all
submodules, git would not be able to determine that `Init.Data.Ord` was
renamed to `Init.Data.Ord.Basic`. This could lead to unnecessary merge
conflicts in the future. Hence, I chose the name `Init.Data.OrdRoot`
instead of `Init.Data.Ord` temporarily. After this PR, I will rename
this module back to `Init.Data.Ord` in a separate PR.
(This is a copy of #9430: I will not touch that PR because it currently
allows to debug a CI problem and pushing commits might break the
reproducibility.)
This PR eliminates uses of `intros x y z` (with arguments) and updates
the `intros` docstring to suggest that `intro x y z` should be used
instead. The `intros` tactic is historical, and can be traced all the
way back to Lean 2, when `intro` could only introduce a single
hypothesis. Since 2020, the `intro` tactic has superceded it. The
`intros` tactic (without arguments) is currently still useful.
This PR upstreams the definition of Rat from Batteries, for use in our
planned interval arithmetic tactic.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR adds two test cases extracted from Mathlib, that `grind` cannot
solve but `omega` can. Originally the multiplication instance came from
`Nat.instSemiring` and `Int.instSemiring`, in minimizing I found that
`Distrib` is already enough.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR fixes an issue when running Mathlib's `FintypeCat` as code,
where an erased type former is passed to a polymorphic function. We were
lowering the arrow type to`object`, which conflicts with the runtime
representation of an erased value as a tagged scalar.
This PR modifies the generation of induction and partial correctness
lemmas for `mutual` blocks defined via `partial_fixpoint`. Additionally,
the generation of lattice-theoretic induction principles of functions
via `mutual` blocks is modified for consistency with `partial_fixpoint`.
The lemmas now come in two variants:
1. A conjunction variant that combines conclusions for all elements of
the mutual block. This is generated only for the first function inside
of the mutual block.
2. Projected variants for each function separately
## Example 1
```lean4
axiom A : Type
axiom B : Type
axiom A.toB : A → B
axiom B.toA : B → A
mutual
noncomputable def f : A := g.toA
partial_fixpoint
noncomputable def g : B := f.toB
partial_fixpoint
end
```
Generated `fixpoint_induct` lemmas:
```lean4
f.fixpoint_induct (motive_1 : A → Prop) (motive_2 : B → Prop) (adm_1 : admissible motive_1)
(adm_2 : admissible motive_2) (h_1 : ∀ (g : B), motive_2 g → motive_1 g.toA)
(h_2 : ∀ (f : A), motive_1 f → motive_2 f.toB) : motive_1 f
g.fixpoint_induct (motive_1 : A → Prop) (motive_2 : B → Prop) (adm_1 : admissible motive_1)
(adm_2 : admissible motive_2) (h_1 : ∀ (g : B), motive_2 g → motive_1 g.toA)
(h_2 : ∀ (f : A), motive_1 f → motive_2 f.toB) : motive_2 g
```
Mutual (conjunction) variant:
```lean4
f.mutual_fixpoint_induct (motive_1 : A → Prop) (motive_2 : B → Prop) (adm_1 : admissible motive_1) (adm_2 : admissible motive_2)
(h_1 : ∀ (g : B), motive_2 g → motive_1 g.toA) (h_2 : ∀ (f : A), motive_1 f → motive_2 f.toB) :
motive_1 f ∧ motive_2 g
```
## Example 2
```lean4
mutual
def f (n : Nat) : Option Nat :=
g (n + 1)
partial_fixpoint
def g (n : Nat) : Option Nat :=
if n = 0 then .none else f (n + 1)
partial_fixpoint
end
```
Generated `partial_correctness` lemmas (in a projected variant):
```lean4
f.partial_correctness (motive_1 motive_2 : Nat → Nat → Prop)
(h_1 :
∀ (g : Nat → Option Nat),
(∀ (n r : Nat), g n = some r → motive_2 n r) → ∀ (n r : Nat), g (n + 1) = some r → motive_1 n r)
(h_2 :
∀ (f : Nat → Option Nat),
(∀ (n r : Nat), f n = some r → motive_1 n r) →
∀ (n r : Nat), (if n = 0 then none else f (n + 1)) = some r → motive_2 n r)
(n r✝ : Nat) : f n = some r✝ → motive_1 n r✝
g.partial_correctness (motive_1 motive_2 : Nat → Nat → Prop)
(h_1 :
∀ (g : Nat → Option Nat),
(∀ (n r : Nat), g n = some r → motive_2 n r) → ∀ (n r : Nat), g (n + 1) = some r → motive_1 n r)
(h_2 :
∀ (f : Nat → Option Nat),
(∀ (n r : Nat), f n = some r → motive_1 n r) →
∀ (n r : Nat), (if n = 0 then none else f (n + 1)) = some r → motive_2 n r)
(n r✝ : Nat) : g n = some r✝ → motive_2 n r✝
```
Mutual (conjunction) variant:
```
f.mutual_partial_correctness (motive_1 motive_2 : Nat → Nat → Prop)
(h_1 :
∀ (g : Nat → Option Nat),
(∀ (n r : Nat), g n = some r → motive_2 n r) → ∀ (n r : Nat), g (n + 1) = some r → motive_1 n r)
(h_2 :
∀ (f : Nat → Option Nat),
(∀ (n r : Nat), f n = some r → motive_1 n r) →
∀ (n r : Nat), (if n = 0 then none else f (n + 1)) = some r → motive_2 n r) :
(∀ (n r : Nat), f n = some r → motive_1 n r) ∧ ∀ (n r : Nat), g n = some r → motive_2 n r
```
This PR modifies `intro` to create tactic info localized to each
hypothesis, making it possible to see how `intro` works
variable-by-variable. Additionally:
- The tactic supports `intro rfl` to introduce an equality and
immediately substitute it, like `rintro rfl` (recall: the `rfl` pattern
is like doing `intro h; subst h`). The `rintro` tactic can also now
support `HEq` in `rfl` patterns if `eq_of_heq` applies.
- In `intro (h : t)`, elaboration of `t` is interleaved with unification
with the type of `h`, which prevents default instances from causing
unification to fail.
- Tactics that change types of hypotheses (including `intro (h : t)`,
`delta`, `dsimp`) now update the local instance cache.
In `intro x y z`, tactic info ranges are `intro x`, `y`, and `z`. The
reason for including `intro` with `x` is to make sure the info range is
"monotonic" while adding the first argument to `intro`.
This PR adds lemmas for the `TreeMap` operations `filter`, `map` and
`filterMap`. These lemmas existed already for hash maps and are simply
ported over from there.
This PR allows most of the `List.lookup` lemmas to be used when
`LawfulBEq α` is not available.
`LawfulBEq` is very strong. Most of the lemmas don't actually require it
-- some only require `ReflBEq`, and only `List.lookup_eq_some_iff`
actually requires `LawfulBEq`.
This PR moves arithmetic of `String.Pos` out of the prelude.
Other `String` declarations are part of the prelude because they are
generated by macros, but this does not seem to be the case for these.
This PR cleans up `optParam`/`autoParam`/etc. annotations before
elaborating definition bodies, theorem bodies, `fun` bodies, and `let`
function bodies. Both `variable`s and binders in declaration headers are
supported.
There are no changes to `inductive`/`structure`/`axiom`/etc. processing,
just `def`/`theorem`/`example`/`instance`.
This PR ensures that equations in the `grind cutsat` module are
maintained in solved form. That is, given an equation `a*x + p = 0` used
to eliminate `x`, the linear polynomial `p` must not contain other
eliminated variables. Before this PR, equations were maintained in
triangular form. We are going to use the solved form to linearize
nonlinear terms.
This PR removes the option `grind +ringNull`. It provided an alternative
proof term construction for the `grind ring` module, but it was less
effective than the default proof construction mode and had effectively
become dead code.
This PR also optimizes semiring normalization proof terms using the
infrastructure added in #9946.
**Remark:** After updating stage0, we can remove several background
theorems from the `Init/Grind` folder.
This PR optimizes the proof terms produced by `grind linarith`. It is
similar to #9945, but for the `linarith` module in `grind`.
It removes unused entries from the context objects when generating the
final proof, significantly reducing the amount of junk in the resulting
terms.
This PR optimizes the proof terms produced by `grind cutsat`. It removes
unused entries from the context objects when generating the final proof,
significantly reducing the amount of junk in the resulting terms.
Example:
```lean
/--
trace: [grind.debug.proof] fun h h_1 h_2 h_3 h_4 h_5 h_6 h_7 h_8 =>
let ctx := RArray.leaf (f 2);
let p_1 := Poly.add 1 0 (Poly.num 0);
let p_2 := Poly.add (-1) 0 (Poly.num 1);
let p_3 := Poly.num 1;
le_unsat ctx p_3 (eagerReduce (Eq.refl true)) (le_combine ctx p_2 p_1 p_3 (eagerReduce (Eq.refl true)) h_8 h_1)
-/
#guard_msgs in -- Context should contain only `f 2`
open Lean Int Linear in
set_option trace.grind.debug.proof true in
example (f : Nat → Int) :
f 1 <= 0 → f 2 <= 0 → f 3 <= 0 → f 4 <= 0 → f 5 <= 0 →
f 6 <= 0 → f 7 <= 0 → f 8 <= 0 → -1 * f 2 + 1 <= 0 → False := by
grind
```
This PR expands `mvcgen using invariants | $n => $t` to `mvcgen; case
inv<$n> => exact $t` to avoid MVar instantiation mishaps observable in
the test case for #9581.
Closes#9581.
This PR implements extended `induction`-inspired syntax for `mvcgen`,
allowing optional `using invariants` and `with` sections.
```lean
mvcgen
using invariants
| 1 => Invariant.withEarlyReturn
(onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
(onContinue := fun traversalState seen =>
⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
with mleave -- mleave is a no-op here, but we are just testing the grammar
| vc1 => grind
| vc2 => grind
| vc3 => grind
| vc4 => grind
| vc5 => grind
```
This PR guards the `Std.Tactic.Do.MGoalEntails` delaborator by a check
ensuring that there are at least 3 arguments present, preventing
potential panics.
This PR fixes the `forIn` function, that previously caused the resulting
Promise to be dropped without a value when an exception was thrown
inside of it. It also corrects the parameter order of the `background`
function.
This PR changes `internalizeCode` to replace all substitutions with
non-param-bound fvars in `Expr`s (which are all types) with `lcAny`,
preserving the invariant that there are no such dependencies. The
violation of this invariant across files caused test failures in a
pending PR, but it is difficult to write a direct test for it. In the
future, we should probably change the LCNF checker to detect this.
This change also speeds up some compilation-heavy benchmarks much more
than I would've expected, which is a pleasant surprise. This indicates
we might get more speedups from reducing the amount of type information
we preserve in LCNF.
This PR fixes a panic in the delaborator for `Std.PRange`. It also
modifies the delaborators for both `Std.Range` and `Std.PRange` to not
use `let_expr`, which cleans up annotations and metadata, since
delaborators must follow the structures of expressions. It adds support
for `pp.notation` and `pp.explicit` options. It also adds tests for
these delaborators.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
This PR adds a guard for a delaborator that is causing panics in
doc-gen4. This is a band-aid solution for now, and @sgraf812 will take a
look when they're back from leave.
This PR ensures `grind cutsat` does not rely on div/mod terms to have
been normalized. The `grind` preprocessor has normalizers for them, but
sometimes they cannot be applied because of type dependencies.
Closes#9907
This PR addresses a missing check in the module system where private
names that remain in the public environment map for technical reasons
(e.g. inductive constructors generated by the kernel and relied on by
the code generator) accidentally were accessible in the public scope.
This PR reviews `grind` annotations for `Option`, preferring to use
`@[grind =]` instead of `@[grind]` (and fixing a few problems revealed
by this), and making sure `@[grind =]` theorems are "fully applied".
This PR lets the unused simp argument linter explain that the given hint
of removing `←` arguments may be too strong, and that replacing them
with `-` arguments can be needed. Fixes#9909.
This PR adds a JSON schema for `lakefile.toml`. Importantly, this schema
is *not* intended for validating `lakefile.toml`, but is instead
optimized for auto-completion and hovers using the [Even Better
TOML](https://marketplace.visualstudio.com/items?itemName=tamasfe.even-better-toml)
VS Code extension.
Once merged, I will attempt to contribute a link to this schema to the
[JSON Schema store](https://github.com/SchemaStore/schemastore). When
that is done, we can integrate the Lean 4 VS Code extension with Even
Better TOML, providing us with language server support in
`lakefile.toml`.
The schema contributed by this PR has the following known deficiencies:
- Superfluous properties do not produce an error.
- The structure of complicated structures (e.g. path or version
patterns) is deliberately not accurately reflected in the schema. Even
Better TOML doesn't seem to handle these structures well in
auto-completion.
- Due to the lack of an accurate declarative spec of the lakefile.toml
format and several deviations from the format to provide better
auto-completions, this schema will have to be kept in sync manually with
the code in Lake, at least for now.
This PR ensures that `Nat.cast` and `Int.cast` of numerals are
normalized by `grind`.
It also adds a `simp` flag for controlling how bitvector literals are
represented. By default, the bitvector simprocs use `BitVec.ofNat`. This
representation is problematic for the `grind ring` and `grind cutsat`
modules. The new flag allows the use of `OfNat.ofNat` and `Neg.neg` to
represent literals, consistent with how they are represented for other
commutative rings.
Closes#9321
This PR improves the heuristic used to select patterns for local
`forall` expressions occurring in the goal being solved by `grind`. It
now considers all singleton patterns in addition to the selected
multi-patterns. Example:
```lean
example (p : Nat → Prop) (h₁ : x < n) (h₂ : ¬ p x) : ∃ i, i < n ∧ ¬ p i := by
grind
```
This PR makes `mvcgen` aggressively eta-expand before trying to apply a
spec. This ensures that `mspec` will be able to frame hypotheses
involving uninstantiated loop invariants in goals for the inductive step
of a loop instead of losing them in a destructive world update.
This PR moves `List.range'_elim` to `List.eq_of_range'_eq_append_cons`
and adds a couple of `grind` annotations for `List.range'`. This will
make it more convenient to work with proof obligations produced by
`mvcgen`.
This PR is initially motivated by noticing `Lean.Grind.Preorder.toLE`
appearing in long Mathlib typeclass searches; this change will prevent
these searches. These changes are also helpful preparation for
potentially dropping the custom `Lean.Grind.*` typeclasses, and unifying
with the new typeclasses introduced in #9729.
This PR adds improved support for proof-by-reflection to the kernel type
checker. It addresses the performance issue exposed by #9854. With this
PR, whenever the kernel type-checks an argument of the form `eagerReduce
_`, it enters "eager-reduction" mode. In this mode, the kernel is more
eager to reduce terms. The new `eagerReduce _` hint is often used to
wrap `Eq.refl true`. The new hint should not negatively impact any
existing Lean package.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR adds new variants of `Array.getInternal` and
`Array.get!Internal` that return their argument borrowed, i.e. without a
reference count increment. These are intended for use by the compiler in
cases where it can determine that the array will continue to hold a
valid reference to the element for the returned value's lifetime.
In the future, this will likely be replaced by a return value borrow
annotation, in which case the special variant of the functions could be
removed, with the compiler inserting an extra `inc` in the non-borrow
cases.
This PR ensures `grind` can E-match patterns containing universe
polymorphic ground sub-patterns. For example, given
```
set_option pp.universes true in
attribute [grind?] Id.run_pure
```
the pattern
```
Id.run_pure.{u_1}: [@Id.run.{u_1} #1 (@pure.{u_1, u_1} `[Id.{u_1}] `[Applicative.toPure.{u_1, u_1}] _ #0)]
```
contains two nested universe polymorphic ground patterns
- `Id.{u_1}`
- `Applicative.toPure.{u_1, u_1}`
This kind of pattern is not common, but it occurs in core.
This PR removes the `inShareCommon` quick filter used in `grind`
preprocessing steps. `shareCommon` is no longer used only for fully
preprocessed terms.
closes#9830
This PR makes `mvcgen` produce deterministic case labels for the
generated VCs. Invariants will be named `inv<n>` and every other VC will
be named `vc<n>.*`, where the `*` part serves as a loose indication of
provenance.
This PR introduces a canonical way to endow a type with an order
structure. The basic operations (`LE`, `LT`, `Min`, `Max`, and in later
PRs `BEq`, `Ord`, ...) and any higher-level property (a preorder, a
partial order, a linear order etc.) are then put in relation to `LE` as
necessary. The PR provides `IsLinearOrder` instances for many core types
and updates the signatures of some lemmas.
**BREAKING CHANGES:**
* The requirements of the `lt_of_le_of_lt`/`le_trans` lemmas for
`Vector`, `List` and `Array` are simplified. They now require an
`IsLinearOrder` instance. The new requirements are logically equivalent
to the old ones, but the `IsLinearOrder` instance is not automatically
inferred from the smaller typeclasses.
* Hypotheses of type `Std.Total (¬ · < · : α → α → Prop)` are replaced
with the equivalent class `Std.Asymm (· < · : α → α → Prop)`. Breakage
should be limited because there is now an instance that derives the
latter from the former.
* In `Init.Data.List.MinMax`, multiple theorem signatures are modified,
replacing explicit parameters for antisymmetry, totality, `min_ex_or`
etc. with corresponding instance parameters.
This PR migrates the ⌜p⌝ notation for embedding pure p : Prop into SPred
σs to expand into a simple, first-order expression SPred.pure p that can
be supported by e-matching in grind.
Doing so deprives ⌜p⌝ notation of its idiom-bracket-like support for
#selector and ‹Nat›ₛ syntax which is thus removed.
This PR replaces some `HashSet Expr`-typed collections of facts in
`omega`'s implementation with plain lists. This change makes some
`omega` calls faster, some slower, but the advantage is that `omega`'s
performance is more independent the state of the name generator that
produces fvar IDs.
I've created this PR for discussion and am happy to hear opinions on
whether this should be merged or not. A good reason *not* to merge is
that it causes regressions in some places and `grind` is expected to
supersede `omega` either way. A good reason to merge is that `omega` is
used all over the place and its flaky performance increases the noise in
future benchmarks.
This PR fixes a bug in `mvcgen` triggered by excess state arguments to
the `wp` application, a situation which arises when working with
`StateT` primitives.
This PR improves the delta deriving handler, giving it the ability to
process definitions with binders, as well as the ability to recursively
unfold definitions. Furthermore, delta deriving now tries all explicit
non-out-param arguments to a class, and it can handle "mixin" instance
arguments. The `deriving` syntax has been changed to accept general
terms, which makes it possible to derive specific instances with for
example `deriving OfNat _ 1` or `deriving Module R`. The class is
allowed to be a pi type, to add additional hypotheses; here is a Mathlib
example:
```lean
def Sym (α : Type*) (n : ℕ) :=
{ s : Multiset α // Multiset.card s = n }
deriving [DecidableEq α] → DecidableEq _
```
This underscore stands for where `Sym α n` may be inserted, which is
necessary when `→` is used. The `deriving instance` command can refer to
scoped variables when delta deriving as well. Breaking change: the
derived instance's name uses the `instance` command's name generator,
and the new instance is added to the current namespace.
This closes
[mathlib4#380](https://github.com/leanprover-community/mathlib4/issues/380).
This PR reorganizes the directory structure of Lake's module test and
renames some of the files to be more descriptive.
Originally, this was meant to be combined with a fix, but that fix
appears to be incorrect, so this is just a refactor.
This PR fixes a bug where the `DecidableEq` deriving handler did not
take universe levels into account for enumerations (inductive types
whose constructors all have no fields). Closes#9541.
This PR adds a script for analyzing `grind` E-matching annotations. The
script is useful for detecting matching loops. We plan to add
user-facing commands for running the script in the future.
This PR allows trailing comma in the argument list of `simp?`, `dsimp?`,
`simpa`, etc... Previously, it was only allowed in the non `?` variants
of `simp`, `dsimp`, `simp_all`.
Closes#7383.
This PR improves the API for invariants and postconditions and as such
introduces a few breaking changes to the existing pre-release API around
`Std.Do`. It also adds Markus Himmel's `pairsSumToZero` example as a
test case.
This PR changes the IR RC pass to take "implied borrows" from
projections into account. If a projected value's lifetime is contained
in that of its parent (or any projection ancestor), then it does not
need its reference count incremented (or later decremented).
I believe that this same technique should generalize to both the
reset/reuse and borrow signature inference passes.
This PR splits out an implementation detail of
MVarId.getMVarDependencies into a top-level function. Aesop was relying
on the function defined in the where clause, which is no longer possible
after #9759.
This PR modifies the pretty printing of anonymous metavariables to use
the index rather than the internal name. This leads to smaller numerical
suffixes in `?m.123` since the indices are numbered within a given
metavariable context rather than across an entire file, hence each
command gets its own numbering. This does not yet affect pretty printing
of universe level metavariables.
For debugging purposes, metavariables that are not defined now pretty
print as `?_mvar.123` rather than cause pretty printing to fail.
This PR combines the simplification and unfold-reducible-constants steps
in `grind` to ensure that no potential normalization steps are missed.
Closes#9610
This PR fixes a bug in the projection over constructor propagator used
in `grind`. It may construct type incorrect terms when a equivalence
class contains heterogeneous equalities.
closes#9769
We compute the liveness information for the join point body, so the only
thing that updateJPLiveVarMap should be adding is the binding of the
params, which we can easily do ourselves.
If we supported recursive join points, I believe this would actually be
a correctness issue, but as-is it doesn't affect the output.
This PR fixes the documentation of the pipe operator |>, which is
currently (emphasis mine):
> Haskell-like pipe operator `|>`. `x |> f` means **the same as the same
as** `f x`,
> and it chains such that `x |> f |> g` is interpreted as `g (f x)`.
This PR implements the option `mvcgen +jp` to employ a slightly lossy VC
encoding for join points that prevents exponential VC blowup incurred by
naïve splitting on control flow.
```lean
def ifs_pure (n : Nat) : Id Nat := do
let mut x := 0
if n > 0 then x := x + 1 else x := x + 2
if n > 1 then x := x + 3 else x := x + 4
if n > 2 then x := x + 1 else x := x + 2
if n > 3 then x := x + 1 else x := x + 2
if n > 4 then x := x + 1 else x := x + 2
if n > 5 then x := x + 1 else x := x + 2
return x
theorem ifs_pure_triple : ⦃⌜True⌝⦄ ifs_pure n ⦃⇓ r => ⌜r > 0⌝⦄ := by
unfold ifs_pure
mvcgen +jp
/-
...
h✝⁵ : if n > 0 then x✝⁵ = 0 + 1 else x✝⁵ = 0 + 2
h✝⁴ : if n > 1 then x✝⁴ = x✝⁵ + 3 else x✝⁴ = x✝⁵ + 4
h✝³ : if n > 2 then x✝³ = x✝⁴ + 1 else x✝³ = x✝⁴ + 2
h✝² : if n > 3 then x✝² = x✝³ + 1 else x✝² = x✝³ + 2
h✝¹ : if n > 4 then x✝¹ = x✝² + 1 else x✝¹ = x✝² + 2
h✝ : if n > 5 then x✝ = x✝¹ + 1 else x✝ = x✝¹ + 2
⊢ x✝ > 0
-/
grind
```
This PR does what #9234 regrettably failed to do: actually reintroduce
the signatures of some `Subarray` functions that are now implemented via
slices (see #9017) in order to ensure backward compatibility and
consistency. With this PR, the old interface is restored. As an added
benefit, `Subarray.forIn` is no longer opaque.
This PR re-implements `IO.waitAny` using Lean instead of C++. This is to
reduce the size and
complexity of `task_manager` in order to ease future refactorings.
There is an import behavioral change of `IO.waitAny` in this PR.
Consider a situation where we have
two promises `p1`, `p2` and call `IO.waitAny [p1.result!, p2.result!]`
and `p1` resolves instantly.
Previously this would just return the result of `p1` and require nothing
else. With the new
implementation if `p2` is released before being resolved this can cause
a panic, even if
`IO.waitAny` has already finished. I argue that this is reasonable
behavior, given that an
invocation of `result!` promises that the promise will eventually be
resolved.
This PR moves the validation of cross-package `import all` to Lake and
the syntax validation of import keywords (`public`, `meta`, and `all`)
to the two import parsers.
It also fixes the error reporting of the fast import parser
(`Lean.parseImports`) and adds positions to its errors.
This PR addresses an outstanding feature in the module system to
automatically mark `let rec` and `where` helper declarations as private
unless they are defined in a public context such as under `@[expose]`.
This PR removes an error which implicitly assumes that the sort of type
dependency between erased types present in the test being added can not
occur. It would be difficult to refine the error using only the
information present in LCNF types, and it is of very little ongoing
value (I don't recall it ever finding an actual problem), so it makes
more sense to delete it.
Fixes#9692.
This PR changes the LCNF `elimDeadBranches` pass so that it considers
all non-`Nat` literal types to be `⊤`. It turns out that fixing this to
correctly handle all of these types with the current abstract value
representation is surprisingly nontrivial, and it's better to just land
the fix first.
This PR adds a version of `CommRing.Expr.toPoly` optimized for kernel
reduction. We use this function not only to implement `grind ring`, but
also to interface the ring module with `grind cutsat`.
This PR updates `release_repos.yml` to reflect that `import-graph` no
longer depends on `batteries`, and reorders the repositories to better
reflect dependencies.
This PR adds propagation rules for functions that take singleton types.
This feature is useful for discharging verification conditions produced
by `mvcgen`. For example:
```lean
example (h : (fun (_ : Unit) => x + 1) = (fun _ => 1 + y)) : x = y := by
grind
```
This removes the early call to `contradiction` from `simpH`, and
replaces it with a quick check if the pattern start with different
constructors.
We already call `simpH` quadratically often (unavoidable), so we want it
to be quick. Most common contradictions are found later on, so maybe we
don't want to the expensive `contradiction` tactic to be run early.
May help with #9598.
This PR adjusts the formatting type classes for `lake query` to no
longer require both a text and JSON form and instead work with any
combination of the two. The classes have also been renamed. In addition,
the query formatting of a text module header has been improved to only
produce valid headers.
This PR restricts Lake's production of thin archives to only the Windows
core build (i.e., `bootstrap = true`). The unbundled `ar` usually used
for core builds on macOS does not support `--thin`, so we avoid using it
unless necessary.
* Have asynchronous environment extensions specify whether they are
manipulate data for declarations from the "outside"/main branch (e.g.
attributes) or from the "inside"/async branch (e.g. data collected from
body elaboration) in order to avoid unnecessary waiting.
* Merge `findStateAsync?` into `getState` via a new, optional
`asyncDecl` parameter.
* Make `mayContainAsync` check an automatic part of `modifyState`.
This PR uses a more simple approach to proving the unfolding theorem for
a function defined by well-founded recursion. Instead of looping a bunch
of tactics, it uses simp in single-pass mode to (try to) exactly undo
the changes done in `WF.Fix`, using a dedicated theorem that pushes the
extra argument in for each matcher (or `casesOn`).
Improves performance for recursive functions with large `match`
statements, as in #9598.
This PR fixes a regression introduced by an optimization in the
`unfoldReducible` step used by the `grind` normalizer. It also ensures
that projection functions are not reduced, as they are folded in a later
step.
This PR adds build times to each build step of the build monitor (under
`-v` or in CI) and delays exiting on a `--no-build` until after the
build monitor finishes. Thus, a `--no-build` failure will now report
which targets blocked Lake by needing a rebuild.
This PR adds normalizers for nonstandard arithmetic instances. The types
`Nat` and `Int` have built-in support in `grind`, which uses the
standard instances for these types and assumes they are the ones in use.
However, users may define their own alternative instances that are
definitionally equal to the standard ones. This PR normalizes such
instances using simprocs. This situation actually occurs in Mathlib.
Example:
```lean
class Distrib (R : Type _) extends Mul R where
namespace Nat
instance instDistrib : Distrib Nat where
mul := (· * ·)
theorem odd_iff.extracted_1_4 {n : Nat} (m : Nat)
(hm : n =
@HMul.hMul _ _ _ (@instHMul Nat instDistrib.toMul)
2 m + 1) :
n % 2 = 1 := by
grind
end Nat
```
This PR adds support for `Fin.val` in `grind cutsat`. Examples:
```lean
example (a b : Fin 2) (n : Nat) : n = 1 → ↑(a + b) ≠ n → a ≠ 0 → b = 0 → False := by
grind
example (m n : Nat) (i : Fin (m + n)) (hi : m ≤ ↑i) : ↑i - m < n := by
grind
example {n : Nat} (m : Nat) (i : Fin n) ⦃j : Fin (n + m)⦄
(this : ↑i + m ≤ ↑j) : ↑j - m < n := by
grind
example {n : Nat} (i : Fin n) (j : Nat) (hj : j < ↑i) : j < n := by
grind
```
This PR ensures that `grind cutsat` processes `ToInt.toInt` applications
provided by the user. Example:
```lean
open Lean Grind
example (x : Fin 3) : ToInt.toInt x ≠ 0 → ToInt.toInt x ≠ 1 → ToInt.toInt x ≠ 2 → False := by
grind -ring
example (x y z : Fin 5) : ToInt.toInt (x + z) = ToInt.toInt y → z = 0 → x = y := by
grind -ring
```
This PR fixes support for `SMul.smul` in `grind ring`. `SMul.smul`
applications are now normalized. Example:
```lean
example (x : BitVec 2) : x - 2 • x + x = 0 := by
grind
```
This PR add constructors `.intCast k` and `.natCast k` to
`CommRing.Expr`. We need them because terms such as `Nat.cast (R := α)
1` and `(1 : α)` are not definitionally equal. This is pervaise in
Mathlib for the numerals `0` and `1`.
```lean
import Mathlib
example {α : Type} [AddMonoidWithOne α] : Nat.cast (R := α) 0 = (0 : α) := rfl -- not defeq
example {α : Type} [AddMonoidWithOne α] : Nat.cast (R := α) 1 = (1 : α) := rfl -- not defeq
example {α : Type} [AddMonoidWithOne α] : Nat.cast (R := α) 2 = (2 : α) := rfl -- defeq from here
-- Similarly for everything past `AddMonoidWithOne` in the Mathlib hierarchy, e.g. `Ring`.
```
This PR adjusts the import graph, primarily of `Lean`, such that the
worst case rebuild time of core (`lean` only) is below 3 minutes on the
speedcenter machine (not captured by benchmark yet).
This PR performs some micro optimizations on fuzzy matching for a `~20%`
instructions win.
The three key changes are:
- try to remove some unnecessary allocations of things such as tuples
- change `containsInOrderLower` to use the efficient `get'` and `next'`
primitives. I hope that we can replace these with iterators on strings
in the second half of this quarter
- Do the same thing as clangd and use `Int16` with the `minValue` being
used for "worst score" while this does have the potential to
over/underflow, if the user is working with a score in the 10000s
something weird is certainly going on already (the score usually seems
to be in the 2 digit area based on some).
As an additional bonus, once we finally have unboxed arrays we will get
some additional cache wins on the 16 bit arrays!
This PR introduces checks to make sure that the IO functions produce
errors when inputs contain NUL bytes (instead of ignoring everything
after the first NUL byte).
This PR continues #9644 , fixing the core build when using an older
system libuv.
This only affected users building Lean from scratch, since the lean
binaries we ship as part of toolchains statically link their own copy of
libuv 1.50+.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This PR changes `lake setup-file` to use the server-provided header for
workspace modules.
This also reverts #9163 as the underlying issue is now fixed.
This PR modifies dot identifier notation so that `(.a : T)` resolves
`T.a` with respect to the root namespace, like for generalized field
notation. This lets the notation refer to private names, follow aliases,
and also use open namespaces. The LSP completions are improved to follow
how dot ident notation is resolved, but it doesn't yet take into account
aliases or open namespaces.
Closes#9629
This PR adds error explanations for two common errors caused by large
elimination from `Prop`. To support this functionality, "nested" named
errors thrown by sub-tactics are now able to display their error code
and explanation.
This PR fixes the core build when using an older system libuv.
This only affected users building Lean from scratch, since the `lean`
binaries we ship as part of toolchains statically link their own copy of
libuv 1.50+.
This PR introduces a `mutual_induct` variant of the generated
(co)induction proof principle for mutually defined (co)inductive
predicates. Unlike the standard (co)induction principle (which projects
conclusions separately for each predicate), `mutual_induct` produces a
conjunction of all conclusions.
## Example
Given the following mutual definition:
```lean4
mutual
def f : Prop := g
coinductive_fixpoint
def g : Prop := f
coinductive_fixpoint
end
```
Standard coinduction principles:
```lean4
f.coind : ∀ (pred_1 pred_2 : Prop), (pred_1 → pred_2) → (pred_2 → pred_1) → pred_1 → f
g.coind : ∀ (pred_1 pred_2 : Prop), (pred_1 → pred_2) → (pred_2 → pred_1) → pred_2 → g
```
New `mutual_induct`principle:
```lean4
f.mutual_induct: ∀ (pred_1 pred_2 : Prop), (pred_1 → pred_2) → (pred_2 → pred_1) → (pred_1 → f) ∧ (pred_2 → g)
```
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR adds support for generating lattice-theoretic (co)induction
proof principles for predicates defined via `mutual` blocks using
`inductive_fixpoint`/`coinductive_fixpoint` constructs.
### Key Changes
- The order on product lattices (used to define fixpoints of mutual
blocks) is unfolded.
- Hypotheses in generated principles are curried.
- Conclusions are projected to focus only on the predicate of interest
(rather than being a conjunction of conclusions for all functions
defined in the `mutual` block.
### Example
Given:
```lean4
mutual
def f : Prop :=
g
coinductive_fixpoint
def g : Prop :=
f
coinductive_fixpoint
end
```
The system now generates these coinduction principles:
```lean4
f.coinduct (pred_1 pred_2 : Prop) (hyp_1 : pred_1 → pred_2) (hyp_2 : pred_2 → pred_1) : pred_1 → f
```
and
```lean4
g.coinduct (pred_1 pred_2 : Prop) (hyp_1 : pred_1 → pred_2) (hyp_2 : pred_2 → pred_1) : pred_2 → g
```
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR adds the separate directions of
`List.pairwise_iff_forall_sublist` as named lemmas.
I want to explore how they could/should be used by `grind` in Mathlib.
This PR brings the Mac OSX build instructions up to date slightly. (They
currently refer to facts "...as of November 2014...")
- Remove specific OS version number from the title as it is out of date
with respect to filename.
- Nonetheless don't change filename for the sake of not breaking
incoming links.
- Update C++ language version to C++14, which I believe is what is
currently required, based on other platform documentation.
- Bump versions of C++ compilers that seem to be current. I expect the
exact values of these version numbers aren't crucial but maybe good for
the reader calibrating a vague sense of whether their compiler is in the
right ballpark.
- Add `lld` to the homebrew clang instructions, because homebrew changed
the way they package llvm tools, spinning the linker off into its own
package.
This PR updates the styling and wording of error messages produced in
inductive type declarations and anonymous constructor notation,
including hints for inferable constructor visibility updates.
This PR optimizes `Lean.Name.toString`, giving a 10% instruction
benefit.
Crucially this is a breaking change as the old `Lean.Name.toString`
method used to support a method for identifying tokens. This method is
now available as `Lean.Name.toStringWithToken` in order to allow for
specialization of the (highly common) `toString` code path which sets
this function to just return `false`.
This PR simplifies the docstring for `propext` significantly.
The old docstring explained general concepts of axioms that are now
covered in the reference manual, and had a large example that was out of
date and has been subsumed by reference manual content.
This PR adds `@[grind =]` to `Prod.lex_def`. Note that `omega` has
special handling for `Prod.Lex`, and this is needed for `grind`'s cutsat
module to achieve parity.
The `isUnderBinder` check is intended to avoid inlining repeated
computations into specializations, but this doesn’t apply to local
function decls whose bodies are already delayed.
This PR adds lemmas about `UIntX.toBitVec` and `UIntX.ofBitVec` and `^`.
These match the existing lemas for `*`.
After #7887 these can be made true by `rfl`.
This PR ensures `ite` and `dite` are to selected as E-matching patterns.
They are bad patterns because the then/else branches are only
internalized after `grind` decided whether the condition is
`True`/`False`.
The issue reported by #9572 has been fixed, but the fix exposed another
issue. The patterns for `List.Pairwise` produce an unbounded number of
E-matching instances.
```lean
example (l : List α) : l.Pairwise R := by
grind
```
This PR fixes an issue in `grind`'s disequality proof construction. The
issue occurs when an equality is merged with the `False` equivalence
class, but it is not the root of its congruence class, and its
congruence root has not yet been merged into the `False` equivalence
class yet.
closes#9562
This PR optimizes the proof terms generated by `grind ring`. For
example, before this PR, the kernel took 2.22 seconds (on a M4 Max) to
type-check the proof in the benchmark `grind_ring_5.lean`; it now takes
only 0.63 seconds.
This PR generalizes `Process.output` and `Process.run` with an optional
`String` argument that can be piped to `stdin`.
To date we have been using shims `Process.runCmdWithInput` in Batteries.
This PR fixes a bug introduced in #7830 where if the cursor is at the
indicated position
```lean
example (as bs : List Nat) : (as.append bs).length = as.length + bs.length := by
induction as with
| nil => -- cursor
| cons b bs ih =>
```
then the Infoview would show "no goals" rather than the `nil` goal. The
PR also fixes a separate bug where placing the cursor on the next line
after the `induction`/`cases` tactics like in
```lean
induction as with
| nil => sorry
| cons b bs ih => sorry
I -- < cursor
```
would report the original goal in the goal list. Furthermore, there are
numerous improvements to error recovery (including `allGoals`-type logic
for pre-tactics) and the visible tactic states when there are errors.
Adds `Tactic.throwOrLogErrorAt`/`Tactic.throwOrLogError` for throwing or
logging errors depending on the recovery state.
This PR restores the feature where in `induction`/`cases` for `Nat`, the
`zero` and `succ` labels are hoverable. This was added in #1660, but
broken in #3629 and #3655 when custom eliminators were added. In
general, if a custom eliminator `T.elim` for an inductive type `T` has
an alternative `foo`, and `T.foo` is a constant, then the `foo` label
will have `T.foo` hover information.
This PR consolidates common attribute-related error messages into
reusable functions and updates the wording and formatting of relevant
error messages.
This extends the specialization behavior of functions taking instance
implicits to ordinary implicit arguments that are of instance type. The
choice between the two is often made for subtle inference-related
reasons. It also affects visibility of these functions, because the
module system makes template-like decls visible to the compiler in other
modules.
This PR makes the second instance of the `inferVisibility` pass run
after the `saveMono` pass. As the comment above the first instance of
the pass indicates, this needs to be after `saveMono` in order to see
all decls with their updated bodies.
This PR upstreams some helper instances for `NameSet` from Batteries.
(These could be generalized to an arbitrary TreeSet, but I'll leave that
for someone else.)
This PR changes `Lean.Grind.NoNatZeroDivisors` so that it is
parametrised by a `NatModule` instance rather than just a `HMul`
instance. This is sufficiently general for our purposes, and is a
band-aid (~40% improvement) for the performance problems we've been
seeing coming from inference here. The problems observed in Mathlib may
not see much improvement, however.
This PR lets the equation compiler unfold abstracted proofs again if
they would otherwise hide recursive calls.
This fixes#8939.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR fixes Lake's handling of a module system `import all`.
Previously, Lake treated `import all` the same a non-module `import`,
importing all private data in the transitive import tree. Lake now
distinguishes the two, with `import all M` just importing the private
data of `M`. The direct private imports of `M` are followed, but they
are not promoted.
This also fixes some other Lake bugs with module system imports that
were discovered in the process.
In the early days of the new compiler, it was common to make tests that
manually compiled a definition with the new compiler. The arity
reduction pass in LCNF deliberately does not compute a fixed point to
find a minimal set of used parameters for performance reasons, but
running it a second time can lead to different decisions being made and
a decl arity mismatch. This has been an issue for multiple people during
development. Removing the tests fixes the problem.
Fixes#9186.
This PR uses `withAbstractAtoms` to prevent the kernel from accidentally
reducing the atoms in the arith normlizer while typechecking. This PR
also sets `implicitDefEqProofs := false` in the `grind` normalizer
This PR corrects the changes to `Lean.Grind.Field` made in #9500.
(The lack of examples of fields in the core repository is a problem! I
guess it is likely that for interval arithmetic we will at least need
`Rat` soon.)
(Almost) only typos in constant names and doc-strings were considered;
grammar was not considered. Also, along others,
`mkDefinitionValInferrringUnsafe` has been fixed :-)
This PR adds a benchmark for the persistent hashmap, in particular also
covering the non
linear insert case which is often hit in practical uses. Furthermore the
same test case is also
added to the treemap benchmark.
This PR makes `mframe`, `mspec` and `mvcgen` respect hygiene.
Inaccessible stateful hypotheses can now be named with a new tactic
`mrename_i` that works analogously to `rename_i`.
This PR surfaces kernel diagnostics even in `example`.
The problem was that the kernel checking happens asynchronously. We
cannot use `reportDiag` in `addDecl`, which spawns that task, due to the
module hierarchy. For non `example`-declaration, `reportDiag` is called
somewhere else later, but for `example`, the `withoutModifyingEnv` in
`elabMutualDef` hid the kernel diagnostics. (But only the kernel
diagnostics; they are in the `Environment`, while the others are in the
`State`).
I also observed that the `reportDiag` in `elabAsync` (but not in
`elabSync`) duplicated the reporting, so without `elab.Async true` you
get the message twice. To fix this, `reportDiag` now resets the
diagnostics. This should avoid reporting counts twice in general (at
least within a linear use of the state).
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR removes vestigial syntax definitions in
`Lean.Elab.Tactic.Do.VCGen` that when imported undefine the `mvcgen`
tactic. Now it should be possible to import Mathlib and still use
`mvcgen`.
This PR adds a few more `*.by_wp` "adequacy theorems" that allows to
prove facts about programs in `ReaderM` and `ExceptM` using the `Std.Do`
framework.
This PR adds a `HPow \a Int \a` field to `Lean.Grind.Field`, and
sufficient axioms to connect it to the operations, so that in future we
can reason about exponents in `grind`. To avoid collisions, we also move
the `HPow \a Nat \a` field in `Semiring` from the extends clause to a
field. Finally, we add some failing tests about normalizing exponents.
This PR makes cdot function expansion take hygiene information into
account, fixing "parenthesis capturing" errors that can make erroneous
cdots trigger cdot expansion in conjunction with macros. For example,
given
```lean
macro "baz% " t:term : term => `(1 + ($t))
```
it used to be that `baz% ·` would expand to `1 + fun x => x`, but now
the parentheses in `($t)` do not capture the cdot. We also fix an
oversight where cdot function expansion ignored the fact that type
ascriptions and tuples were supposed to delimit expansion, and also now
the quotation prechecker ignores the identifier in `hygieneInfo`. (#9491
added the hygiene information to the parenthesis and cdot syntaxes.)
This fixes a bug discovered by [Google
DeepMind](https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P1/index.html),
which made use of `useλy . x=>y.rec λS p=>?_`. The `use` tactic from
Mathlib wrapped the provided term in a type ascription, and so this was
equivalent to `use fun x => λy x x=>y.rec λS p=>?_`. (Note that cdot
function expansion is not able to take into account *where* the cdots
are located, and it is syntactically valid to insert an identifier into
the binder list like this. If we ever want to address this in the
future, we could have cdots expand into a special term that wraps an
identifier that evaluates to a local, but which would cause errors in
other contexts.)
Design note: we put the `hygieneInfo` on the open parenthesis rather
than at the end, since that way the hygiene information is available
even when there are parsing errors. This is important since we rely on
being able to elaborate partial syntax to get elab info (e.g. in `(a.`
to get completion info). Note that syntax matchers check that the
`hygieneInfo` is actually present, so such partial syntax would not be
matched.
This PR adds a feature where `structure` constructors can override the
inferred binder kinds of the type's parameters. In the following, the
`(p)` binder on `toLp` causes `p` to be an explicit parameter to
`WithLp.toLp`:
```lean
structure WithLp (p : Nat) (V : Type) where toLp (p) ::
ofLp : V
```
This reflects the syntax of the feature added in #7742 for overriding
binder kinds of structure projections. Similarly, only those parameters
in the header of the `structure` may be updated; it is an error to try
to update binder kinds of parameters included via `variable`.
Closes#9072.
Fixes a possible bug from stale caches when creating the type of the
constructor.
This PR resolves an issue where the `Meta.Context.configKey` field is
private but we still want to use the constructor of the structure for
setting other fields, which would be prevented by the module system
checks:
```lean
structure Context where
private config : Config := {}
private configKey : UInt64 := config.toKey
...
def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
-- cannot call private constructor of `Meta.Context`!
(·.1) <$> info.runCoreM (x.run { lctx := lctx } { mctx := info.mctx })
```
Instead, the private field is extracted into an (existing) structure
that applies its default value:
```lean
/-- Configuration with key produced by `Config.toKey`. -/
structure ConfigWithKey where
private mk ::
config : Config := {}
key : UInt64 := config.toKey
structure Context where
keyedConfig : ConfigWithKey := default
```
Thus `Context`'s constructor remains public without exposing a way to
set `key` directly.
This PR fixes a kernel type mismatch that occurs when using `grind` on
goals containing non-standard `OfNat.ofNat` terms. For example, in issue
#9477, the `0` in the theorem `range_lower` has the form:
```lean
(@OfNat.ofNat
(Std.PRange.Bound (Std.PRange.RangeShape.lower (Std.PRange.RangeShape.mk Std.PRange.BoundShape.closed Std.PRange.BoundShape.open)) Nat)
(nat_lit 0)
(instOfNatNat (nat_lit 0)))
```
instead of the more standard form:
```lean
(@OfNat.ofNat
Nat
(nat_lit 0)
(instOfNatNat (nat_lit 0)))
```
Closes#9477
This PR improves the `evalInt?` function, which is used to evaluate
configuration parameters from the `ToInt` type class. This PR also adds
a new `evalNat?` function for handling the `IsCharP` type class, and
introduces a configuration option:
```
grind (exp := <num>)
```
This option controls the maximum exponent size considered during
expression evaluation. Previously, `evalInt?` used `whnf`, which could
run out of stack space when reducing terms such as `2^1024`.
closes#9427
This PR adds `binrel%` macros for `!=` and `≠` notation defined in
`Init.Core`. This allows the elaborator to insert coercions on both
sides of the relation, instead of committing to the type on the left
hand side.
I first discovered this bug while working on Brouwer's fixed point
theorem. See the discussion on Zulip at [#lean4 > Elaboration of
`≠` @
💬](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elaboration.20of.20.60.E2.89.A0.60/near/526236907).
This PR replaces the proof of the simplification lemma `Nat.zero_mod`
with
`rfl` since it is, by design, a definitional equality. This solves an
issue
whereby the lemma could not be used by the simplifier when in 'dsimp'
mode.
Closes#9389
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR introduces tactic `mleave` that leaves the `SPred` proof mode by
eta expanding through its abstractions and applying some mild
simplifications. This is useful to apply automation such as `grind`
afterwards.
Relates to #9363.
This PR adds support in the `mintro` tactic for introducing `let`/`have`
binders in stateful targets, akin to `intro`. This is useful when
specifications introduce such let bindings.
Closes#9365.
This PR makes `PProdN.reduceProjs` also look for projection functions.
Previously, all redexes were created by the functions in `PProdN`, which
used primitive projections. But with `mkAdmProj` the projection
functions creep in via the types of the `admissible_pprod_fst` theorem.
So let's just reduce both of them.
Fixes#9462.
The `isRef` check being removed here used to be an optimization, because
this structure only tracked whether ref counting operations need to be
inserted at all. Now the structure also tracks whether the value needs
to be checked for being a scalar or not, which is something that can be
refined by a `cases` arm, since inductive types can have a mix of scalar
and non-scalar constructors.
This PR fixes an issue that caused some `deriving` handlers to fail when
the name of the type being declared matched that of a declaration in an
open namespace.
Closes#9366
This PR improves the 'Go to Definition' UX, specifically:
- Using 'Go to Definition' on a type class projection will now extract
the specific instances that were involved and provide them as locations
to jump to. For example, using 'Go to Definition' on the `toString` of
`toString 0` will yield results for `ToString.toString` and `ToString
Nat`.
- Using 'Go to Definition' on a macro that produces syntax with type
class projections will now also extract the specific instances that were
involved and provide them as locations to jump to. For example, using
'Go to Definition' on the `+` of `1 + 1` will yield results for
`HAdd.hAdd`, `HAdd α α α` and `Add Nat`.
- Using 'Go to Declaration' will now provide all the results of 'Go to
Definition' in addition to the elaborator and the parser that were
involved. For example, using 'Go to Declaration' on the `+` of `1 + 1`
will yield results for `HAdd.hAdd`, `HAdd α α α`, `Add Nat`,
``macro_rules | `($x + $y) => ...`` and `infixl:65 " + " => HAdd.hAdd`.
- Using 'Go to Type Definition' on a value with a type that contains
multiple constants will now provide 'Go to Definition' results for each
constant. For example, using 'Go to Type Definition' on `x` for `x :
Array Nat` will yield results for `Array` and `Nat`.
### Details
'Go to Definition' for type class projections was first implemented by
#1767, but there were still a couple of shortcomings with the
implementation. E.g. in order to jump to the instance in `toString 0`,
one had to add another space within the application and then use 'Go to
Definition' on that, or macros would block instances from being
displayed. Then, when the .ilean format was added, most 'Go to
Definition' requests were already handled using the .ileans in the
watchdog process, and so the file worker never received them to handle
them with the semantic information that it has available.
This PR resolves most of the issues with the previous implementation and
refactors the 'Go to Definition' control flow so that 'Go to Definition'
requests are always handled by the file worker, with the watchdog merely
using its .ilean position information to update the positions in the
response to a more up-to-date state. This is necessary because the file
worker obtains its position information from the .oleans, which need to
be rebuilt in order to be up-to-date, while the watchdog always receives
.ilean update notifications from each active file worker with the
current position information in the editor.
Finally, all of the 'Go to Definition' code is refactored to be easier
to maintain.
### Breaking changes
`InfoTree.hoverableInfoAt?` has been generalized to
`InfoTree.hoverableInfoAtM?` and now takes a general `filter` argument
instead of several boolean flags, as was the case before.
This PR removes uses of `Lean.RBMap` in Lean itself.
Furthermore some massaging of the import graph is done in order to avoid
having `Std.Data.TreeMap.AdditionalOperations` (which is quite
expensive) be the critical path for a large chunk of Lean. In particular
we can build `Lean.Meta.Simp` and `Lean.Meta.Grind` without it thanks to
these changes.
We did previously not conduct this change as `Std.TreeMap` was not
outperforming `Lean.RBMap` yet, however this has changed with the new
code generator.
This PR addresses the lean crash (stack overflow) with nested induction
and the generation of the `SizeOf` spec lemmas, reported at #9018.
It does not address the underlying issue that in these cases, the
generated SizeOf code does not match the the SizeOf function found by
instance search, and thus the generation fails.
This seem hard to fix: `mkSizeOfMinors` would have to recognize that
given, say, `List (Id Tree)`, the derived instance (assuming there was
one for `Tree`) is not the same as for `List Tree`.
The problem seems just about as hard as getting derived SizeOf right in
the presence of nested induction and non-canonical SizeOf instances.
This PR fixes the behavior of `String.prev`, aligning the runtime
implementation with the reference implementation. In particular, the
following statements hold now:
- `(s.prev p).byteIdx` is at least `p.byteIdx - 4` and at most
`p.byteIdx - 1`
- `s.prev 0 = 0`
- `s.prev` is monotone
Closes#9439
This PR adds the number of jobs run to the final message Lake produces
on a successfully run of `lake build`.
**Examples**
```
Build completed successfully (1 job).
Build completed successfully (6 jobs).
```
This PR adds the `libPrefixOnWindows` package and library configuration
option. When enabled, Lake will prefix static and shared libraries with
`lib` on Windows (i.e., the same way it does on Unix).
This PR changes the Lake local cache infrastructure to restore
executables and shared and static libraries from the cache. This means
they keep their expected names, which some use cases still rely on.
This PR adds a hint to the "invalid projection" message suggesting the
correct nested projection for expressions of the form `t.n` where `t` is
a tuple and `n > 2`.
This feature was originally proposed by @nomeata in #8986.
This PR improves the error messages produced by the `split` tactic,
including suggesting syntax fixes and related tactics with which it
might be confused.
Note that, to avoid clashing with the new error message styling
conventions used in these messages, this PR also updates the formatting
of the message produced by `throwTacticEx`.
Closes#6224
This PR changes `IRType.boxed` to map `erased` to `tobject` rather than
`object`, since `erased` has a representation of a boxed scalar 0 when
we are forced to represent it at runtime. This case does not occur at
all in the Lean codebase.
This PR updates the formatting of, and adds explanations for, "unknown
identifier" errors as well as "failed to infer type" errors for binders
and definitions.
It attempts to ameliorate some of the confusion encountered in #1592 by
modifying the wording of the "header is elaborated before body is
processed" note and adding further discussion and examples of this
behavior in the corresponding error explanation.
An earlier PR (#9017) replaced certain subarray functions such as
`Subarray.foldl` with generic slice functions `Slice.foldl`. For
backward compatibility reasons, This PR reintroduces `Subarray.foldl`
etc. as aliases for the `Slice` versions.
This PR adds Lake tests for builds involving the Lean module system and
fixes some bugs encountered in the process. In particular, it fixes the
parsing of private imports and how Lake handles the `import all` of a
private import.
This PR fixes some issues with the Lake tests on Windows and macOS. It
also avoids downloading Mathlib in the `init` test, which was currently
doing this after changes to the `math-lax` template in #8866.
To skip the Mathlib download in `init`, an undocumented `--offline`
option was added`. This option is currently meant for internal use only.
This PR increases the number of cases where `isArrowProposition` returns
a result other than `.undef`. This function is used to implement the
`isProof` predicate, which is invoked on every subterm visited by
`simp`.
This PR adds improves the "invalid named argument" error message in
function applications and match patterns by providing clickable hints
with valid argument names. In so doing, it also fixes an issue where
this error message would erroneously flag valid match-pattern argument
names.
This PR adds support for compilation of `casesOn` for subsingletons. We
rely on the elaborator's type checking to restrict this to inductives in
`Prop` that can actually eliminate into `Type n`. This does not yet
cover other recursors of these types (or of inductives not in `Prop` for
that matter).
This PR implements a simple optimization: dependent implications are no
longer treated as E-matching theorems in `grind`. In
`grind_bitvec2.lean`, this change saves around 3 seconds, as many
dependent implications are generated. Example:
```lean
∀ (h : i + 1 ≤ w), x.abs.getLsbD i = x.abs[i]
```
This PR adds a benchmark to our suite, specifically targeting the fact
that local hypotheses
are currently not indexed in simp and can thus cause significant
slowdowns compared to having them
as external declarations.
This PR splits up `Module.recBuildLean` into smaller functions and
optimizes the implementation of `Module.cacheOutputArtifacts` for the
new compiler. Now, all functions within `Lake.Build.Module` take Lean
<1s to compile.
This PR updates Lake to resolve the `.olean` files for transitive
imports for Lean through the `modules` field of `lean --setup`. This
enables means the Lean can now directly use the `.olean` files from the
Lake cache without needed to locate them at a specific hierarchical
path.
Resolving transitive imports still has a performance penalty, but it is
now much less.
This is mostly a refactoring that replaces other analyses with type
information, but due to the introduction of `tagged` it also has the
side effect of eliminating ref counting ops entirely for types that
always have a tagged scalar representation, e.g. `Unit`.
This PR fixes a bug at `mkCongrSimpCore?`. It fixes the issue reported
by @joehendrix at #9388.
The fix is just commit: afc4ba617f. The
rest of the PR is just cleaning up the file.
closes#9388
This PR fixes an unsafe trick where a sentinel for a hash table of Exprs
(keyed by pointer) is created by constructing a value whose runtime
representation can never be a valid Expr. The value chosen for this
purpose was Unit.unit, which violates the inference that Expr has no
scalar constructors. Instead, we change this to a freshly allocated Unit
× Unit value.
A micro-benchmark for plain, mostly first-order rewriting of simp:
This uses axiom to make it independent of specific optimization (e.g.
for `Nat`).
It generates a “list” of 128 `b`s followed by 128 `a` and uses
bubble-sort to to sort it and compares it against the expected output.
This PR changes the dependency cloning mechanism in lake so the log
message that lake is cloning a
dependency occurs before it is finished doing so (and instead before it
starts). This has been a
huge source of confusion for users that don't understand why lake seems
to be just stuck for no
reason when setting up a new project, the output now is:
```
λ lake +lean4 new math math
info: downloading mathlib `lean-toolchain` file
info: math: no previous manifest, creating one from scratch
info: leanprover-community/mathlib: cloning https://github.com/leanprover-community/mathlib4
<hang>
info: leanprover-community/mathlib: checking out revision 'cd11c28c6a0d514a41dd7be9a862a9c8815f8599'
```
This PR fixes a performance issue that occurs when generating equation
lemmas for functions that use match-expressions containing several
literals. This issue was exposed by #9322 and arises from a combination
of factors:
1. Literal values are compiled into a chain of dependent if-then-else
expressions.
2. Dependent if-then-else expressions are significantly more expensive
to simplify than regular ones.
3. The `split` tactic selects a target, splits it, and then invokes
`simp` on the resulting subgoals. Moreover, `simp` traverses the entire
goal bottom-up and does not stop after reaching the target.
This PR addresses the issue by introducing a custom simproc that avoids
recursively simplifying nested if-then-else expressions. It does **not**
alter the user-facing behavior of the `split` tactic because such a
change would be highly disruptive. Instead, the PR adds a new flag,
`backward.split` to control the behavior of the user-facing `split`
tactic. It is currently set to `true`, i.e., the old behavior is still
the default one. In a future PR, we should set this flag to `false` by
default and begin repairing all affected proofs.
closes#9322
This PR modifies the encoding from `Nat` to `Int` used in `grind
cutsat`. It is simpler, more extensible, and similar to the generic
`ToInt`. After update stage0, we will be able to delete the leftovers.
This PR correctly populates the `xType` field of the `IR.FnBody.case`
constructor. It turns out that there is no obvious consequence for this
being incorrect, because it is conservatively recomputed by the `Boxing`
pass.
This PR changes the implementation of `trace.Compiler.result` to use the
decls as they are provided rather than looking them up in the LCNF mono
environment extension, which was seemingly done to save the trouble of
re-normalizing fvar IDs before printing the decl. This means that the
`._closed` decls created by the `extractClosed` pass will now be
included in the output, which was definitely confusing before if you
didn't know what was happening.
This currently relies on the encoding pun of Nat.zero as the first
tagged constructor of Nat. Since Nat.succ is lowered to addition, it
makes sense to also lower Nat.zero to a zero literal. This might also
expose more optimization opportunities in the future.
This PR fixes IR constructor argument lowering to correctly handle an
irrelevant argument being passed for a relevant parameter in all cases.
This happened because constructor argument lowering (incompletely)
reimplemented general LCNF-to-IR argument lowering, and the fix is to
just adopt the generic helper functions. This is probably due to an
incomplete refactoring when the new compiler was still on a branch.
This PR uses the `mkCongrSimpForConst?` API in `simp` to reduce the
number of times the same congruence lemma is generated. Before this PR,
`grind` would spend `1.5`s creating congruence theorems during
normalization in the `grind_bitvec2.lean` benchmark. It now spends
`0.6`s. This PR should make an even bigger difference after we merge
#9300.
This PR removes the unnecessary requirement of `BEq α` for
`Array.any_push`, `Array.any_push'`, `Array.all_push`, `Array.all_push'`
as well as `Vector.any_push` and `Vector.all_push`.
This PR replaces the `reduceCtorEq` simproc used in `grind` by a much
more efficient one. The default one use in `simp` is just overhead
because the `grind` normalizer is already normalizing arithmetic.
In a separate PR, we will push performance improvements to the default
`reduceCtorEq`.
This PR fixes `toISO8601String` to produce a string that conforms to the
ISO 8601 format specification. The previous implementation separated the
minutes and seconds fragments with a `.` instead of a `:` and included
timezone offsets without the hour and minute fragments separated by a
`:`.
Closes#9235
This PR moves the implementation of `lean_add_extern`/`addExtern` from
C++ into Lean. I believe is the last C++ helper function from the
library/compiler directory being relied upon by the new compiler. I put
it into its own file and duplicated some code because this function
needs to execute in CoreM, whereas the other IR functions live in their
own monad stack. After the C++ compiler is removed, we can move the IR
functions into CoreM.
This PR optimizes support for `Decidable` instances in `grind`. Because
`Decidable` is a subsingleton, the canonicalizer no longer wastes time
normalizing such instances, a significant performance bottleneck in
benchmarks like `grind_bitvec2.lean`. In addition, the
congruence-closure module now handles `Decidable` instances, and can
solve examples such as:
```lean
example (p q : Prop) (h₁ : Decidable p) (h₂ : Decidable (p ∧ q)) : (p ↔ q) → h₁ ≍ h₂ := by
grind
```
This PR adds support for `.mdata` in LCNF mono types (and then drops it
at the IR type level instead). This better matches the behavior of
extern decls in the C++ code of the old compiler, which is still being
used to create extern decls at the moment and will soon be replaced.
This is covered by existing tests.
This PR fixes the bug that `collectAxioms` didn't collect axioms
referenced by other axioms. One of the results of this bug is that
axioms collected from a theorem proved by `native_decide` may not
include `Lean.trustCompiler`.
Closes#8840.
This PR demotes the builtin elaborators for `Std.Do.PostCond.total` and
`Std.Do.Triple` into macros, following the DefEq improvements of #9015.
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR makes `isDefEq` detect more stuck definitional equalities
involving smart unfoldings. Specifically, if `t =?= defn ?m` and `defn`
matches on its argument, then this equality is stuck on `?m`. Prior to
this change, we would not see this dependency and simply return `false`.
Fixes#8766.
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
This PR improves the `congr` tactic so that it can handle function
applications with fewer arguments than the arity of the head function.
This also fixes a bug where `congr` could not make progress with
`Set`-valued functions in Mathlib, since `Set` was being unfolded and
making such functions have an apparently higher arity.
This addresses issue #2128 for the `congr` tactic, but not `simp` and
others.
This PR adds theorem `BitVec.clzAuxRec_eq_clzAuxRec_of_getLsbD_false` as
a more general statement than `BitVec.clzAuxRec_eq_clzAuxRec_of_le`,
replacing the latter in the bitblaster too.
This PR makes the logic and tactics of `Std.Do` universe polymorphic, at
the cost of a few definitional properties arising from the switch from
`Prop` to `ULift Prop` in the base case `SPred []`.
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR migrates usages of `Std.Range` to the new polymorphic ranges.
This PR unfortunately increases the transitive imports for
frequently-used parts of `Init` because the ranges now rely on iterators
in order to provide their functionality for types other than `Nat`.
However, iteration over ranges in compiled code is as efficient as
before in the examples I checked. This is because of a special
`IteratorLoop` implementation provided in the PR for this purpose.
There were two issues that were uncovered during migration:
* In `IndPredBelow.lean`, migrating the last remaining range causes
`compilerTest1.lean` to break. I have minimized the issue and came to
the conclusion it's a compiler bug. Therefore, I have not replaced said
old range usage yet (see #9186).
* In `BRecOn.lean`, we are publicly importing the ranges. Making this
import private should theoretically work, but there seems to be a
problem with the module system, causing the build to panic later in
`Init.Data.Grind.Poly` (see #9185).
* In `FuzzyMatching.lean`, inlining fails with the new ranges, which
would have led to significant slowdown. Therefore, I have not migrated
this file either.
This PR adds a benchmark for the rewriting engine of bv_decide, based on
a problem extracted from
SMT-LIB. Note that this problem has significant elaboration time itself
due to its sheer size though
the overall execution time is split approximately 50:50 between
elaboration and rewriting.
This PR improves the startup time for `grind ring` by generating the
required type classes on demand. This optimization is particularly
relevant for files that make hundreds of calls to `grind`, such as
`tests/lean/run/grind_bitvec2.lean`. For example, before this change,
`grind` spent 6.87 seconds synthesizing type classes, compared to 3.92
seconds after this PR.
We can probably remove `lcUnreachable` once we delete the old compiler,
but for now it makes more sense to move it earlier, since LCNF already
has `Code.unreachable`.
This PR changes the `toMono` pass to consider the type of an application
and erase all arguments corresponding to erased params. This enables a
lightweight form of relevance analysis by changing the mono type of a
decl. I would have liked to unify this with the behavior for
constructors, but my attempt to give constructors the same behavior in
#9222 (which was in preparation for this PR) had a minor performance
regression that is really incidental to the change. Still, I decided to
hold off on it for the time being. In the future, we can hopefully
extend this to constructors, extern decls, etc.
This PR removes code that has the false assumption that LCNF local vars
can occur in types. There are other comments in `ElimDead.lean`
asserting that this is not possible, so this must have been a change
early in the development of the new compiler.
This PR makes the LCNF `elimDeadBranches` pass handle unsafe decls a bit
more carefully. Now the result of an unsafe decl will only become ⊤ if
there is value flow from a recursive call.
These are used by the checker for `.ctor`, but I don't think that that
unboxed types will reuse `.ctor`, whose implementation details are
intimately connected to our runtime representation of objects.
This PR changes the `getLiteral` helper function of `elimDeadBranches`
to correctly handle inductives with constructors. This function is not
used as often as it could be, which makes this issue rare to hit outside
of targeted test cases.
This PR extends the `Eq` simproc used in `grind`. It covers more cases
now. It also adds 3 reducible declarations to the list of declarations
to unfold.
This PR implements `exists` normalization using a simproc instead of
rewriting rules in grind. This is the first part of the PR, after update
stage0, we must remove the normalization theorems.
This PR changes the compiler's specialization analysis to consider
higher-order params that are rebundled in a way that only changes their
`Prop` arguments to be fixed. This means that they get specialized with
a mere `@[specialize]`, rather than the compiler having to opt-in to
more aggressive parameter-specific specialization.
This PR implements `forall` normalization using a simproc instead of
rewriting rules in `grind`. This is the first part of the PR, after
update stage0, we must remove the normalization theorems.
This PR fixes stealing of `⇓` syntax by the new notation for total
postconditions by demoting it to non-builtin syntax and scoping it to
`Std.Do`.
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR tries to improve the E-matching pattern inference for `grind`.
That said, we still need better tools for annotating and maintaining
`grind` annotations in libraries.
closes#9125
This PR removes the `Subarray`-specific `toArray`, `foldlM` and `foldl`
methods and instead provides these operations on `Std.Slice`, which are
implemented with the `ToIterator` instance of the slice. Calling
`subarray.toArray` etc. still works, since `Subarray` is an abbreviation
for `Slice _`.
Because the benchmarks are not so clear, to be safe, I will merge this
only after the release. In contrast to the ranges, the iteration over
slices is not quite as efficient as the old `Subarray`-specific
implementation, which would require either more optimizations in the
iterator library (special `IteratorLoop` and `IteratorCollect`
implementations) or better unboxing support by the compiler.
This PR makes the `pullInstances` pass avoid pulling any instance
expressions containing erased propositions, because we don't correctly
represent the dependencies that remain after erasure.
This PR disables the use of the header produced by `lake setup-file` in
the server for now. It will be re-enabled once Lake takes into account
the header given by the server when processing workspace modules.
Without that, `setup-file` header can produce odd behavior when the file
on disk and in an editor disagree on whether the file participates in
the module system.
This PR fixes `undefined symbol: lean::mpz::divexact(lean::mpz const&,
lean::mpz const&)` when building without `LEAN_USE_GMP`
This fixes a regression in #8089
This PR makes `mvcgen` split ifs rather than applying specifications.
Doing so fixes a bug reported by Rish.
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR resolves a defeq diamond, which caused a problem in Mathlib:
```
import Mathlib
example (R : Type) [I : Ring R] :
@AddCommGroup.toGrindIntModule R (@Ring.toAddCommGroup R I) =
@Lean.Grind.Ring.instIntModule R (@Ring.toGrindRing R I) := rfl -- fails
```
This PR fixes two issues with Lake's process of creating static
archives.
Lake now always recreates static archives by first deleting any existing
one and then recreating it. `ar rcs` does not remove delete files, so
running it when the archive already exists can leave behind "ghost"
symbols of removed object files.
Second, Lake now use `T` rather than `--thin` to create thin archives.
While `--thin` is the recommended spelling, older versions of LLVM `ar`
do not support it. Thus, either choice produces tradeoffs. `T` is chosen
to make Lake consistent with the Lean core's own (Make) build scripts.
This PR enforces the non-inlining of _override impls in the base phase
of LCNF compilation. The current situation allows for constructor/cases
mismatches to be exposed to the simplifier, which triggers an assertion
failure. The reason this didn't show up sooner for Expr is that Expr has
a custom extern implementation of its computed field getter.
Fixes#9156.
This test was originally checked in for a panic in the pretty printer,
but at some point the output of every LCNF simp pass was added to
#guard_msgs output. Since this is printing LCNF built by the stage0
compiler, this causes a lot of unnecessary churn.
This PR changes the key Lake uses for the `,ir` artifact in the content
hash data structure to `r`, maintaining the convention of single
character key names.
This PR fixes the syntax of `grind` modifiers to use `patternIgnore` for
cases where both unicode and ascii variants are matched. This fixes an
issue where several variants of grind syntax weren't accepted (e.g.
`@[grind ← gen]`). Additionally, this reduces the chance that we get
another syntax matching bootstrap hell.
This PR wraps `simpLemma` and `grindLemma` in `ppGroup` to make sure
that the modifiers aren't printed separately from the term / identifier.
Example:
```
simp only [very_long_lemma_oh_no_can_you_please_stop_we're_getting_to_the_limit, ←
wait_this_is_rewritten_backwards_oh_uhh_where's_the_arrow_you_ask?_oh_wait_it's_up_there!]
==>
simp only [very_long_lemma_oh_no_can_you_please_stop_we're_getting_to_the_limit,
← wait_this_is_rewritten_backwards_and_wow_it's_very_clear_and_obvious]
```
This PR tightens the IR typing rules around applications of closures.
When re-reading some code, I realized that the code in `mkPartialApp`
has a clear typo—`.object` and `type` should be swapped. However, it
doesn't matter, because later IR passes smooth out the mismatch here. It
makes more sense to be strict up-front and require applications of
closures to always return an `.object`.
This PR removes a rather ugly hack in the module system, exposing the
bodies of theorems whose type mention `WellFounded`.
The original motivation was that reducing well-founded definitions (e.g.
in `by rfl`) requires reducing proofs, so they need to be available.
But reducing proofs is generally fraught with peril, and we have been
nudging our users away from using it for a while, e.g. in #5182. Since
the module system is opt-in and users will gradually migrate to it, it
may be reasonable to expect them to avoid reducing well-founded
recursion in the process
This way we don't need hacks like this (which, without evidence, I
believe would be incomplete anyways) and we get the nice guarantee that
within the module system, theorems bodies are always private.
This PR removes some unnecessary `Decidable*` instance arguments by
using lemmas in the `Classical` namespace instead of the `Decidable`
namespace.
This might lead to some additional dependency on classical axioms, but
large parts of the standard library are relying on them either way.
This PR ensures that the state is reverted when compilation using the
new compiler fails. This is especially important for noncomputable
sections where the compiler might generate half-compiled functions which
may then be erroneously used while compiling other functions.
This PR generalizes the `a^(m+n)` grind normalizer to any semirings.
Example:
```
variable [Field R]
example (M : R) (h₀ : M ≠ 0) {n : Nat} (hn : n > 0) : M ^ n / M = M ^ (n - 1) := by
cases n <;> grind
```
This PR adds support for representing more inductive as enums,
summarized up as extending support to those that fail to be enums
because of parameters or irrelevant fields. While this is nice to have,
it is actually motivated by correctness of a future desired
optimization. The existing type representation is unsound if we
implement `object`/`tobject` distinction between values guaranteed to be
an object pointer and those that may also be a tagged scalar. In
particular, types like the ones added in this PR's tests would have all
of their constructors encoded via tagged values, but under the natural
extension of the existing rules of type representation they would be
considered `object` rather than `tobject`.
This PR converts the `lowerEnumToScalarType?` cache to a cache of IR
types of named types. This is more sensible than just focusing on the
enum optimization, and due to uniform representation of polymorphism we
have to compile `Constant T1` and `Constant T2` to the same
representation.
Bumps
[dawidd6/action-download-artifact](https://github.com/dawidd6/action-download-artifact)
from 10 to 11.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/dawidd6/action-download-artifact/releases">dawidd6/action-download-artifact's
releases</a>.</em></p>
<blockquote>
<h2>v11</h2>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/dawidd6/action-download-artifact/compare/v10...v11">https://github.com/dawidd6/action-download-artifact/compare/v10...v11</a></p>
</blockquote>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="ac66b43f0e"><code>ac66b43</code></a>
node_modules: upgrade</li>
<li><a
href="9b54a0a70c"><code>9b54a0a</code></a>
Update README.md</li>
<li>See full diff in <a
href="https://github.com/dawidd6/action-download-artifact/compare/v10...v11">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>
This PR changes ToIR to call `lowerEnumToScalarType?` with
`ConstructorVal.induct` rather than the name of the constructor itself.
This was an oversight in some refactoring of code in the new compiler
before landing it. It should not affect runtime of compiled code (due to
the extra tagging/untagging being optimized by LLVM), but it does make
IR for the interpreter slightly more efficient.
This PR fixes spacing in the `grind` attribute and tactic syntax.
Previously `@[grind]` was incorrectly pretty-printed as `@[grind ]`, and
`grind [...] on_failure ...` was pretty-printed `grind [...]on_failure
...`. Fixes that `on_failure` was reserved as keyword.
Since version 4, Lean is a partially bootstrapped program: most parts of the
Lean is a bootstrapped program: the
frontend and compiler are written in Lean itself and thus need to be built before
building Lean itself - which is needed to again build those parts. This cycle is
broken by using pre-built C files checked into the repository (which ultimately
@@ -73,6 +73,11 @@ 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.
NOTE: A full rebuild of stage 1 will only be triggered when the *committed* contents of `stage0/` are changed.
Thus if you change files in it manually instead of through `update-stage0-commit` (see below) or fetching updates from git, you either need to commit those changes first or run `make -C build/release clean-stdlib`.
The same is true for further stages except that a rebuild of them is retriggered on any committed change, not just to a specific directory.
Thus when debugging e.g. stage 2 failures, you can resume the build from these failures on but may want to explicitly call `clean-stdlib` to either observe changes from `.olean` files of modules that built successfully or to check that you did not break modules that built successfully at some prior point.
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>
@@ -82,13 +87,13 @@ gh workflow run update-stage0.yml
```
Leaving stage0 updates to the CI automation is preferable, but should you need
to do it locally, you can use `make update-stage0-commit` in `build/release` to
update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to
to do it locally, you can use `make -C build/release update-stage0-commit` to
update `stage0` from `stage1` or `make -C build/release/stageN update-stage0-commit` to
update from another stage. This command will automatically stage the updated files
and introduce a commit,so make sure to commit your work before that.
and introduce a commit,so make sure to commit your work before that.
If you rebased the branch (either onto a newer version of `master`, or fixing
up some commits prior to the stage0 update, recreate the stage0 update commits.
up some commits prior to the stage0 update), recreate the stage0 update commits.
The script `script/rebase-stage0.sh` can be used for that.
The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`)
@@ -9,7 +9,7 @@ You should not edit the `stage0` directory except using the commands described i
## Development Setup
You can use any of the [supported editors](../setup.md) for editing the Lean source code.
If you set up `elan` as below, opening `src/` as a *workspace folder* should ensure that stage 0 (i.e. the stage that first compiles `src/`) will be used for files in that directory.
Please see below for specific instructions for VS Code.
### Dev setup using elan
@@ -68,6 +68,10 @@ code lean.code-workspace
```
on the command line.
You can use the `Refresh File Dependencies` command as in other projects to rebuild modules from inside VS Code but be aware that this does not trigger any non-Lake build targets.
In particular, after updating `stage0/` (or fetching an update to it), you will want to invoke `make` directly to rebuild `stage0/bin/lean` as described in [building Lean](../make/index.md).
You should then run the `Restart Server` command to update all open files and the server watchdog process as well.
### `ccache`
Lean's build process uses [`ccache`](https://ccache.dev/) if it is
renderedStatement:="Std.DHashMap.Raw.Const.get.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Raw α fun x => β)\n (a : α) (h : a ∈ m) : β"
renderedStatement:="Std.DHashMap.Raw.Const.get.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α]\n (m : Std.DHashMap.Raw α fun x => β) (a : α) (h : a ∈ m) : β",
description:="Operations that take as input an associative container and return a 'single' piece of information (e.g., `GetElem` or `isEmpty`, but not `toList`)."
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.
