feat(Linter/DocString): ignore Verso linter errors about links and LaTeX

[Vierkantor]

I went through the weekly linting log and found most of the warnings come from three sources. All of these are sensical syntax in our current Markdown dialect, and should be fixed automatically by a script, instead of manually. I expect after these changes we'll be down to hundreds of linter errors rather than two thousand.

• References [between square brackets] without a following link URL. Verso has different implementations for references depending on what kind they are, and since there are a thousand references we should be using a script to fix these.
• Autolinks: bare URLs or URLs between . Autolinks are intentionally not supported by Verso but replacing every https://... with [https://...](https://...) would be too noisy.
• LaTeX blocks: Verso does have TeX blocks but with an incompatible syntax. Better to fix it with a script.

I ended up using preprocessing in addition to postprocessing to filter out errors: using the error message we can determine whether it is a reference, but for errors caused by autolinks and LaTeX blocks I couldn't figure out how to do so easily: the information about the parse error does report a string position but this is always the last character of the docstring. So instead we modify the docstring before it is passed into Verso to get rid of the offending syntax.

---

[github-actions]

PR summary 551ca8f603

Import changes exceeding 2%

%	File
+100.00%	Mathlib.Tactic.Linter.DocString

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Linter.DocString	1	2	+1 (+100.00%)

Import changes for all files

Files	Import difference
There are 7829 files with changed transitive imports taking up over 339393 characters: this is too many to display!
You can run ci-tools/scripts/pr_summary/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ isSilencedVersoWarning
+ lintVersoSyntax

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./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).