Zulip Chat Archive

Stream: lean4

Topic: Showing syntax in generated documentation


Raghuram (May 20 2022 at 18:41):

I was looking at https://leanprover-community.github.io/mathlib4_docs/Init/Tactics.html and thought it would be nice if instead of showing the generated ParserDescr declarations, it showed the actual syntax of the tactic/etc. being defined. For example, even the direct source code

syntax (name := rewriteSeq) "rewrite " (config)? rwRuleSeq (location)? : tactic

is (seems to be?) more useful than def Lean.Parser.Tactic.rewriteSeq : Lean.ParserDescr.

Is this plausible/desirable/feasible?

Henrik Böving (May 20 2022 at 18:48):

If it is possible right now I do not know how to do it (otherwise I would already have done it). That does however not mean it cannot be done. The elaborator for these syntax declarations would have to store the information about the original syntax somewhere :tm: so doc-gen can fetch it.

Gabriel Ebner (May 20 2022 at 19:19):

The ParserDescr definitions are easy to parse, there's no need to keep the original syntax around.

Henrik Böving (May 20 2022 at 19:26):

Should we have delaborators for ParserDescr then?

Henrik Böving (Jul 23 2022 at 12:26):

So i started on this:

import Lean

open Lean PrettyPrinter

abbrev StxUnexpander := TSyntax `term  UnexpandM (TSyntax `stx)
def unexpandCat : StxUnexpander
  | `(ParserDescr.cat $cat $prec) =>
    let prec : TSyntax `prec := prec.raw
    `(stx| $cat:$prec)
  | _ => throw ()

But I'm running into the issue that Lean does not like the antiquotations this way of course because they could also be interpreted as "$cat with this stx category". Is there a way to create this syntax node nicely none the less? Or do I have to write some manual Syntax.node stuff here?

Sebastian Ullrich (Jul 23 2022 at 12:53):

You can work around that by making the kind of the first antiquotation explicit

$cat:ident:$prec

Last updated: Dec 20 2023 at 11:08 UTC