Stream: Coq devs & plugin devs

Topic: roadmap


view this post on Zulip Ali Caglayan (Jun 23 2022 at 12:24):

@Maxime Dénès where can we find the roadmap?

view this post on Zulip Maxime Dénès (Jun 23 2022 at 12:28):

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.

view this post on Zulip Maxime Dénès (Jun 23 2022 at 12:28):

Unfortunately, we spent less time during the working group on the roadmap than I had hoped. But we'll catch up.

view this post on Zulip Ali Caglayan (Jun 23 2022 at 12:39):

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?

view this post on Zulip Maxime Dénès (Jun 23 2022 at 13:13):

I won't be able to do it immediately. But yes, it will be shared internally so that core devs can contribute to it.

view this post on Zulip Maxime Dénès (Jun 23 2022 at 13:20):

And of course this is just for the boostrapping process, the roadmap and contributions to it are meant to be public.

view this post on Zulip Théo Zimmermann (Jun 23 2022 at 13:37):

Ali is not a core dev for instance. Probably we can work on a public document as long as it is called a draft.

view this post on Zulip Karl Palmskog (Jun 23 2022 at 13:46):

OK, so are you sharing this stuff with non-core? would be interested in taking a look (read only).

view this post on Zulip Enrico Tassi (Jun 23 2022 at 14:29):

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...

view this post on Zulip Maxime Dénès (Jun 25 2022 at 08:14):

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.

view this post on Zulip Maxime Dénès (Jun 25 2022 at 08:14):

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.

view this post on Zulip Maxime Dénès (Jun 25 2022 at 08:16):

And I agree with Enrico, the next step is a dedicated call. The document is almost empty for now...

view this post on Zulip Gaëtan Gilbert (Jun 25 2022 at 08:16):

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

view this post on Zulip Maxime Dénès (Jun 25 2022 at 08:17):

I didn't say the bootstrapping should be strictly restricted to core devs, btw.

view this post on Zulip Maxime Dénès (Jun 25 2022 at 08:17):

The point is to minimize entropy and make it more comfortable for core devs to express their constraints.

view this post on Zulip Matthieu Sozeau (Jun 25 2022 at 08:32):

@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.

view this post on Zulip Enrico Tassi (Jun 25 2022 at 14:25):

@Matthieu Sozeau are these rules written somewhere? It would be good to give them some formality, IMO.

view this post on Zulip Matthieu Sozeau (Jun 25 2022 at 14:27):

Right, I can do that as well.

view this post on Zulip Ali Caglayan (Oct 04 2022 at 17:57):

Hello, any progress on the roadmap?

view this post on Zulip Maxime Dénès (Oct 05 2022 at 12:32):

Not yet, but we will resume the work on it soon.

view this post on Zulip Cyril Cohen (Jul 19 2023 at 09:26):

Now the roadmap is there how to contribute to it? Personally I'd like to contribute an item about the standard library.

view this post on Zulip Cyril Cohen (Jul 19 2023 at 12:23):

@Théo Zimmermann

view this post on Zulip Théo Zimmermann (Jul 19 2023 at 12:25):

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.

view this post on Zulip Théo Zimmermann (Jul 19 2023 at 12:27):

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.

view this post on Zulip Karl Palmskog (Aug 01 2023 at 07:27):

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

view this post on Zulip Maxime Dénès (Aug 01 2023 at 07:43):

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