A specific file triggers rpc errors

Stream: mathlib4

[Joël Riou]

When I open the file Mathlib.CategoryTheory.Abelian.Refinements (current mathlib master branch) in VSCode, it becomes very unstable: when I try to see the details of a proof, the infoview would always show "Error updating: Error fetching goals: Rpc error: InternalError: parenthesize: uncaught backtrack exception. ". Does anyone see the same problem when opening this file? If this is reproducible, would anyone know how to fix the bug?

[Matthew Ballard]

Odd behavior on nvim also. I am missing the state on some (most) proof lines. The exception seems to be goals accomplished messages.

[Matthew Ballard]

Apparently {S₁ S₂ : ShortComplex C} are not used?

[Matthew Ballard]

Here is something I have not seen yet [error when printing message: parenthesize: uncaught backtrack exception]

[Matthew Ballard]

Here is a statement with the error:

lemma epi_iff_surjective_up_to_refinements (f : X ⟶ Y) (A : C) (y : A ⟶  Y):
      ∃ (A' : C) (π : A' ⟶  A) (h : Epi π) (x : A' ⟶  X), True := by --π ≫ y = x ≫ f := by

[Matthew Ballard]

It goes away if you remove Mathlib.Algebra.Homology.ShortComplex.Exact from the imports

[Joël Riou]

Thanks. A more minimal example is as follows:

import Mathlib.CategoryTheory.EpiMono
import Mathlib.Util.Delaborators

open CategoryTheory

variable {C : Type*} [Category C] {A X Y : C} (f : X ⟶ Y) (y : A ⟶ Y)

lemma test1 : ∃ (A' : C) (π : A' ⟶ A) (x : A' ⟶ X), π ≫ y = x ≫ f := by
  sorry

lemma test2 : ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f := by
  sorry /- Error updating: Error fetching goals: Rpc error:
    InternalError: parenthesize: uncaught backtrack exception.-/

Removing the import to Mathlib.Util.Delaborators makes test2 work.

[Matthew Ballard]

You beat me :)

[Mauricio Collares]

The same issue (I think) is being discussed in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/doc-gen4.20missing.20declaration

[Kyle Miller]

Minimaler example:

import Mathlib.Util.Delaborators

theorem test1 : ∃ (_ : True), True := by
  sorry

theorem test2 : ∃ (_ : True) (x : Nat), True := by
  sorry /- Error updating: Error fetching goals: Rpc error:
    InternalError: parenthesize: uncaught backtrack exception.-/

[Kyle Miller]

#8070 fixes Joël's example

[Patrick Massot]

Did you also try with exists_ne_mem_inter_of_not_pairwise_disjoint?

[Matthew Ballard]

It does.