Stream: Coq devs & plugin devs

Topic: Post-Coq Call Stdlib CEP discussion


view this post on Zulip Notification Bot (Mar 12 2024 at 15:44):

28 messages were moved here from #Coq devs & plugin devs > coq call by Théo Zimmermann.

view this post on Zulip Théo Zimmermann (Mar 12 2024 at 15:48):

The comparison with mathlib is interesting given that mathlib was precisely split out of the main Lean repository (where it initially started) and it became thriving because of that split. I think that this is (together with Zulip) even one of the main reasons of the success of mathlib: a large monorepo where everyone feel they can contribute without being a programmer. IMHO the dual repo approach (cf. the updated CEP) is the best way to achieve something similar.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 12 2024 at 16:41):

Thanks for organizing the topic @Théo Zimmermann

Actually I was going to say that indeed putting stdlib in its own repos is not a big problem, but also I am not optimistic it will make things better. If we want that to happen tho, we need first to port the test-suite to Dune, etc... and discuss some key use cases that we support badly now, and will become a pain point if the split happens, in particular, developers need a way for given a .v file, open a development Coq with that file as fast as possible. (Coq Universe was designed for that)

Another thought that came to my mind is that while the coupling as of today is low, I am not sure this is a desirable property. I am convinced that the future of ITPs for the masses will require co-development of tactics and proofs, and the split makes this harder, and reinforces the (IMO bad) habit of workarounding problems of tactics / implementation in the proofs. math-comp was developed that way, and actually, as of today, the coupling of Lean and mathlib, despite having been in separate repos, has greatly increased as they have discovered that fixing Lean bugs that were affecting mathlib as led to this co-development de-facto.

view this post on Zulip Pierre Roux (Mar 12 2024 at 16:54):

Emilio Jesús Gallego Arias said:

developers need a way for given a .v file, open a development Coq with that file as fast as possible.

Is make given_file.vo then open your editor really that bad?

view this post on Zulip Pierre Roux (Mar 12 2024 at 16:59):

Emilio Jesús Gallego Arias said:

Pierre Roux said:

FWIW, for mathcomp, we have quite many libraries using it now and, in part thanks to CI, things are not that bad, far from it.

I wonder how the current effort you folks are doing would have been if you had a fully monolithic repos including Coq

Probably pretty nightmarish, if even possible with current tooling. This means that repo would have included coq-elpi which is developped on Coq latest for good reasons. How would you handle the two branches master and mathcomp-1? As for handling dependencies, I'd tend to consider that nix-shell is good enough at making this reasonnably transparent.

view this post on Zulip Pierre Roux (Mar 12 2024 at 17:03):

Emilio Jesús Gallego Arias said:

the (IMO bad) habit of workarounding problems of tactics / implementation in the proofs. math-comp was developed that way

You have a point. Although my understanding (I might be completely wrong, I'm too young to know the details) is that this pertains more to human/social reasons than technical ones.

view this post on Zulip Théo Zimmermann (Mar 12 2024 at 17:03):

Another thought that came to my mind is that while the coupling as of today is low, I am not sure this is a desirable property. I am convinced that the future of ITPs for the masses will require co-development of tactics and proofs

Sure, but again, the Lean experience there is showing that the solution to that is to use a meta language that is comprehensible by the proof assistant users (in Lean, it is Lean itself, while in Coq, it could be Coq through template Coq, Ltac2 or Elpi).

view this post on Zulip Théo Zimmermann (Mar 12 2024 at 17:16):

Pierre Roux said:

Emilio Jesús Gallego Arias said:

developers need a way for given a .v file, open a development Coq with that file as fast as possible.

Is make given_file.vo then open your editor really that bad?

The point Emilio makes here is that this command would not track inter-project dependencies at a fine granularity (or at all), whereas Dune / Coq Universe do achieve this, which is better.

view this post on Zulip Pierre Roux (Mar 13 2024 at 10:03):

Thanks for the explanation. TBH currently I feel like I don't really need that. But maybe it's that kind of tool that you don't miss when you don't know them and you could no longer live without once you discover them. Hard to say in advance.

view this post on Zulip Pierre Roux (Mar 13 2024 at 10:04):

Théo Zimmermann said:

the Lean experience there is showing that the solution to that is to use a meta language that is comprehensible by the proof assistant users (in Lean, it is Lean itself, while in Coq, it could be Coq through template Coq, Ltac2 or Elpi).

And enabling the use of such metalanguages in the stdlib is one of the key motivations of the CEP.

view this post on Zulip Hugo Herbelin (Mar 13 2024 at 19:15):

A few comments on the CEP:

view this post on Zulip Hugo Herbelin (Mar 13 2024 at 19:15):

I also agree with Emilio that library development and Coq features nourish themselves. We have the chance to be a group that includes both developers of the system and developers of libraries. We have to keep it alive. Hearing people advocating bypassing limitations of Coq rather than seizing an opportunity of improving Coq makes me sad.

view this post on Zulip Théo Zimmermann (Mar 18 2024 at 13:03):

The stdlib is used and we have a responsability about it. The responsability of keeping alive the developments that depend on it.

The responsability of making a "standard" library as good as what anyone else would like to expect from a standard library.

I agree with these two statements, but I think they need to be addressed separately. To address the first statement might require to preserve some existing and non-optimal libraries, that we want to discourage new users and new projects to use, while addressing the second statement might require creating something new or repurposing something that is not currently in the stdlib as the new standard...

In a sense, this is summarized by this third sentence with which I agree fully:

Technical debts should not prevent us to go ahead.

view this post on Zulip Théo Zimmermann (Mar 18 2024 at 13:05):

On the other hand, I think you should think differently what "bypassing limitations of Coq rather than fixing them" means. This is how both MathComp and MathLib (with respect to Lean) managed to be a success. If library authors stopped developing libraries every time they encounter a limitation that could be fixed, we would never had got libraries of this scale.

view this post on Zulip Andres Erbsen (Mar 18 2024 at 16:13):

Thank you all for the thoughtful comments. One thing that seems to shine through but has not been stated explicitly is that even if responsible curation and co-development are desirable, "keeping" the stdlib would mean that we need to agree on what we want it to be like, whereas "does not enjoy special status" would be a step towards different subgroups developing competing approaches. To decide which one would better serve the community, it seems important to have a sense for how much agreement there actually is: for example, on whether sophisticated elaboration a la elpi is desired.

view this post on Zulip Andres Erbsen (Mar 18 2024 at 16:23):

Another observation on the same point: I think a part of the argument for coq+stdlib to become a dual-repo pair like lean+mathlib essentially relies on the stdlib not having other dependencies, lest we get into cross-repo-change-coordination issues we know are exceedingly painful with current tooling. On the other hand, I am not sure whether people pushing for the split would still want it with that constraint.

view this post on Zulip Julien Puydt (Mar 20 2024 at 08:38):

A Coq limitation should indeed not prevent external libraries from moving on, or they wouldn't be able to make any progress.
But if they have a workaround or improvement to propose, that should go into Coq itself pretty fast.


Last updated: Oct 13 2024 at 01:02 UTC