all your bases belong to us #1

jmikedupont2 · 2025-05-10T19:25:12Z

removing private
untested wip.
use as your own risk

This PR adds support for generating IR from the LCNF representation of the new compiler.

) These lemmas were inconsistently marked as `@[simp]`, but they seem generally useful, so this uniformly marks this lemmas as `@[simp]` for all map variants.

…rover#8216) This PR completes adding `@[grind]` annotations for `Option` lemmas, and incidentally fills in some `Option` API gaps/defects.

This PR continues adding `@[grind]` attributes for List/Array/Vector, particularly to the lemmas involving the `toList`/`toArray` functions.

This PR adds the `--setup` option to the `lean` CLI. It takes a path to a JSON file containing information about a module's imports and configuration, superseding that in the module's own file header. This will be used by Lake to specify paths to module artifacts (e.g., oleans and ileans) separate from the `LEAN_PATH` schema. To facilitate JSON serialization of the header data structure, `NameMap` JSON instances have been added to core, and `LeanOptions` now makes use of them.

This PR adds diagnostic information for the commutative ring procedure in `grind`.

This PR fixes the `simplifyBasis` procedure in the commutative ring procedure in `grind`.

This PR includes upgrades to the `release_checklist.py` script prepared while releasing v4.20.0-rc1.

This PR fixes an issue where, depending on the host glibc version, Lean-built executables fail with an assertion in `ld.so`.

