feat: implement pi-base cross-reference attribute

[Deicyde]

Adds a @[pibase ID] cross-reference attribute for canonical pi-base identifiers.

The parser accepts IDs of the form P000001, S000023, and T000001, and routes them to the corresponding properties/, spaces/, or theorems/ page on topology.pi-base.org.

Tests cover docstring insertion, #pibase_tags, all three URL routes, and malformed IDs.

This PR was prepared with assistance from Codex. Based heavily on #41290

[github-actions]

PR summary 02afce1ebc

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ Lean.TSyntax.getPibaseId
+ p
+ pibaseIdAntiquot.parenthesizer
+ pibaseIdFn
+ pibaseIdKind
+ pibaseIdNoAntiquot
+ pibaseIdNoAntiquot.formatter
+ pibaseIdParser
+ s
+ t

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 02afce1).

• +14 new declarations
• −0 removed declarations

+Lean.PrettyPrinter.Formatter.pibaseIdNoAntiquot.formatter
+Lean.PrettyPrinter.Parenthesizer.pibaseIdAntiquot.parenthesizer
+Lean.TSyntax.getPibaseId
+Mathlib.CrossRef.Database.pibase
+Mathlib.CrossRef.Database.pibase.elim
+Mathlib.CrossRef.Database.pibase.sizeOf_spec
+Mathlib.CrossRef.pibaseIdFn
+Mathlib.CrossRef.pibaseIdKind
+Mathlib.CrossRef.pibaseIdNoAntiquot
+Mathlib.CrossRef.pibaseIdParser
+Mathlib.CrossRef.pibaseIdParser.formatter
+Mathlib.CrossRef.pibaseIdParser.parenthesizer
+Mathlib.CrossRef.pibaseTag
+Mathlib.CrossRef.pibaseTags

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 02afce1ebc
Reference commit 5a0753dc72

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Deicyde]

LLM-generated

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[joneugster]

Thanks for the PR!

[joneugster]

Suggested change

	def url (db : Database) (id : String) : String :=
	match db with
	| .kerodon => "https://kerodon.net/tag/" ++ id
	| .lmfdb => "https://www.lmfdb.org/knowledge/show/" ++ id
	| .pibase =>
	let path := match id.toList with
	| 'P' :: _ => "properties/"
	| 'S' :: _ => "spaces/"
	| 'T' :: _ => "theorems/"
	| _ => ""
	"https://topology.pi-base.org/" ++ path ++ id
	| .stacks => "https://stacks.math.columbia.edu/tag/" ++ id
	| .wikidata => "https://www.wikidata.org/wiki/" ++ id
	def url : Database → String → String
	| .kerodon, id => "https://kerodon.net/tag/" ++ id
	| .lmfdb, id => "https://www.lmfdb.org/knowledge/show/" ++ id
	| .pibase, id =>
	let path := match id.toList with
	| 'P' :: _ => "properties/"
	| 'S' :: _ => "spaces/"
	| 'T' :: _ => "theorems/"
	| _ => ""
	"https://topology.pi-base.org/" ++ path ++ id
	| .stacks, id => "https://stacks.math.columbia.edu/tag/" ++ id
	| .wikidata, id => "https://www.wikidata.org/wiki/" ++ id

more idiomatic pattern