Stream: CUDW 2020

Topic: WG: Coq ecosystem


view this post on Zulip Jim Fehrle (Nov 17 2020 at 04:09):

What is "Coq Platform" about?

Repeating an earlier comment of mine, I would be interested in the following. Michael gave it a thumbs up. Anyone else? But please schedule at 4 PM CET or later.

One possible topic I've thought about a couple times is a discussion to identify the top 10 improvements we'd like to see in Coq and its ecosystem. I have some ideas (some likely good and some maybe not). I have a limited sense of others' thoughts on this. I'm sure it will include several things that are already in progress, but maybe there are other possible improvements that deserve more attention, perhaps from out-of-the-box thinking. Not sure CUDW is the good forum for this, though.

view this post on Zulip Karl Palmskog (Nov 17 2020 at 06:45):

a general "Coq ecosystem" workgroup sounds good to me. In my mind, this would be complementary to work on the Coq Platform, which is typically about curation of libraries/plugins associated with a Coq major version.

view this post on Zulip Enrico Tassi (Nov 17 2020 at 07:35):

Jim Fehrle said:

One possible topic I've thought about a couple times is a discussion to identify the top 10 improvements we'd like to see in Coq and its ecosystem. I have some ideas (some likely good and some maybe not). I have a limited sense of others' thoughts on this. I'm sure it will include several things that are already in progress, but maybe there are other possible improvements that deserve more attention, perhaps from out-of-the-box thinking. Not sure CUDW is the good forum for this, though.

IMO this is a great point. It would by nice to have a little survey (even here on zulip) of what people would rank

view this post on Zulip Karl Palmskog (Nov 17 2020 at 10:31):

I think an ecosystem topic should also include things like:

view this post on Zulip Jim Fehrle (Nov 30 2020 at 22:22):

Some ideas on how we might better serve the community:

view this post on Zulip Karl Palmskog (Dec 01 2020 at 02:54):

surveys and lists of potential improvements to Coq are great, but Jim's post IMO belongs in the "Coq ecosystem" WG - coq-community focuses on package maintenance and automation to help maintenance.

view this post on Zulip Karl Palmskog (Dec 01 2020 at 03:06):

for example, we will document packages regardless of whether they are recommended for wider use (e.g., by beginners) or not

view this post on Zulip Karl Palmskog (Dec 01 2020 at 08:55):

@Cyril Cohen can you move Jim's post just above to https://coq.zulipchat.com/#narrow/stream/255971-CUDW-2020/topic/WG.3A.20Coq.20ecosystem

view this post on Zulip Théo Zimmermann (Dec 01 2020 at 08:59):

Done. I thought that moving message across topics was something anyone could do.

view this post on Zulip Karl Palmskog (Dec 01 2020 at 09:01):

ah you're right, I forgot that we are all in the same stream

view this post on Zulip Karl Palmskog (Dec 01 2020 at 09:30):

@Emilio Jesús Gallego Arias are you available to chat a bit on BBB sometime before lunch today? E.g., about Dune stuff, SerAPI, etc.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 01 2020 at 10:01):

@Karl Palmskog yes, I'm available

view this post on Zulip Jim Fehrle (Dec 02 2020 at 05:11):

Is there any plan to have an ecosystem discussion this week? Due to the time difference, I have no idea what's going on or what's being planned. Not eager to read every Zulip message to find out--perhaps one of you could let me know if and when there will be a discussion in this channel.

view this post on Zulip Théo Zimmermann (Dec 02 2020 at 09:18):

Nothing has been planned so far, but we can do that, at a time that suits you (maybe after plenaries).

view this post on Zulip Théo Zimmermann (Dec 02 2020 at 09:19):

BTW, with Zulip it is easy to ignore any topic that you are not interested in to be able to focus more specifically on those that matter to you.

view this post on Zulip Jim Fehrle (Dec 02 2020 at 19:35):

Thanks--is Thursday afternoon the only slot left? IIRC Friday is typically only a half day. I would be reluctant to get up early Thursday morning not knowing whether such a session is scheduled. OTOH we could have a discussion another time, it doesn't have to be part of CUDW and might be done without a video conference, perhaps as a CEP discussion.

(I think we could generate an initial "top 10" list with a small group, then have a user survey to refine that list. But doing a survey requires some thoughtful preparation and data summary/analysis afterword. Not to mention ensuring that the survey influences what we do going forward--otherwise why bother doing the survey?)

view this post on Zulip Gaëtan Gilbert (Dec 02 2020 at 20:42):

Friday is typically only a half day.

that's when people have to travel

view this post on Zulip Jim Fehrle (Dec 02 2020 at 20:50):

Yeah, though a lot less travel this year :-(.

view this post on Zulip Karl Palmskog (Dec 02 2020 at 21:53):

Thursday afternoon works for me, but I can also do Friday...

view this post on Zulip Karl Palmskog (Dec 02 2020 at 21:54):

would help if a specific time is suggested so I know when to double-check the BBB/Zulip

view this post on Zulip Jim Fehrle (Dec 03 2020 at 07:21):

How about 5 PM Friday your time?

view this post on Zulip Karl Palmskog (Dec 03 2020 at 07:42):

5pm Friday works for me, but maybe others like Theo could comment as well

view this post on Zulip Théo Zimmermann (Dec 03 2020 at 08:54):

5PM on Friday works for me to. It's better than Thursday since there is the social event on Thursday at that time.

view this post on Zulip Jim Fehrle (Dec 03 2020 at 21:09):

If we do a survey, it would make sense to present the "Top 10 Improvements" as a small part of the Coq Workshops [e.g., the one-day sessions at POPL] if that's timely.

view this post on Zulip Jim Fehrle (Dec 04 2020 at 16:00):

@Théo Zimmermann @Karl Palmskog are you there? Shall we o video?

view this post on Zulip Théo Zimmermann (Dec 04 2020 at 16:00):

Yes, we should go to one of the breakout rooms.

view this post on Zulip Karl Palmskog (Dec 04 2020 at 16:01):

I'm here.

view this post on Zulip Karl Palmskog (Dec 04 2020 at 16:03):

in room 2 now

view this post on Zulip Karl Palmskog (Dec 05 2020 at 03:04):

quick summary of plans:

Other idea: survey of how and for what Coq is used in research (should be repeatable so can be compared over time, "systematic literature review")

view this post on Zulip Karl Palmskog (Dec 05 2020 at 11:00):

Ideas for systematic review questions:

view this post on Zulip Karl Palmskog (Dec 05 2020 at 22:23):

we should also note for posterity Théo's ideas for how to handle comments:

both of these have the advantage of long-term sustainability, i.e., they do not require web application maintenance by community members

view this post on Zulip Théo Zimmermann (Dec 06 2020 at 11:57):

And the discussion favored the second solution for a prototype / MVP.


Last updated: Oct 16 2021 at 07:02 UTC