Short-term roadmap for Coq #69
Conversation
|
I think I'd like an item about retiring the STM in the next 6 months, but I was not present during the meeting so I don't know if others want to help with the reviews. More precisely I first want to make the code paths of a simple, linear, compiler agree with what the STM does, or viceversa, and then proceed as discussed in the CEP about CoqIDE. A PR is already open, about side effects, and I think I even have reviewes but needs finishing. But I may need more like that one. |
|
@gares I was hoping to be able to answer at the Coq Call today, but feel free to push commits adding your plans to the roadmap, and then we can check if there are volunteers to help with these plans. Personally, I do not consider it realistic to remove the STM in the next 6 months. Deprecating the STM in the next 6 months (i.e., proving that we do not need to rely on it anymore) would be already quite an achievement, probably. |
|
I meant, we don't need it for coqc. |
Draft rewrite rules for 069-coq-roadmap.md
Co-authored-by: Jim Fehrle <[email protected]>
|
|
||
| - Consolidation of documentation, so that it is easy for users to find | ||
| documentation about the included packages, ideally with a consistant | ||
| presentation. |
There was a problem hiding this comment.
Would be great if opam-installing a package could include its documentation and coqdoc (whether the package is in the platform or not) and then have an easy way to access the doc from the GUI.
Also look at ways to enhance coqdoc to make it more useful.
EDIT: Provide a command to show the logical names of installed packages and their opam package names. The mapping is not available now, you have to know or guess. And a way to get version numbers for packages within Coq.
Co-authored-by: Jim Fehrle <[email protected]>
Talk about the universe polymorphism roadmap
Update 069-coq-roadmap.md
Add STM retirement to 069-coq-roadmap.md
|
I moved the stdlib part (thanks a lot @Zimmi48 for writing it) to the ressource part since @CohenCyril agreed to work on it with me. |
Update 069-coq-roadmap.md
With special focus on short term roadmap for now.
Co-authored-by: Pierre Roux <[email protected]>
| - The long term roadmap is focused on what our vision for the future of Coq is | ||
| and not necessarily how we are going to achieve it. It is used to provide | ||
| general ideas that we can check our medium and short term roadmaps against, | ||
| and to give users more clarity on what the future of Coq could look like. It | ||
| should include our vision of what kind of users Coq will target in the future. |
There was a problem hiding this comment.
I think these thoughts are out of place. We should eventually state the goals for Coq and describe some of the principal user groups. Then items in the roadmap fit into those goals. That should be earlier in the document, maybe at the beginning of the motivation section. But maybe not fleshed out in any detail in this version of the roadmap.
Co-authored-by: Jim Fehrle <[email protected]>
SkySkimmer
force-pushed
the
coq-roadmap
branch
from
556219e
to
609c3b4
Compare
| - Gaëtan Gilbert, Pierre Maria Pédrot | ||
| - in progress (maybe done by 8.21) | ||
| - notably https://github.com/coq/coq/pull/19228 | ||
|
|
||
| Make template poly more usable and more robust, basing the metatheory on sort poly. | ||
|
|
||
| TODO: | ||
|
|
||
| - metatheory in metacoq (?) | ||
| - allow template univs which don't appear in the conclusion | ||
| (eg `u` in `eq : forall A:Type@{u}, A -> A -> Prop`) | ||
| - remove above-Prop restriction in template poly (?) | ||
| - I feel like I forgot something but can't remember what |
|
Sorry, I accidentally deleted the branch. Did not intend to close this PR (until we decide what the new living format for the short-term roadmap will be). |
This is a draft PR for now because each item in the list should be completed with some more precise description of what they mean, what the planned outcomes are, etc. This work can only be done by those who proposed the items on the roadmap. Furthermore, we may need to add missing items or move items around, depending on actual availability of people to work on them.
Rendered: https://github.com/coq/ceps/blob/coq-roadmap/text/069-coq-roadmap.md