docgen strange daggers

Stream: general

[Christian Merten]

While I am at it, this is another thing I noticed: In docs#CategoryTheory.Limits.PreservesPullback.iso_inv_fst_assoc, note that there is no Z✝ declared anywhere, but the f argument is printed as f : X ⟶ Z✝. The pretty-printer does something else:

import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

#check CategoryTheory.Limits.PreservesPullback.iso_inv_fst_assoc

prints the f argument correctly as f : X ⟶ Z and the second Z variable as Z✝.

[Kevin Buzzard]

Oh ha ha, the reassoc attribute is introducing a new Z which hammers the Z already present in the statement of PreservesPullback.iso_inv_fst.

[Kyle Miller]

Interesting, the #check command prints it correctly:

CategoryTheory.Limits.PreservesPullback.iso_inv_fst_assoc.{v₁, v₂, u₁, u₂} {C : Type u₁} [Category.{v₁, u₁} C]
  {D : Type u₂} [Category.{v₂, u₂} D] (G : C ⥤ D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [PreservesLimit (cospan f g) G]
  [HasPullback f g] [HasPullback (G.map f) (G.map g)] {Z✝ : D} (h : G.obj X ⟶ Z✝) :
  (PreservesPullback.iso G f g).inv ≫ G.map (pullback.fst f g) ≫ h = pullback.fst (G.map f) (G.map g) ≫ h

What is docgen doing instead? I had been under the impression it used this signature pretty printer.

[Kyle Miller]

(Oh, I should read your message in full. I changed the algorithm for how #check prints signatures this release and I suddenly was concerned that I broke it!)

[Kyle Miller]

It looks like doc-gen has it's own signature printer. The bug is that the types of the arguments are pretty printed in the context where all the arguments have already been brought into scope. This means that it's following the normal Lean rules, where the first Z is now out-of-scope.

@Henrik Böving Maybe a fix would be to change the name.hasMacroScopes check to name.hasMacroScopes || (<- getLCtx).hasUserName name? (Didn't check that this would work, but I know functions like this exist somewhere and are used in the signature delaborator at least.)

[Kyle Miller]

https://github.com/leanprover/doc-gen4/pull/231 changes how signatures are pretty printed to use the same algorithm as the core signature pretty printer used by #check.

[Henrik Böving]

Merged the above PR, behavior is now the same as with #check :tada: