From cd63bd15a429bad94e6ec03424203a21e087a70e Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 15 Aug 2025 23:32:03 +0200 Subject: [PATCH] fix: better robustness in the face of overloaded tactic syntax If tactic aliases are not registered, we now pick the first one with a docstring, rather than the first one. This way, missing docs don't break the build. We also emit warnings on overloads to make the situation more clear. --- src/verso-manual/VersoManual/Docstring.lean | 57 ++++++++++++++++----- 1 file changed, 44 insertions(+), 13 deletions(-) diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean index 5d7f0b3a8..7af16537b 100644 --- a/src/verso-manual/VersoManual/Docstring.lean +++ b/src/verso-manual/VersoManual/Docstring.lean @@ -1641,7 +1641,7 @@ def Block.tactic (name : Lean.Elab.Tactic.Doc.TacticDoc) («show» : Option Stri data := ToJson.toJson (name, «show») structure TacticDocsOptions where - name : String ⊕ Name + name : StrLit ⊕ Ident «show» : Option String replace : Bool allowMissing : Option Bool @@ -1657,12 +1657,12 @@ def TacticDocsOptions.parse : ArgParse m TacticDocsOptions := .namedD `replace .bool false <*> .named `allowMissing .bool true where - strOrName : ValDesc m (String ⊕ Name) := { + strOrName : ValDesc m (StrLit ⊕ Ident) := { description := "First token in tactic, or canonical parser name" signature := .Ident ∪ .String get := fun - | .name x => pure (.inr x.getId) - | .str s => pure (.inl s.getString) + | .name x => pure (.inr x) + | .str s => pure (.inl s) | .num n => throwErrorAt n "Expected tactic name (either first token as string, or internal parser name)" } @@ -1671,15 +1671,35 @@ instance : FromArgs TacticDocsOptions m := ⟨TacticDocsOptions.parse⟩ end open Lean Elab Term Parser Tactic Doc in -private def getTactic (name : String ⊕ Name) : TermElabM TacticDoc := do +private def getTactic (name : StrLit ⊕ Ident) : TermElabM TacticDoc := do for t in ← allTacticDocs do - if .inr t.internalName == name || .inl t.userName == name then - return t + match name with + | .inr name => if t.internalName == name.getId then return t + | .inl name => if t.userName == name.getString then return t + let n : MessageData := + match name with + | .inl x => x + | .inr x => x + let blame : Syntax := name.elim TSyntax.raw TSyntax.raw + throwErrorAt blame m!"Tactic not found: {n}" + + +open Lean Elab Term Parser Tactic Doc in +private def getTacticOverloads (name : StrLit ⊕ Ident) : TermElabM (Array TacticDoc) := do + let mut out := #[] + for t in ← allTacticDocs do + match name with + | .inr name => if t.internalName == name.getId then out := out.push t + | .inl name => if t.userName == name.getString then out := out.push t + + if out.size > 0 then return out let n : MessageData := match name with | .inl x => x | .inr x => x - throwError m!"Tactic not found: {n}" + let blame : Syntax := name.elim TSyntax.raw TSyntax.raw + throwErrorAt blame m!"Tactic not found: {n}" + open Lean Elab Term Parser Tactic Doc in private def getTactic? (name : String ⊕ Name) : TermElabM (Option TacticDoc) := do @@ -1691,15 +1711,26 @@ private def getTactic? (name : String ⊕ Name) : TermElabM (Option TacticDoc) : @[directive] def tactic : DirectiveExpanderOf TacticDocsOptions | opts, more => do - let tactic ← getTactic opts.name + let tactics ← getTacticOverloads opts.name + let blame : Syntax := opts.name.elim TSyntax.raw TSyntax.raw + let withDocs := tactics.filter (·.docString.isSome) + -- Prefer overloads with docstrings to overloads without + let tactic ← + if h : tactics.size = 0 then throwErrorAt blame "Tactic not found" + else if h : withDocs.size > 0 then pure withDocs[0] + else pure tactics[0] + if tactics.size > 1 then + logWarningAt blame s!"Found {tactics.size} overloads: {tactics.map (toString ·.internalName) |>.toList |> ", ".intercalate}" Doc.PointOfInterest.save (← getRef) tactic.userName if tactic.userName == tactic.internalName.toString && opts.show.isNone then throwError "No `show` option provided, but the tactic has no user-facing token name" let contents ← if opts.replace then pure #[] else - let some mdAst := tactic.docString >>= MD4Lean.parse - | throwError "Failed to parse docstring as Markdown" + let some str := tactic.docString + | throwError "Tactic {tactic.userName} ({tactic.internalName}) has no docstring" + let some mdAst := MD4Lean.parse str + | throwError m!"Failed to parse docstring as Markdown. Docstring contents:\n{repr str}" mdAst.blocks.mapM (blockFromMarkdownWithLean []) let userContents ← more.mapM elabBlock ``(Verso.Doc.Block.other (Block.tactic $(quote tactic) $(quote opts.show)) #[$(contents ++ userContents),*]) @@ -1835,7 +1866,7 @@ structure ConvTacticDoc where docs? : Option String open Lean Elab Term Parser Tactic Doc in -def getConvTactic (name : String ⊕ Name) (allowMissing : Option Bool) : TermElabM ConvTacticDoc := +def getConvTactic (name : StrLit ⊕ Ident) (allowMissing : Option Bool) : TermElabM ConvTacticDoc := withOptions (allowMissing.map (fun b opts => verso.docstring.allowMissing.set opts b) |>.getD id) do let .inr kind := name | throwError "Strings not yet supported here" @@ -1843,7 +1874,7 @@ def getConvTactic (name : String ⊕ Name) (allowMissing : Option Bool) : TermEl let some convs := parserState.categories.find? `conv | throwError "Couldn't find conv tactic list" for ⟨k, ()⟩ in convs.kinds do - if kind.isSuffixOf k then + if kind.getId.isSuffixOf k then return ⟨k, ← getDocString? (← getEnv) k⟩ throwError m!"Conv tactic not found: {kind}"