This PR changes the behaviour of `apply?` so that the `sorry` it uses to close the goal is non-synthetic. (Recall that correct use of synthetic sorries requires that the tactic also generates an error message, which we don't want to do in this situation.) Either this PR or leanprover#8230 are sufficient to defend against the problem reported in leanprover#8212.

…eanprover#8235)

This PR fixes an issue where the combination of `extern_lib` and `precompileModules` would lead to "symbol not found" errors.

…ver#8238) This PR avoids an issue where, through other potential bugs, constants that are tracked by `Kernel.Environment` but not `Environment` are not persisted.

This PR fixes the 'goals accomplished' diagnostics. They were accidentally broken in leanprover#7902. Regression test tbd in a future PR.

This PR omits cases from functional induction/cases principles that are implemented `by contradiction` (or, more generally, `False.elim`, `absurd` or `noConfusion). Breaking change in the sense that there are fewer goals to prove after using functional induction. Fixes leanprover#8103.

…er#8249)

…r#8241) This PR changes the behavior of the `rename` tactic to skip over implementation detail hypotheses when finding a hypothesis to rename. Closes leanprover#8240.

…er#8254) This PR fixes unintended inlining of `ToJson`, `FromJson`, and `Repr` instances, which was causing exponential compilation times in `deriving` clauses for large structures.

This PR fixes the typo `Int.edivx y` to `Int.ediv x y` in `Int/DivMod/Basic`

…es (leanprover#8225) This PR adds additional infrastructure for error message formatting. Specifically, it adds convenience formatters for hints and notes, including the ability to attach code actions to hint messages using a "Try This"-like widget, along with several convenience formatters for message data. --------- Co-authored-by: Joachim Breitner <[email protected]>

This PR rewords the `application type mismatch` error message by more specifically mentioning that the problem is with the final argument. This is useful when the same argument is passed to the function multiple times. We decided against using a wording which specifically mentions the "function expression", because users who are not used to currying might not think of the `f a` in `f a b` as a function.

This PR adjusts the error message when `apply` fails to unify. It is clearer about distinguishing the term being applied and the goal, as well as distinguishing the "conclusion" of the given term and the term itself. --------- Co-authored-by: Joachim Breitner <[email protected]>

This PR makes `#guard_msgs` to treat `trace` messages separate from `info`, `warning` and `error`. It also introduce the ability to say `#guard_msgs (pass info`, like `(drop info)` so far, and also adds `(check info)` as the explicit form of `(info)`, for completeness. Fixes leanprover#8266

…f` (leanprover#8271) This PR changes `addPPExplicitToExposeDiff` to show universe differences and to visit into projections, e.g.: ``` error: tactic 'rfl' failed, the left-hand side (Test.mk (∀ (x : PUnit.{1}), True)).1 is not definitionally equal to the right-hand side (Test.mk (∀ (x : PUnit.{2}), True)).1 ``` for ```lean inductive Test where | mk (x : Prop) example : (Test.mk (∀ _ : PUnit.{1}, True)).1 = (Test.mk (∀ _ : PUnit.{2}, True)).1 := by rfl ```

This PR improves the type-as-hole error message. Type-as-hole error for theorem declarations should not admit the possibility of omitting the type entirely. --------- Co-authored-by: Joachim Breitner <[email protected]>

This PR ensures the congruence closure in `grind` and find non-dependent arrow congruences. That is, it can apply the `implies_congr` theorem.

This PR optimizes lean_nat_shiftr for scalar operands. The new compiler converts Nat divisions into right shifts, so this now shows up as hot in some profiles.

This PR the support for arrows in the congruence closure procedure used in `grind`.

… in `grind` (leanprover#8281) This PR improves the module used to prove auxiliary type cast equalities in `grind`.

We need to track rfl status in both the private and public scope once defs may become irreducible in the latter.

This PR fixes “declaration has free variables” errors when generating a splitter for a match statement with named patterns. Fixes leanprover#8274.

This PR adds a new variant of equations for matchers, namely “congruence equations” that generalize the normal matcher equations. They have unrestricted left-hand-sides, extra equality assumptions relating the discriminiants with the patterns and thus prove heterogenous equalities. In that sense they combine congruence with rewriting. They can be used to rewrite matcher applications where, due to dependencies, `simp` would fail to rewrite the discriminants, and will be used when producing the unfolding induction theorems.

…anprover#8277) This PR improves the generation of `.induct_unfolding` by rewriting `match` statements more reliably, using the new “congruence equations” introduced in leanprover#8284. Fixes leanprover#8195.

adding json to the mix is not easy, going to prototype it in user space first

jmikedupont2 · 2025-05-11T22:47:39Z

structure ExposeEnv extends Lean.Environment where
    deriving Lean.ToJson

def toExposeEnv (env : Lean.Environment) : ExposeEnv := { toEnvironment := env }

instance : Lean.ToJson Lean.Elab.Command.State where
    toJson s := Lean.Json.mkObj [
      ("env", Lean.ToJson.toJson (Lean.toJson (toExposeEnv s.env))),
      ("messages", Lean.toJson s.messages),
      ("scopes", Lean.toJson s.scopes)
    ]

zwarich and others added 30 commits May 3, 2025 05:34

feat: LCNF -> IR translation (leanprover#8211)

afab374

This PR adds support for generating IR from the LCNF representation of the new compiler.

chore: consistently add @[simp] to getKey_eq map lemmas (leanprover#8186

6e2e1a4

) These lemmas were inconsistently marked as `@[simp]`, but they seem generally useful, so this uniformly marks this lemmas as `@[simp]` for all map variants.

feat: complete addition of @[grind] annotations for Option (leanp…

80349ac

…rover#8216) This PR completes adding `@[grind]` annotations for `Option` lemmas, and incidentally fills in some `Option` API gaps/defects.

chore: cleanup of @[grind] lemmas for Option (leanprover#8217)

d005a30

chore: more @[grind] annotations for List/Array/Vector (leanprover#8218)

132c608

This PR continues adding `@[grind]` attributes for List/Array/Vector, particularly to the lemmas involving the `toList`/`toArray` functions.

feat: diagnostics for comm ring procedure in grind (leanprover#8224)

8cc4505

This PR adds diagnostic information for the commutative ring procedure in `grind`.

fix: simplifyBasis (leanprover#8226)

ef603cf

This PR fixes the `simplifyBasis` procedure in the commutative ring procedure in `grind`.

feat: upgrades to release_checklist.py script (leanprover#8192)

208ff3e

This PR includes upgrades to the `release_checklist.py` script prepared while releasing v4.20.0-rc1.

fix: ld.so linking on Linux (leanprover#8228)

cdb18f4

This PR fixes an issue where, depending on the host glibc version, Lean-built executables fail with an assertion in `ld.so`.

chore: update release_checklist.py to check new release notes page (l…

9576e48

…eanprover#8235)

fix: extern_lib and precompileModules on macOS (leanprover#8236)

9c7cb14

This PR fixes an issue where the combination of `extern_lib` and `precompileModules` would lead to "symbol not found" errors.

fix: make sure all kernel constants are persisted eventually (leanpro…

af51e3e

…ver#8238) This PR avoids an issue where, through other potential bugs, constants that are tracked by `Kernel.Environment` but not `Environment` are not persisted.

fix: broken goals accomplished (leanprover#8242)

65b37b4

This PR fixes the 'goals accomplished' diagnostics. They were accidentally broken in leanprover#7902. Regression test tbd in a future PR.

chore: update stage0

c96dfa5

chore: make builtinRuntimeTypes an Array rather than a List (leanprov…

cd100b8

…er#8249)

chore: post-stage0 fixes for leanprover#8171 (leanprover#8250)

edcad9a

chore: update stage0

529fb5c

fix: have rename ignore implementation detail hypotheses (leanprove…

e602bdc

…r#8241) This PR changes the behavior of the `rename` tactic to skip over implementation detail hypotheses when finding a hypothesis to rename. Closes leanprover#8240.

fix: exponential compilation times due to inlined instances (leanprov…

02cbe49

…er#8254) This PR fixes unintended inlining of `ToJson`, `FromJson`, and `Repr` instances, which was causing exponential compilation times in `deriving` clauses for large structures.

chore: fix typo in Int/DivMod/Basic (leanprover#8255)

732471f

This PR fixes the typo `Int.edivx y` to `Int.ediv x y` in `Int/DivMod/Basic`

fix: improve type-as-hole error message (leanprover#8262)

eabde77

This PR improves the type-as-hole error message. Type-as-hole error for theorem declarations should not admit the possibility of omitting the type entirely. --------- Co-authored-by: Joachim Breitner <[email protected]>

feat: add support for implies_congr in grind (leanprover#8275)

ddf5512

This PR ensures the congruence closure in `grind` and find non-dependent arrow congruences. That is, it can apply the `implies_congr` theorem.

zwarich and others added 6 commits May 11, 2025 01:39

feat: optimize lean_nat_shiftr for scalars (leanprover#8268)

575b478

This PR optimizes lean_nat_shiftr for scalar operands. The new compiler converts Nat divisions into right shifts, so this now shows up as hot in some profiles.

fix: arrow congruence in grind (leanprover#8280)

9096eb1

This PR the support for arrows in the congruence closure procedure used in `grind`.

feat: improve procedure for proving auxiliary type casting equalities…

e681855

… in `grind` (leanprover#8281) This PR improves the module used to prove auxiliary type cast equalities in `grind`.

fix: rfl theorem tracking in the module system (leanprover#8215)

1f85fd2

We need to track rfl status in both the private and public scope once defs may become irreducible in the latter.

fix: left-over free variables in splitter (leanprover#8285)

ca73223

This PR fixes “declaration has free variables” errors when generating a splitter for a match statement with named patterns. Fixes leanprover#8274.

jmikedupont2 force-pushed the introspector branch from 4c27d68 to a6f2a62 Compare May 11, 2025 15:21

nomeata and others added 2 commits May 11, 2025 15:26

fix: FunInd: rewrite matches more reliably in .induct_unfolding (le…

33aaaba

…anprover#8277) This PR improves the generation of `.induct_unfolding` by rewriting `match` statements more reliably, using the new “congruence equations” introduced in leanprover#8284. Fixes leanprover#8195.

wip

226aa9a

jmikedupont2 force-pushed the introspector branch from a5103ac to 226aa9a Compare May 11, 2025 17:37

github-actions bot added the changes-stage0 label May 11, 2025

mike dupont added 6 commits May 11, 2025 13:53

wip

2c2a275

wip

b4e5134

be more careful

6418daf

how did this get reverted?

a95b345

builds

6e26dd4

wip

16e818f

adding json to the mix is not easy, going to prototype it in user space first

wip

e574f94

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

all your bases belong to us #1

all your bases belong to us #1

Uh oh!

jmikedupont2 commented May 10, 2025

Uh oh!

jmikedupont2 commented May 11, 2025

Uh oh!

Uh oh!

all your bases belong to us #1

Are you sure you want to change the base?

all your bases belong to us #1

Uh oh!

Conversation

jmikedupont2 commented May 10, 2025

Uh oh!

jmikedupont2 commented May 11, 2025

Uh oh!

Uh oh!