Stream: Coq users

Topic: Outreachy and Google Summer of Code for Coq


view this post on Zulip Paolo Giarrusso (Nov 15 2021 at 14:45):

Thinking about “support” tooling, like pycoq/serapi/formatting/IDEs/…, I was wondering whether there would be interesting projects for the GSoC… it seems that Coq has not participated much in the past (https://thealphadollar.me/GSoCOrgFrequency/), and the entry barrier for the core is probably too high, but maybe tooling would be more reasonable?

view this post on Zulip Théo Zimmermann (Nov 15 2021 at 14:56):

That's an interesting angle to approaching Coq for the GSoC indeed! Thanks for raising the issue @Paolo Giarrusso. I know that at least @Emilio Jesús Gallego Arias would be interested.

view this post on Zulip Théo Zimmermann (Nov 15 2021 at 14:57):

I personally lack a good overview of what GSoC entails, so I cannot really say if I'd be available to mentor.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:13):

I was actually talking with people about this already

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:13):

I am more interested in doing a joint GSOC with OCaml

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:13):

Coq was dismissed in the past [we applied once] and the feedback is that it was too marginal for the scope of GSOC, and IMHO they are correct, I CC @Gabriel Scherer just in case

view this post on Zulip Gabriel Scherer (Nov 15 2021 at 15:30):

I don't have time to push for a GSoC application myself, but I think we could find OCaml people interested in helping/supporting, if you wish to work at the OCaml level.

view this post on Zulip Gabriel Scherer (Nov 15 2021 at 15:31):

This being said, I'm very surprised that Coq is not considered notable enough for a GSoc application. Did that rejection happen 15 years ago, when the proof assistant still had an offensive name or something?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:32):

Thanks @Gabriel Scherer , if you could provide to us (in private) a list of OCaml people that could be interested we'd be very happy to discuss more.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:33):

Gabriel Scherer said:

This being said, I'm very surprised that Coq is not considered notable enough for a GSoc application. Did that rejection happen 15 years ago, when the proof assistant still had an offensive name or something?

I think I did apply in 2016/17? I don't think it was due to the name, I agree with them, Coq is a research project and thus a bit out of scope for GSOC

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:33):

Maybe notable is not the right term, not enough "mainstream" ? On the other hand we could try again, but I'm unsure

view this post on Zulip Gabriel Scherer (Nov 15 2021 at 15:34):

Well if you prefer to run through OCaml and you are in fact willing to work for our benefit, it's all the better for us, I guess. But still a shame.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:36):

There is a lot of common OCaml infrastructure we use, such as dune, opam, LSP and UI support could also be shared, we have need for better debugging, performance debugging, evaluation, etc...

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:36):

So I think there is a real need to take one / two persons on a common project, but indeed, that's open

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:37):

And a few cool projects I have in the Coq side, and that could be in scope for Coq, are 100% OCaml programming!

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:38):

See the old page I did https://github.com/coq/coq/wiki/GoogleSummerOfCode

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:38):

For example, odoc support for Coq

view this post on Zulip Yannick Forster (Nov 16 2021 at 16:42):

Emilio Jesús Gallego Arias said:

Maybe notable is not the right term, not enough "mainstream" ? On the other hand we could try again, but I'm unsure

Maybe what is missing is a compact argumentation why Coq should be considered mainstream. If I understand correctly the last application was 6 years ago. Hasn't the number of companies using Coq increased a lot since then?

view this post on Zulip Karl Palmskog (Nov 16 2021 at 16:45):

recall also the popularity ratings discussed here. We also discussed that a large portion of artifacts at POPL and related conferences (many of which are sponsored by Google) are using Coq.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 16 2021 at 17:14):

You all make good points, so indeed maybe we can try Coq alone; I think now we have better support to claim we are a true OSS project thanks to all the work you follks have done

view this post on Zulip Karl Palmskog (Nov 16 2021 at 17:29):

what is usually missing from Coq marketing are all those one-off formalizations people make for papers and private discovery that are seemingly never mentioned outside the specialist communities, not submitted to the opam archive, etc. Getting stats there (as opposed to from GitHub and Stack Overflow) is super hard

view this post on Zulip Karl Palmskog (Nov 16 2021 at 17:40):

but here is what I would probably push in an application:

view this post on Zulip Karl Palmskog (Nov 16 2021 at 17:43):

