|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Kim Morrison |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public meta import Lean.Data.Json |
| 9 | +public import Mathlib.Init |
| 10 | + |
| 11 | +/-! |
| 12 | +# Fetching cross-reference snippets |
| 13 | +
|
| 14 | +The Mathlib counterpart of `scripts/crossref-snippet.lean`: given a database |
| 15 | +(`stacks`, `kerodon`, or `wikidata`) and a tag, fetch a one-line |
| 16 | +`(title, description)` snippet from the upstream site. |
| 17 | +
|
| 18 | +This module is used by `Mathlib/Tactic/Widget/CrossRefHover.lean` so that the |
| 19 | +LSP widget on a cross-reference attribute can call back into the server to |
| 20 | +resolve a snippet on demand. The script in PR 1 of this stack reimplements |
| 21 | +roughly the same logic; we keep that script self-contained (no Mathlib import, |
| 22 | +runs via `lake env lean --run`) and this module isolated from `IO.Process` |
| 23 | +dependency-wise, so the two evolve in parallel. |
| 24 | +
|
| 25 | +The `Database` enum and its `URL` / `label` projections also live here; they |
| 26 | +are re-exported through `Mathlib.Tactic.CrossRefAttribute` for the attribute |
| 27 | +infrastructure. |
| 28 | +-/ |
| 29 | + |
| 30 | +namespace Mathlib.CrossRef |
| 31 | + |
| 32 | +/-- The supported external databases. |
| 33 | +
|
| 34 | +When adding a new case, also update each of these: |
| 35 | +- `databaseURL`, `databaseLabel`, `Database.name`, `Database.ofName?`, |
| 36 | + the per-database branch in `fetchSnippet`, and `gerbyBase?` below; |
| 37 | +- the parser, `syntax (name := ...)`, `registerBuiltinAttribute`, and |
| 38 | + `#X_tags` trace command in `Mathlib/Tactic/CrossRefAttribute.lean`; |
| 39 | +- the parallel `Database` enum and per-database fetch implementation in |
| 40 | + `scripts/crossref-snippet.lean`; |
| 41 | +- the `databases` list in `scripts/extract-crossref-tags.lean`; |
| 42 | +- the `pretty` dict in `mathlib-ci`'s |
| 43 | + `scripts/crossref_review/crossref-pr-comment.py`. -/ |
| 44 | +public inductive Database where |
| 45 | + | kerodon |
| 46 | + | stacks |
| 47 | + | wikidata |
| 48 | + deriving BEq, Hashable, Repr |
| 49 | + |
| 50 | +/-- The base URL for an external database's tag pages. Always ends with `/`. -/ |
| 51 | +public def databaseURL : Database → String |
| 52 | + | .kerodon => "https://kerodon.net/tag/" |
| 53 | + | .stacks => "https://stacks.math.columbia.edu/tag/" |
| 54 | + | .wikidata => "https://www.wikidata.org/wiki/" |
| 55 | + |
| 56 | +/-- The display label used in docstring links and trace output. -/ |
| 57 | +public def databaseLabel : Database → String |
| 58 | + | .kerodon => "Kerodon Tag" |
| 59 | + | .stacks => "Stacks Tag" |
| 60 | + | .wikidata => "Wikidata" |
| 61 | + |
| 62 | +/-- A short machine-readable tag (`"kerodon"`, `"stacks"`, `"wikidata"`) |
| 63 | +that's stable to round-trip through JSON. Used by the widget. -/ |
| 64 | +public def Database.name : Database → String |
| 65 | + | .kerodon => "kerodon" |
| 66 | + | .stacks => "stacks" |
| 67 | + | .wikidata => "wikidata" |
| 68 | + |
| 69 | +/-- Parse the short name back into a `Database`. -/ |
| 70 | +public def Database.ofName? : String → Option Database |
| 71 | + | "kerodon" => some .kerodon |
| 72 | + | "stacks" => some .stacks |
| 73 | + | "wikidata" => some .wikidata |
| 74 | + | _ => none |
| 75 | + |
| 76 | +/-- `Database.name` and `Database.ofName?` roundtrip. This catches at compile time |
| 77 | +any drift between the two when a new case is added to `Database`. -/ |
| 78 | +public theorem Database.ofName?_name (d : Database) : Database.ofName? d.name = some d := by |
| 79 | + cases d <;> rfl |
| 80 | + |
| 81 | +/-- The outcome of trying to fetch a snippet. -/ |
| 82 | +public inductive SnippetOutcome where |
| 83 | + /-- Upstream returned a (title, description). Either may be empty. -/ |
| 84 | + | ok (title : String) (description : String) |
| 85 | + /-- The tag was authoritatively missing upstream. -/ |
| 86 | + | missing |
| 87 | + /-- A transient problem (network, parse, …). -/ |
| 88 | + | network (reason : String) |
| 89 | + deriving Repr |
| 90 | + |
| 91 | +/-- The `User-Agent` curl sends. Wikidata's API will throttle anonymous clients |
| 92 | +without one, so we identify ourselves. -/ |
| 93 | +private def userAgent : String := |
| 94 | + "mathlib-crossref-widget/1 (https://github.com/leanprover-community/mathlib4)" |
| 95 | + |
| 96 | +/-- Make a GET request and return `(http-status, body)`. Status is `0` if curl |
| 97 | +itself failed. We append the HTTP status to the body via `-w '\n%{http_code}'` |
| 98 | +and recover it from the final line — that avoids juggling a temp file. -/ |
| 99 | +private def fetchUrl (url : String) : IO (Nat × String) := do |
| 100 | + let output ← IO.Process.output { |
| 101 | + cmd := "curl" |
| 102 | + args := #["-sSL", "--max-time", "10", "-A", userAgent, |
| 103 | + "-w", "\n%{http_code}", url] |
| 104 | + } |
| 105 | + if output.exitCode != 0 then return (0, "") |
| 106 | + let parts := output.stdout.splitOn "\n" |
| 107 | + match parts.reverse with |
| 108 | + | last :: rest => |
| 109 | + let body := "\n".intercalate rest.reverse |
| 110 | + let status := last.trimAscii.toString.toNat?.getD 0 |
| 111 | + return (status, body) |
| 112 | + | [] => return (0, "") |
| 113 | + |
| 114 | +/-- Replace runs of whitespace by a single space and strip leading/trailing ws. -/ |
| 115 | +private def flattenWhitespace (s : String) : String := |
| 116 | + let go : Char → (String × Bool) → (String × Bool) := fun c (acc, prevSpace) => |
| 117 | + let isWs := c == ' ' || c == '\t' || c == '\n' || c == '\r' |
| 118 | + if isWs then |
| 119 | + if prevSpace || acc.isEmpty then (acc, true) |
| 120 | + else (acc.push ' ', true) |
| 121 | + else |
| 122 | + (acc.push c, false) |
| 123 | + let (out, _) := s.toList.foldl (fun st c => go c st) ("", false) |
| 124 | + out.trimAscii.toString |
| 125 | + |
| 126 | +/-- Best-effort HTML→text. We treat `<x…>` as a tag only when `x` is a letter, |
| 127 | +`/`, or `!`, so a literal `<` inside LaTeX (`0 < 1`) is preserved. -/ |
| 128 | +private def stripHtml (html : String) : String := |
| 129 | + let chars := html.toList |
| 130 | + let rec go : List Char → Bool → String → String |
| 131 | + | [], _, acc => acc |
| 132 | + | '<' :: rest, false, acc => |
| 133 | + match rest with |
| 134 | + | c :: _ => |
| 135 | + if c.isAlpha || c == '/' || c == '!' then go rest true acc |
| 136 | + else go rest false (acc.push '<') |
| 137 | + | [] => acc.push '<' |
| 138 | + | '>' :: rest, true, acc => go rest false acc |
| 139 | + | _ :: rest, true, acc => go rest true acc |
| 140 | + | c :: rest, false, acc => go rest false (acc.push c) |
| 141 | + let raw := go chars false "" |
| 142 | + let decoded := raw |
| 143 | + |>.replace " " " " |
| 144 | + |>.replace "&" "&" |
| 145 | + |>.replace "<" "<" |
| 146 | + |>.replace ">" ">" |
| 147 | + |>.replace """ "\"" |
| 148 | + |>.replace "'" "'" |
| 149 | + flattenWhitespace decoded |
| 150 | + |
| 151 | +open Lean in |
| 152 | +/-- Walk a path of object keys in a `Json` value, returning the leaf as a |
| 153 | +string if every step succeeds and the leaf is a string. -/ |
| 154 | +private def jsonStrPath? (j : Json) (path : List String) : Option String := |
| 155 | + let rec go (cur : Json) : List String → Option String |
| 156 | + | [] => cur.getStr?.toOption |
| 157 | + | k :: rest => |
| 158 | + match cur.getObjVal? k with |
| 159 | + | .ok next => go next rest |
| 160 | + | .error _ => none |
| 161 | + go j path |
| 162 | + |
| 163 | +/-! ### Wikidata -/ |
| 164 | + |
| 165 | +open Lean in |
| 166 | +private def fetchWikidata (qid : String) : IO SnippetOutcome := do |
| 167 | + let url := s!"https://www.wikidata.org/w/api.php?action=wbgetentities&ids={qid}\ |
| 168 | + &languages=en&props=labels%7Cdescriptions&format=json" |
| 169 | + let (status, body) ← fetchUrl url |
| 170 | + if status != 200 then return .network s!"wikidata HTTP {status}" |
| 171 | + match Json.parse body with |
| 172 | + | .error e => return .network s!"wikidata json: {e}" |
| 173 | + | .ok json => |
| 174 | + match json.getObjVal? "error" with |
| 175 | + | .ok err => |
| 176 | + let code := jsonStrPath? err ["code"] |>.getD "" |
| 177 | + let info := jsonStrPath? err ["info"] |>.getD code |
| 178 | + if code == "no-such-entity" then return .missing |
| 179 | + else return .network s!"wikidata {code}: {info}" |
| 180 | + | _ => |
| 181 | + match json.getObjVal? "entities" with |
| 182 | + | .error _ => return .network "wikidata: no `entities` field" |
| 183 | + | .ok entities => |
| 184 | + match entities.getObjVal? qid with |
| 185 | + | .error _ => return .missing |
| 186 | + | .ok ent => |
| 187 | + match ent.getObjVal? "missing" with |
| 188 | + | .ok _ => return .missing |
| 189 | + | _ => |
| 190 | + let label := jsonStrPath? ent ["labels", "en", "value"] |>.getD "" |
| 191 | + let desc := jsonStrPath? ent ["descriptions", "en", "value"] |>.getD "" |
| 192 | + return .ok (flattenWhitespace label) (flattenWhitespace desc) |
| 193 | + |
| 194 | +/-! ### Stacks / Kerodon (Gerby) -/ |
| 195 | + |
| 196 | +/-- The base URL for a Gerby-style database, or `none` for Wikidata. -/ |
| 197 | +private def gerbyBase? : Database → Option String |
| 198 | + | .stacks => some "https://stacks.math.columbia.edu" |
| 199 | + | .kerodon => some "https://kerodon.net" |
| 200 | + | .wikidata => none |
| 201 | + |
| 202 | +/-- Return the substring of `s` after the first occurrence of `needle`, |
| 203 | +or `none` if `needle` is absent. -/ |
| 204 | +private def afterFirst? (s needle : String) : Option String := |
| 205 | + let parts := s.splitOn needle |
| 206 | + match parts with |
| 207 | + | _ :: rest@(_ :: _) => some (needle.intercalate rest) |
| 208 | + | _ => none |
| 209 | + |
| 210 | +/-- Take everything up to (but not including) the first occurrence of `c`. -/ |
| 211 | +private def takeUntilChar (s : String) (c : Char) : String := |
| 212 | + String.ofList (s.toList.takeWhile (· != c)) |
| 213 | + |
| 214 | +/-- Pull the environment type (`Lemma`, `Proposition`, …) and reference number |
| 215 | +from the `/content/statement` HTML. Both Stacks and Kerodon wrap each tag in |
| 216 | +`<article class="env-{TYPE}" id="{TAG}">` and lead with |
| 217 | +`<a ...>Lemma <span data-tag="...">14.32.3</span>.</a>`. -/ |
| 218 | +private def parseGerbyTitle (html : String) : String := |
| 219 | + let envType := |
| 220 | + match afterFirst? html "class=\"env-" with |
| 221 | + | none => "" |
| 222 | + | some rest => takeUntilChar rest '"' |
| 223 | + let reference := |
| 224 | + match afterFirst? html "data-tag=\"" with |
| 225 | + | none => "" |
| 226 | + | some afterAttr => |
| 227 | + match afterFirst? afterAttr ">" with |
| 228 | + | none => "" |
| 229 | + | some inside => takeUntilChar inside '<' |
| 230 | + let cap := envType.capitalize |
| 231 | + flattenWhitespace (if reference.isEmpty then cap else s!"{cap} {reference}") |
| 232 | + |
| 233 | +private def fetchGerby (db : Database) (tag : String) : IO SnippetOutcome := do |
| 234 | + let some base := gerbyBase? db | return .network s!"{db.name}: no Gerby base" |
| 235 | + let url := s!"{base}/data/tag/{tag}/content/statement" |
| 236 | + let (status, body) ← fetchUrl url |
| 237 | + if status != 200 then return .network s!"{db.name} HTTP {status}" |
| 238 | + -- Gerby returns HTTP 200 even for missing tags; detect via body text. |
| 239 | + if body.trimAscii.toString == "This tag does not exist." then return .missing |
| 240 | + let title := parseGerbyTitle body |
| 241 | + let snippet := stripHtml body |
| 242 | + if title.isEmpty && snippet.isEmpty then |
| 243 | + return .network s!"{db.name}: could not parse statement" |
| 244 | + return .ok title snippet |
| 245 | + |
| 246 | +/-- Fetch one snippet from the appropriate upstream database. -/ |
| 247 | +public def fetchSnippet (db : Database) (tag : String) : IO SnippetOutcome := |
| 248 | + match db with |
| 249 | + | .wikidata => fetchWikidata tag |
| 250 | + | _ => fetchGerby db tag |
| 251 | + |
| 252 | +end Mathlib.CrossRef |
0 commit comments