Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Formal roadmaps need to be explained and documented #2016

Open
1 of 2 tasks
jcommelin opened this issue Feb 19, 2020 · 0 comments
Open
1 of 2 tasks

Formal roadmaps need to be explained and documented #2016

jcommelin opened this issue Feb 19, 2020 · 0 comments
Labels
needs-documentation This PR is missing required documentation

Comments

@jcommelin
Copy link
Member

jcommelin commented Feb 19, 2020 •
edited by robertylewis
Loading

To do:

  • Add some documentation about, like, what a formal roadmap is supposed to be and how people should interact with them. Right now it's a directory with a confusing name and no explanation.
  • It should also be added to CI, or the files in there will rot before too long.

See also https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.231914.20formal.20roadmap/near/188487184
robertylewis added a commit that referenced this issue Feb 20, 2020
@robertylewis
chore(ci): check roadmap directory
4ba5ea6 
partially addresses #2016
@robertylewis robertylewis mentioned this issue Feb 20, 2020
Merged
7 tasks
robertylewis added a commit that referenced this issue Feb 20, 2020
@robertylewis
chore(ci): check roadmap directory (#2022)
43dd938 
* chore(ci): check roadmap directory

partially addresses #2016

* fix roadmap compilation
@robertylewis robertylewis added the needs-documentation This PR is missing required documentation label Feb 25, 2020
@robertylewis robertylewis changed the title Formal roadmaps Formal roadmaps need to be explained and documented Mar 10, 2020
anrddh pushed a commit to anrddh/mathlib that referenced this issue May 15, 2020
@robertylewis @anrddh
chore(ci): check roadmap directory (leanprover-community#2022)
b931566 
* chore(ci): check roadmap directory

partially addresses leanprover-community#2016

* fix roadmap compilation
anrddh pushed a commit to anrddh/mathlib that referenced this issue May 16, 2020
@robertylewis @anrddh
chore(ci): check roadmap directory (leanprover-community#2022)
8bd551c 
* chore(ci): check roadmap directory

partially addresses leanprover-community#2016

* fix roadmap compilation
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
needs-documentation This PR is missing required documentation
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@robertylewis @jcommelin