PANIC at Lean.Expr.appArg! application expected

Stream: lean4

[Floris van Doorn]

When updating the Carleson project to the latest version, I get a few hundred panics, both in CI and locally:

PANIC at Lean.Expr.appArg! Lean.Expr:896:15: application expected

See e.g. the Build Project step in this run: https://github.com/fpvandoorn/carleson/actions/runs/10279969927/job/28446338121

It seems to be related to docs#Nat.reducePow

[Jeremy Tan]

It probably has to do with simps and simpas. Apply the following diff to my PR https://github.com/fpvandoorn/carleson/pull/109 and run lake build Carleson.Defs; there will be no panic

out.diff

[Jeremy Tan]

diff --git a/Carleson/Defs.lean b/Carleson/Defs.lean
index 320f371..c70e04f 100644
--- a/Carleson/Defs.lean
+++ b/Carleson/Defs.lean
@@ -471,13 +471,13 @@ lemma Θ.finite_and_mk_le_of_le_dist {x₀ : X} {r R : ℝ} {f : Θ X} {k : ℕ}
   simp_rw [Cardinal.mk_fintype, Finset.coe_sort_coe, Fintype.card_coe]
   norm_cast
   classical calc
-    _ = ∑ _ ∈ 𝓩, 1 := by simp
+    _ = ∑ _ ∈ 𝓩, 1 := by rw [Finset.sum_const, smul_eq_mul, mul_one]
     _ ≤ ∑ u ∈ 𝓩, (g u).card := Finset.sum_le_sum fun z hz ↦ Finset.card_pos.mpr (g_ne z hz)
     _ = (𝓩.biUnion g).card := (Finset.card_biUnion (fun z hz z' hz' ↦ g_pd hz hz')).symm
     _ ≤ 𝓩'.card := by
       refine Finset.card_le_card fun _ h ↦ ?_
       rw [Finset.mem_biUnion] at h
-      exact Finset.mem_of_subset (by simp [g]) h.choose_spec.2
+      exact Finset.mem_of_subset (by simp only [Finset.filter_subset, g]) h.choose_spec.2
     _ ≤ (2 ^ a) ^ k := c𝓩'
     _ ≤ _ := by rw [C2_1_1, mul_comm, pow_mul]

@@ -487,4 +487,4 @@ lemma Θ.card_le_of_le_dist {x₀ : X} {r R : ℝ} {f : Θ X} {k : ℕ}
     Nat.card 𝓩 ≤ C2_1_1 k a := by
   obtain ⟨f𝓩, c𝓩⟩ := finite_and_mk_le_of_le_dist h𝓩 h2𝓩
   lift 𝓩 to Finset (Θ X) using f𝓩
-  simpa using c𝓩
+  simpa only [Nat.card_eq_fintype_card, Cardinal.mk_fintype, Nat.cast_le] using c𝓩

[Jeremy Tan]

But revert any one of the three changes and a panic will appear. Even more tellingly, running simp(a)? on the three simp(a)s in question suggests the useless lemma defaultA in each case

[Jeremy Tan]

Attached is the panic obtained by leaving out the first change
panic-out.txt

[Sebastian Ullrich]

Is it possible the subterm matching (_ ^ _ : Nat) is merely defeq to hPow applied to two arguments but not structurally so?

[Jeremy Tan]

@Sebastian Ullrich here's the smallest I've got the panic to so far

import Mathlib.Data.Finset.Card

class CompatibleFunctions (X : ℕ) (A : outParam ℕ) where
  Θ : Type*

export CompatibleFunctions (Θ)

@[simp] abbrev defaultA (a : ℕ) : ℕ := 2 ^ a

variable {X : ℕ} [CompatibleFunctions X (defaultA 4)]

/-- PANIC -/
lemma Θ.panic {𝓩 : Finset (Θ X)} : 𝓩.card = 𝓩.card * 1 := by simp

[Jeremy Tan]

If you change the abbrev to def the panic goes away

[Jeremy Tan]

Or Finset to List (and card to length), or ^ to *

[Sebastian Ullrich]

Thanks, that matches my hypothesis exactly

[Jeremy Tan]

Simpler:

import Mathlib.Data.Multiset.Basic

class G (A : outParam ℕ) where Z : Type*

export G (Z)

@[simp] abbrev f (a : ℕ) : ℕ := 2 ^ a

variable [G (f 1)]

example {s : Multiset Z} : Multiset.card s = Multiset.card s := by simp

[Jeremy Tan]

The panic now goes away upon changing 1 to 0

[Eric Wieser]

Looks like a missing unless e.isAppOfArity declName arity do return .continue, which is present on the other binary operator reductions

[Henrik Böving]

I guess doing a let_expr based match would be fine as well.

[Jeremy Tan]

Eric Wieser said:

Looks like a missing unless e.isAppOfArity declName arity do return .continue, which is present on the other binary operator reductions

but where would that go in the lean4 repo?

[Eric Wieser]

On the first line of Nat.reducePow, to match Nat.reduceBin

[Eric Wieser]

Henrik Böving said:

I guess doing a let_expr based match would be fine as well.

Or let ~q() :wink:

[Jeremy Tan]

Yeah, I've got an #mwe

universe u

class G (A : outParam Nat) where Z : Type u

export G (Z)

abbrev f (a : Nat) : Nat := 2 ^ a

variable [G (f 0)]

example {s : Z} : s = s := by simp only [Nat.reducePow]

[Jeremy Tan]

Filed at https://github.com/leanprover/lean4/issues/4947

[Jeremy Tan]

It sure seems to me that this is a regression from lean4#4637

[Matthew Ballard]

Eric Wieser said:

Looks like a missing unless e.isAppOfArity declName arity do return .continue, which is present on the other binary operator reductions

Indeed this fixes it.

[Jeremy Tan]

Matthew Ballard said:

Indeed this fixes it.

I tried fixing it myself. I couldn't find the right line to put that

[Matthew Ballard]

https://github.com/leanprover/lean4/blob/daa22187642d4cf6954c39a23eab20d8a8675416/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean#L58

[Matthew Ballard]

Then you probably want to a make your example into a test that fails before the fix and passes afterwards

[Jeremy Tan]

declName and arity don't appear in the variables

[Matthew Ballard]

You need to specialize them to the existing situation HPow.hPow and 6

[Jeremy Tan]

Matthew Ballard said:

You need to specialize them to the existing situation HPow.hPow and 6

I added a file 9999.lean to lean4/tests/lean with my example but how do I run it?

[Jeremy Tan]

Which directory do I have to be in and what command must I give

[Jeremy Tan]

wait...

[Kim Morrison]

@Jeremy Tan see https://lean-lang.org/lean4/doc/dev/testing.html for running tests.

[Kim Morrison]

(If you find problems in the test docs please let us know!)

[Jeremy Tan]

(deleted)

[Jeremy Tan]

@Kim Morrison I've got a diff ready. Should I fork and PR or have you accept me into the lean4 org and then PR?

[Jeremy Tan]

out.diff

[Jeremy Tan]

how should I title my PR anyway?

[Jeremy Tan]

@Kim Morrison https://github.com/leanprover/lean4/pull/4968

[Jeremy Tan]

Should I rebase onto nightly-with-mathlib? OK, rebased

[Jeremy Tan]

Is there anything I have done wrong with my PR?

[Sebastian Ullrich]

@Jeremy Tan Looks good to me. Could you move the test into run/? Then you don't need the empty expected file

[Jeremy Tan]

Sebastian Ullrich said:

Jeremy Tan Looks good to me. Could you move the test into run/? Then you don't need the empty expected file

done

[Eric Wieser]

Jeremy Tan said:

It sure seems to me that this is a regression from lean4#4637

I left some comments on this PR; it's not clear to me that this is effective at preventing blowups on large powers

[Jeremy Tan]

Anyway I tried the rebase command suggested but still no Batteries/mathlib CI

[Kim Morrison]

I will try to have a look at the CI next week. My first guess is that we are running into GitHub API rate limits. This has been a known problem (not specific to this step, but all over our infrastructure) for a couple of weeks now.

[Jeremy Tan]

@Floris van Doorn For now I have silenced the panics in my https://github.com/fpvandoorn/carleson/pull/109 by adding attribute [-simp] Nat.reducePow at the start of 9 files

[Jeremy Tan]

Eric Wieser said:

I left some comments on this PR; it's not clear to me that this is effective at preventing blowups on large powers

Do you have code where it still blows up on large powers?

[Kim Morrison]

@Jeremy Tan, you aren't meant to change the PR target to nightly-with-mathlib (as you did, and Sebastian changed back), but rather rebase using git rebase -i origin/nightly-with-mathlib. Could you try this?

[Jeremy Tan]

@Kim Morrison I did that, but Leo has already pushed a fix (lean4#4988)

[Jeremy Tan]

The tag is still not showing up in mathlib

[Kim Morrison]

Jeremy Tan said:

The tag is still not showing up in mathlib

What do you mean?

[Jeremy Tan]

@Kim Morrison OK, I think I've got it right with lean4#5011

[Jeremy Tan]

then why did I get this out of the blue failure? https://github.com/leanprover/lean4/actions/runs/10368758759/job/28703042712

[Joachim Breitner]

This happens ocasionally, haven’t debugged yet when this happens. You can ignore it, not your PR’s fault. Maybe something with github rate limits or so.

[Jeremy Tan]

jq: error (at <stdin>:5): Cannot index string with string "body"

[Joachim Breitner]

This is from

              existing_comment="$(curl -L -s -H "Authorization: token ${{ secrets.MATHLIB4_BOT }}" \
                                      -H "Accept: application/vnd.github.v3+json" \
                                      "https://api.github.com/repos/leanprover/lean4/issues/${{        steps.workflow-info.outputs.pullRequestNumber }}/comments" \
                                      | jq 'first(.[] | select(.body | test("^- . Mathlib") or         startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-mathlib4-bot"))')"
              existing_comment_id="$(echo "$existing_comment" | jq -r .id)"
              existing_comment_body="$(echo "$existing_comment" | jq -r .body)"

and I have been staring at this point wondering how in echo "$existing_comment" | jq -r .body it can be that jq receives a string literal (and not either a json object or nothing). :shrug:
Maybe I should add some debugging output there

[Eric Wieser]

Maybe rate limits are returned as a single string?

[Henrik Böving]

Yeah we've been seeing rate limits on the mathlib4 community bot in a lot of runs recently @Joachim Breitner