PANIC

Stream: lean4

[Kevin Buzzard]

Is this supposed to happen?

PANIC.png I'm on yesterday's mathlib4. And there's a gazillion lines of

...

/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_elabMutualDef_go___lambda__1+0xbe3)[0x7f3f8df5d513]
/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_elabMutualDef_go___lambda__1___boxed+0xbd)[0x7f3f8df5f48d]
/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/../lib/lean/libleanshared.so(lean_apply_5+0x32e)[0x7f3f8e5b681e]
/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/../lib/lean/libleanshared.so(l_Lean_Meta_withLCtx___at___private_Lean_Elab_Match_0__Lean_Elab_Term_withToClear___spec__25___rarg+0x4f)[0x7f3f8d72db1f]
/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_withUsed___rarg+0x325)[0x7f3f8df16625]
/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_elabMutualDef_go___lambda__2+0x5ef)[0x7f3f8df5ef3f]
/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_elabMutualDef_go___lambda__3+0xbf7)[0x7f3f8df600e7]
/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/../lib/lean/libleanshared.so(lean_apply_8+0x5e8)[0x7f3f8e5b8f68]
/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_withFunLocalDecls_loop___rarg+0x311)[0x7f3f8df0d591]
/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_withFunLocalDecls_loop___rarg___lambda__1+0x78)[0x7f3f8df0d228]
/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/../lib/lean/libleanshared.so(lean_apply_8+0x57b)[0x7f3f8e5b8efb]
/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withAuxDecl___rarg___lambda__1+0x269)[0x7f3f8df905b9]

[Kevin Buzzard]

Sorry, this should be in #lean4 I guess. Can someone move it? I don't think I can? Panic just happened again -- am getting a lot of them in this file. I'll just start a new thread with a possible repro

[Kevin Buzzard]

Here I can reliably get a PANIC by e.g. deleting a and b.

Lean server printed an error: PANIC at Lean.MetavarContext.getDecl Lean.MetavarContext:395:17: unknown metavariable backtrace:

STDERR is

...
/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_withFunLocalDecls_loop___rarg+0x311)[0x7f138a3bd591]
/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_withFunLocalDecls_loop___rarg___lambda__1+0x78)[0x7f138a3bd228]
/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/../lib/lean/libleanshared.so(lean_apply_8+0x57b)[0x7f138aa68efb]
/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withAuxDecl___rarg___lambda__1+0x269)[0x7f138a4405b9]

I tried redownloading oleans but this didn't seem to fix the problem for me. Can anyone else reproduce?

[Notification Bot]

This topic was moved here from #general > PANIC by Eric Wieser.

[Kyle Miller]

I seem to be getting different error:

$ lake build Mathlib.CategoryTheory.Bicategory.Functor
[... skipping output ...]
./././Mathlib/CategoryTheory/Bicategory/Functor.lean:302:25: error: type mismatch
  fun a b f ↦ ?m.46768 a b f
has type
  (a : a✝ ⟶ b✝) →
    (b : ?m.46765 a) → (f : ?m.46766 a b) → ?m.46767 a b f : Sort (imax (v₁ + 1) ?u.46756 ?u.46759 ?u.46762)
but is expected to have type
  ∀ (f : a✝ ⟶ b✝),
    PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} ↦ PrelaxFunctor.map₂ src✝ } (λ_ f).hom =
      (fun {a b c} f g ↦ ?m.46600 f g) (𝟙 a✝) f ≫
        (fun a ↦ ?m.46582 a) a✝ ▷
            Prefunctor.map (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} ↦ PrelaxFunctor.map₂ src✝ }) f ≫
          (λ_
              (Prefunctor.map (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} ↦ PrelaxFunctor.map₂ src✝ })
                f)).hom : Prop
the following variables have been introduced by the implicit lambda feature
  a✝ : B
  b✝ : B
you can disable implict lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.
./././Mathlib/CategoryTheory/Bicategory/Functor.lean:304:46: error: unknown identifier 'map_comp_naturality_left_assoc'
./././Mathlib/CategoryTheory/Bicategory/Functor.lean:310:2: error: using 'exit' to interrupt Lean
error: external command `/home/kmill/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/lean` exited with code 1

[Kevin Buzzard]

Right -- you compile and you get that error, which says "delete a and b from the line I flagged" and when I delete them it panics

[Eric Wieser]

Did you try using @fun a b f instead of deleting a and b?

[Kyle Miller]

Oh right, I did read that part of your message but forgot to make the edit. I'm still getting a different error. I edited both lines 302 and 306

./././Mathlib/CategoryTheory/Bicategory/Functor.lean:304:46: error: unknown identifier 'map_comp_naturality_left_assoc'
./././Mathlib/CategoryTheory/Bicategory/Functor.lean:308:47: error: unknown identifier 'map_comp_naturality_right_assoc'
./././Mathlib/CategoryTheory/Bicategory/Functor.lean:310:2: error: using 'exit' to interrupt Lean
error: external command `/home/kmill/.elan/toolchains/leanprover--lean4---nightly-2023-02-10/bin/lean` exited with code 1

[Dan Velleman]

Any progress on this? I am also getting strange errors on nightly-2023-02-10.

[Kevin Buzzard]

My PANIC issue is still an issue but I have evidence that it's being caused by using aesop in category theory instead of aesop_cat, and I can't reproduce; I just get the error a lot when I'm editing a file, but restarting Lean always fixes it.

[Dan Velleman]

The following proof works:

example (P Q : Prop) : P ∧ Q → Q ∧ P := by
  intro (⟨h1, h2⟩ : P ∧ Q)
  show Q ∧ P; exact And.intro h2 h1
  done

Now, suppose I decide to edit the intro line. If I delete the P ∧ Q) at the end of that line, I get a PANIC at Lean.Expr.mvarId!. I don't know how to tell what's causing it.

Sorry this example is so strange--it took me a while to find a MWE that consistently causes this.

[Dan Velleman]

I'm using leanprover/lean4:nightly-2023-03-07.