Zulip Chat Archive

Stream: general

Topic: doc display

Rob Lewis (Mar 20 2020 at 14:17):

After the next PR lands, you'll see some changes in the doc display for tactics. Here's a preview: https://robertylewis.com/mathlib_docs/commands.html#add_tactic_doc

From now on, instead of updating tactics.md when you add a new tactic, you should use that add_tactic_doc command instead. There will be a PR to mathlib soon that updates the contribution instructions and deletes the old .md files.

Rob Lewis (Mar 20 2020 at 14:19):

(That PR will also clean up the "tags" on commands/tactics/etc. They're not very well coordinated right now, since there was no convenient way to see them until recently!)

Scott Morrison (Mar 20 2020 at 16:46):

Where will I go to read about all the tactics, once tactics.md is gone?

Johan Commelin (Mar 20 2020 at 16:47):

To the mathlib docs

Patrick Massot (Mar 20 2020 at 16:47):

https://leanprover-community.github.io/mathlib_docs/tactics.html presumably

Gabriel Ebner (Mar 20 2020 at 16:47):

https://leanprover-community.github.io/mathlib_docs/tactics.html

Rob Lewis (Mar 20 2020 at 16:47):

https://leanprover-community.github.io/mathlib_docs/tactics.html

Johan Commelin (Mar 20 2020 at 16:48):

Lolololol

Patrick Massot (Mar 20 2020 at 16:48):

I was first :tada:

Bryan Gin-ge Chen (Mar 20 2020 at 17:05):

We should remember to replace the content of the old markdown files with links to the relevant pages on the mathlib docs page instead of deleting them completely.

Scott Morrison (Mar 20 2020 at 17:37):

Ok. I guess I'll be sad having to leave VSCode, but I understand this is an unpopular opinion. :-)

Patrick Massot (Mar 20 2020 at 17:38):

Did you use to read tactics.md in VScode?

Scott Morrison (Mar 20 2020 at 17:38):

Yees

Patrick Massot (Mar 20 2020 at 17:39):

We can certainly have a button to open the community doc website in VS code

Patrick Massot (Mar 20 2020 at 17:39):

Just like we can read TPIL in VS code

Scott Morrison (Mar 20 2020 at 17:39):

I rely on the search feature in VS Code for everything... in fact if I wanted to read the help on conv, I would type # conv in the search box :-)

Patrick Massot (Mar 20 2020 at 17:40):

The help for any given tactic will still be in the same file as the tactic definition, very close to it.

Gabriel Ebner (Mar 20 2020 at 18:12):

Would it be better if tactic docs were written in doc strings instead of description := "five page string literal"? Then you even get syntax highlighting for the markdown in vscode. #2201

Patrick Massot (Mar 20 2020 at 18:13):

Wasn't it already discussed?

Gabriel Ebner (Mar 20 2020 at 18:17):

Where? Am I missing something?

Patrick Massot (Mar 20 2020 at 18:25):

In the original discussion of this whole tactic doc refactor.

Gabriel Ebner (Mar 20 2020 at 18:27):

I'm sorry. I really can't recall any discussion on it. And I can't find anything relevant on the github PR or on zulip here.

Johan Commelin (Mar 20 2020 at 18:39):

I also remember it being discussed (but don't remember the arguments) and I can't find it back either.

Scott Morrison (Mar 20 2020 at 19:01):

I think we already have this. See abel, for example.

Gabriel Ebner (Mar 20 2020 at 19:14):

Ah, I see what you mean. There is already a functionality to copy doc strings from tactic declarations. The PR adds an additional feature: it also allows you to add descriptions as a doc string that should not go on a tactic declaration (e.g. if you add a common description for a family of multiple tactics).

Gabriel Ebner (Mar 20 2020 at 19:16):

Examples: cache (combines unfreezeI, resetI, and half a dozen other tactics), norm_cast (norm_cast, rw_mod_cast, ...), etc.

Last updated: Dec 20 2023 at 11:08 UTC