feat: use `nondep` flag in `Expr.letE` and `LocalContext.ldecl` by kmill · Pull Request #8804 · leanprover/lean4

kmill · 2025-06-16T00:12:01Z

This PR implements first-class support for nondependent let expressions in the elaborator; recall that a let expression let x : t := v; b is called nondependent if fun x : t => b typechecks, and the notation for a nondependent let expression is have x := v; b. Previously we encoded have using the letFun function, but now we make use of the nondep flag in the Expr.letE constructor for the encoding. This has been given full support throughout the metaprogramming interface and the elaborator. Key changes to the metaprogramming interface:

Local context ldecls with nondep := true are generally treated as cdecls. This is because in the body of a have expression the variable is opaque. Functions like LocalDecl.isLet by default return false for nondependent ldecls. In the rare case where it is needed, they take an additional optional allowNondep : Bool flag (defaults to false) if the variable is being processed in a context where the value is relevant.
Functions such as mkLetFVars by default generalize nondependent let variables and create lambda expressions for them. The generalizeNondepLet flag (default true) can be set to false if have expressions should be produced instead. Breaking change: Uses of letLambdaTelescope/mkLetFVars need to use generalizeNondepLet := false. See the next item.
There are now some mapping functions to make telescoping operations more convenient. See mapLetTelescope and mapLambdaLetTelescope. There is also mapLetDecl as a counterpart to withLetDecl for creating let/have expressions.
Important note about the generalizeNondepLet flag: it should only be used for variables in a local context that the metaprogram "owns". Since nondependent let variables are treated as constants in most cases, the value field might refer to variables that do not exist, if for example those variables were cleared or reverted. Using mapLetDecl is always fine.
The simplifier will cache its let dependence calculations in the nondep field of let expressions.
The intro tactic still produces dependent local variables. Given that the simplifier will transform lets into haves, it would be surprising if that would prevent intro from creating a local variable whose value cannot be used.

Note that nondependence of lets is not checked by the kernel. To external checker authors: If the elaborator gets the nondep flag wrong, we consider this to be an elaborator error. Feel free to typecheck letE n t v b true as if it were app (lam n t b default) v and please report issues.

This PR follows up from #8751, which made sure the nondep flag was preserved in the C++ interface.

ghost · 2025-06-16T00:42:59Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e2a947c2e6871f406b965bf1c66ef72e0fdc0599 --onto 957b904ef9fd11ed9cb49f12fcc9d7b989c01900. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-16 00:42:59)
💥 Mathlib branch lean-pr-testing-8804 build failed against this PR. (2025-06-18 18:06:15) View Log
💥 Mathlib branch lean-pr-testing-8804 build failed against this PR. (2025-06-18 21:01:12) View Log
💥 Mathlib branch lean-pr-testing-8804 build failed against this PR. (2025-06-18 21:33:00) View Log
💥 Mathlib branch lean-pr-testing-8804 build failed against this PR. (2025-06-18 22:23:04) View Log
💥 Mathlib branch lean-pr-testing-8804 build failed against this PR. (2025-06-18 23:38:18) View Log
✅ Mathlib branch lean-pr-testing-8804 has successfully built against this PR. (2025-06-19 00:21:50) View Log
✅ Mathlib branch lean-pr-testing-8804 has successfully built against this PR. (2025-06-19 06:27:40) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2ebc001dd1ce72c134abfe79859780e71df7e3a8 --onto db499e96aac8ad654c8ed5ab40c4e6885d38c9a1. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-22 22:06:10)

This PR makes changes for compatibility with leanprover/lean4#8804. The key difference is that `nondep := true` should be treated as a cdecl. The `LocalDecl.isLet` will return false for such ldecls.

leodemoura · 2025-06-22T02:14:09Z

src/Lean/Elab/Binders.lean

-    withLetDecl id.getId (kind := kind) type val fun x => do
+  let result ←
+    withLetDecl id.getId (kind := kind) type val (nondep := !useLetExpr) fun x => do
      addLocalVarInfo id x


Nice. @kmill No action needed here. I am just marking non trivial changes that I have already checked.