pretty funny stats here, we have a lot of people, comparatively, using DuckDuckGo to find Coq: https://github.com/coq/coq/graphs/traffic

view this post on Zulip Théo Zimmermann (Nov 17 2021 at 09:10):

Thanks a lot for your summary Karl! And thanks for making me look at this page, it had been a while since I hadn't. I just discovered that we have 39 visitors who came from code.gouv.fr, the platform that the French government just launched a week ago about open source code from public administrations.

view this post on Zulip Théo Zimmermann (Nov 17 2021 at 09:11):

Interestingly, the Coq repository is the most starred repository on the entire code.gouv.fr platform (just before OCaml).

view this post on Zulip Théo Zimmermann (Nov 17 2021 at 09:12):

(It's only the five most forked repository there, though. The most forked one is opam-repository for obvious reasons.)

view this post on Zulip Karl Palmskog (Nov 17 2021 at 09:12):

I didn't see until now that the Coq repo has more stars than OCaml, maybe because OCaml came later to GitHub

view this post on Zulip Théo Zimmermann (Nov 17 2021 at 09:15):

No, that doesn't seem to be the explanation: https://star-history.t9t.io/#coq/coq&ocaml/ocaml

view this post on Zulip Paolo Giarrusso (Nov 17 2021 at 09:19):

Coq has fewer alternatives than OCaml? But it's still surprising the "proof assistant market" is so big! We'll find out it's because of crypto, isn't it? :sweat_smile:

view this post on Zulip Théo Zimmermann (Nov 17 2021 at 09:31):

In terms of industrial users, probably, but in terms of general interest from the (CS) public, I'm pretty sure that's not the only reason.

view this post on Zulip Karl Palmskog (Nov 17 2021 at 09:32):

hmm, one might consider comparing graphs in this post by Gabriel Scherer with some equivalent for OCaml to look for clues

view this post on Zulip Emilio Jesús Gallego Arias (Nov 17 2021 at 10:27):

So folks, are you then intersted in building a Coq-only application? Should we assemble a working group.

IIRC, the most critical step is to have a nice list of projects, we could do a call in coq-club

view this post on Zulip Karl Palmskog (Nov 17 2021 at 10:36):

do you want to do it "core Coq only", or "Coq+ecosystem"? I can have opinions about the latter, but not much on the former

view this post on Zulip Karl Palmskog (Nov 17 2021 at 10:36):

for example, I would count this as Coq+ecosystem, but doesn't touch Coq much: https://github.com/coq-community/manifesto/issues/19 ("Hoogle like search")

view this post on Zulip Théo Zimmermann (Nov 17 2021 at 11:35):

I think it's clearly Coq+ecosystem in the mind of all of us. In fact, the point of Paolo above was that contributing to Coq itself is too hard, and it is mostly by proposing contributions in the ecosystem that we can onboard newcomers.

view this post on Zulip Karl Palmskog (Nov 17 2021 at 18:23):

I forget the most boring measure of all: citations of publications. Probably we should make a list of "top publications related to Coq" and sum up their Google Scholar or Web of Science citations, behold that it's probably many thousands, and declare that this is "excellent" [in the sense of "research excellence"]

view this post on Zulip Emilio Jesús Gallego Arias (Jan 28 2022 at 14:07):

Hi folks, sorry I searched on the wrong stream

view this post on Zulip Emilio Jesús Gallego Arias (Jan 28 2022 at 14:08):

Let me cut and paste what I wrote on the dev stream

view this post on Zulip Emilio Jesús Gallego Arias (Jan 28 2022 at 14:08):

Hi folks, as kindly pointed out by @Gabriel Scherer , GSOC and Outreachy applications for 2022 have just opened.

I'm afraid I'm too busy as of today to lead this, but I'll be happy to help / co-lead would someone else be interested in submitting a proposal for Coq

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 17:18):

Hi folks, as outlined in the Coq call, I've done a call for help with this topic, https://twitter.com/ejgallego/status/1489286346489438211

Hi folks, at @CoqLang we are looking for people interested in being @outreachy and Google Summer of Code mentors. Get in touch if you would like to help! We hope this can help improving the dire situation of our community in terms of diversity, even if minimally.

- Emilio J. Gallego Arias (@ejgallego)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 17:18):

I will point people to this Zulip thread in case anyone want to discuss


Last updated: Jan 31 2023 at 14:03 UTC