Roadmap document for standard library std#561

Stream: general

[Mario Carneiro]

Resharing this WIP std4 roadmap in general for greater visibility: Roadmap. We are interested in your feedback, either here or on the PR.

[Thea Brick]

I'm not really sure what is intended by the documentation section? Is it referring to adding descriptions to the mathlib4 docs page or something else entirely?

The other sections of the roadmap seem much more concrete (we will do these things) whereas the documentation section is much more nebulous ("we will describe the tactics").

[Mario Carneiro]

(cc: @Joe Hendrix )

[Mario Carneiro]

I don't think it's nebulous, although it's not particularly detailed, or perhaps we're not sure what else to say about the documentation of tactics. I think we could aim for a little more, like the add_tactic_doc command from lean 3 that allowed classifying tactics and putting them on a unified documentation page.

[Joe Hendrix]

Yes, I would like to have tactics documented in a way that we can both build a reference manual similar to the Mathlib 3 tactic's page and also be able to refer to that when people are writing tutorials, manuals and other documents in Verso. I think my priorities personally are focused on other areas though so it'd be great to get help here both in planning and technical work.

[Bolton Bailey]

I am definitely in favor of more tools for monadic verification, this has been something that would be helpful on one of my projects, and it seems a bit too program-verification related for mathlib.