leodemoura · 2025-06-22T02:17:09Z

src/Lean/Elab/MutualDef.lean

-      if !zetaDeltaFVarIds.contains fvarId then
-        /- Non-dependent let-decl. See comment at src/Lean/Meta/Closure.lean -/
+      if nondep || !zetaDeltaFVarIds.contains fvarId then
+        /- Nondependent let-decl. See comment at src/Lean/Meta/Closure.lean -/


@kmill This is an optimization, correct? I am assuming that if fvarId is in zetaDeltaFVarIds and nondep is true, then the nondep annotation is incorrect.

Correct, if nondep is true then it is not possible for zetaDeltaFVarIds to contain fvarId. This is just a small optimization.

Added a comment mentioning this invariant.

leodemoura · 2025-06-22T02:18:04Z

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

+    | Expr.letE n type val body nondep =>
+      -- Turn `have`s into `let`s if they are not propositions.
+      let nondep ← pure nondep <&&> not <$> Meta.isProp type
+      mapLetDecl n (← loop below type) (← loop below val) (nondep := nondep) (usedLetOnly := false) fun x => do


Remind me of the rationale for turning have to let in structural recursion, Kyle?

leodemoura · 2025-06-22T02:20:25Z

src/Lean/Elab/PreDefinition/WF/Preprocess.lean

  return .continue <| matcherApp'.toExpr

