Checking the type class construction for a term

Stream: general

[Yiming Xu]

Say, for

@[ext]
structure Hom (M N : Action V G) where
  hom : M.V ⟶ N.V
  comm : ∀ g : G, M.ρ g ≫ hom = hom ≫ N.ρ g := by aesop_cat

and

structure Action (G : MonCat.{u}) where
  V : V
  ρ : G ⟶ MonCat.of (End V)

They are both \hom, and should be group homomorphisms.

Even if I know they are homomorphisms, I would like to know how can I construct such a term. But in Lean sessions, what can I do to check how is the notions of "group homomorphisms" defined here? Hovering the mouse over them both leads to the quiver stuff only.

[Johan Commelin]

If you hover over them, there should be some implicit argument telling you that MonCat is a quiver. And inside that, an argument that it is a quiver because it is a category. And inside that, an argument that MonCat is a category.

Now, if you click "Go to definition", that will take you to the category structure on MonCat. This will tell you that it is the category of Bundled monoids with monoid homomorphims.

And there you can click on "Go to definition" and go to the mathlib definition of monoid homomorphism.

[Yiming Xu]

Johan Commelin said:

If you hover over them, there should be some implicit argument telling you that MonCat is a quiver. And inside that, an argument that it is a quiver because it is a category. And inside that, an argument that MonCat is a category.

Now, if you click "Go to definition", that will take you to the category structure on MonCat. This will tell you that it is the category of Bundled monoids with monoid homomorphims.

And there you can click on "Go to definition" and go to the mathlib definition of monoid homomorphism.

It does not tell me MonCat is a quiver. See the screenshot:
image.png

May I please ask if there is some setting stuff that I got wrong?

[Yiming Xu]

Same for this one:
image.png

[Johan Commelin]

Aah, yes, at that point it doesn't.
But if you have

variable (M N : MonCat)
example : M \hom N := _ -- put your cursor before the `_`

then in the goal view you can hover over the \hom.

[Johan Commelin]

Sorry. I agree that this is not the easiest UX.

[Johan Commelin]

@Kyle Miller Do you think we could get hover info from the elaborator when hovering over something like \hom in the source? Because there must be some instance floating around (either variable or constant) that makes the elaborator happy when it parses \hom. It would be cool to get easy access to that in all hovers, not just the goal view.

[Yiming Xu]

image.png

[Yiming Xu]

and in goalview:
image.png

[Yiming Xu]

Does it seem to be correct? (There is an error on the red underscore, but I can still see the MonCat stuff.)

[Yiming Xu]

But it does not give me the definition of a homomorphism in MonCat... Let me see if I am in trouble...

[Yiming Xu]

Johan Commelin said:

Aah, yes, at that point it doesn't.
But if you have

variable (M N : MonCat)
example : M \hom N := _ -- put your cursor before the `_`

then in the goal view you can hover over the \hom.

Sorry I think I can still not get hovering to lead me to the definition of the categorical structure of MonCat.

[Yiming Xu]

I tried everything clickable here:
image.png

[Yiming Xu]

Seems not able to reach the definition... I would wish I can do that because finding out the definitions by hand does take long, especially if one do not have a fixed category to work with.

[Johan Commelin]

This looks good. I think you can now drill down deeper by following catToReflQuiver.

[Yiming Xu]

Johan Commelin said:

This looks good. I think you can now drill down deeper by following catToReflQuiver.

This takes me to:

instance catToReflQuiver {C : Type u} [inst : Category.{v} C] : ReflQuiver.{v+1, u} C :=
  { inst with }

[Yiming Xu]

This seems unexpected to me because I would like to see the category construction.

[Yiming Xu]

In the sense that I can see obj are... hom are ... .

[Yiming Xu]

i.e. the explicit fields.

[Yiming Xu]

Or the first place that the instance [Category MonCat] is constructed.

[Johan Commelin]

image.png

[Johan Commelin]

I could get more hovers

[Johan Commelin]

And that final one contains the definition of the category structure on MonCat.

[Johan Commelin]

Can you reproduce this?

[Yiming Xu]

image.png

[Yiming Xu]

But the click brings me to the definition of large category stuff.

[Yiming Xu]

It takes me here:
image.png

[Edward van de Meent]

The right path here goes through instMonCatLargeCategory

[Yiming Xu]

Edward van de Meent said:

The right path here goes through instMonCatLargeCategory

It seems to be non-clickable to me.

[Edward van de Meent]

Go to its definition

[Yiming Xu]

Edward van de Meent said:

Go to its definition

Lean refuses, it says something like "Nodefinition...."

[Yiming Xu]

It shows the message for less than 1 sec so I am not able to take a screenshot.

[Johan Commelin]

Aahrg, is this one of those edge cases, where it is an instance produced by deriving?

[Johan Commelin]

Sorry, you seem to have hit a couple of nasty speedbumps.

[Johan Commelin]

