get docstring for tactic

Stream: lean4

[Jon Eugster]

Using Lean.findDocString? env name I can get the docstring of a declaration, but that does not seem to work for tactics. How would I retrieve the docstring of a tactic, say simp?

[Mario Carneiro]

the docstring on a tactic is the docstring on the syntax declaration for that tactic:

import Mathlib.Tactic.HelpCmd

#help tactic simp
-- syntax "simp"... [Lean.Parser.Tactic.simp]

open Lean Meta Elab
#eval show MetaM _ from do
  let some s ← findDocString? (← getEnv) ``Lean.Parser.Tactic.simp | failure
  println! s
-- The `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
-- non-dependent hypotheses. It has many variants: ...

[Jon Eugster]

Thanks!
Now I just have to figure out how to get ``Lean.Parser.Tactic.simp starting from a Name/Ident saying just simp, but that is a problem for another day. Maybe just something along the lines of ``(tactic| ${name}) (not on the computer anymore)

[Mario Carneiro]

that's what the first line was for

[Mario Carneiro]

the #help command implements exactly this lookup

[Mario Carneiro]

although depending on the context you might want to just parse a syntax instead. What are you actually trying to do?

[Jon Eugster]

Looking quickly at #help it isnt completely obvious to me how that lookup works, but maybe Ill figure it out when I look at it for another 20min

As for why, it's for the games (NNG, etc). The author can provide documentation for introduced tactics with a command like

TacticDoc simp "some text"

and I would like to use the tactic's docstring in case they don't provide a documentation that way.

[Mario Carneiro]

why not just require the author to do the lookup and refer to the appropriately namespaced constant?

[Alexander Bentkamp]

We simply would like to make it as easy as possible for authors. Game authors are not necessarily good metaprogrammers.

[Mario Carneiro]

they can just use #help to look up the names, as indicated

[Mario Carneiro]

Note that looking up a tactic by its initial token is a lossy process, which is why #help acts more like a search engine. If you actually want to identify a particular tactic you need something more precise

[Mario Carneiro]

An alternative would be to have your syntax accept a full (syntactically correct) tactic expression and look up the name that way

[Mario Carneiro]

import Lean

open Lean Meta
elab doc:docComment "tactic_doc" t:tactic : command => do
  let doc := doc.getDocString.trim
  let kind := t.raw.getKind
  logInfo m!"adding doc {repr doc} to {kind}"

/-- some text -/ tactic_doc simp
-- adding doc "some text" to Lean.Parser.Tactic.simp
/-- some text -/ tactic_doc cases ·
-- adding doc "some text" to Lean.Parser.Tactic.cases
/-- some text -/ tactic_doc · skip
-- adding doc "some text" to cdot
/-- some text -/ tactic_doc skip
-- adding doc "some text" to Lean.Parser.Tactic.skip
/-- some text -/ tactic_doc rw [·]
-- adding doc "some text" to Lean.Parser.Tactic.rwSeq

[Jon Eugster]

Thanks Mario for the help! I wasn't quite aware that this tactic lookup is not a bijective process form the first token itself. I just had an hour on the train to compress #help into something that should hopefully work well enough:

def getTacticDocstring (name: Name) : CommandElabM String := do
  let name := name.toString (escape := false)
  let mut decls : Lean.RBMap String (Array SyntaxNodeKind) compare := {}

  let env ← getEnv

  let catName : Name := `tactic
  let catStx : Ident := mkIdent catName -- TODO
  let some cat := (Parser.parserExtension.getState env).categories.find? catName
    | throwErrorAt catStx "{catStx} is not a syntax category"
  liftTermElabM <| Term.addCategoryInfo catStx catName
  for (k, _) in cat.kinds do
    let mut used := false
    if let some tk := do getHeadTk (← (← env.find? k).value?) then
      let tk := tk.trim
      if name ≠ tk then -- was `!name.isPrefixOf tk`
        continue
      used := true
      decls := decls.insert tk ((decls.findD tk #[]).push k)
  for (_name, ks) in decls do
    for k in ks do
      if let some doc ← findDocString? env k then
        return doc

  logWarning <| m!"Could not find a docstring for this tactic, consider adding one " ++
    m!"using `TacticDoc {name} \"some doc\"`"
  return ""

Full MWE

/- Modified from Mathlib.Tactic.HelpCmd -/
import Lean

namespace Lean.Expr

def constName (e : Expr) : Name :=
  e.constName?.getD Name.anonymous

/-- Return the function (name) and arguments of an application. -/
def getAppFnArgs (e : Expr) : Name × Array Expr :=
  withApp e λ e a => (e.constName, a)

end Lean.Expr

open Lean Meta Elab Tactic Command

/-- Gets the initial string token in a parser description. For example, for a declaration like
`syntax "bla" "baz" term : tactic`, it returns `some "bla"`. Returns `none` for syntax declarations
that don't start with a string constant. -/
partial def getHeadTk (e : Expr) : Option String :=
  match e.getAppFnArgs with
  | (``ParserDescr.node, #[_, _, p]) => getHeadTk p
  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getHeadTk p
  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getHeadTk p
  | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getHeadTk p
  | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
  | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => some tk
  | (``Parser.withAntiquot, #[_, p]) => getHeadTk p
  | (``Parser.leadingNode, #[_, _, p]) => getHeadTk p
  | (``HAndThen.hAndThen, #[_, _, _, _, p, _]) => getHeadTk p
  | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
  | (``Parser.symbol, #[.lit (.strVal tk)]) => some tk
  | _ => none

def getTacticDocstring (name: Name) : CommandElabM String := do
  let name := name.toString (escape := false)
  let mut decls : Lean.RBMap String (Array SyntaxNodeKind) compare := {}

  let env ← getEnv

  let catName : Name := `tactic
  let catStx : Ident := mkIdent catName -- TODO
  let some cat := (Parser.parserExtension.getState env).categories.find? catName
    | throwErrorAt catStx "{catStx} is not a syntax category"
  liftTermElabM <| Term.addCategoryInfo catStx catName
  for (k, _) in cat.kinds do
    let mut used := false
    if let some tk := do getHeadTk (← (← env.find? k).value?) then
      let tk := tk.trim
      if name ≠ tk then -- was `!name.isPrefixOf tk`
        continue
      used := true
      decls := decls.insert tk ((decls.findD tk #[]).push k)
  for (_name, ks) in decls do
    for k in ks do
      if let some doc ← findDocString? env k then
        return doc

  logWarning <| m!"Could not find a docstring for this tactic, consider adding one " ++
    m!"using `TacticDoc {name} \"some doc\"`"
  return ""

#eval (getTacticDocstring `simp)

I'm not sure if this might fail in some exotic cases, but hopefully it works for most common tactics.