-/-- `let x := (wfParam e); body[x] ==> let x := e; body[wfParam y] -/
+private def anyLetValueIsWfParam (e : Expr) : Bool :=


@nomeata I am assuming you are happy with these changes. I am asking because you own this file.

Yes, looks good!

leodemoura · 2025-06-22T02:30:11Z

src/Lean/LocalContext.lean

+    Instead, `revert x` *must* produce the goal `⊢ ∀ x : α, b`.
+    Furthermore, given a goal `⊢ have x : α := v; b`, the `intro x` tactic should yield a *dependent* `ldecl`,
+    since users expect to be able to make use of the value of `x`,
+    and also the value creates a hidden source of dependencies on other local variables.


@kmill You justified well the design decisions, but it would be great to include a note saying how one gets a nondep ldecl into the local context x : α := v (nondep) ⊢ b since intro will introduce a dependent one for have.

Extended the note

leodemoura · 2025-06-22T02:31:56Z

src/Lean/LocalContext.lean

+    since users expect to be able to make use of the value of `x`,
+    and also the value creates a hidden source of dependencies on other local variables.
+  - Also: `value` might not be type correct. Metaprograms may decide to pretend that all `nondep := true`
+    `ldecl`s are `cdecl`s (for example, when reverting variables). As a consequence, nondep `ldecl`s may


Should we have a debugging flag to force Lean to type check the value at functions such as withLetDecl?

I'll keep this in mind. Thinking about possible metaprogramming mistakes, maybe mkBinding could check that the value's fvars are all in context?

leodemoura · 2025-06-22T02:34:30Z

src/Lean/LocalContext.lean

  | d, _                       => d

+/-- Sets the `nondep` flag of an `ldecl`, otherwise returns `cdecl`s unchanged. -/
+def setNondep : LocalDecl → Bool → LocalDecl


@kmill Should we add a note saying that it is the caller responsibility to ensure dep => nondep transitions are correct?

Added some guidelines to the docstring

leodemoura · 2025-06-22T02:54:39Z

src/Lean/Meta/Basic.lean

 -/
-def lambdaLetTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α :=
-  map2MetaM (fun k => lambdaTelescopeImp e true .none k (cleanupAnnotations := cleanupAnnotations)) k
+def lambdaLetTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) (preserveNondepLet := true) : n α :=


In the current master, lambdaLetTelescope stops at have. For example, the following example prints 1.

import Lean def c : Nat → Nat → Bool := fun x => have y := 1; fun z => x == y + z open Lean Meta in run_meta do let decl ← getConstInfo ``c lambdaLetTelescope decl.value! fun xs _ => IO.println xs.size

I am not defending the current behavior.
The comment above suggests that this example will print 3 if preserveNondepLet := false. What happens if preserveNondepLet := true. I am assuming it will "consume" the have and mark it as nondep in the local context.

Yes, now haves are always consumed and that prints 3. Setting preserveNondepLet controls whether the nondep flag will be cleared. I've added this to the tests:

def c : Nat → Nat → Bool := fun x => have y := 1; fun z => x == y + z /-- info: #[false, true, false] #[false, false, false] -/ #guard_msgs in open Lean Meta in run_meta do let decl ← getConstInfo ``c lambdaLetTelescope decl.value! fun xs _ => do IO.println <| ← xs.mapM fun x => return (← x.fvarId!.getDecl).isNondep lambdaLetTelescope decl.value! (preserveNondepLet := false) fun xs _ => do IO.println <| ← xs.mapM fun x => return (← x.fvarId!.getDecl).isNondep

leodemoura · 2025-06-22T02:56:05Z

src/Lean/Meta/Basic.lean

+
+See also `mapLetTelescope` for entering and rebuilding the telescope.
+-/
+def letTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) (preserveNondepLet := true) (nondepLetOnly := false) : n α :=


I am assuming there is no way to consume only dependent lets.

Correct, there's no way to do that at the moment (I haven't needed it yet).

leodemoura · 2025-06-22T03:01:16Z

src/Lean/Meta/Closure.lean

      let zetaDeltaFVarIds ← getZetaDeltaFVarIds
-      if !zetaDeltaFVarIds.contains fvarId then
+      if nondep || !zetaDeltaFVarIds.contains fvarId then
        /- Non-dependent let-decl


Same as comment above. I am assuming this is an optimization.

Added a comment about the invariant

leodemoura · 2025-06-22T03:05:05Z

src/Lean/Meta/ExprDefEq.lean

      match lctx.findFVar? fvar with
-      | some (.ldecl (value := v) ..) => check v
+      | some (.ldecl (nondep := false) (value := v) ..) => check v
      | _ =>


@kmill Could you please document this change? We need a why? and example showing why the previous behavior was incorrect.

Added an explanation and example.

leodemoura · 2025-06-22T03:06:03Z

src/Lean/Meta/ExprDefEq.lean

      if mvarDecl.lctx.contains fvarId then
        return true
-      if let some (LocalDecl.ldecl ..) := lctx.find? fvarId then
+      if let some (LocalDecl.ldecl (nondep := false) ..) := lctx.find? fvarId then


Same. See previous comment.

Added a comment pointing to the new comment in CheckAssignment.checkFVar.

leodemoura · 2025-06-22T03:07:37Z

src/Lean/Meta/Tactic/FunInd.lean

          mkForallFVars #[x] body'

-    | .letE n t v b _ =>
+    | .letE n t v b nondep =>


@nomeata Are you happy with the changes to this file?

leodemoura · 2025-06-22T03:09:11Z

src/Lean/Meta/Tactic/Lets.lean

-        mkLetFun decl.toExpr decl.value e
+def mkLetDecls (decls : Array LocalDecl') (e : Expr) : Expr :=
+  decls.foldr (init := e) fun { decl, isLet } e =>
+    Expr.letE decl.userName decl.type decl.value (e.abstract #[decl.toExpr]) (nondep := !isLet)


leodemoura · 2025-06-22T03:12:09Z

src/Lean/Meta/Tactic/Simp/Main.lean

    let bx := b.instantiate1 x
+    if nondep then
+      let bxType ← whnf (← inferType bx)
+      if (← dependsOn bxType x.fvarId!) then


@kmill Could you please add a comment here explaining this part? We will forget.

Added an explanation.

By the way, I have a followup PR that intends to replace this code. Brief preview: if simp comes across a nondep := false let, then it can run letToHave on it (which is slightly cheaper than isTypeCorrect, and it addresses the "TODO" comment in this function, by handling all lets simultaneously), and otherwise we can do the nondepDepVar/nondep determination on an entire telescope at once, using code similar to what you wrote for letFun.

leodemoura · 2025-06-22T03:13:39Z

src/Lean/Meta/Tactic/Simp/Main.lean

    return { expr := e }
-  else if isNonDepLetFun e then
-    simpNonDepLetFun e
+  else if let some (args, n, t, v, b) := e.letFunAppArgs? then


@kmill Comment?

Added a comment/explanation that this piece of code is in flux. (It should be addressed in time for the next release, so hopefully this comment is short-lived!)

nomeata

Leo asked me to give this a read-through, too.

High-level thought: I’m a bit worried about the complexities around ldecl behaving one way or another depending on their flag and various flags on the functions acting on them. If it wasn’t for backwards compat, would we do it this way, or would entering a have just leave a cdecl in the context, and leave it to whoever rebuilds the expression to remember to use a nondep expression? But you probably considered that design and chose this one for a reason.

In a few cases my brain has trouble keeping up with an optional boolean flag that is called non-something, too much negation and boolean blindness. In terms of API design, at least for those functions where one flag is common and the other is very rare and possibly dangerous or at least hairy to get right, if it’d be better to have separate functions with more speaking names.

nomeata · 2025-06-22T09:10:07Z

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

+    | Expr.letE n type val body nondep =>
+      -- Turn `have`s into `let`s if they are not propositions.
+      let nondep ← pure nondep <&&> not <$> Meta.isProp type
+      mapLetDecl n (← loop below type) (← loop below val) (nondep := nondep) (usedLetOnly := false) fun x => do


Remind me of the rationale for turning have to let in structural recursion, Kyle?

nomeata · 2025-06-22T09:11:42Z

src/Lean/Elab/PreDefinition/Structural/IndPred.lean

-      withLetDecl n (← loop type) (← loop val) fun x => do
-        mkLetFVars #[x] (← loop (body.instantiate1 x))
+    | Expr.letE n type val body nondep =>
+      mapLetDecl n (← loop type) (← loop val) (nondep := nondep) fun x => do


I like the mapLetDecl combinator to capture that idioms here, I think I wanted something like that before. Maybe later we’ll want it for mapForall etc. as well. (And then generalize the result from Expr to a HasExpr type class so that we can return (Bool, Expr) or (Expr, Expr) … :-))

src/Lean/Elab/PreDefinition/WF/Preprocess.lean

nomeata · 2025-06-22T09:20:02Z

src/Lean/Elab/PreDefinition/WF/Preprocess.lean

  return .continue <| matcherApp'.toExpr

-/-- `let x := (wfParam e); body[x] ==> let x := e; body[wfParam y] -/
+private def anyLetValueIsWfParam (e : Expr) : Bool :=


