issues with Qq in doc-gen

Stream: general

[Jireh Loreaux]

@Henrik Böving it seems like doc-gen has quite some trouble with Qq. Probably you already know this, and maybe it's a hard problem, but in case you don't, see for example, docs#Qq.checkTypeQ

[Henrik Böving]

I wasnt aware no, ill take a look when I'm home thanks!

[Henrik Böving]

Oh that does look bad yes

[Henrik Böving]

Does QQ have any sort of delaborator that doc-gen misses out on here? @Gabriel Ebner if it doesn't there isn't really much I can do about it.

[Kyle Miller]

It does seem to be missing Q(...) notation. Here's how that declaration pretty prints from within Lean:

Qq.checkTypeQ {u : Lean.Level} (e : Lean.Expr)
  (ty :
    let u := u;
    Q(Sort u)) :
  Lean.MetaM (Option Q(«$ty»))

[Kyle Miller]

versus in doc-gen:

def Qq.checkTypeQ{u : Lean.Level} (e : Lean.Expr) (ty : let u := u; Qq.Quoted (Lean.Expr.sort u)) :
    Lean.MetaM (Option (Qq.Quoted ty))

[Henrik Böving]

Aha! I think I have a clue. when I #print from within the file MetaM.lean in QQ itself I get

def Qq.checkTypeQ : {u : Level} →
  Expr →
    (ty :
        let u := u;
        Quoted (Expr.sort u)) →
      MetaM (Option (Quoted ty)) :=

and doc-gen does very much work from a perspective of analyzing one olean/module at a time to benefit from more fine grained parallelism. Since the delaborators are defined in a file separate from the syntax the delaboration is not available here. So you want to import the delaborator in all the files that it doesn't import to enable pretty printing I guess?

[Gabriel Ebner]

I think the quickest fix is to import Qq.Delab from Qq.MetaM. I've pushed that change just now, and it should hit doc-gen once mathlib upgrades.

[Scott Morrison]

Mathlib upgrade: #6857