https://github.com/leanprover-community/mathlib4/blob/c9cb88e7c1a95c987df4d3d68dd55f4c90d5bf11/Mathlib/Algebra/Category/MonCat/Basic.lean#L53-L53

[Yiming Xu]

Nothing to sorry about and thanks very much for all the elaboration!

[Yiming Xu]

Do you mean that this case is not normal?

[Johan Commelin]

Line 41 of that file shows you MonoidHom. You can click on that, and find the definition of monoid homs.

[Yiming Xu]

Is there is a "normal case" that I can try the hovering trick?

[Johan Commelin]

Yes, I think it started out normal, but then you hit some speedbumps.

[Johan Commelin]

Write

#check 3 + 4 = 5

then you get
image.png

[Yiming Xu]

Johan Commelin said:

https://github.com/leanprover-community/mathlib4/blob/c9cb88e7c1a95c987df4d3d68dd55f4c90d5bf11/Mathlib/Algebra/Category/MonCat/Basic.lean#L53-L53

I find this:

@[to_additive]
structure MonoidHom (M : Type*) (N : Type*) [MulOneClass M] [MulOneClass N] extends
  OneHom M N, M →ₙ* N

following the MonoidHom in the link.

So does the problem actually comes from the fact that the instance MonCat is a category is never written out explicitly?

[Johan Commelin]

That should be an example of the normal case. Where you can find out what the addition is on Nat.

[Yiming Xu]

Johan Commelin said:

That should be an example of the normal case. Where you can find out what the addition is on Nat.

It takes me to this:

instance instAddNat : Add Nat where
  add := Nat.add

Seems great.

[Kyle Miller]

Johan Commelin said:

Kyle Miller Do you think we could get hover info from the elaborator when hovering over something like \hom in the source? Because there must be some instance floating around (either variable or constant) that makes the elaborator happy when it parses \hom. It would be cool to get easy access to that in all hovers, not just the goal view.

That information should be there already, and it's a matter of whether the hovers themselves are showing this information. If I remember correctly, the hover code intentionally only shows the term if it's a constant. I think that's because most of the time you would rather have the hover be compact, and the type is the most commonly useful information. It's also useful knowing which constant an identifier resolved to.

(@Marc Huisinga does VS Code have any interactions that could be used to ask a hover to show a more detailed version? I know you can click on hovers to "activate" them for example, which makes them stick around even if you move your mouse — can these activated hovers have UI features like a checkbox to make the current hover detailed? Is there such a thing as a document hover that's hoverable?)

[Marc Huisinga]

You could use a subset of HTML if we were to enable it to do this, but the VS Code UX for hovers that can change their content is pretty bad: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Showing.20two.20doc-string

[Kyle Miller]

Thanks @Marc Huisinga. What do you think about having something like set_option hovers.alwaysShowValues true that would make hovers show values, default false? This would have been useful to have around for debugging in a number of cases.

[Julian Berman]

It's worth looking at rust-analyzer I think if that hasn't been done already. I don't know how it looks in VSCode probably the same?, but in Neovim rust-analyzer's (really rustaceanvim)'s hovers are clickable / contain hover actions!

[Julian Berman]

Specifically they look like this:

Screenshot 2024-11-23 at 14.29.38.png

[Marc Huisinga]

Kyle Miller said:

Thanks Marc Huisinga. What do you think about having something like set_option hovers.alwaysShowValues true that would make hovers show values, default false? This would have been useful to have around for debugging in a number of cases.

I think that an obscure config option isn't much of an improvement over the current situation. It's also worth keeping in mind that these terms in the editor hover panel will not be interactive.

[Marc Huisinga]

Julian Berman said:

It's worth looking at rust-analyzer I think if that hasn't been done already. I don't know how it looks in VSCode probably the same?, but in Neovim rust-analyzer's (really rustaceanvim)'s hovers are clickable / contain hover actions!

You can make VS Code hovers have clickable markdown links that execute VS Code commands, but I'm not sure if that is much of a help here.

[Kyle Miller]

The current situation is that I can only find the elaborated value of a term by indirect methods, perhaps doing #print and hoping I can find the subterm that corresponds to what I'm interested in, but with a debug option like this I would be able to directly locate the term. This would really help debugging elaboration issues, even if the terms aren't themselves hoverable.

[Marc Huisinga]

Sure, I wouldn't mind an option like this as a tool for debugging elaborators, but I'm skeptical about whether it will help with the kind of question in this thread. Needing to know some debug option that you can enable to get the info you want in some specific cases is still pretty horrible UX.

[Kyle Miller]

I agree — I'm seeing this sort of like the slew of pp options that are similarly obscure but inconvenient to live without.

[Marc Huisinga]

Kyle Miller said:

I agree — I'm seeing this sort of like the slew of pp options that are similarly obscure but inconvenient to live without.

I think it's more likely that we can get that situation in particular under control at some point because we actually control the UI there (as opposed to editor hovers) :-)