feat(CrossRefAttribute): add @[wikidata] attribute (leanprover-community#39284)

This PR adds a Wikidata cross-reference attribute alongside the existing
Stacks and Kerodon ones, accepting identifiers of the form `QN+`, plus
a `#wikidata_tags`/`#wikidata_tags!` trace command.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Author: jcommelin

Mathlib/Tactic/CrossRefAttribute.lean

@@ -16,6 +16,7 @@ to entries in external mathematical databases:
 
 * `@[stacks TAG]` — [Stacks Project](https://stacks.math.columbia.edu/tags)
 * `@[kerodon TAG]` — [Kerodon](https://kerodon.net/tag/)
+* `@[wikidata QID]` — [Wikidata](https://www.wikidata.org)
 
 Each attribute records the cross-reference in an environment extension and appends
 a link to the declaration's docstring.
@@ -35,17 +36,20 @@ namespace Mathlib.CrossRef
 inductive Database where
   | kerodon
   | stacks
+  | wikidata
   deriving BEq, Hashable
 
 /-- The base URL for an external database's tag pages. Always ends with `/`. -/
 def databaseURL : Database → String
   | .kerodon => "https://kerodon.net/tag/"
   | .stacks => "https://stacks.math.columbia.edu/tag/"
+  | .wikidata => "https://www.wikidata.org/wiki/"
 
 /-- The display label used in docstring links and trace output. -/
 def databaseLabel : Database → String
   | .kerodon => "Kerodon Tag"
   | .stacks => "Stacks Tag"
+  | .wikidata => "Wikidata"
 
 /-- A cross-reference from a Mathlib declaration to an entry in an external database. -/
 structure Tag where
@@ -84,6 +88,8 @@ def addCrossRefDoc (db : Database) (decl : Name) (idStr comment : String) : Core
 
 open Parser
 
+/-! ### Stacks (and Kerodon) parser -/
+
 /-- `stacksTag` is the node kind of Stacks Project Tags: a sequence of digits and
 uppercase letters. -/
 abbrev stacksTagKind : SyntaxNodeKind := `stacksTag
@@ -117,6 +123,42 @@ def stacksTagNoAntiquot : Parser := {
 def stacksTagParser : Parser :=
   withAntiquot (mkAntiquot "stacksTag" stacksTagKind) stacksTagNoAntiquot
 
+/-! ### Wikidata parser -/
+
+/-- `wikidataId` is the node kind of Wikidata identifiers: the letter `Q` followed by digits. -/
+abbrev wikidataIdKind : SyntaxNodeKind := `wikidataId
+
+/-- The main parser for Wikidata identifiers: it accepts `Q` followed by one or more digits. -/
+def wikidataIdFn : ParserFn := fun c s =>
+  let i := s.pos
+  let s := takeWhileFn (fun c => c.isAlphanum) c s
+  if s.hasError then
+    s
+  else if s.pos == i then
+    ParserState.mkError s "wikidata id"
+  else
+    let id := c.extract i s.pos
+    match id.toList with
+    | 'Q' :: rest@(_ :: _) =>
+      if rest.all Char.isDigit then
+        mkNodeToken wikidataIdKind i true c s
+      else
+        ParserState.mkUnexpectedError s
+          "Wikidata ids must consist of the letter Q followed by digits."
+    | _ =>
+      ParserState.mkUnexpectedError s
+        "Wikidata ids must start with the letter Q followed by one or more digits."
+
+@[inherit_doc wikidataIdFn]
+def wikidataIdNoAntiquot : Parser := {
+  fn   := wikidataIdFn
+  info := mkAtomicInfo "wikidataId"
+}
+
+@[inherit_doc wikidataIdFn]
+def wikidataIdParser : Parser :=
+  withAntiquot (mkAntiquot "wikidataId" wikidataIdKind) wikidataIdNoAntiquot
+
 end Mathlib.CrossRef
 
 open Mathlib.CrossRef
@@ -126,6 +168,11 @@ def Lean.TSyntax.getStacksTag (stx : TSyntax stacksTagKind) : CoreM String := do
   let some val := Syntax.isLit? stacksTagKind stx | throwError "Malformed Stacks tag"
   return val
 
+/-- Extract the underlying identifier as a string from a `wikidataId` node. -/
+def Lean.TSyntax.getWikidataId (stx : TSyntax wikidataIdKind) : CoreM String := do
+  let some val := Syntax.isLit? wikidataIdKind stx | throwError "Malformed Wikidata id"
+  return val
+
 namespace Lean.PrettyPrinter
 
 namespace Formatter
@@ -134,17 +181,26 @@ namespace Formatter
 @[combinator_formatter stacksTagNoAntiquot] def stacksTagNoAntiquot.formatter :=
   visitAtom stacksTagKind
 
+/-- The formatter for Wikidata identifier syntax. -/
+@[combinator_formatter wikidataIdNoAntiquot] def wikidataIdNoAntiquot.formatter :=
+  visitAtom wikidataIdKind
+
 end Formatter
 
 namespace Parenthesizer
 
 /-- The parenthesizer for Stacks Project Tags syntax. -/
 @[combinator_parenthesizer stacksTagNoAntiquot] def stacksTagAntiquot.parenthesizer := visitToken
 
+/-- The parenthesizer for Wikidata identifier syntax. -/
+@[combinator_parenthesizer wikidataIdNoAntiquot] def wikidataIdAntiquot.parenthesizer := visitToken
+
 end Lean.PrettyPrinter.Parenthesizer
 
 namespace Mathlib.CrossRef
 
+/-! ### Stacks / Kerodon attribute -/
+
 /-- The syntax category for the database name. -/
 declare_syntax_cat stacksTagDB
 
@@ -177,14 +233,36 @@ initialize Lean.registerBuiltinAttribute {
   applicationTime := .beforeElaboration
 }
 
+/-! ### Wikidata attribute -/
+
+/-- The `wikidata` attribute.
+Use it as `@[wikidata Q12345 "Optional comment"]` to associate a Mathlib declaration with
+the corresponding [Wikidata](https://www.wikidata.org) item.
+
+The identifier must be the letter `Q` followed by one or more digits.
+-/
+syntax (name := wikidataTag) "wikidata" wikidataIdParser (ppSpace str)? : attr
+
+initialize Lean.registerBuiltinAttribute {
+  name := `wikidataTag
+  descr := "Apply a Wikidata identifier to a declaration."
+  add := fun decl stx _attrKind => do
+    let (id, comment) := ← match stx with
+      | `(attr| wikidata $id $[$comment]?) => return (id, comment)
+      | _ => throwUnsupportedSyntax
+    addCrossRefDoc .wikidata decl (← id.getWikidataId) ((comment.map (·.getString)).getD "")
+  -- docstrings are immutable once an asynchronous elaboration task has been started
+  applicationTime := .beforeElaboration
+}
+
 end Mathlib.CrossRef
 
-/-- Return the array of `Tag`s in the environment, sorted alphabetically by tag. -/
+/-- Returns the array of `Tag`s in the environment, sorted alphabetically by tag. -/
 private def Lean.Environment.getSortedCrossRefs (env : Environment) : Array Tag :=
   let tags := PersistentEnvExtension.getState tagExt env
   tags.2.flatten.appendList tags.1 |>.qsort (·.tag < ·.tag)
 
-/-- Return the declaration names of results carrying the cross-reference `tag`. -/
+/-- Returns the declaration names of results carrying the cross-reference `tag`. -/
 private def Lean.Environment.getCrossRefDeclNames (env : Environment) (tag : String) :
     Array Name :=
   env.getSortedCrossRefs.filterMap fun d => if d.tag == tag then some d.declName else none
@@ -236,4 +314,16 @@ or declaration type (for definitions, structures, instances, etc.) after each su
 elab (name := kerodonTags) "#kerodon_tags" tk:("!")? : command =>
   traceCrossRefs .kerodon (tk.isSome)
 
+/-- The `#wikidata_tags` command retrieves all declarations that have the `wikidata` attribute.
+
+For each found declaration, it prints a line
+```
+'declaration_name' corresponds to tag 'declaration_tag'.
+```
+The variant `#wikidata_tags!` also adds the theorem statement (for theorems)
+or declaration type (for definitions, structures, instances, etc.) after each summary line.
+-/
+elab (name := wikidataTags) "#wikidata_tags" tk:("!")? : command =>
+  traceCrossRefs .wikidata (tk.isSome)
+
 end Mathlib.CrossRef

MathlibTest/CrossRefAttribute.lean

@@ -69,6 +69,34 @@ True
 #guard_msgs in
 #kerodon_tags!
 
+namespace W
+
+@[wikidata Q12345 "A Wikidata comment"]
+theorem wikiTagged : True := .intro
+
+end W
+
+/-- info: some ([Wikidata Q12345](https://www.wikidata.org/wiki/Q12345) (A Wikidata comment)) -/
+#guard_msgs in
+run_cmd
+  Lean.logInfo m!"{← Lean.findDocString? (← Lean.getEnv) `W.wikiTagged}"
+
+/--
+info:
+[Wikidata Q12345](https://www.wikidata.org/wiki/Q12345) corresponds to declaration 'W.wikiTagged'. (A Wikidata comment)
+-/
+#guard_msgs in
+#wikidata_tags
+
+/-- error: <input>:1:5: Wikidata ids must consist of the letter Q followed by digits. -/
+#guard_msgs in #parse Mathlib.CrossRef.wikidataIdFn => "Q12X3"
+
+/-- error: <input>:1:6: Wikidata ids must start with the letter Q followed by one or more digits. -/
+#guard_msgs in #parse Mathlib.CrossRef.wikidataIdFn => "P12345"
+
+/-- info: Q42 -/
+#guard_msgs in #parse Mathlib.CrossRef.wikidataIdFn => "Q42"
+
 section errors
 
 open Lean Parser Mathlib.CrossRef