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 3dfdb5d9f5

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 20ddbc3).

• +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 3dfdb5d9f5
Reference commit f041774a2d

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!

[Deicyde]

-awaiting-author

[joneugster]

Sorry @thorimur, I've simply forgot to self-assign this PR when I looked at it last week!

I've now extracted the part of your style suggestion which affects new code, see comments above.

There's one unresolved suggestion to add a -- TODO to the code to mark existing (and copied) technical debt. I have no clear opinion on that as the PR is just reusing existing patterns.

[Deicyde]

-awaiting-author

[joneugster]

Thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by joneugster.