missing doc of `#check_failure`

Stream: general

[Asei Inoue]

import Mathlib.Tactic

-- error: no command declarations start with #check_failure
#help command "#check_failure"

[Kim Morrison]

It looks like #help command does not pick up doc-strings from @[builtin_command_parser] in any case: #help command "open" and #help command "export" fail to return the doc-strings from src/Lean/Parser/Command.lean.

So I think it's two steps to address this: fix #help command, and then PR doc-strings to src/Lean/Parser/Command.lean.

[Mario Carneiro]

It's not that #help command fails to pick up #check_failure, it fails to parse the parser to find the head token (that is "#check_failure") such that the prefix search works. Note that the line

syntax ... [Parser.Command.check_failure]

shows up in #help command.

(It also fails to show documentation because #check_failure doesn't have any documentation. Ditto for open and export, although I haven't tested this on nightly.)

[Mario Carneiro]

the #help issue is fixed in #12287

[Kim Morrison]

Indeed, I was looking at open and export on nightly, where doc-strings have recently been added.