Stream: CUDW 2020

Topic: WG: Coq ecosystem

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.

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.

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

Karl Palmskog (Nov 17 2020 at 10:31):

I think an ecosystem topic should also include things like:

• outside perceptions/image of Coq, marketing
• attracting new people to Coq usage and development
• facilitating community sustainability/growth

Jim Fehrle (Nov 30 2020 at 22:22):

Some ideas on how we might better serve the community:

• Do a community survey to understand users' needs and perceptions, akin to the recent OCaml survey
• Develop a "top 10 most beneficial improvements to Coq" statement reflecting the survey, filed issues, our ideas and plans, perhaps how we differentiate Coq from similar tools. Perhaps identifying which user subgroups an improvement is most important to. I'm sure we're already doing some of these.
• Create a website that catalogs available Coq developments, allowing comments on packages, etc. Benjamin Pierce suggested this to me about 2 years ago, he thought it would make a real difference for the community.

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.

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

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

Théo Zimmermann (Dec 01 2020 at 08:59):

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

Karl Palmskog (Dec 01 2020 at 09:01):

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

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.

Emilio Jesús Gallego Arias (Dec 01 2020 at 10:01):

@Karl Palmskog yes, I'm available

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.

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

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.

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?)

Gaëtan Gilbert (Dec 02 2020 at 20:42):

Friday is typically only a half day.

that's when people have to travel

Jim Fehrle (Dec 02 2020 at 20:50):

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

Karl Palmskog (Dec 02 2020 at 21:53):

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

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

Jim Fehrle (Dec 03 2020 at 07:21):

How about 5 PM Friday your time?

Karl Palmskog (Dec 03 2020 at 07:42):

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

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.

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.

Jim Fehrle (Dec 04 2020 at 16:00):

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

Théo Zimmermann (Dec 04 2020 at 16:00):

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

Karl Palmskog (Dec 04 2020 at 16:01):

I'm here.

Karl Palmskog (Dec 04 2020 at 16:03):

in room 2 now

Karl Palmskog (Dec 05 2020 at 03:04):

quick summary of plans:

• CEP for survey of the Coq community (not just coq-community), including question on what versions people are using, what usage problems they have, wishlist of features
• CEP for new package website which crucially includes possibility of commenting on packages (but not rating the "best")

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")

Karl Palmskog (Dec 05 2020 at 11:00):

Ideas for systematic review questions:

• What are the principal areas in which researchers apply Coq?
• Who are the researchers that apply Coq (e.g., affiliation, nationality)?
• How has the applications of Coq changed over time (w.r.t. area, researchers)?

Karl Palmskog (Dec 05 2020 at 22:23):

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

• relying on an external system with spam protection like Disqus;
• using GitHub's pull request system and let only GitHub users add manually reviewed comments to static website

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

Théo Zimmermann (Dec 06 2020 at 11:57):

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

Last updated: Oct 13 2024 at 01:02 UTC