roadmap/

Stream: mathlib4

[Mauricio Collares]

There's probably no need to track this in the port dashboard since there are only two math files in there, but should the roadmap directory be ported?

[Mauricio Collares]

I don't know if mathlib3 CI tests it

[Joseph Myers]

I tend to think that the roadmap/ directory is a failed experiment that isn't worth porting. We have several other ways of tracking possible new things to formalize, including (a) GitHub issues in the mathlib and mathlib4 repositories (most of the open mathlib issues are probably also relevant to mathlib4 and it would make sense to move or copy them in some way); (b) GitHub projects at the level of the individual repositories (likewise; mathlib has both "Projects" and "Projects (classic)"); (c) GitHub projects at the level of the leanprover-community organization; (d) entries in .yaml files showing no declaration for a given concept or result (those files definitely need porting to mathlib4 - including both the CI that checks all the named declarations actually exist, and the CI that puts the outputs on the website); (e) formal blueprints used in specific larger projects. I don't think roadmaps are needed in addition to all those mechanisms.

As well as .yaml files needing porting, some miscellaneous .md files such as CITATION.md or archive/imo/README.md should also be ported. And there are a few Lean files in docs/tutorial/, I don't know if those are useful to port.