Documenting non-interactive tactics

Stream: general

[Patrick Massot]

@Mario Carneiro what's the problem with documenting non-interactive tactics?

[Mario Carneiro]

I am not saying don't document it, I'm saying document it in the docstring

[Patrick Massot]

Yes I understand

[Patrick Massot]

my question is why only in the docstring?

[Mario Carneiro]

What is the purpose of general documentation? You want to make people aware that the tactic exists and how to use it. Local tactics need not have this kind of exposure, it is sufficient to have documentation for people who see it and want to know what it does or how it works

[Patrick Massot]

Ok, it's true in this case one can hope people interested in creating such instances will have a look at existing ones, see the tactic and follow the link

[Patrick Massot]

It's difficult for me but ok, I'll go and remove some doc :cry:

[Patrick Massot]

You can go back merging :wink:

[Patrick Massot]

Done

[Kevin Buzzard]

Patrick -- I have pre-docs at https://github.com/kbuzzard/mathlib/tree/WIP_docs/docs/WIPs , just in some branch of my mathlib fork, and you could do the same (and probably do).

[Kevin Buzzard]

When I'm done with affine schemes (and I know I'm always saying this but I am nearly done -- I currently find myself actually working on an interface for localization of rings) I was going to spend some time taking stock and working out what to do next, and I might well spend some time tidying stuff up.