Conversation
| /-- | ||
| Serves as a global storage for all `TacticDocEntry`s we have added throughout mathlib codebase. | ||
| When [doc-gen](https://github.com/leanprover-community/doc-gen) generates documentation, it will | ||
| access this storage to find each `tacticDocEntry` along with its greatest-priority docstring. |
There was a problem hiding this comment.
tacticDocEntry -> TacticDocEntry
There was a problem hiding this comment.
I used tacticDocEntry as "an instance of TacticDocEntry", is that not a widespread way to say things in Lean?
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 |
| /-- | ||
| describe what the command does here | ||
| -/ | ||
| add_tactic_doc |
There was a problem hiding this comment.
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 myTdeIs that right? What is the reason for this change from the mathlib3 version?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
Fixed this & added a test.
Mathlib/Tactic/AddTacticDoc.lean
Outdated
| elab metaDocString:docComment ? "add_tactic_doc " tdeStx:term : command => do | ||
| -- 1. Turn tde:TSyntax argument into the actual tde:TacticDocEntry object | ||
| let tdeName : Name ← resolveGlobalConstNoOverloadWithInfo tdeStx | ||
| let tde : TacticDocEntry ← unsafe evalConstCheck TacticDocEntry ``TacticDocEntry tdeName |
There was a problem hiding this comment.
This unsafe makes me nervous. Is there a way to avoid it?
There was a problem hiding this comment.
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.
|
I removed the Alternatively, we could put |
Note that Mario already removed this file in #684. |
|
Should it be merged/are we waiting for the second reviewer, @dwrensha? |
|
I don't have the permission to merge, so this is waiting on the review of someone who does. |
| add_tactic_doc { | ||
| name := "never defined separately", | ||
| category := DocCategory.hole_cmd, | ||
| decl_names := [`one] | ||
| } |
There was a problem hiding this comment.
Can it also support the following syntax:
| 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 { }.
There was a problem hiding this comment.
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)
There was a problem hiding this comment.
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.
…kesare_add_tactic_doc
This reverts commit 9cd961f.
|
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 |
Ports the
add_tactic_docandgetTacticDocEntriesfrom 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
TacticDocEntryjust toDocEntry,add_tactic_doctoadd_doc_entry, etc.?inherit_description_fromtoinherit_docstring_from?