Zulip Chat Archive

Stream: mathlib4

Topic: Goal state not updating, bugs, etc.

Adam Topaz (Feb 23 2023 at 18:02):

I've ported quite a few files from category theory in the last few days, and I'm finding the user experience to be quite terrible in some cases.
The main issue I am facing is situations where the goal state is simply not updating, and I have to restart the lean4 server to see the updates. It seems that there are some errors popping up, but I don't know where they are coming from. I recorded a video of me trying to prove something very simple which would have taken less than 5 seconds in lean3, but these UX issues are just making it a very annoying experience.

I don't know where to start diagnosing these issues. Any ideas?

Peek-2023-02-23-10-58.mp4

Matthew Ballard (Feb 23 2023 at 18:03):

Do you have a bunch of orphaned lean processes?

Adam Topaz (Feb 23 2023 at 18:03):

I dont' know

Adam Topaz (Feb 23 2023 at 18:04):

Let me convert that video to a GIF that I can embed, one sec

Sebastian Ullrich (Feb 23 2023 at 18:04):

Could you please post the entire error message here, as text?

Adam Topaz (Feb 23 2023 at 18:04):

output.gif

Adam Topaz (Feb 23 2023 at 18:05):

@Sebastian Ullrich it's huge.

Adam Topaz (Feb 23 2023 at 18:05):

but I can do it

Sebastian Ullrich (Feb 23 2023 at 18:05):

It will probably repeat, you can try to isolate a single instance

Sebastian Ullrich (Feb 23 2023 at 18:06):

E.g. from the first line to the first empty line, hopefully

Adam Topaz (Feb 23 2023 at 18:07):

The error in the infoview is 

