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.
