feat: port addTacticDoc

[lakesare]

Ports the add_tactic_doc and getTacticDocEntries from Lean 3 doc_commands.lean.
A notable change is Lean 3 version used user attributes to memorize the doc entries, Lean 4 version uses environment extension.

Questions

• Should we rename TacticDocEntry just to DocEntry, add_tactic_doc to add_doc_entry, etc.?
• Rename inherit_description_from to inherit_docstring_from?
• Whomever will be reviewing this - please take a look at the related PR at feat: port add_decl_doc #499 (comment), answer to that question will tell us how to name/group our documentation files.

[dwrensha]

tacticDocEntry -> TacticDocEntry

[lakesare]

I used tacticDocEntry as "an instance of TacticDocEntry", is that not a widespread way to say things in Lean?

[dwrensha]

Should we rename TacticDocEntry just to DocEntry, add_tactic_doc to add_doc_entry, etc.?

My opinion is that it's better to keep the old names for now, to maximize discoverability during the port. (I don't think that #align can help us much, because these things are primarily used in tactic files, which are getting ported by hand.) If we want to rename them before the port is done, then backporting the renaming to mathlib3 first seems to me like way to go.

[dwrensha]

It looks like your version actually requires that the TacticDocEntry is split out into a separate def, like this:

def myTde : tde: TacticDocEntry { name := "display name of the tactic",
  category := cat,
  decl_names := [`dcl_1, `dcl_2],
  tags := ["tag_1", "tag_2"] }
  
  add_tactic_doc myTde

Is that right? What is the reason for this change from the mathlib3 version?

[lakesare]

The change is accidental, it should accept a structure!
Do you have some pointers as to what tdeStx:______ should be to accept a structure?

---

Wojciech gave me some pointers (tdeStx:term is already the right type), I'll fix it.

[lakesare]

Fixed this & added a test.

[dwrensha]

This unsafe makes me nervous. Is there a way to avoid it?

[digama0]

This particular pattern is fairly normal, and I would expect it to come up in something like this where we want to make an actual TacticDocEntry from a syntax representing such. This is automated to some extent by declare_config_elab but that is specialized for config arguments in tactics.

[lakesare]

I removed the DocCommands.lean file because we need neither add_decl_doc (it's already implemented in Lean 3) nor copy_doc_string (we can use attribute [inherit_doc ffrom] tto).

Alternatively, we could put addTacticDoc command into DocCommands.lean and describe the new documentation methods in the module docstring (Lean 3's add_decl_doc and inherit_doc).

[dwrensha]

I removed the DocCommands.lean file because we need neither add_decl_doc (it's already implemented in Lean 3) nor copy_doc_string (we can use attribute [inherit_doc ffrom] tto).

Note that Mario already removed this file in #684.

[lakesare]

Should it be merged/are we waiting for the second reviewer, @dwrensha?

[dwrensha]

I don't have the permission to merge, so this is waiting on the review of someone who does.

[digama0]

Can it also support the following syntax:

Suggested change

	add_tactic_doc {
	name := "never defined separately",
	category := DocCategory.hole_cmd,
	decl_names := [`one]
	}
	add_tactic_doc where
	name := "never defined separately"
	category := DocCategory.hole_cmd
	decl_names := [`one]

This is the Command.whereStructInst parser. You can implement this as a macro that expands to the version with the { }.

[lakesare]

It can't!
Not super sure how to do it though (I'm porting another tactic at the moment, so I might only return to learning macros in a few weeks, wouldn't want this PR to go stale in the meantime).

Something along these lines?

macro metaDocString:docComment ? "add_tactic_doc " tdeStx:Lean.Parser.Command.whereStructInst : command => do
  `(add_tactic_doc $tdeStx)

[digama0]

kind of, except that the macro you just wrote calls itself recursively. You would need to convert the where expression into a structure declaration with braces so that you can call the other version of the declaration.

[jcommelin]

This pull request has not seen any activity for quite a while, and it does not pass all CI checks or has merge conflicts. For these reasons, I am closing it now.

If you are still interested in getting this PR merged, please re-open the PR, update the branch, and make sure that all CI checks pass, Please label the PR with awaiting-review when ready.