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?
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.
I personally lack a good overview of what GSoC entails, so I cannot really say if I'd be available to mentor.
I was actually talking with people about this already
I am more interested in doing a joint GSOC with OCaml
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
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.
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?
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.
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
Maybe notable is not the right term, not enough "mainstream" ? On the other hand we could try again, but I'm unsure
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.
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...
So I think there is a real need to take one / two persons on a common project, but indeed, that's open
And a few cool projects I have in the Coq side, and that could be in scope for Coq, are 100% OCaml programming!
See the old page I did https://github.com/coq/coq/wiki/GoogleSummerOfCode
For example, odoc support for Coq
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?
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.
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
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
but here is what I would probably push in an application:
pretty funny stats here, we have a lot of people, comparatively, using DuckDuckGo to find Coq: https://github.com/coq/coq/graphs/traffic
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.
Interestingly, the Coq repository is the most starred repository on the entire code.gouv.fr platform (just before OCaml).
(It's only the five most forked repository there, though. The most forked one is opam-repository for obvious reasons.)
I didn't see until now that the Coq repo has more stars than OCaml, maybe because OCaml came later to GitHub
No, that doesn't seem to be the explanation: https://star-history.t9t.io/#coq/coq&ocaml/ocaml
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:
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.
hmm, one might consider comparing graphs in this post by Gabriel Scherer with some equivalent for OCaml to look for clues
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
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
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")
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.
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"]
Hi folks, sorry I searched on the wrong stream
Let me cut and paste what I wrote on the dev stream
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
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)I will point people to this Zulip thread in case anyone want to discuss
Last updated: Oct 13 2024 at 01:02 UTC