Gabriel Scherer (Oct 17 2020 at 19:17): Gabriel Scherer (Oct 17 2020 at 19:17):@Talia Ringer (Gitter import) reminded me that I should advertise the OCaml User Survey 2020 within the Coq community. If you have some experience with programming in OCaml directly, please participate to the survey!
(cc @Théo Zimmermann, who is in charge of the upcoming Coq User Survey 2020, see also https://github.com/tchajed/coq-survey .)
Karl Palmskog (Oct 18 2020 at 18:17):@Gabriel Scherer just curious whether the OCaml Software Foundation accepts anonymous ad-hoc donations of smaller amounts, like the Inria foundation does for Coq development. This is not clear to me from the website, which seems 100% targeted at industrial partnerships: https://ocaml-sf.org/becoming-a-sponsor/
Karl Palmskog (Oct 18 2020 at 18:20):in my opinion, having people "vote" on inclusion of features/improvements by targeted donations would be nice (both for Coq and OCaml)
Théo Zimmermann (Oct 18 2020 at 18:23):You probably meant @Talia Ringer. I'll disable the other account.
Karl Palmskog (Oct 18 2020 at 18:24):@Théo Zimmermann maybe you can open a discussion somewhere for the Coq User Survey (e.g., here or on GitHub), I have some input on questions if it's not too late
Théo Zimmermann (Oct 18 2020 at 18:24):Gabriel Scherer said:
(cc Théo Zimmermann, who is in charge of the upcoming Coq User Survey 2020, see also https://github.com/tchajed/coq-survey .)
Am I? Have I announced such a thing anywhere?
Théo Zimmermann (Oct 18 2020 at 18:25):There will certainly be no such thing in 2020. In the future, sure, that'd be a great thing to do.
Karl Palmskog (Oct 18 2020 at 18:26):ah, I got my hopes up for a moment, but would be nice for 2021 for sure.
Paolo Giarrusso (Oct 18 2020 at 18:27):@Karl Palmskog where can I find details on that donation scheme? I was only aware of https://coq.inria.fr/consortium
Karl Palmskog (Oct 18 2020 at 18:28):Gabriel can confirm, but in retrospect it may have been a question without the question mark: "who is in charge of the upcoming Coq User Survey 2020 [question mark here]"
Karl Palmskog (Oct 18 2020 at 18:29):Paolo Giarrusso said:
Karl Palmskog where can I find details on that donation scheme? I was only aware of https://coq.inria.fr/consortium
you have the general statement on that page:
If you wish to financially support the development of Coq and its community, you can make a donation to Inria. Please contact Maxime Dénès.
Karl Palmskog (Oct 18 2020 at 18:30):a donation is in my view very different from sponsorship. I'm happy to donate to Coq development, but I have no intention of becoming a "Coq sponsor [or consortium member]" in any capacity, anonymous or not (same for OCaml)
Paolo Giarrusso (Oct 18 2020 at 18:31):Ah I misread; "targeted donations" was a proposal
Théo Zimmermann (Oct 18 2020 at 18:32):I believe that these donations are still relatively non-trivial to set up, so they are not typically thought for individuals wanting to donate a couple dozen euros.
Karl Palmskog (Oct 18 2020 at 18:32):right [about it being a proposal to do targeted donations]. I'm sure there are lots of reasons why people don't do it, but it would be nice
Karl Palmskog (Oct 18 2020 at 18:33):@Théo Zimmermann 5K EUR is a very high bar still (which is the one set by OCaml)
Karl Palmskog (Oct 18 2020 at 18:41):anyway, I guess I can make public my biggest OCaml complaint (which was asked about in the survey): the still-very-high complexity in build management and packaging of OCaml-based projects. I've developed/built Coq-extraction-based projects for maybe 5 years now, and the number of gotchas and breadth of knowledge required is close to the absurd. Right now, we are also seemingly caught in a pain spot where we are trying to migrate to Dune but have to support all old build management
Gabriel Scherer (Oct 18 2020 at 19:31):Re. targeted donations: no, unfortunately right now we cannot do this. Our administrative people don't know how to do it in a scalable way, due to (not-so-good processes and) a legal requirement in France that you give a "fiscal receipt" to each donor.
Gabriel Scherer (Oct 18 2020 at 19:33):I was not aware that the Coq Consortium accepted individual donations (is it really the case?), but it may be bcause it doesn't have the same sort of non-profit status?
In any case, at the OCaml Software Foundation we have been asking our admin. for individual dontations, and hopefully one day they will be possible.
Karl Palmskog (Oct 18 2020 at 19:39):I asked an organization to do an ad-hoc donation to the Coq Consortium in lieu of payment for some work I did, and Maxime recently confirmed it appeared on his end. But I interpret what Gabriel says as that something like this would not be possible with OSF (which is regrettable)
Maxime Dénès (Oct 20 2020 at 12:26):@Gabriel Scherer AFAIK, there is no requirement to emit a "fiscal receipt" for a donation, unless you want eligibility to some tax exemption.
Maxime Dénès (Oct 20 2020 at 12:27):Inria knows how to setup individual donations, they do it for some projects like Plantnet and Scikit-learn (I believe)
Maxime Dénès (Oct 20 2020 at 12:28):I mean small individual donations
Maxime Dénès (Oct 20 2020 at 12:28):the Coq Consortium doesn't accept donations of a dozen euros, like @Théo Zimmermann said, but that's primarily because the administrative overhead is too high
Maxime Dénès (Oct 20 2020 at 12:31):For plantnet for example, you can see they accept paypal donations, so I guess small individual ones : https://plantnet.org/en/donations/
Maxime Dénès (Oct 20 2020 at 12:31):and it is operated by a foundation, so I guess the same status as the OCaml Software Foundation
Maxime Dénès (Oct 20 2020 at 12:35):my understanding was that the Inria Foundation didn't want to work on such crowd-funding strategies for not-so-huge projects like OCaml or Coq
Maxime Dénès (Oct 20 2020 at 12:40):I guess one thing that is more complex is the compatibility of the concept of "targeted donation" w.r..t the French law
Maxime Dénès (Oct 20 2020 at 12:41):What would be fine is to have a pool of resources made by collecting donations, and use polls to understand how we want to use these resources
Maxime Dénès (Oct 20 2020 at 12:42):But for example, restricting the poll to donators would most likely be going against the definition of a donation in the French law
Maxime Dénès (Oct 20 2020 at 12:42):(we'd need to ask a jurist, of course)
Théo Zimmermann (Oct 20 2020 at 12:47):And what about setting up a specific project corresponding to some user demand (a priori) and asking for donations to support this project? That would amount to targeted donations, but probably more in line with the French law...
Maxime Dénès (Oct 20 2020 at 13:08):Yes, this seems fine to me too
Karl Palmskog (Oct 21 2020 at 16:42):one thing that would be interesting to hear is where in the Coq ecosystem more resources (e.g., manpower ) would help the most. Not obvious to me at all whether this is in "core Coq" or Coq tooling or infrastructure
Cody Roux (Oct 21 2020 at 17:43):There can never be enough tooling. I have often been wishing for better "hammers", which I think is on the map, slightly more informative Search, which is (sort of?) on the map and nice, well-integrated basic analysis libraries which I think has gotten better.
Karl Palmskog (Oct 21 2020 at 17:45):@Cody Roux did you try sauto? Let's just say that part of CoqHammer is something that I think the community is underusing at the moment
Karl Palmskog (Oct 21 2020 at 17:48):and as a tool developer/packager, it is not easy to reach users, even with effort spent on packaging, etc. Many are even unaware of the basics of coq_makefile, which comes bundled with Coq
Paolo Giarrusso (Oct 21 2020 at 17:57):IIRC, coq_makefile is never mentioned in software foundations — or has that changed?
Karl Palmskog (Oct 21 2020 at 17:58):coq_makefile is a sort of unsung hero in that with the right scripting on top it works back to Coq 8.5, and is near-certain to be an improvement over the horrors that people inflict on their custom Coq makefiles
Paolo Giarrusso (Oct 21 2020 at 18:03):the million $ question becomes how to integrate it with your custom makefile — cargo culting is strong there
Paolo Giarrusso (Oct 21 2020 at 18:05):uh, I had missed https://coq.github.io/doc/v8.12/refman/practical-tools/utilities.html#reusing-extending-the-generated-makefile
Karl Palmskog (Oct 21 2020 at 18:06):that example is bad IMO
Karl Palmskog (Oct 21 2020 at 18:07):it gives the right idea, but from my recollection it screws up PHONY for CoqMakefile.local
Gaëtan Gilbert (Oct 21 2020 at 18:24):why is KNOWNFILES phony in that?
Paolo Giarrusso (Oct 21 2020 at 18:31):I wanted to say, for once, that the manual was actually fine, to my surprise, and I didn’t have the heart to compare it to my usual source.
Paolo Giarrusso (Oct 21 2020 at 18:32):Anyway, if somebody fixes that (not volunteering), the leftover problems are just that proof general spoils you, and that IME few people try to look at the manual.
Paolo Giarrusso (Oct 21 2020 at 18:34):my user experience was “let’s teach a fellow PhD student to use Coq” “let’s be gentle and not use emacs but coqide (in ~2014-2016)” “wait can you split your code in two files, why doesn’t that work”
Cody Roux (Oct 21 2020 at 20:09):@Karl Palmskog Slight hypocrisy on my part: I've never tried CoqHammer in earnest, partly for the legitimate reason of trying to keep my dependencies down, but also somewhat out of laziness. coq_makefile I do use, and it's great.
Théo Zimmermann (Oct 21 2020 at 21:04):The sauto tactic does not need any other dependency than just CoqHammer.
Karl Palmskog (Oct 22 2020 at 06:01):and inadvertently, this illustrates my point that existing tooling is likely to be underused, especially tooling that is a "dependency". With the Coq platform, there will be fewer excuses for not adding dependencies.
Pierre Courtieu (Oct 22 2020 at 09:06):Karl Palmskog said:
and inadvertently, this illustrates my point that existing tooling is likely to be underused, especially tooling that is a "dependency". With the Coq platform, there will be fewer excuses for not adding dependencies.
Suppose we had a working info, then it would be interesting to have a tool that replaces all uses of say sauto by the output of info sauto. This would 1) speed up script but more importantly 2) remove the dependency.
Paolo Giarrusso said:
the leftover problems are just that proof general spoils you, and that IME few people try to look at the manual.
Interesting, can you elaborate on this?
Karl Palmskog (Oct 22 2020 at 09:13):reading the sauto paper, I'm not at all convinced info sauto would reasonably be able to provide anything intelligible that you would want in your source code. Better that we assume everyone has the Coq Platform fully installed and CoqHammer is part of the platform
Karl Palmskog (Oct 22 2020 at 09:24):I think we will have to accept that dependency minimization will (and should) give a worse and worse experience over time for Coq users, unlike for other proof assistants (e.g., Isabelle, HOL4 , HOL Light bundle a ton of stuff, and seem to include more and more over time). I would prefer "core Coq" to be about solving issues like Unifall rather than maintaining/distributing lots of proof automation tools
Théo Zimmermann (Oct 22 2020 at 09:40):I hope that users will view depending on the platform as some form of dependency minimization since this will offer guarantees that go beyond the usual dependency usage.
Pierre Courtieu (Oct 22 2020 at 09:48):Karl Palmskog said:
reading the sauto paper, I'm not at all convinced
info sautowould reasonably be able to provide anything intelligible that you would want in your source code. Better that we assume everyone has the Coq Platform fully installed and CoqHammer is part of the platform
I see your point, but I was not suggesting to really expand sauto in the source code but rather have a "release code". In source code I think info could be used to have a cache for any automatic tactic.
Ralf Jung (Oct 22 2020 at 12:02):Karl Palmskog said:
it gives the right idea, but from my recollection it screws up PHONY for
CoqMakefile.local
yeah I had lots of "fun" with that in the Iris Makefile
Paolo Giarrusso (Oct 22 2020 at 12:14):@Pierre Courtieu the spoling is from "compile before require", which coqide doesn't have.
Paolo Giarrusso (Oct 22 2020 at 12:14):(or vscoq, or probably coqtail)
Pierre Courtieu (Oct 24 2020 at 21:57):That is indeed a great feature from Hendrik Tews. Especially now that it supports vos mode.
Karl Palmskog (Nov 15 2020 at 16:23):for anyone following this, results from the survey here: https://docs.google.com/forms/d/1OZV7WCprDnouU-rIEuw-1lDTeXrH_naVlJ77ziXQJfg/viewanalytics
Karl Palmskog (Nov 15 2020 at 16:27): Karl Palmskog (Nov 15 2020 at 16:46):also interesting (if I'm reading correctly):
"The three OCaml pillars", maybe?
Enrico Tassi (Nov 16 2020 at 18:27):I recommend reading "What is a pain point when learning the OCaml language?", then think about Coq
Last updated: May 31 2023 at 04:01 UTC