aesop failure

Stream: Infinity-Cosmos

[Emily Riehl]

A recent bump of mathlib broke the following proof in the file CoherentIso:

/-- From an isomorphism in a category, one can build a functor out of `WalkingIso` to
that category.-/
def fromIso {X Y : C} (e : X ≅ Y) : WalkingIso ⥤ C where
  obj := fun
    | zero => X
    | one => Y
  map := @fun
    | zero, zero, _ => 𝟙 _
    | zero, one,  _ => e.hom
    | one,  zero, _ => e.inv
    | one,  one,  _ => 𝟙 _

The error reads could not synthesize default value for field 'map_comp' of 'CategoryTheory.Functor' using tactics. I fixed this with a horrible case split

  map_comp := by
    intro X Y Z f g
    match X, Y, Z with
    | zero, zero, zero => simp
    | zero, zero, one => simp
    | zero, one, zero => simp
    | zero, one, one => simp
    | one, zero, zero => simp
    | one, zero, one => simp
    | one, one, zero => simp
    | one, one, one => simp

but surely there's a better way?

[Kevin Buzzard]

How far does aesop_cat get? The proof you post looks like the kind of thing aesop or aesop_cat would find; it does intro and cases and simp, in fact this is exactly the kind of thing it does (so I'm slightly surprised that it can't find this proof).

If you can be bothered, you can debug in the following way; checkout a commit of the repo before the bump where things were working, prove map_comp with whatever the default tactic is (presumably aesop_cat?) and then use show_term to see what proof it discovered. Does the same proof still work after the bump?

[Joël Riou]

We can instruct Lean how to do the case split:

  map_comp := by rintro (_ | _) (_ | _) (_ | _) _ _ <;> simp

[Joël Riou]

It could be interesting to report this breakage to the authors of theaesop tactic.

[Matthew Ballard]

I guess grind is still a WIP?

[Nick Ward]

Possibly unrelated, but the bump also seems to have affected build times. In particular, lake build at 0745a95 tries to rebuild most of mathlib, while time lake build at 9aaaa34(before the bump) takes about 2 minutes.

[Dean Young]

(deleted)

[Kevin Buzzard]

Oh that is the known cache issue which won't be fixed until rc2: see e.g. the "Updating to 4.15.0" thread in #general

[Emily Riehl]

Is this "Updating to 4.15.0" something I need to pay attention to/understand as a maintainer of a lean project?

[Kim Morrison]

The only thing you need to know is --- please do not attempt to update projects downstream of Mathlib to v4.16.0-rc1. Either update to v4.15.0, or wait until v4.16.0-rc2 is released.

[Pietro Monticone]

@Emily Riehl Fixed it by downgrading from v4.16.0-rc1 to v4.15.0.