@Maxime Dénès where can we find the roadmap?
I didn't publish it yet. We will probably need to finish organizing the contribution to all core devs to it, to start with something that makes sense.
Unfortunately, we spent less time during the working group on the roadmap than I had hoped. But we'll catch up.
If you don't want to publish it just yet, could you create a private repo so that we can give some suggestions and feedback?
I won't be able to do it immediately. But yes, it will be shared internally so that core devs can contribute to it.
And of course this is just for the boostrapping process, the roadmap and contributions to it are meant to be public.
Ali is not a core dev for instance. Probably we can work on a public document as long as it is called a draft.
OK, so are you sharing this stuff with non-core? would be interested in taking a look (read only).
Can't we just finish it? Instead of discussing the level of secrecy of a 10 lines draft? As in making a dedicated call ASAP...
The document will be shared, discussed and elaborated publicly, after it is first bootstrapped internally. Doing it publicly from the start has failed in the past, because people are less willing to make explicit their personal constraints and agenda.
I realize it is a bit frustrating to discuss publicly (here) a document that is not yet public. Which is precisely why I had avoided doing it.
And I agree with Enrico, the next step is a dedicated call. The document is almost empty for now...
Théo Zimmermann said:
Ali is not a core dev for instance. Probably we can work on a public document as long as it is called a draft.
What's the definition of core dev again? Maybe we should promote Ali
I didn't say the bootstrapping should be strictly restricted to core devs, btw.
The point is to minimize entropy and make it more comfortable for core devs to express their constraints.
@Gaëtan a core dev is in the core team (as reflected in the team page), currently the process is that someone of the core team proposes a new member and if everyone agrees I add him to the team. Core devs get right to vote on issues like the current renaming question. We added Jason (last year IIRC), we can propose Ali's integration as well, I'm also in favor of including him.
@Matthieu Sozeau are these rules written somewhere? It would be good to give them some formality, IMO.
Right, I can do that as well.
Hello, any progress on the roadmap?
Not yet, but we will resume the work on it soon.
Now the roadmap is there how to contribute to it? Personally I'd like to contribute an item about the standard library.
@Théo Zimmermann
I guess you can either write your item as a comment in the PR thread, or as a PR as Théo did in https://github.com/coq/ceps/pull/70.
Note the rules though (https://github.com/coq/ceps/blob/coq-roadmap/text/069-coq-roadmap.md#detailed-design), items that are deemed important may be added to the "Other axes, without sufficient resources" part easily, but getting to the first part means that we have secured commitments from several persons to work on them.
something that was not clear to me even after roadmap discussion at Coq Workshop: since VsCoq2 has official Inria support/resources, shouldn't it be part of the roadmap? I think users will find it very useful to know that there is an "official long term supported GUI" for Coq
Sure, it would be natural that the Coq roadmap mentions VsCoq. VsCoq having its own detailed roadmap.
Last updated: Sep 09 2024 at 05:02 UTC