| module | |
| import Lean.Elab.Tactic.Doc | |
| /-! | |
| This test checks that the first tokens are found for the tactics that ship with Lean when in a | |
| module. | |
| In the past, the first token detection code attempted to process the descriptor in the environment; | |
| this failed in modules because the parser was not loaded. This test, along with tacticDocAllNonmod, | |
| check that the code works correctly both in and out of modules. | |
| -/ | |
| open Lean.Elab.Tactic.Doc | |
| #guard_msgs in | |
| open Lean in | |
| #eval do | |
| let docs ← allTacticDocs | |
| let userNames := docs.map TacticDoc.userName | |
| if userNames.size < 50 then | |
| throwError "Implausibly few user names found: {userNames}" | |
| for n in userNames do | |
| if n.startsWith "Lean.Parser.Tactic" && n ≠ "Lean.Parser.Tactic.nestedTactic" then | |
| logError "Didn't find a first token for tactic parser {n}" |