Yes, looks good!

nomeata · 2025-06-22T09:27:56Z

src/Lean/LocalContext.lean

+/-- Returns true if this is an `ldecl`. If `allowNondep` is false (the default), then requires that `nondep` be false. -/
+def isLet : LocalDecl → (allowNondep : Bool := false) → Bool
+  | cdecl .., _ => false
+  | ldecl (nondep := false) .., _ => true
+  | ldecl (nondep := true) .., allowNondep => allowNondep


The only use of the optional parameter is through isLetVar, and there it is isn’t used, it seems.

I wonder if we get easier to understand code if isLet and isLetVar doesn’t take an optional parameter, and we have separate functions isLetOrHave and isLetOrHaveVar for what’s now (allowNonDep := true). Especially if we don’t expect meta-code to be “dynamically generic” in the allowNonDep flag.

I guess we’d also need letOrHaveValue?. Up to you.

Sorry, had to step away before your last message — I was going to say that I'll review this part of the API again after a couple PRs.

Any thoughts about generalizeNondepLet? I'm wondering if I got the polarity wrong on that one, but I couldn't think of anything else to call it. At least it's used infrequently enough that it wouldn't be hard to change it later.

I had to think when I read it, but then concluded that the name is correct 🤷🏻

nomeata · 2025-06-22T12:41:00Z

src/Lean/LocalContext.lean

