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.