invalid occurrence of universe level 'u_1' at 'CategoryTheory.MonoidalNatIso.ofComponents', it does not occur at the declaration type, nor it is explicit universe level provided by the user, occurring at expression
  sorryAx.{u_1}
    (Eq.{(max u₁ v₂) + 1}
      (CategoryStruct.comp.{max u₁ v₂, max (max (max u₁ u₂) v₁) v₂}
        (let src := (NatIso.ofComponents.{v₁, v₂, u₁, u₂} app naturality').inv;
        MonoidalNatTrans.mk.{v₁, v₂, u₁, u₂} (NatTrans.mk.{v₁, v₂, u₁, u₂} fun X => (app X).inv))
        (MonoidalNatTrans.mk.{v₁, v₂, u₁, u₂} (NatTrans.mk.{v₁, v₂, u₁, u₂} fun X => (app X).hom)))
      (CategoryStruct.id.{max u₁ v₂, max (max (max u₁ u₂) v₁) v₂} G))
at declaration body
  fun {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D]
      {F G : LaxMonoidalFunctor C D}
      (app : (X : C) → Prefunctor.obj F.toFunctor.toPrefunctor X ≅ Prefunctor.obj G.toFunctor.toPrefunctor X)
      (naturality' :
        ∀ {X Y : C} (f : X ⟶ Y),
          Prefunctor.map F.toFunctor.toPrefunctor f ≫ (app Y).hom =
            (app X).hom ≫ Prefunctor.map G.toFunctor.toPrefunctor f)
      (unit' : F.ε ≫ (app (𝟙_ C)).hom = G.ε)
      (tensor' :
        ∀ (X Y : C),
          LaxMonoidalFunctor.μ F X Y ≫ (app (X ⊗ Y)).hom = ((app X).hom ⊗ (app Y).hom) ≫ LaxMonoidalFunctor.μ G X Y) =>
    Iso.mk (MonoidalNatTrans.mk (NatTrans.mk fun (X : C) => (app X).hom))
      (let src : G.toFunctor ⟶ F.toFunctor := (NatIso.ofComponents app naturality').inv;
      MonoidalNatTrans.mk (NatTrans.mk fun (X : C) => (app X).inv))

Adam Topaz (Feb 23 2023 at 18:07):

but there are further errors in stderror

Adam Topaz (Feb 23 2023 at 18:09):

stderr

Adam Topaz (Feb 23 2023 at 18:10):

I had to truncate that error quite a bit because zulip only lets me send 10000 characters at a time :rofl:

Adam Topaz (Feb 23 2023 at 18:11):

here is the full trace:
https://gist.githubusercontent.com/adamtopaz/7e9399049af7962e7d07a570c706c44b/raw/424d0a28dd92899c6982f2a78700af9dfe32cfe4/error.txt

Matej Penciak (Feb 23 2023 at 18:12):

I've run into these same issues as well! It's weird because I seem to only run into them in ports of the CategoryTheorypart of the library.

Adam Topaz (Feb 23 2023 at 18:13):

I wonder if it has to do with aesop (specifically the aesop_cat we use for the autoparams)?

Adam Topaz (Feb 23 2023 at 18:17):

The video above also highlights the fact that ext is not as strong as it used to be, but I think that's a separate issue

Matthew Ballard (Feb 23 2023 at 18:24):

I crash often in vim leaving a bunch of orphaned processes. Clearing those significantly speeds me up. This may not be a generalizable though.

Matthew Ballard (Feb 23 2023 at 18:27):

I found CategoryTheory.PEmpty to be very taxing on the infoview despite being so short

Matthew Ballard (Feb 23 2023 at 18:29):

#lean4 > PANIC is relevant

Matthew Ballard (Feb 23 2023 at 18:30):

Purely wild speculation: universe unification is expensive for some reason

Adam Topaz (Feb 23 2023 at 18:31):

My completely uninformed opinion would agree with you... it seems that lean is just refusing to unify u_1 in sorryAx.{u_1} (whatever that means) with the correct universe level.

Jannis Limperg (Feb 23 2023 at 18:38):

It's certainly possible that Aesop is somehow messing up the universes. Could you point me to a file where this happens, preferably a small one?

Matthew Ballard (Feb 23 2023 at 18:39):

I am not sure aesop is the culprit but CategoryTheory.PEmpty is about ~50 lines but I had to fight to finish it

Adam Topaz (Feb 23 2023 at 18:39):

@Jannis Limperg the file I was working on is this one: https://github.com/leanprover-community/mathlib4/blob/0048499e13503ec9d09b42cb4fde0ff546dc51df/Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean

Adam Topaz (Feb 23 2023 at 18:39):

But PEmpty will probably be easier to go through

Adam Topaz (Feb 23 2023 at 18:41):

Adam Topaz said:

Jannis Limperg the file I was working on is this one: https://github.com/leanprover-community/mathlib4/blob/0048499e13503ec9d09b42cb4fde0ff546dc51df/Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean

This is the port/CategoryTheory.Monoidal.NaturalTransformation branch of mathlib4

Jannis Limperg (Feb 23 2023 at 18:42):

Thanks, I'll have a look.

Matej Penciak (Feb 23 2023 at 23:02):

A potentially interesting additional data point: I was running into the same issue of the goal state not updating in the CategoryTheory.Quotient (!4#2339) port, and what I was able to do was explicitly add sorry to all the declarations aesop_cat was trying to fill by default (In this case the id_comp, comp_id, and assoc fields for Category). Then going in and filling each declaration by hand, I didn't run into any issues with the goal state anymore

Jannis Limperg (Feb 27 2023 at 14:26):

I've looked at the PEmpty file now, see !4#2519. Aesop was weak because it was missing some straightforward rules about PEmpty and Discrete.

The infoview slowness is probably just a performance issue, but I'm not sure how to address it. In emptyEquivalence, aesop_cat is called 16 times. Many of these calls take between 100 and 380ms on my machine for a total of 2665ms. And Lean re-elaborates the whole definition every time you change something, so it's not exactly pleasant to work on. The runtime of each Aesop call is completely dominated by simp, so I guess it's time to finally think about how to properly cache the simp calls during normalisation.

I'll take a look at the NaturalTransformation file now.

Jannis Limperg (Feb 27 2023 at 14:27):

Btw you can set_option trace.aesop.profile if you suspect that Aesop is slow.

Adam Topaz (Feb 27 2023 at 14:33):

I don't think slowness was my main issue, but rather that the goal state didn't update, no matter how long I waited, until I restarted the lean4 server.

Adam Topaz (Feb 27 2023 at 14:55):

I'm curious why your PR has this line 

@[ext, aesop safe cases (rule_sets [CategoryTheory])]

for Discrete, given that we already had

attribute [aesop safe tactic (rule_sets [CategoryTheory])] Std.Tactic.Ext.extCore'`

Adam Topaz (Feb 27 2023 at 14:56):

Am I misunderstanding how ext and/or aesop works?

Matthew Ballard (Feb 27 2023 at 14:56):

I think if you want to use it with ext too

Matthew Ballard (Feb 27 2023 at 14:57):

My understanding that is that aesop_cat should be finishing, but it would be nice to confirm that

Matthew Ballard (Feb 27 2023 at 14:58):

(I need an aesop tutorial...)

Matthew Ballard (Feb 27 2023 at 15:00):

Adam Topaz said:

I'm curious why your PR has this line 

@[ext, aesop safe cases (rule_sets [CategoryTheory])]

for Discrete, given that we already had

attribute [aesop safe tactic (rule_sets [CategoryTheory])] Std.Tactic.Ext.extCore'`

Can we move this to a separate topic for just asking how to do X with aesop? I have questions...

Matthew Ballard (Feb 27 2023 at 15:08):

Matthew Ballard said:

I think if you want to use it with ext too

Sorry now I am confused too

Matthew Ballard (Feb 27 2023 at 15:10):

But just @[ext] doesn't seem to have informed aesop of the existence of lemmas in a few cases I have seen

Jannis Limperg (Feb 27 2023 at 15:11):

What does ext usually do? I don't actually know. :innocent:

Matthew Ballard (Feb 27 2023 at 15:14):

In general I am not sure but most of the examples I see are like funext

Jannis Limperg (Feb 27 2023 at 15:14):

Okay, it just applies extensionality lemmas to the target. The cases rule splits hypotheses of Discrete type, which here serves to extract the PEmpty element. Whether this is always the right move I'm not sure.

Jannis Limperg (Feb 27 2023 at 15:17):

Matthew Ballard said:

My understanding that is that aesop_cat should be finishing, but it would be nice to confirm that

Yes afaik. In fact, I'll try to force Aesop to fail when it can't solve the goal. Maybe this solves/works around the universe issue (which I haven't been able to reproduce yet).

Matthew Ballard (Feb 27 2023 at 15:18):

Here is an example I am currently looking at boiled down a bit: 

def Wrapper (J : Type) := Option J
inductive Pair where
| left : Pair
| right : Pair
abbrev SlimWrap : Type := Wrapper Pair

I have a hypothesis of j : SlimWrap in my context but however I tag these with aesop I cannot seem to get cases to fire

Jannis Limperg (Feb 27 2023 at 15:27):

Try to make an norm unfold rule for Wrapper. Maybe also for SlimWrap, though Aesop should be able to see through it. Then a cases rule for Option.

Jannis Limperg (Feb 27 2023 at 15:27):

Or just a cases rule for Wrapper might also work.

Adam Topaz (Feb 27 2023 at 15:30):

I was under the impression that ext is supposed to apply the ext lemma generated by the attribute on Discrete and that aesop is supposed to try to use the tactic ext.

Matthew Ballard (Feb 27 2023 at 15:36):

Here is my attempt at the actual problem !4#2522. In diagramIsoCospan, I cannot case on j.

Jannis Limperg (Feb 27 2023 at 15:37):

Adam Topaz said:

I was under the impression that ext is supposed to apply the ext lemma generated by the attribute on Discrete and that aesop is supposed to try to use the tactic ext.

Yes, but that does not help us with the goals we have in PEmpty. The proofs there all come down to recognising that we have x : Discrete PEmpty in the context, so we also have x' : PEmpty and the goal is trivial. Doing cases on Discrete hypotheses is one way to teach Aesop this. (We could also use less aggressive rules, e.g. a local cases rule or a global rule that concludes PEmpty from Discrete PEmpty.)

Adam Topaz (Feb 27 2023 at 15:41):

Oh ignore me. I missed the fact that this aesop attribute was about cases. I somehow read ext instead :rofl:

Jannis Limperg (Feb 27 2023 at 16:09):

Matthew Ballard said:

Here is my attempt at the actual problem !4#2522. In diagramIsoCospan, I cannot case on j.

I'm really confused by this example actually. Aesop's simp seems to unfold WalkingCospan as desired, but then still leaves it in the post-normalisation goal. Investigating.

Jannis Limperg (Feb 27 2023 at 16:50):

The root cause of this failure to unfold WalkingCospan appears to be that simp_all, which Aesop uses for unfolding, only affects propositional hypotheses. This is by design, but should probably not apply to definitional unfolding. I wanted to refactor the unfolding infrastructure anyway, so I guess that's going to happen now. But it'll take a bit I'm afraid.

Matthew Ballard (Feb 27 2023 at 17:07):

Thanks for taking a look. I can work around it for now.

Matthew Ballard (Feb 27 2023 at 17:08):

Happy to know that I was aesoping correctly

Jannis Limperg (Feb 27 2023 at 18:09):

Regarding the original issue: I could not reproduce the hangs/panics, but I could reproduce the 'unknown universe' error which was presumably responsible for them. This error goes away when we force the auto-param aesop_cats to fail unless they solve the goal. (Previously, they could 'succeed' but leave the goal unsolved.) I'm not sure whether this is really the root issue, but if it unblocks the port I'm happy enough. PR !4#2527. @Adam Topaz could you rebase on top of this PR and test whether you still get hangs?

Matthew Ballard (Feb 27 2023 at 21:24):

I am not sure what the issue with ext that is referred to a few times in the porting notes is actually but I don't think that aesop_cat can replace all of its uses.

Adam Topaz (Feb 27 2023 at 21:34):

@Matthew Ballard what's the issue? I think adding funext to the tactics that aesop_cat tries would go a long way.

Matthew Ballard (Feb 27 2023 at 21:36):

aesop is finishing and ext should not be.

Adam Topaz (Feb 27 2023 at 21:36):

oh I see.

Adam Topaz (Feb 27 2023 at 21:37):

Well, ext can finish in some cases, like if the goal is a = b with a b : PUnit or something

Matthew Ballard (Feb 27 2023 at 21:38):

True, but generally. There were some issues with tagging existing extensionality lemmas with @[ext]. I didn't really pay attention to the errors and followed the existing porting notes. Something about reduced functionality in ext in Lean 4. Let me try to dig something up.

Adam Topaz (Feb 27 2023 at 21:39):

Oh Gabriel explained this somewhere recently.

Adam Topaz (Feb 27 2023 at 21:39):

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ext.2Ffunext/near/329329566

Adam Topaz (Feb 27 2023 at 21:39):

is that what you're referring to?

Matthew Ballard (Feb 27 2023 at 21:40):

Perhaps, but I remember the tag itself erroring

Adam Topaz (Feb 27 2023 at 21:41):

hmmm....

Matthew Ballard (Feb 27 2023 at 21:43):

docs4#CategoryTheory.Iso.inv_ext I think is an example

Matthew Ballard (Feb 27 2023 at 21:45):

@[ext] attribute only applies to structures or lemmas proving x = y, got ?f.inv = ?g

Matthew Ballard (Feb 27 2023 at 21:45):

theorem inv_ext {f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : f.hom ≫ g = 𝟙 X) : f.inv = g

Matthew Ballard (Feb 27 2023 at 21:46):

-- Porting note: `@[ext]` used to accept lemmas like this. Now we add an aesop rule

Matthew Ballard (Feb 27 2023 at 21:46):

(deleted)

Adam Topaz (Feb 27 2023 at 21:47):

It seems that @Mario Carneiro wrote the Lean4 ext attribute. Mario, is there a good reason to disallow such lemmas?

Mario Carneiro (Feb 27 2023 at 21:48):

I think so, that doesn't seem like an ext lemma to me

Mario Carneiro (Feb 27 2023 at 21:49):

I mean it is at best topically related to extensionality

Mario Carneiro (Feb 27 2023 at 21:49):

the old ext was essentially just apply_rules with a more suggestive name

Matthew Ballard (Feb 27 2023 at 21:50):

Link

Mario Carneiro (Feb 27 2023 at 21:51):

I don't think it is a good idea to have ext be nondeterministic / have many options for what it can apply and pick them based on the phase of the moon

Mario Carneiro (Feb 27 2023 at 21:52):

In this example normal extensionality would also clearly be applicable, this is just a slightly simplified form

Matthew Ballard (Feb 27 2023 at 21:52):

It is not terrible to spell out apply Foo.ext in its place which is what I've done up to this point.

Mario Carneiro (Feb 27 2023 at 21:53):

actually it's not even introducing a variable, this is just moving the g to the other side... how is this extensionality?

Mario Carneiro (Feb 27 2023 at 21:53):

I think you should indeed just apply it like a regular theorem, that seems a lot more clear

Adam Topaz (Feb 27 2023 at 21:53):

what about lemmas like docs#category_theory.limits.prod.hom_ext

Adam Topaz (Feb 27 2023 at 21:54):

I think those are in the same spirit as the one Matt mentioned, and IMO are indeed extensionality in the categorical sense

Adam Topaz (Feb 27 2023 at 21:54):

I hope the ext attribute works in this case...

Mario Carneiro (Feb 27 2023 at 21:54):

those look like proper extensionality lemmas

Mario Carneiro (Feb 27 2023 at 21:55):

they should work with ext

Adam Topaz (Feb 27 2023 at 21:55):

so is the issue the fact that the LHS of the problematic lemma involves a function inv?

Mario Carneiro (Feb 27 2023 at 21:55):

the criteria is: it should be proving x = y where the type of x and y is something interesting (and the type of the equality in the hypotheses should be something simpler)

Adam Topaz (Feb 27 2023 at 21:56):

the type of x and y in both cases is the type of morphisms between two objects in a category. Why is one more interesting than the other?

Mario Carneiro (Feb 27 2023 at 21:56):

and x and y should be variables here

Adam Topaz (Feb 27 2023 at 21:56):

okay so that's the issue.

Matthew Ballard (Feb 27 2023 at 21:57):

prod.hom_ext took ext without error --- I think...

Adam Topaz (Feb 27 2023 at 21:57):

that's good. But I can imagine some combination in category theory that would give issues.
Let me try to come up with an example

Mario Carneiro (Feb 27 2023 at 21:58):

Adam Topaz said:

the type of x and y in both cases is the type of morphisms between two objects in a category. Why is one more interesting than the other?

Ideally, it should not overlap with other extensionality lemmas. Is this an equality between two objects in a particular category or an arbitrary one?

Adam Topaz (Feb 27 2023 at 21:58):

arbitrary

Mario Carneiro (Feb 27 2023 at 21:58):

because I would assume that equality between arbitrary morphisms is already covered

Mario Carneiro (Feb 27 2023 at 21:58):

because only the type of the equality is used for the dispatch

Mario Carneiro (Feb 27 2023 at 22:00):

if the type of the equality is already "morphisms in an arbitrary category", then the hypotheses are not simpler than the conclusion

Matthew Ballard (Feb 27 2023 at 22:01):

Equality in Rapper (arbitrary category) from equality in arbitrary category is what I usually find

Mario Carneiro (Feb 27 2023 at 22:01):

that's a good ext lemma

Matthew Ballard (Feb 27 2023 at 22:03):

Adam can probably cook up something more challenging though

Adam Topaz (Feb 27 2023 at 22:13):

Okay, this is a bit cooked up, but here is some lemma that's in between the two lemmas discussed above, and the ext attribute indeed fails here as well.

import Mathlib

open CategoryTheory
variable (C : Type _) [Category C]

structure prod (X Y : C) where
  P : C
  p1 : P ⟶ X
  p2 : P ⟶ Y
  lift : (Z : C) → (f1 : Z ⟶ X) → (f2 : Z ⟶ Y) → Z ⟶ P
  uniq : ∀ Z f1 f2 (g : Z ⟶ P), g ≫ p1 = f1 → g ≫ p2 = f2 → g = lift Z f1 f2

@[ext]
lemma prod_lift_ext (X Y Z : C) (P : prod C X Y)
  (f1 : Z ⟶ X) (f2 : Z ⟶ Y) (g : Z ⟶ P.P)
  (h1 : g ≫ P.p1 = f1) (h2 : g ≫ P.p2 = f2) :
  g = P.lift _ f1 f2 :=
P.uniq Z f1 f2 g h1 h2

Adam Topaz (Feb 27 2023 at 22:14):

I think it's fair to say that the assumptions are simpler than the conclusion in this case.

Adam Topaz (Feb 27 2023 at 22:20):

So if I understand correctly, the error arises in the following line: https://github.com/leanprover/std4/blob/9a43e832fc20cf0b94f5041b9bec70945d409d12/Std/Tactic/Ext/Attr.lean#L64

I'm willing to accept the fact that removing this line would cause issues down the line (if not immediately), but it would be nice to get an explanation of why.

Mario Carneiro (Feb 27 2023 at 22:25):

I don't think this should qualify extensionality lemma, because it is not about arbitrary objects of the type being equal, it is very specifically about destructing P.lift expressions

Mario Carneiro (Feb 27 2023 at 22:26):

This is an induction principle, not an extensionality principle

Mario Carneiro (Feb 27 2023 at 22:29):

This is more of an abstract criterion for categorizing lemmas, it could plausibly be a lint instead because it will probably not actually break the tactic

Mario Carneiro (Feb 27 2023 at 22:29):

although it will probably wastefully try to apply the lemma more than necessary

Adam Topaz (Feb 27 2023 at 23:11):

okay, yes I agree this is an induction and not an extensionality principle.

Adam Topaz (Feb 27 2023 at 23:13):

I don't know why exactly, but I'm a little suspicious about relying on aesop_cat to apply such lemmas. Maybe we can have a separate tactic that applies these "non-extensionality" extensionality lemmas. Applying such things is one of the important aspects of the automation in the category theory library in mathlib3.

Yaël Dillies (Mar 24 2023 at 10:10):

I too am having troubles with the user experience, but I seem to have a somewhat different problem. I am working on !4#2502. I fixed some errors, restarted the server because the infoview wasn't updating. But instead of recompiling the file and giving me new errors to fix, the server recompiled the unmodified file (??)

Sebastian Ullrich (Mar 24 2023 at 10:28):

That's a new one afaik. It's strange, if the server is restarted, it must be the extension sending it the wrong code.

Yaël Dillies (Mar 24 2023 at 10:30):

FWIW, closing and reopening VScode fixed it.

Last updated: Dec 20 2023 at 11:08 UTC