Cyril Cohen (Jul 06 2020 at 10:39): Cyril Cohen (Jul 06 2020 at 10:39):The organic growth of the stdlib is what led us to the current status, so encouraging PRs without a clear baseline (for refactoring or growing) seems to me like a dangerous thing.
Théo Zimmermann (Jul 06 2020 at 10:43):Cyril Cohen said:
The organic grows of the stdlib is what led us to the current status, so encouraging PRs without a clear baseline (for refactoring or growing) seems to me like a dangerous thing.
There's a big difference though which is that the organic growth happened without any reviews. The PR mechanism changed everything!
Cyril Cohen (Jul 06 2020 at 10:45):Théo Zimmermann said:
Cyril Cohen said:
The organic grows of the stdlib is what led us to the current status, so encouraging PRs without a clear baseline (for refactoring or growing) seems to me like a dangerous thing.
There's a big difference though which is that the organic growth happened without any reviews. The PR mechanism changed everything!
Well, I agree it changes something, I disagree it changes everything: what will the reviewers say if they do not follow a common goal that has been clearely announced? How to encourage contributing if the review is going to arbitrate a posteriori on the content. Example: I refactor the stdlib (let's say I extract relevant parts of mathcomp using Maxime's work) and I PR it to Coq... what will be the answer?
Théo Zimmermann (Jul 06 2020 at 10:46):Cyril Cohen said:
Théo Zimmermann said:
Cyril Cohen said:
The organic grows of the stdlib is what led us to the current status, so encouraging PRs without a clear baseline (for refactoring or growing) seems to me like a dangerous thing.
There's a big difference though which is that the organic growth happened without any reviews. The PR mechanism changed everything!
Well, I agree it changes something, I disagree it changes everything: what will the reviewers say if they do not follow a common goal that has been clearely announced? How to encourage contributing if the review is going to arbitrate a posteriori on the content. Example: I refactor the stdlib (let's say I extract relevant parts of mathcomp using Maxime's work) and I PR it to Coq... what will be the answer?
There's a rather small stdlib-maintainers team and I don't see much dissensus within it.
Cyril Cohen (Jul 06 2020 at 10:48):@Théo Zimmermann so if there is not "much dissensus" within the stdlib-maintainer, maybe they can make a manifesto of the stdlib, so everyone can know in which direction to contribute and which refactorings are encouraged/discouraged, which naming conventions are ok and not ok, etc?
Pierre-Marie Pédrot (Jul 06 2020 at 10:50):@Cyril Cohen we have no naming convention, no fixed style for the statement of lemmas, and so on so forth
Pierre-Marie Pédrot (Jul 06 2020 at 10:50):I don't think reviewing helped in that respect, things are done using the "wet finger" technique
Cyril Cohen (Jul 06 2020 at 10:50):Pierre-Marie Pédrot said:
Cyril Cohen we have no naming convention, no fixed style for the statement of lemmas, and so on so forth
So, when there is a PRs, how is the suggestion of name changes, restatement, missing stuff handled?
Cyril Cohen (Jul 06 2020 at 10:51):Pierre-Marie Pédrot said:
I don't think reviewing helped in that respect, things are done using the "wet finger" technique
I guess this is the answer of my question...
Pierre-Marie Pédrot (Jul 06 2020 at 10:51):To the taste of the reviewer, which are not even consistent within their own brain
Cyril Cohen (Jul 06 2020 at 10:51):Pierre-Marie Pédrot said:
To the taste of the reviewer, which are not even consistent within their own brain
Are you an stdlib maintainer?
Pierre-Marie Pédrot (Jul 06 2020 at 10:51):I think I used to be
Pierre-Marie Pédrot (Jul 06 2020 at 10:52):I do receive notifications for reviews on some components of the stdlib, but I am not fully aware of which ones
Pierre-Marie Pédrot (Jul 06 2020 at 10:52):But now I am mostly inactive since the situation is fairly depressing
Théo Zimmermann (Jul 06 2020 at 10:54):I think Pierre-Marie's view does not reflect the reality of stdlib maintenance nowadays.
Cyril Cohen (Jul 06 2020 at 10:56):Théo Zimmermann said:
I think Pierre-Marie's view does not reflect the reality of stdlib maintenance nowadays.
Fine. Could [you and other stdlib maintainers] provide an answer to my questions?
Théo Zimmermann (Jul 06 2020 at 10:56):@Anton Trunov could maybe join the discussion when he's available [I'm not a maintainer myself but followed the activity closely]
Pierre-Marie Pédrot (Jul 06 2020 at 10:57):@Théo Zimmermann @Cyril Cohen it is undoubtedly true that there is no written rule for naming nor style
Anton Trunov (Jul 06 2020 at 11:00):Hi everyone, I'm here, just joined the zoom link
Karl Palmskog (Jul 06 2020 at 11:09):my initial question that arguably triggered the Stdlib discussion was:
Q: What's the core devs' opinions on the Stdlib development? Should it grow more or be or just be maintained? Should Coq itself be "partial" to Stdlib, given that there are (arguably) other libraries of similar status?
Cyril Cohen (Jul 06 2020 at 11:10):And @Théo Zimmermann 's answer (please correct me) was roughly that "the Stdlib is not dead, please feel free to send PRs". Then follows my original post at the top of this topic.
Karl Palmskog (Jul 06 2020 at 11:11):basically, I was hoping for a more clear direction for Stdlib than the one hinted at by Hugo and Théo (I think Cyril's comments are spot on w.r.t. this)
Anton Trunov (Jul 06 2020 at 11:12):Example: I refactor the stdlib (let's say I extract relevant parts of mathcomp using Maxime's work) and I PR it to Coq... what will be the answer?
@Cyril Cohen I personally think that would be a very valuable addition as long as it is backwards compatible or e.g. deprecates some things with a clear reason for doing so, etc.
Anton Trunov (Jul 06 2020 at 11:13):I agree we should have a contributing guide for the stdlib
Cyril Cohen (Jul 06 2020 at 11:14):Anton Trunov said:
Example: I refactor the stdlib (let's say I extract relevant parts of mathcomp using Maxime's work) and I PR it to Coq... what will be the answer?
Cyril Cohen I personally think that would be a very valuable addition as long as it is backwards compatible or e.g. deprecates some things with a clear reason for doing so, etc.
Does this mean that stdlib2 is a clear consensus of stdlib maintainers?
Maxime Dénès (Jul 06 2020 at 11:15):Today stdlib2 is a project that is independent from stdlib.
Maxime Dénès (Jul 06 2020 at 11:15):IMHO it is a bit early to talk about consensus, because we are still exploring for example the compat/breakage tradeoff.
Théo Zimmermann (Jul 06 2020 at 11:16):Indeed, let's keep the discussions of stdlib1 / stdlib2 separate.
Maxime Dénès (Jul 06 2020 at 11:16):For example, I have this branch where I try to re-express the stdlib prelude on top of stdlib2.
Théo Zimmermann (Jul 06 2020 at 11:16):The discussion here was about stdlib1.
Karl Palmskog (Jul 06 2020 at 11:16):yes, I only ever talked about Stdlib1
Cyril Cohen (Jul 06 2020 at 11:16):I think it is very relevant. Would you encourage people contributing to stdlib1 rather than focusing efforts on stdlib2?
Théo Zimmermann (Jul 06 2020 at 11:16):And my point was precisely that stdlub1 is still alive as long as stdlib2 is under development.
Maxime Dénès (Jul 06 2020 at 11:16):The pb is I hit a lot of bugs related to features of Coq (like primitive projections, tactics) before being even able to evaluate the compatibility story.
Théo Zimmermann (Jul 06 2020 at 11:17):stdlib2 is not really open to external contributions yet...
Maxime Dénès (Jul 06 2020 at 11:17):Indeed, but just because it is a bit early in terms of stage.
Maxime Dénès (Jul 06 2020 at 11:17):So I'd say people should be free to contribute to stdlib1 meanwhile, or to wait and see where stdlib2 goes.
Maxime Dénès (Jul 06 2020 at 11:19):But I didn't see an answer to @Cyril Cohen's question: how are stdlib1 PRs evaluated? Especially in terms of adherence to the recommended style.
Maxime Dénès (Jul 06 2020 at 11:20):(I saw PMP's answer, but then it was dismissed without a correction)
Maxime Dénès (Jul 06 2020 at 11:21):Théo Zimmermann said:
And my point was precisely that stdlub1 is still alive as long as stdlib2 is under development.
Even after probably, it would make sense to keep a minimally maintained stdlib1 for developments that haven't yet been ported.
Théo Zimmermann (Jul 06 2020 at 11:22):Yeah, it's a bit hard for me to do long answers while also organizing the workshop. That's why I called Anton to participate in this discussion. But I can also write longer answers in a few days when I recover.
Anton Trunov (Jul 06 2020 at 11:22):Let me outline some informal guidelines the stdlib maintainers follow.
Right now we expect
Cyril Cohen (Jul 06 2020 at 11:27):@Anton Trunov thanks. Can you give details for your two last points?
Paolo Giarrusso (Jul 06 2020 at 11:40):If stdlib1 is a collection of libraries, once Coq-platform is up, one could think about _splitting_ portions of it into separate libraries.
Paolo Giarrusso (Jul 06 2020 at 11:42):That worked for the Scala community, which also had similar problems for similar reasons (born in an academic setting without much code review, and later transitioned to an industrial language).
Paolo Giarrusso (Jul 06 2020 at 11:44):Also, a separate libraries can be released much more often than the stdlib, while mixing Coq 8.10 with stdlib 8.10.1 is impossible — or can that change?
Anton Trunov (Jul 06 2020 at 11:45):@Cyril Cohen Those are great questions! Unfortunately, to give precise answers would amount to writing an stdlib contributing guide :)
I'm sorry for being evasive here, but let me suggest to go on an adhoc basis here. (I guess you have the mathcomp style in mind, my personal opinion is that it's totally fine)
We are trying to make contributing to the stdlib a more welcoming process and I think that the overwhelming majority of PRs get merged eventually.
To comment on the "eventually" part: I think that we significantly reduced time intervals needed to merge a PR lately.
I would like to encourage you to open a PR or an issue if you'd like to discuss the concrete changes you are proposing.
Anton Trunov (Jul 06 2020 at 11:46):I hope @Hugo Herbelin could also comment here.
Enrico Tassi (Jul 06 2020 at 11:47):I've the feeling that if you want to boost stdlib1 you should start moving out everything that is not a stdlib (logics, paradoxes, type theory, the reals, ... files with french names, ...). Some of these are very interesting to me, but I can hardly imagine them begin of general interest. A bit like what @Paolo G. Giarrusso hints to.
Enrico Tassi (Jul 06 2020 at 11:50):Maybe it's a silly parallel, but before tiding up my "spontaneously organized" garage, I push everything out (but for what is already in its place) ;-)
Anton Trunov (Jul 06 2020 at 11:50):Even the structure of GitHub teams suggest that to a certain extent -- we have a dedicated team of maintainers for the reals :)
Anton Trunov (Jul 06 2020 at 11:51):We can certainly try splitting those things out if there is a consensus from the whole of Coq team
Paolo Giarrusso (Jul 06 2020 at 11:51):and the updates to the reals library sounded orthogonal to Coq evolution
Paolo Giarrusso (Jul 06 2020 at 11:52):but let me reinforce: IMHO you need the platform being ready first, to minimize impact on users.
Paolo Giarrusso (Jul 06 2020 at 11:53):Hm: can/should you keep the logical paths after such a split? If not, is that a problem?
Enrico Tassi (Jul 06 2020 at 11:54):The "idea" is moving the reals out was quite consensual a long ago, but since then Vincent pushed many improvements and he is a big fan of the monorepo approach... I'm pretty sure he would not be happy.
I totally agree that with a solid platform to move things to, the process could be way more consensual.
Paolo Giarrusso (Jul 06 2020 at 11:58):Oh, aren't changes to reals isolated to theories/Reals? If they aren't, that complicates things.
Anton Trunov (Jul 06 2020 at 12:01):I think it's mostly isolated to theories/Reals, but QArith and setoid_ring and micromega plugins depend on Reals
Paolo Giarrusso (Jul 06 2020 at 12:02):Beyond that, "separate opam packages", "separate release cycles" and "separate repos" _can_ be separate decisions. coq-reals could be a distinct library that's still released in sync with Coq...
Paolo Giarrusso (Jul 06 2020 at 12:03):@Anton Trunov no clue on reals, wonder how hard would it be to split them...
Paolo Giarrusso (Jul 06 2020 at 12:04):let me confess: it's great Coq has reals, but I'm afraid I won't use them anytime soon (the parts of SF I studied don't either).
Paolo Giarrusso (Jul 06 2020 at 12:06):so, not much clue there in particular.
Also I wouldn't mind if Coq compiled faster, after splitting those out.
Anton Trunov (Jul 06 2020 at 12:06):me too :) that's something a lot of verification / PL people would want
Bas Spitters (Jul 06 2020 at 12:14):@Vincent Semeria, @Michael Soegtrop @Hugo Herbelin and @Guillaume Melquiond have been involved in a discussion on the stdlib reals.
Karl Palmskog (Jul 06 2020 at 12:24):+1 to pulling the reals and other non-core parts out of Stdlib
Emilio Jesús Gallego Arias (Jul 06 2020 at 12:25):A small comment, we are ready to actually turn the stdlib into it's own package (c.f.: https://github.com/coq/coq/pull/12567) This could be helpful in terms of organization
Vincent Semeria (Jul 06 2020 at 16:42):The plan we have with @Michael Soegtrop , @Hugo Herbelin and @Guillaume Melquiond is to carve out CoRN's fast reals into a new and independent OPAM package, that will be part of the Coq platform and that we will recommend as the constructive real analysis in Coq.
Karl Palmskog (Jul 06 2020 at 16:59):correct me if I'm wrong here, but isn't Coq the only major proof assistant which has an extensive body of results in constructive real analysis? I think this can be a flagship project of its own which may attract students and others interested in intuitionism
Vincent Semeria (Jul 06 2020 at 17:39):Indeed, I do not know another repository of constructive mathematics as big as Coq's CoRN. We do want to give a good place to constructive mathematics in the Coq platform, so that they are used and people can contribute. We thought of delivering all of CoRN in the platform, but we think it's too big. We'll start with constructive real analysis.
Théo Zimmermann (Jul 06 2020 at 18:59):Great to see you here @Vincent Semeria!
Théo Zimmermann (Jul 06 2020 at 18:59):Earlier @Enrico Tassi said:
The "idea" is moving the reals out was quite consensual a long ago, but since then Vincent pushed many improvements and he is a big fan of the monorepo approach... I'm pretty sure he would not be happy.
Vincent is already a major contributor and maintainer of CoRN and has moved parts of his contributions that were still experimental out of the stdlib to CoRN.
Théo Zimmermann (Jul 06 2020 at 19:00):I think the most important distinction today to make between stdlib and non-stdlib is that stdlib is very stable (in the sense that it has to make Coq's full CI compile, even if overlays are needed).
Théo Zimmermann (Jul 06 2020 at 19:01):Every experimental and unstable code is more appropriately contributed to external libraries.
Théo Zimmermann (Jul 06 2020 at 19:02):On the other hand, wanting to pull large (stable) parts out of the Coq repo is IMHO begging for the "bignums disaster".
Théo Zimmermann (Jul 06 2020 at 19:02):But I'm all in favor of splitting the stdlib in smaller components that can even be distributed as separate opam packages!
Théo Zimmermann (Jul 06 2020 at 19:03):(And having one maintainer team for each of these components and working are making these smaller components more self-consistent---which should be easier than making the whole stdlib more self-consistent.)
Théo Zimmermann (Jul 06 2020 at 19:04):All I'm saying is that splitting the parts that ought to be stable out of the Coq repository is going to bring little benefit and lots of drawback.
Enrico Tassi (Jul 06 2020 at 19:33):Théo Zimmermann said:
On the other hand, wanting to pull large (stable) parts out of the Coq repo is IMHO begging for the "bignums disaster".
IIRC what went wrong here is that some ML code (hard to compile by third parties) was moved out and stopped being tested (hence broke many times).
Bas Spitters (Jul 06 2020 at 20:16):@Théo Zimmermann just to connect some dots: the plan with @Vincent Semeria is to connect the stdlib reals with corn and math-classes.
{ In fact. to connect it again, as this was done before, to compute with classical real numbers. ]
The design criteria for math-classes, extlib and stdlibpp are all quite similar due to overlap in contributors.
So, if we want to connect some more, that could be a place to start.
Théo Zimmermann (Jul 06 2020 at 20:34):Enrico Tassi said:
Théo Zimmermann said:
On the other hand, wanting to pull large (stable) parts out of the Coq repo is IMHO begging for the "bignums disaster".
IIRC what went wrong here is that some ML code (hard to compile by third parties) was moved out and stopped being tested (hence broke many times).
I might be mistaken but I don't believe it ever stopped being tested. What went wrong (IMHO) is that we are unable to properly maintain several repositories at once as a team (as also witnessed by the general state of the www repository where PRs take sometimes months to years to get answered).
Hugo Herbelin (Jul 06 2020 at 22:11):@CyrilCohen: I feel quite in line with @Anton Trunov's answer. In particular:
what style should new files in the library adhere to (namings, modules/TC/CS, currying, phrasing, Prop/Type/bool, allowed tactics and proof style...)?
My current view about accepting PRs in the standard library boils down to 1) be consistent with the existing style of the file / part of the library it is added 2) seize the opportunity of an addition to possibly improve the overall consistency 3) the observation that there is no strong consensus of what a tactic script should look like, regarding more-compact vs more-pedestrian style, regarding the amount of use of automation, regarding the level of details (like by/now vs assumption/discriminate/...), etc., thus no strong constraint on proof styles (except use of bullets for structurations and easier debugging + naming of used hypotheses for better robustness) 4) pay attention to what is done in other "stdlib" and possibly take benefit of the experience of other libraries.
My own view about Prop/Type/bool is that all are relevant, so my conclusion is that there is a need for each of them and my recommendation would be to provide all variants with an appropriate naming to distinguish between them (like adding b or _bool for properties to bool, adding _type for properties to Type). That's not always so simple, though. Sometimes, an hProp put in Type behaves differently than when put in Prop for limitations of the tactics (IIRC), while it should be equivalent.
About currying, I have no strong opinion. I suspect it is rare that statements are not curryed in the standard library. More generally, I'd be tempted to adopt the point of view that a "smart" apply should be able to automatically reason modulo currying, as we do in mathematics.
The same for Prop and bool. There is a level of abstraction, which we should be able to teach to Coq, where it should not make a difference whether your statement is formulated of the form leb n p = true or le n p (which roughly means having a unification algorithm able to use "views" on the fly). More generally, there should be a level of abstraction where reasoning in bool or in decidable Prop should not make a different to the user (though I don't know exactly how to implement this).
About TC vs CS, I should add that there is first a debate between nested algebraic structures vs flattened algebraic structures. I'm convinced that a proof assistant should be able to manage a graph of inclusion of structures implicitly, but I'm not fully convinced that structures should absolutely adopt a nested representation (like it is in CoRN or MathComp). It is maybe just that I'm missing experience, and I'm very eager to get more comments about it, but in the case of real numbers, for instance, I feel that the flat approach of the standard library is clearer and easier to manipulate than the CoRN approach.
About modules, I'm personally not a big fan of higher-order modules (functors), but there is an interest in modules for extraction to OCaml. So, it is somehow also a matter of taste. Also, the use of modules for Arith and ZArith to share a large bunch of lemmas at once makes sense to me (even if coqdoc is not able to render the final content in a useful way).
In any case, thanks for asking these kinds of questions. We need to discuss more about these things to make progresses (and we should not exclude changing Coq itself when relevant).
Hugo Herbelin (Jul 06 2020 at 22:27):A few more thoughts about the discussion:
We should define what a standard library is and clarify whether we are talking about a standard library or a collection of standard contents.
For instance, lists, arithmetic, algebra, logic, real analysis, relations, orders, big ops, hott, category theory, etc., etc., etc. all seem relevant to me as components of a standard library.
We should valorize every work contributing to standard content.
For instance, Coq newcomers should easily find what standard contents are available to them, with explanations of the specificities/rationales/advantages of this or that library providing contents about this or that subject. Of course, providing such an explanation is quite a lot of work since it already requires to be able to compare libraries. But I believe we are enough users to have studied different libraries to be able to provide such summaries. Then, this information should be available the opam page, from the coq-community page, from the platform page, from the current stdlib page.
Regarding the stdlib, there is no reason to throw the baby out with the bathwater; in particular, many users are dependent on the standard library and there is no reason to force them to break their development, and even less if they are willing to improve the standard library.
There are many technical (and difficult) questions about how to develop standard contents.
The naming issue is somehow one of the simplest. As mentioned by @Cyril Cohen bool reasoning vs Prop reasoning; algebraic hierarchy vs flat structures; type classes, coercions, canonical structures; partial functions to option or with default value, or with side condition, dependently-typed data structures vs data structures annotated with a side condition, etc. are all difficult technical questions.
At the current stage of growth of Coq, I'm a bit dubious that a consensus on what a standard library should look like can ever be obtained. I believe that we have more to gain at allowing improvements of the libraries, at establishing gateways between different libraries providing similar results (logipedia-style, œcumenical) than at looking for an ideal about which there are little reasons it shall be the same for everyone (but I may also be wrong).
A direction I think we could investigate as soon of now is to focus on a few delimited libraries, such as Booleans, lists, and reals, and to see what can be done to get the best of all existing approaches. I'd be tempted to seek for making available to all users the sup of all what has been proven and is available. Looking in this direction would force us also to improve Coq.
Bas Spitters (Jul 07 2020 at 07:37):Thanks @Hugo Herbelin that is very thoughtful.
About the corn hierarchy, it's 20 years old, and coq has improved since then. That was one of the reasons we started math-classes, to experiment with the then new type classes. Meanwhile, there is an interesting proposal from lean to improve type class search. They claim it should work for Coq too. @robbert also asked for improvements to unification, something that @Maxime Dénès is working on.
I'd like to see an experiment with @Enrico Tassi s hierarchy builder on (such new) type classes.
There are interesting experiments in both agda and Ahrend with type classes. We've discussed them here before, I could try to find them again if someone turns this discussion into something more structured.
Bas Spitters (Jul 07 2020 at 07:38):About modules for extraction, I wonder what can be done now that we have the experiments with verified extraction using meta-coq.
Enrico Tassi (Jul 07 2020 at 08:22):Théo Zimmermann said:
Earlier Enrico Tassi said:
The "idea" is moving the reals out was quite consensual a long ago, but since then Vincent pushed many improvements and he is a big fan of the monorepo approach... I'm pretty sure he would not be happy.
Vincent is already a major contributor and maintainer of CoRN and has moved parts of his contributions that were still experimental out of the stdlib to CoRN.
That is great! I guess he changed his mind a little then, or I misunderstood his position in the first place. Anyway, this indicates we can eventually move the reals out.
Paolo Giarrusso (Jul 07 2020 at 08:23):@Bas Spitters On hierarchy-builder + typeclasses, IIUC @Janno has done some recent experiments but run into trouble; @robbert also tried combining CS and typeclasses (without HB), but he was blocked by tactic unification/w_unify. There are some comments in https://gitlab.mpi-sws.org/iris/iris/-/issues/303, but probably they can summarize better themselves.
Enrico Tassi (Jul 07 2020 at 08:32):Paolo G. Giarrusso said:
Bas Spitters On hierarchy-builder + typeclasses, IIUC Janno has done some recent experiments but run into trouble
Janno faced a bug in HB we still have to investigate (my bad): https://github.com/math-comp/hierarchy-builder/issues/72
Bas Spitters (Jul 07 2020 at 08:39):@Paolo G. Giarrusso thanks. I don't see the bug with w_unify discussed. Has it been reported?
Karl Palmskog (Jul 07 2020 at 08:41):another comment on Stdlib contributions besides the 6+ month release cycle: it's not very simple for newcomers to build/install Coq master, which is currently a requirement for any Stdlib contributions. I see this also as an argument for breaking out things from Stdlib (even in the face of bignums-like issues). Separate libraries can have more relaxed requirements on which versions they build on.
Paolo Giarrusso (Jul 07 2020 at 08:47):@Bas Spitters I don't know if it's a bug, w_unify is just different and "deprecated", except you can't avoid it easily with typeclasses.
Paolo Giarrusso (Jul 07 2020 at 08:49):And fixing that is part of the Unifall project — but it's not easy.
Paolo Giarrusso (Jul 07 2020 at 08:56):Actually — I could at least link to https://gitlab.mpi-sws.org/iris/iris/-/issues/303#note_48993, where Robbert does mention "w_unify" (he writes "old unification", but that's what he means). Math-comp devs also mentioned in this WS trying to use typeclasses, they might have run into similar problems.
Anton Trunov (Jul 07 2020 at 09:25):Karl Palmskog said:
another comment on Stdlib contributions besides the 6+ month release cycle: it's not very simple for newcomers to build/install Coq
master, which is currently a requirement for any Stdlib contributions. I see this also as an argument for breaking out things from Stdlib (even in the face of bignums-like issues). Separate libraries can have more relaxed requirements on which versions they build on.
Can't the newcomer clone the Coq repo, use a release version of Coq to modify the stdlib, open a PR and just rely on CI?
Karl Palmskog (Jul 07 2020 at 09:32):I guess this is possible in theory, but is it user-friendly when you likely get a slew of build failures?
Bas Spitters (Jul 07 2020 at 09:34):Thanks. That may be a good datapoint for @Maxime Dénès then...
Enrico Tassi (Jul 07 2020 at 09:42):I believe splitting out the development of any stdlib can work as long as we have a working platform thing. The day we release Coq at least the standard library has to work. In some sense the release of Coq coincides with the release of a core of the platform, which includes the stdlib.
This looks reasonable to decouple the development of Coq and stdlib, but I don't see a good story for really decoupling the release of the two which is what @Karl Palmskog seems to advocate with the objective to ease the contribution and increase the reward for contributors.
Am I right in this "summary"?
Karl Palmskog (Jul 07 2020 at 09:50):it's not only about increasing rewards/incentives for contributors. Coq releases have been known to be 10-12 months apart. This means that no library fixes (say, for earlier versions of Coq) can reach any library users during this time (assuming Coq/stdlib are in the same repo/tarballs/etc.). There could also come a point where it becomes impossible to both support the current stable Coq version and the upcoming Coq version, which means that stable Coq users will be forced to upgrade to get any updates at all. With separate releases, you can still support the stable Coq users with fixes.
Christian Doczkal (Jul 07 2020 at 09:50):@Enrico Tassi , I think you only half-right. Yes, the stdlib should be compatible with Coq the day of the release, but that doesn't mean is has to make a release the day Coq makes a release. This would only be the case when the Coq release introduces a change that can neither be anticipated nor allows for cross-version compatibility.
Karl Palmskog (Jul 07 2020 at 09:58):but for clarity, I think we should distinguish "repo separation" and "project separation". It's definitely possible to run two "different" projects, with their own contribution guidelines, CI pipeline, maintainers, etc. in the same repo. What I think we are discussing here is whether the only user delivery of a "separate"/decoupled stdlib should be via Coq releases, e.g., in Coq release tarballs.
Enrico Tassi (Jul 07 2020 at 09:58):FTR Coq major releases are 6 months apart now, this is what we currently try to implement (with some delays, but we are not too far off). It used to be 9 month before that, and unbounded before that ;-). Between major releases there are typically two point releases.
I agree with you both w.r.t the coupling of Coq and the stdlib, I was indeed to strict/defensive.
Karl Palmskog (Jul 07 2020 at 10:01):OK, so regarding point releases. The policy of most RMs has been extremely conservative in point releases (absolutely don't break anything). If this will continue, there basically can't be any stdlib updates in point releases.
Karl Palmskog (Jul 07 2020 at 10:11):one summary of my view might be: handle Stdlib development/releases like MathComp does (but not necessarily with a parallel infrastructure). For example, MC 1.11.0 is already out and will be compatible with 8.12.0, but there could be a release of MC later during the 8.12 cycle.
Paolo Giarrusso (Jul 07 2020 at 10:47):I indeed run into this recently: if you want to upstream some utility code for Coq 8.11, I can submit a patch to stdpp, depend on a new stdpp snapshot tomorrow and drop my copy; and that code is also usable with Coq 8.8.2. That might work with MC today, but is unrealistic with the stdlib _with the current policy_.
Paolo Giarrusso (Jul 07 2020 at 10:48):As a data point, I created a "fix" to https://github.com/coq/coq/issues/12147, and I use it, but I submitted it to stdpp: https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/149.
Hugo Herbelin (Jul 07 2020 at 11:35):@Karl Palmskog: Is your point that maintenance, evolutions, extensions of the stdlib, or of components of it, would be more active, or even, maybe, be taking more ambitious directions, if moved to coq-community repositories? If yes, how would you organize this development?
Karl Palmskog (Jul 07 2020 at 11:41):@Hugo Herbelin I think I've stated my reasons above for decoupling Stdlib (make it possible to depend on versions of stdlib independently of Coq like MathComp, a dedicated/optimized workflow for Stdlib contributions, independent-of-Coq releases that can contain "fresh" improvements for stable Coq). The question of a pulling out code to coq-community (or some repo in the Coq org) can be discussed separately, since it could all be done inside the coq/coq repo if that's what maintainers would prefer. But I think decoupled releases are crucial.
Decoupling doesn't automatically bring in more active development, but I think it would make contributions less daunting than today, with faster turnaround time from PR to release. Maintainers could be more radical in accepting changes when they know that users can depend on previous releases (even with new Coq), and upgrade at their own pace.
W.r.t. organization, it could mean Stdlib maintainers become more independent of Coq maintainers, make plans for revision/extension that are independent of Coq features/compatibility, etc. In the Coq Platform, Stdlib becomes more akin to "one library you can choose to use, if you want to", and not what everybody is recommended/supposed to use.
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:19):Certainly decoupling the stdlib would have some advantages, and the problems with sync would remain mostly the same. Whether to put it in a separate repos or not is also a question. Likely, Coq would have to vendor it anyways I think.
Cyril Cohen (Jul 07 2020 at 21:10):@Hugo Herbelin
I tend to interpret your comment and the one below it as advocating for a continuation of the organic growth of the stdlib as it was, preserving the style of the existing and extending in whatever self-consistent way PRs are suggested, thus potentially combining results written in various styles without any uniformization criterion. This is exactly what I deemed dangerous. IMHO an stdlib is the last place where the absence of consensus should be allowed.
Illustrating various features should be done in a dedicated gallery repo/package/dir, with pointers to full fledged libraries exploiting them (if any). Compatibility with the current stdlib can be preserved (so that no one's development breaks) by pulling it out as suggested in this thread, and perhaps the most important change is renaming it, since it's for me one of the most confusing part: the stdlib has nothing standard about it.
Cyril Cohen (Jul 07 2020 at 21:15):In summary, my dearest wish about it is either a clear and sound standardization, or a public and official confession of non standardness... (or both)
Paolo Giarrusso (Jul 07 2020 at 22:12):How reasonable would it be, maybe after splitting the stdlib in smaller pieces, to make the entire current naming scheme part of the Compat modules?
Compat modules, you get in addition the historic names, say using Notations.That's a massive amount of work, but even before that — is it even feasible, or is the result unusable due to excessively many bugs?*
*Bug number 1: You can't alias modules. No, Module B := A. isn't usable. You might think it is, except it duplicates all hints in A. Because hints are available on Require not Import, and B counts as required :sob:
Emilio Jesús Gallego Arias (Jul 07 2020 at 22:20):Note that we could do the split right now, if you look at https://github.com/coq/coq/pull/12567 then only thing to do is to see how we handle the naming of the ocaml packages
Emilio Jesús Gallego Arias (Jul 07 2020 at 22:20):the most logical thing would be to have something such as coq depending on coq-core and coq-stdlib
Paolo Giarrusso (Jul 07 2020 at 22:24):Well, you might want to split things in even smaller libraries before trying that. If that needn't wait for the platform, that's cool. But the more you want to do, the more coordination will take — you don't want to rush these things have to fix them later, IMHO, and as I personally learned from Robbert.
Paolo Giarrusso (Jul 07 2020 at 22:25):And to answer to @Hugo Herbelin directly: mentally alpha-renaming is far from free when needed in papers, or with libraries. Once you start using a library with consistent names, you can _predict_ names and write, dunno rewrite lookup_insert or rewrite fmap_cons lookup_cons and have it work — or almost.
Hugo Herbelin (Jul 09 2020 at 07:29):@Cyril Cohen: My point is not to advocate organic growth, I was precisely saying that my recommendation was to respect the style of the specific library in which a modification is made (by specific library, I mean List, or Bool, or QArith, etc. knowing that each of them was developed by different persons or groups of persons; the later is actually probably more characteristic of the status of the "stdlib" than the term "organic growth").
I was not advocating for not looking for consensus, I was advocating for minimal consistency rules over which I believe we all agree, observing precisely that there does not seem to exist a consensus on how to build a library (bool/Prop/Type, flat/nested algebraic structures, modules/TC/CS, proof styles, notations attached to structures vs notations attached to instances of the structures, ...). And it is because of this absence of consensus that my conclusion was that the only reasonable approach was to be "œcumenic".
In practice, we have to do with the different components of the "stdlib" as they are, which de facto are used and (as far as I can judge) accepted as they are by many users. The standard-library-relevant contents developed around should be advertised at their due value and this was also the point of my message.
In summary, my dearest wish about it is either a clear and sound standardization, or a public and official confession of non standardness... (or both)
Personally, and this engages only me, I don't believe that we have reached a point where it is clear how to build a proof assistant and a fortiori how to build a "standard" library. Of course, we are able to build libraries that exploit some features, like small scale reflection, canonical structures, type classes, modules, -no-indices-matter, ... but I would not claim that one approach is the "standard" one (or preferred one). This view is maybe deceiving for users who would like a message telling that "we" know what is good, but as far as I'm concerned, I'm not able to deliver such message. So, at the end, I don't know what kind of standardization we can expect more than organizing the different approaches in compatible ways (as I described above). In the meantime, there are libraries (in the Coq ecosystem) which can be used, and which we maintain, and I don't know what more you think should be done (than what I suggested to do above).
@Cyril Cohen, I don't know what you exactly intend by "clear" and "sound" standardization. I can only repeat that the "stdlib" is made of different components made by different people, at different stages of the history of Coq, and providing consistency within a component seems a reasonable enough goal. I don't believe that we can hope more w/o the investment of more people.
Hugo Herbelin (Jul 09 2020 at 07:29):More specifically, about decoupling the releases of what is called "stdlib", I have no opinion. What has been said above by different people seems to make sense to me.
Hugo Herbelin (Jul 09 2020 at 07:31):@Paolo Giarrusso: Regarding naming schemes, I don't think that providing a different naming of lemmas would be a big deal to implement (we have the experience of tools for that). The difficult part is rather to arrive to a naming scheme which is relatively consensual within the community.
Maybe could you also explain what you have in mind when you say "changed to the correct names".
Hugo Herbelin (Jul 09 2020 at 07:32):Regarding proof styles, as said above, I observe big differences between people and I'm not sure that there exists strong arguments in favor of one style over another beside a few basic rules (indentation, bullets, naming). Moreover, if we really want one day to uniformize proof styles, I'm pretty sure we would be able to develop tools able to apply refactoring rules to proof scripts.
If the question is about standardizing a way to write proofs, I see no evidence that we find a consensus in the community beyond a few rules such as the one I described. This is something which evolves with time if not with fashion, and which is also very personal.
Hugo Herbelin (Jul 09 2020 at 07:32):More about naming:
Paolo Giarrusso (Jul 09 2020 at 08:17):On the last point: AFAIK, neither Google nor Microsoft have offered support for synonyms in an IDE. And IDEs require very large investments, which often require a large user base (to some extent; both Coq and Agda have better IDEs than Haskell with fewer users).
Paolo Giarrusso (Jul 09 2020 at 08:22):I dispute that the stdlib is accepted. math-comp replaces it, while stdpp modifies lots of stdlib choices in more or less invasive ways.
Paolo Giarrusso (Jul 09 2020 at 08:26):Having local consistency is better than nothing, but the wish is for library-scale consistency.
Théo Zimmermann (Jul 09 2020 at 08:35):Folks! This discussion is a huge effort to follow. If you want anything to come out of it, you should make concrete proposals and open dedicated topics / issues / CEPs to discuss them. I have an opinion on a lot of these issues, but I'm certainly not going to answer anymore to share them here.
Paolo Giarrusso (Jul 09 2020 at 08:36):And it's true that many Coq coding styles are possible — some questions have more _technical_ tradeoffs (CS/TC/modules/...), others not.
Even in other languages, choosing one coding style does not require showing that it's better than others, nor absolute consensus.
It _might_ require a BFDL, but one that earned people's trust (like Haskell's committee "syntax czar", per Haskell's HOPL paper) — but that's a more sociological matter, maybe closer to @Théo Zimmermann's dissertation topic.
Paolo Giarrusso (Jul 09 2020 at 08:38):(I agree with @Théo Zimmermann and I'll stop now; can't carve out topics myself now, but I'd be happy to join them).
Hugo Herbelin (Jul 09 2020 at 20:57):Paolo Giarrusso said:
On the last point: AFAIK, neither Google nor Microsoft have offered support for synonyms in an IDE. And IDEs require very large investments, which often require a large user base (to some extent; both Coq and Agda have better IDEs than Haskell with fewer users).
I'm unsure to agree. Writing completion in CoqIDE was not very costly for instance. And I believe that providing a CoqIDE mode where, when, after an apply or rewrite a special key allows to give Search which pops up a menu where you can choose the statement you intend to use, would not be so difficult. (I'm talking about CoqIDE which I know better, but I guess this would be similar in other UIs). Don't you believe so?
[If there is some interest in discussing the feasibility of such feature and/or thinking at how to design such feature, in one UI or the other, and to avoid digressing too much here, I can open a new topic in the UI stream]
Hugo Herbelin (Jul 09 2020 at 22:43):Paolo Giarrusso said:
I dispute that the stdlib is accepted. math-comp replaces it, while stdpp modifies lots of stdlib choices in more or less invasive ways.
I guess it depends on people. The people I'm used to work with uses mostly stdlib. Regarding math-comp, I don't know it very well. I know that there are people who loves it but there are also people to tell that it is difficult to enter and constrained to a given style [note that I'm here reflecting what I heard, not statistics!].
In any case, I don't see how we can avoid to have to take into account the needs of everyone.
Hugo Herbelin (Jul 09 2020 at 22:45):Paolo Giarrusso said:
It _might_ require a BFDL, but one that earned people's trust (like Haskell's committee "syntax czar", per Haskell's HOPL paper) — but that's a more sociological matter, maybe closer to Théo Zimmermann's dissertation topic.
I believe that there is tradition in Coq to be more welcoming than dictatorial. Already with Gérard Huet, the "standard library" was made of contributions from different people. Christine Paulin had also a policy to welcome contributions. For instance Sets was done in Sophia, ZArith was done by a contributor in Brittany.
When Georges Gonthier started the 4-color and Feit-Thompson projets, he could have decided to work consensually with the existing stdlib but, what I saw is that, and I think this is what others perceived too, he preferred to explore his own way with his own conventions (actually it is not clear to me that he intended to build a "standard library"; what I perceived is that he intended to build as directly as possible a solid mathematical infrastructure for reaching the 4-color then Feit-Thompson achievements). Personally, I would have liked that he and his group seized the opportunity of the 4C and Feit-Thompson theorem to contribute to a common project which federated all users but as far as I can tell, this is not what happened, or at least not in extents we could have expected.
I don't know the motivation of ext-lib and stdpp but I don't believe they are to be opposed to the "stdlib" (since you know stdpp more, maybe you'd like to tell more about it).
(BTW, if you want to talk about standard contents, CoRN, UniMath and HoTT have also a lot to say.)
In any case, in the absence of the tradition of a BDFL for Coq, I believe that one thing we can do, and should do, is that all people having to contribute something to standard libraries work together at finding a common ground. This is a reason for my call to try to experiment at doing so on relatively well-delimited libraries such as bool, lists and reals. And this is actually also a motivation for having proposed a "library" topic at the coq workshop.
There are different questions. Among the easy ones, there is the naming of lemmas, the order of arguments, the naming of arguments (x, y or n, m, or n1, n2, etc), the curryfication or not of hypotheses, the implicit status of arguments, ... If a consensus is obtained in the direction of a unique style, we could then provide a translator, so that all existing libraries can adopt that style. If the consensus is otherwise that it is better to provide different styles, then we shall think at ways to support different styles (e.g. synonyms when it is about naming, or mechanisms so that, say, the users can decide that all lemmas about nat uses the names n,m,p in this order, or a way to equally support, say eq_trans x y z H1 H2 or eq_trans H1 H2, as we already do for eq_refl). Regarding the difficult questions (TC/CS/modules, flat/nested, bool/Prop, ...), I don't see however how to avoid providing the different approaches.
Technically, I don't know how to proceed. Maybe the next implementor meeting in Fall could be a nice opportunity to discuss about library design decisions, in which case we could start accumulating technical material to prepare the meeting.
Even in other languages, choosing one coding style does not require showing that it's better than others, nor absolute consensus.
Maybe you're right and maybe the consensus would converge in the direction to trust a committee (like the "syntax czar" that you are mentioning), why not.
Hugo Herbelin (Jul 09 2020 at 22:56):PS: Following @Théo Zimmermann's remark, if who already participated to the discussion, namely @Paolo Giarrusso, @Cyril Cohen, @Bas Spitters, @Karl Palmskog, @Emilio Jesús Gallego Arias, @Enrico Tassi, @Anton Trunov, @Pierre-Marie Pédrot, @Vincent Semeria are interested to pursue a discussion on this topic, we could use wiki or issue pages. If @Maxime Dénès is also interested, we could maybe also use the discussion pages of the stdlib2 project.
Cyril Cohen (Jul 09 2020 at 23:52):@Hugo Herbelin even leaving aside "[someone] could have done [something you would have liked] but instead did [something you don't like]" and "I don't know about [X] but [something about X]" statements, your messages are too long and difficult for me to read and intellectualize in the context of a chatroom. I am not interested in endless debates, and I am not ready to pursue a discussion on the wiki or an issue unless we expose the problem in a factual way (e.g. no blaming/ad-hominem, authority argument, ...) and discuss very concrete strategies to attend it. Can we agree on this process?
@Théo Zimmermann does that sound to you like a good way to move forward from here?
Cyril Cohen (Jul 09 2020 at 23:54):If that's the case, as I said, my two preferred strategies are:
A. splitting/renaming "stdlib" to whatever does not contain the word "std"/"standard" in it, and explicitly pointing newcomers to the various available equivalents of a standard lib e.g. coq/mathcomp, coq/stdpp, coq/HoTT, etc since it almost feels like working in different systems.
B. performing a standardization by a committee, whoever this committee is, so that coq/stdlib has an overall coherence. The process I suggest is chronologically 1. create an initial manifesto and contributing guide. 2. work on refactoring according to these: allow only refactoring PRs and ask people to take a lock before working on a PR (and possibly update the contributing guide on the way). 3. accept any PR fitting the contributing guide (and update it if necessary).
Should we open a CEP, add these two strategies to start with, and let people can contribute?
Also, what would be the decision process and if there a committee, how should it be constituted?
Cyril Cohen (Jul 10 2020 at 00:01):(Note that my strategy B does not involve accommodating coq/mathcomp, coq/stdpp, coq/HoTT, etc, just making "std" mean "standard")
Théo Zimmermann (Jul 10 2020 at 08:12):Yes, a CEP is in order but no, it should not put the two strategies on an equal footing. A CEP is not the start of yet another endless discussion, it is a concrete proposal to discuss.
Théo Zimmermann (Jul 10 2020 at 08:12):But more importantly, this CEP should clearly state which problems it is trying to solve, because this part is still unclear to me.
Théo Zimmermann (Jul 10 2020 at 08:13):Also, do not expect to write this CEP collaboratively. A CEP should have one or very few authors / leaders.
Théo Zimmermann (Jul 10 2020 at 08:14):Personally, I'm not going to participate in writing the CEP because I have already spent important efforts on improving the situation of the stdlib and I feel like today's situation is not so bad (and has clearly improved compared to the past).
Théo Zimmermann (Jul 10 2020 at 08:15):Just as a proof of my past efforts:
Théo Zimmermann (Jul 10 2020 at 08:17):
Théo Zimmermann (Jul 10 2020 at 08:21):IMHO the recent move to maintainer teams (during the 8.12 release cycle) was a critical shift to make contributing a better experience, especially in some parts of the system that were more neglected, like the stdlib. I feel like this is not entirely by chance that 8.12 had so many more stdlib contributions than the previous releases.
Emilio Jesús Gallego Arias (Jul 10 2020 at 11:14):The discussion is indeed fairly complex, I will just add my 50cts:
stdlib2 fits well that role, in view of the work Vincent did comparing different alternatives, etc... Hugo Herbelin (Jul 10 2020 at 18:03):Cyril Cohen said:
Hugo Herbelin even leaving aside "[someone] could have done [something you would have liked] but instead did [something you don't like]" and "I don't know about [X] but [something about X]" statements, your messages are too long and difficult for me to read and intellectualize in the context of a chatroom. I am not interested in endless debates, and I am not ready to pursue a discussion on the wiki or an issue unless we expose the problem in a factual way (e.g. no blaming/ad-hominem, authority argument, ...) and discuss very concrete strategies to attend it. Can we agree on this process?
Being factual and proposing concrete strategies is what I'm trying to do (or at least what I believe trying to do). Sorry if I missed to do so. I've presented what I consider to be problems to me and I'm trying conversely to understand the problems that you and others are raising. Sorry again if I fail to do so.
If I mentioned names, it is to give a bit of historical context (which I tried to present in a factual way, so please give your own formulation of the facts if you think I'm partial) and to talk about my regrets (which is different from blaming). I wish we can find a common description of the situation on which we agree.
I tend to dislike authority arguments very much, so, I'm curious about what looks to you like authority argument in what I said.
Hugo Herbelin (Jul 10 2020 at 18:04):This being said, we need to act. Your point B looks to me more challenging and thus interesting but I'm also concerned by organizing the different existing libraries in ways which allow to use or combine them without giving the feeling that we are working in different systems, and this is not covered by your point B.
Hugo Herbelin (Jul 10 2020 at 18:05):A few things are unclear to me in what is defended. This includes:
Init, Bool, Logic, Lists, the library on nat, the library on Z, FSets, QArith, Reals, Classes, Relations, etc. as different libraries or as one single library (because the dependencies are after all relatively loose between them). Last updated: Apr 19 2024 at 11:02 UTC