+- If the declaration is for a variable whose dependencies are not completely under the caller's control,
+  then setting `nondep := false` must not be done.
+- Even if the caller does have complete control, setting `nondep := false` should not be done.
+  The cautions about caches and metavariables still apply.


This sounds like there isn’t a need to even support nondep := false, if it shouldn't be done. Do we need it?

Although, the only use case I see in this diff is

-- Clear the flag if it's not a prop. let decl' := decl.setNondep <| ← pure decl.isNondep <&&> Meta.isProp decl.type

And it seems that this may do a (nondep := true) → (nondep := false) transition… if this is something that shouldn’t be done, do we need a comment there why we do it?

I wonder again if the code was clearer if we have separate setNondep and clearNonDep functions, and write it like this:

-- Clear the flag if it's not a prop. if (← Meta.isProp decl.type) the decl := decl.clearNondep

assuming we can afford the Meta.isProp check, or

-- Clear the flag if it's not a prop. if (← decl.isNondep <&&> Meta.isProp decl.type) the decl := decl.clearNondep

I've tried to clarify this docstring.

I was trying to use "must not" vs "should not" technically, but that's too confusing. There's an example of ok nondep := false usage and why, taken from the WF changes.

src/Lean/Meta/Basic.lean

src/Lean/LocalContext.lean

src/Lean/Meta/Tactic/FunInd.lean

src/Lean/Meta/Tactic/Lets.lean

kmill · 2025-06-22T16:59:35Z

@nomeata

High-level thought: I’m a bit worried about the complexities around ldecl behaving one way or another depending on their flag and various flags on the functions acting on them. If it wasn’t for backwards compat, would we do it this way, or would entering a have just leave a cdecl in the context, and leave it to whoever rebuilds the expression to remember to use a nondep expression? But you probably considered that design and chose this one for a reason.

It's reasonable to worry about whether backwards compatibility was a consideration, but I tried to make the design be from first principles. A case study we have is what it's been like to work with letFun, where you have to enter it as a cdecl and then awkwardly apply the letfun constructor at the correct points in a telescope. In an earlier version of letToHave, I had to have a completely custom telescoping function that recorded the have values in a separate data structure. Being able to record the values in the local context reduces the complexity (plus now everything that uses lambdaLetTelescope automatically can enter haves, saving some incidental quadratic complexity). Note that mapLetTelescope does not do everything that you might want with a let telescope, and having a convenient place for sticking the value so that mkLetFVars "just works" is very convenient (modulo needing to set the appropriate flag!)

There seems to be something fundamental here with there being variables where in different situations the value is either known or not known, and I wish I had some more theory to support it. That lack of supporting theory is a weakness of this design in my opinion.

Another design idea I had was to add an hdecl constructor. There were a few reasons I didn't:

There's a nice parallel between the nondep flag of Expr.letE and the nondep flag of ldecl.
Adding a constructor would need some more expr.h changes.
There is enough nondep flag manipulation around where I thought it was clear that requiring code that switches between ldecl and hdecl as necessary would be more complex.

In any case, so long as metaprograms use LocalDecl.isLet, LocalDecl.value?, and other accessors, they don't need to worry about cdecl vs ldecl. It's just "does it have a value (that I can use)?" so long as you don't set any of the flags.

In a few cases my brain has trouble keeping up with an optional boolean flag that is called non-something, too much negation and boolean blindness.

It seems like a negation, but I think in practice "nondependent" is a positive quality. It could have been called "simple"/"fun"/"have"/etc. The default value for the flag is nondep := false, and that's the safe default. Every have in theory is still type correct as a let. The flag is enabled only when a have is safe, and we can talk about clearing the flag, which goes back to the less-conservative expression.

In terms of API design, at least for those functions where one flag is common and the other is very rare and possibly dangerous or at least hairy to get right, if it’d be better to have separate functions with more speaking names.

