Notation in namespace not showing in pp

Stream: lean4

[Peter Nelson]

I'm having an issue since 4.8.0 with notation not showing in the (VScode) pretty-printer when defined in a namespace.

Removing the namespace fixes the below. Can someone tell me how to make it appear?

import Mathlib.Data.Set.Basic

namespace Set

def MySubset {α : Type} (s t : Set α) : Prop := s ⊆ t

infix:50 " ⊆⊆ " => MySubset

example {α : Type} (s t : Set α) (h : s ⊆⊆ t) : s ⊆ t := by
  -- pp shows `h : s.MySubset t` rather than `s ⊆⊆ t`.
  exact h

end Set

[Yaël Dillies]

Could this have to do with pp_dot now being the default?

[Peter Nelson]

On mobile, but guessing that pp_nodot will fix it. Presumably this isn’t intended behaviour, though.

[Kyle Miller]

Thanks for the report, looking into fixing this. Most notations go through a notation typeclass, which prevents this interaction between the dot notation pretty printer and the unexpander from infix/etc.

The issue is that the dot notation pretty printer can collapse projections to parent structures, so to prevent any backtracking in pretty printing, once it determines that dot notation is possible it commits to it.

[Peter Nelson]

pp_nodot does fix it for the time being. Is there any way to (in a local project) add that attribute to a declaration already in mathlib that has been broken by this?

If I try attribute [pp_nodot] Matroid.Restriction (for example), then I get invalid attribute 'pp_nodot', declaration is in an imported module.

[Kyle Miller]

Unfortunately no, since pp_nodot is a TagAttribute.

If this is for fixing pretty printing, then what you could do is make a delaborator (rather than an unexpander) which would be unaffected.

[Kyle Miller]

If you add this chunk of code it'll fix pretty printing locally:

open Lean PrettyPrinter Delaborator SubExpr in
@[delab app.Matroid.Restriction]
private def delabRestriction : Delab :=
  whenPPOption getPPNotation <| whenNotPPOption getPPExplicit do
    guard <| (← getExpr).getAppNumArgs = 3
    let a ← withAppFn <| withAppArg delab
    let b ← withAppArg delab
    `($a ≤r $b)

[Joël Riou]

Otherwise, in order to fix the pretty printing globally in mathlib, is adding pp_nodot the recommended solution?

[Kyle Miller]

I'm hoping to fix this in time for the next rc (it seems like there will be one), so I'd hold off on adding pp_nodots if that's possible. What notations are affecting you @Joël Riou?

[Joël Riou]

I have observed this behaviour also for docs#CategoryTheory.Functor.comp, but if there is a better fix, I can wait :-)

[Kyle Miller]

Once lean4#4071 finishes building and succeeds in building mathlib, I'll check that these mathlib notations actually pretty print