feat: more infrastructure for tactic documentation

[david-christiansen]

This is the groundwork for a tactic index in generated documentation, as there was in Lean 3. There are a few challenges to getting this to work well in Lean 4:

• There's no natural notion of tactic identity - a tactic may be specified by multiple syntax rules (e.g. the pattern-matching version of intro is specified apart from the default version, but both are the same from a user perspective)
• There's no natural notion of tactic name - here, we take the pragmatic choice of using the first keyword atom in the tactic's syntax specification, but this may need to be overridable someday.
• Tactics are extensible, but we don't want to allow arbitrary imports to clobber existing tactic docstrings, which could become unpredictable in practice.

For tactic identity, this PR introduces the notion of a tactic alternative, which is a syntax specification that is really "the same as" an existing tactic, but needs to be separate for technical reasons. This provides a notion of tactic identity, which we can use as the basis of a tactic index in generated documentation. Alternative forms of tactics are specified using a new @[tactic_alt IDENT] attribute, applied to the new tactic syntax. It is an error to declare a tactic syntax rule to be an alternative of another one that is itself an alternative. Documentation hovers now take alternatives into account, and display the docs for the canonical name.

Tactic tags, created with the register_tactic_tag command, specify tags that may be applied to tactics. This is intended to be used by doc-gen and Verso. Tags may be applied using the @[tactic_tag TAG1 TAG2 ...] attribute on a canonical tactic parser, which may be used in any module to facilitate downstream projects introducing tags that apply to pre-existing tactics. Tags may not be removed, but it's fine to redundantly add them. The collection of tags, and the tactics to which they're applied, can be seen using the #print tactic tags command.

Extension documentation provides a structured way to document extensions to tactics. The resulting documentation is gathered into a bulleted list at the bottom of the tactic's docstring. Extensions are added using the tactic_extension TAC command. This can be used when adding new interpretations of a tactic via macro_rules, when extending some table or search index used by the tactic, or in any other way. It is a command to facilitate its flexible use with various extension mechanisms.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-4490 has successfully built against this PR. (2024-06-18 16:48:36) View Log
• ✅ Mathlib branch lean-pr-testing-4490 has successfully built against this PR. (2024-06-19 06:35:48) View Log
• ✅ Mathlib branch lean-pr-testing-4490 has successfully built against this PR. (2024-06-19 07:43:39) View Log
• ✅ Mathlib branch lean-pr-testing-4490 has successfully built against this PR. (2024-06-19 11:34:01) View Log
• ✅ Mathlib branch lean-pr-testing-4490 has successfully built against this PR. (2024-06-19 13:02:25) View Log
• ✅ Mathlib branch lean-pr-testing-4490 has successfully built against this PR. (2024-06-19 13:57:21) View Log
• ✅ Mathlib branch lean-pr-testing-4490 has successfully built against this PR. (2024-06-20 20:00:07) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d020a9c5a694726b40ac86da353592eda4122ffe --onto 357b52928f905bfb85a3496e411cf12fa20e730c. (2024-06-21 08:53:02)

[robertylewis]

My hotel wifi died and I don't want to get a core dev setup going on phone data, so I'm not 100% sure these code suggestions are right. But this looks fantastic, should do the job very nicely!

[david-christiansen]

@robertylewis I think this should meet your needs now - please give it a whirl at let me know! I don't want to merge before you've had a chance to validate that it supports the workflow that you're looking for.

[david-christiansen]

I like that, but I'll use alt to make the attribute name a bit shorter (@[tactic_alt theRealTactic]).

[david-christiansen]

!bench

[leanprover-bot]

Here are the benchmark results for commit ca52b81.
The entire run failed.
Found no significant differences.

[david-christiansen]

!bench

[leanprover-bot]

Here are the benchmark results for commit 55dc835.
There were significant changes against commit 1cf71e5:

  Benchmark   Metric         Change
  ===========================================
- parser      instructions     1.5% (918.2 σ)

[david-christiansen]

@Kha - what do you think? Is that instruction count hit too severe?