Yes, this is the purpose of the map* functions. The generalizeNondepLets flag is rather low-level, and I hope it's rare that anyone will need it. There was only one instance of it being needed in mathlib/batteries/aesop/qq (see funprop in https://github.com/leanprover-community/mathlib4/pull/26132/files), and even in that case I think it's just a matter of augmenting the telescoping API with a version that can map a function on types/values before they are added to the local context. (I think that's out of scope for this PR.)

Something that helped me feel like the approach in the PR was on the right track is that none of the uses of the LocalDecl accessors outside of the core algorithms need to adjust the allowNondep argument. (Going back to the point of reasoning about negations, I made this flag be default-false because true means that you are going out of your way to enable accessing normally inaccessible values.)

Remind me of the rationale for turning have to let in structural recursion, Kyle?

I'll check this one again. I know there was a motivating test case, but I don't remember if it was (1) because of changes to simp in this PR, which caches nondependence in the letE expression or (2) if it is necessary once letToHave is being universally applied in a future PR.

(I'll respond to your other comments directly.)

nomeata · 2025-06-22T17:57:39Z

Thanks, that's convincing.

Something that helped me feel like the approach in the PR was on the right track is that none of the uses of the LocalDecl accessors outside of the core algorithms need to adjust the allowNondep argument.

Hm, but isn't that even more reason to make it not look as if allowNondep := true is “equally valid” as the default? If you want users who don't think hard to use the safe default, my sense is that that's achieved more likely if the advanced option is a separate function.

But we are entering superficial bike shedding territory, and it's not like the rest of Lean's API is designed with psychological nudges in mind, so it's ok as is.

digama0 · 2025-06-22T18:35:17Z

What's the situation around kernel changes here? Should the kernel now treat nondep := true lets like have? When entering binders should it use ldecl or cdecl?

kmill · 2025-06-22T18:42:32Z

@digama0 Quoting the PR summary: "Note that nondependence of lets is not checked by the kernel." For the time being, we'll rely on the elaborator typechecker to spot-check nondep usage. (Or, possibly, in some contexts such as proofs we might have the elaborator use a letFun/beta-redex encoding to keep the variable from being unfolded during checking, for performance.)

If you want to implement checking it in an external checker, then I think there are two main options: either convert letE n t v b true to app (lam n t b default) v when you come across it, or, if you're using LocalContext logic, create a cdecl for the fvar when checking b.

This PR implements first-class support for nondependent let expressions in the elaborator; recall that a let expression `let x := v; b` is called *nondependent* if `fun x => b` typechecks, and the notation for a nondependent let expression is `have x := v; b`. Previously we encoded `have` using the `letFun` function, but now we make use of the `nondep` flag in the `Expr.letE` constructor for the encoding. This has been fully supported throughout the metaprogramming interface and the elaborator. Note that nondependence of lets is not checked by the kernel. Follows up from leanprover#8751, which made sure the nondep flag was preserved in the C++ interface.

…prover#8804) This PR implements first-class support for nondependent let expressions in the elaborator; recall that a let expression `let x : t := v; b` is called *nondependent* if `fun x : t => b` typechecks, and the notation for a nondependent let expression is `have x := v; b`. Previously we encoded `have` using the `letFun` function, but now we make use of the `nondep` flag in the `Expr.letE` constructor for the encoding. This has been given full support throughout the metaprogramming interface and the elaborator. Key changes to the metaprogramming interface: - Local context `ldecl`s with `nondep := true` are generally treated as `cdecl`s. This is because in the body of a `have` expression the variable is opaque. Functions like `LocalDecl.isLet` by default return `false` for nondependent `ldecl`s. In the rare case where it is needed, they take an additional optional `allowNondep : Bool` flag (defaults to `false`) if the variable is being processed in a context where the value is relevant. - Functions such as `mkLetFVars` by default generalize nondependent let variables and create lambda expressions for them. The `generalizeNondepLet` flag (default true) can be set to false if `have` expressions should be produced instead. **Breaking change:** Uses of `letLambdaTelescope`/`mkLetFVars` need to use `generalizeNondepLet := false`. See the next item. - There are now some mapping functions to make telescoping operations more convenient. See `mapLetTelescope` and `mapLambdaLetTelescope`. There is also `mapLetDecl` as a counterpart to `withLetDecl` for creating `let`/`have` expressions. - Important note about the `generalizeNondepLet` flag: it should only be used for variables in a local context that the metaprogram "owns". Since nondependent let variables are treated as constants in most cases, the `value` field might refer to variables that do not exist, if for example those variables were cleared or reverted. Using `mapLetDecl` is always fine. - The simplifier will cache its let dependence calculations in the nondep field of let expressions. - The `intro` tactic still produces *dependent* local variables. Given that the simplifier will transform lets into haves, it would be surprising if that would prevent `intro` from creating a local variable whose value cannot be used. Note that nondependence of lets is not checked by the kernel. To external checker authors: If the elaborator gets the nondep flag wrong, we consider this to be an elaborator error. Feel free to typecheck `letE n t v b true` as if it were `app (lam n t b default) v` and please report issues. This PR follows up from leanprover#8751, which made sure the nondep flag was preserved in the C++ interface.

This PR adds the following features to `simp`: - A routine for simplifying `have` telescopes in a way that avoids quadratic complexity arising from locally nameless expression representations, like what #6220 did for `letFun` telescopes. Furthermore, simp converts `letFun`s into `have`s (nondependent lets), and we remove the #6220 routine since we are moving away from `letFun` encodings of nondependent lets. - A `+letToHave` configuration option (enabled by default) that converts lets into haves when possible, when `-zeta` is set. Previously Lean would need to do a full typecheck of the bodies of `let`s, but the `letToHave` procedure can skip checking some subexpressions, and it modifies the `let`s in an entire expression at once rather than one at a time. - A `+zetaHave` configuration option, to turn off zeta reduction of `have`s specifically. The motivation is that dependent `let`s can only be dsimped by let, so zeta reducing just the dependent lets is a reasonable way to make progress. The `+zetaHave` option is also added to the meta configuration. - When `simp` is zeta reducing, it now uses an algorithm that avoids complexity quadratic in the depth of the let telescope. - Additionally, the zeta reduction routines in `simp`, `whnf`, and `isDefEq` now all are consistent with how they apply the `zeta`, `zetaHave`, and `zetaUnused` configurations. The `letToFun` option is addressing a TODO in `getSimpLetCase` ("handle a block of nested let decls in a single pass if this becomes a performance problem"). Performance should be compared to before #8804, which temporarily disabled the #6220 optimizations for `letFun` telescopes. Good kernel performance depends on carefully handling the `have` encoding. Due to the way the kernel instantiates bvars (it does *not* beta reduce when instantiating), we cannot use congruence theorems of the form `(have x := v; f x) = (have x ;= v'; f' x)`, since the bodies of the `have`s will not be syntactically equal, which triggers zeta reduction in the kernel in `is_def_eq`. Instead, we work with `f v = f' v'`, where `f` and `f'` are lambda expressions. There is still zeta reduction, but only when converting between these two forms at the outset of the generated proof.

* chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: bump to nightly-2025-06-19 * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * lint --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Cameron Zwarich <cameron@lean-fro.org> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Sebastian Graf <sg@lean-fro.org> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>

* cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: bump to nightly-2025-06-19 * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * Merge master into nightly-testing * unused simp args * chore: bump to nightly-2025-06-29 * chore: adaptations for nightly-2025-06-29 * Merge master into nightly-testing * chore: robustify `open Mathlib` benchmark * deprecations * Update lean-toolchain for testing leanprover/lean4#9086 * Merge master into nightly-testing * fixes * chore: bump to nightly-2025-06-30 * lake update * lake update * lake update * lake update * lake update * . --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Cameron Zwarich <cameron@lean-fro.org> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Sebastian Graf <sg@lean-fro.org> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>

@Kha

* fix * fixes * chore: adaptations for nightly-2025-06-16 (leanprover-community#25994) * chore: bump to nightly-2025-06-03 * fix * fix * Update lean-toolchain for testing leanprover/lean4#8610 * fix * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 (leanprover-community#26043) * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 --------- Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: adaptations for nightly-2025-06-18 (leanprover-community#26077) * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> * chore: bump to nightly-2025-06-19 * feat: add algebra shims for Grind.Nat/IntModule (leanprover-community#26133) This PR adds shims so `grind` will understand Mathlib's `AddCommMonoid` and `AddCommGroup`. (Subsequent shims will connect up the order structures for modules and rings.) * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * feat: generalize grind algebra shims (leanprover-community#26131) This PR extends the shims converting from Mathlib to `Lean.Grind` typeclasses, now that `grind` knows about (non-commutative)-(semi)-rings. * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 (leanprover-community#26209) * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * chore: bump to nightly-2025-06-19 * fix * remove mul_hmul * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * chore: adaptations for nightly-2025-06-26 (#2) * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * chore: adaptations for nightly-2025-06-27 (#3) * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * Merge master into nightly-testing * unused simp args * chore: bump to nightly-2025-06-29 * chore: adaptations for nightly-2025-06-29 * chore: adaptations for nightly-2025-06-28 (#5) * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: bump to nightly-2025-06-19 * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * lint --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Cameron Zwarich <cameron@lean-fro.org> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Sebastian Graf <sg@lean-fro.org> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com> * Merge master into nightly-testing * chore: robustify `open Mathlib` benchmark * deprecations * Update lean-toolchain for testing leanprover/lean4#9086 * Merge master into nightly-testing * fixes * chore: bump to nightly-2025-06-30 * lake update * lake update * lake update * lake update * lake update * . * Merge master into nightly-testing * Merge master into nightly-testing * Merge master into nightly-testing * Merge master into nightly-testing * cleanup * unusedSimpArgs * bump toolchain * lake update * Merge master into nightly-testing * Merge master into nightly-testing * chore: adaptations for nightly-2025-07-01 * add adaptation note * add adaptation note * chore: bump to nightly-2025-07-02 * fixes * Merge master into nightly-testing * fixes * update test output * Merge master into nightly-testing * Merge master into nightly-testing * chore: bump to nightly-2025-07-03 * chore: adaptations for nightly-2025-07-03 --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Cameron Zwarich <cameron@lean-fro.org> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Sebastian Graf <sg@lean-fro.org> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>

kmill added the changelog-language Language features and metaprograms label Jun 16, 2025

kmill requested review from Vtec234, kim-em and leodemoura as code owners June 16, 2025 00:12

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jun 16, 2025

kmill force-pushed the kmill_ldecl_nondep branch from 5a5650a to 0b63061 Compare June 18, 2025 17:30

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Jun 18, 2025

Update lean-toolchain for testing leanprover/lean4#8804

65b3924

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jun 18, 2025

Update lean-toolchain for testing leanprover/lean4#8804

1dd9eb0

ghost added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Jun 18, 2025

kmill mentioned this pull request Jun 20, 2025

refactor: avoid using LocalDecl constructors directly leanprover-community/quote4#87

Merged

kmill mentioned this pull request Jun 20, 2025

refactor: avoid using LocalDecl constructors directly leanprover-community/aesop#235

Merged

leodemoura reviewed Jun 22, 2025

View reviewed changes

nomeata reviewed Jun 22, 2025

View reviewed changes

kmill added 5 commits June 22, 2025 14:26

fix handling of lets in WF after discussion with Joachim

106dd1f

address Leo's comments

e9eaba7

Joachim review

e4c4576

fix changes to Lean/Elab/Binders after rebase

2f02cad

kmill force-pushed the kmill_ldecl_nondep branch from 8c4d1cf to 2f02cad Compare June 22, 2025 21:40

kmill added this pull request to the merge queue Jun 22, 2025

Merged via the queue into leanprover:master with commit 02c8c2f Jun 22, 2025
15 checks passed

kmill mentioned this pull request Jun 24, 2025

feat: optimized simp routine for let telescopes #8968

Merged

Conversation

kmill commented Jun 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ghost commented Jun 16, 2025 • edited by ghost Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

nomeata left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

kmill commented Jun 16, 2025 •

edited

Loading

ghost commented Jun 16, 2025 •

edited by ghost

Loading

kmill commented Jun 22, 2025 •

edited

Loading