Karl Palmskog (Dec 07 2021 at 13:56): Karl Palmskog (Dec 07 2021 at 13:56):(related to this) something I'd like to know is: who are the actual maintainers of bignums? Should one use a particular "team ping" in issues on GitHub?
Karl Palmskog (Dec 07 2021 at 13:59):if the project needs more collective effort/ownership, maybe you guys would consider moving it to coq-community, where more people can potentially respond to PRs and issues...
Théo Zimmermann (Dec 07 2021 at 15:03):So...
Théo Zimmermann (Dec 07 2021 at 15:03):Moving bignums out of Coq was a huge mistake.
Théo Zimmermann (Dec 07 2021 at 15:03):Done for stupid reasons (speed up the build).
Théo Zimmermann (Dec 07 2021 at 15:04):Since then, bignums maintenance has taken a serious hit.
Théo Zimmermann (Dec 07 2021 at 15:04):Everything outside the main Coq repo is managed less well. For the www repo and some others we have maintainer teams, but nothing yet for bignums.
Théo Zimmermann (Dec 07 2021 at 15:05):I've proposed moving bignums to coq-community but there was a bit of backlash.
Théo Zimmermann (Dec 07 2021 at 15:07):And more importantly, a reason to procrastinate was that there were some discussions of moving bignums back to the Coq repo.
Emilio Jesús Gallego Arias (Dec 07 2021 at 15:24):@Théo Zimmermann you raise a good point, what would you like to happen here?
I was under the impression that bignums had a few devs interested on it and active, so do you folks think it is more of a manpower problem, or just that the way the infrastructure is setup is not making the maintainers aware of problems?
Théo Zimmermann (Dec 07 2021 at 15:25):I don't think it's a manpower problem. There are a few interested devs like you said, which is sufficient.
Théo Zimmermann (Dec 07 2021 at 15:25):It's more of a process and infrastructure problem.
Emilio Jesús Gallego Arias (Dec 07 2021 at 15:28):How could we make progress on this front then? I have the feeling we have been a bit too distributed working on this, a true Baazar model (cc: @Maxime Dénès which is interested on this and maybe active again)
The CI was developed fully async, the bot was way more structured but for example not in coordiantion with build system / overlays work. Coq community did a great job and provided a lot of feedback but we failed to implement it on the build side likely due to lack of manpower:
Emilio Jesús Gallego Arias (Dec 07 2021 at 15:28):So I dunno, seems to me we should structure the work on infrastructure a bit better?
Emilio Jesús Gallego Arias (Dec 07 2021 at 15:28):Not easy tho, due to our own constraints a researchers
Théo Zimmermann (Dec 07 2021 at 15:36):My point was that coq-community works pretty well already, and moving bignums to coq-community would solve the maintenance issues that we are facing for bignums (because coq-community already has the processes and tools that are lacking for bignums today).
Emilio Jesús Gallego Arias (Dec 07 2021 at 15:55):Théo Zimmermann said:
My point was that coq-community works pretty well already, and moving bignums to coq-community would solve the maintenance issues that we are facing for bignums (because coq-community already has the processes and tools that are lacking for bignums today).
Oh I see, thanks! Let's move the thing to coq community right now then!
Emilio Jesús Gallego Arias (Dec 07 2021 at 15:56):You guys are the experts here, but from a bit of thinking I am feeling than even the stdlib could be better maintained in coq community
Emilio Jesús Gallego Arias (Dec 07 2021 at 15:56):_à la mathlib_ ?
Karl Palmskog (Dec 07 2021 at 15:56):@Emilio Jesús Gallego Arias if you want to get the process started we are unfortunately a bit formalistic: https://github.com/coq-community/manifesto/issues/new?labels=move-project&template=1-move-a-project.md&title=Proposal+to+move+project+X+to+coq-community
Karl Palmskog (Dec 07 2021 at 15:57):and we also want the current authors/maintainers to approve explicitly of the move (preferably old ones as well)
Karl Palmskog (Dec 07 2021 at 15:58):the Stdlib discussion I feel is above my paygrade, but please bring it up in the core team at some point.
Emilio Jesús Gallego Arias (Dec 07 2021 at 15:58):Thanks @Karl Palmskog , I am not the right person to lead that IMHO; w.r.t. my comment above I'd be more interested on how to make better progress on many of the tooling I've been working on, I have all this feedback, but so far I find myself a bit alone and lacking dev time.
Maybe coq dune etc... should be put into coq-community?
Emilio Jesús Gallego Arias (Dec 07 2021 at 15:59):serapi / pycoq should certainly move at some point I guess
Emilio Jesús Gallego Arias (Dec 07 2021 at 15:59):or even to the main coq repos? I dunno
Karl Palmskog (Dec 07 2021 at 15:59):the person initiating the coq -community process doesn't have to be the driver/leader. You can just make a proposal and hopefully it will work out.
Emilio Jesús Gallego Arias (Dec 07 2021 at 15:59):I didn't thought at first the location of the repos would be so important, but I am likely wrong
Karl Palmskog (Dec 07 2021 at 16:00):well, in coq-community the location has meaning in that there are lots of people who can merge PRs
Karl Palmskog (Dec 07 2021 at 16:01):this is both a strength and also arguably a weakness sometimes
Karl Palmskog (Dec 07 2021 at 16:01):we want to improve governance processes over time but right now things seem to get done eventually...
Karl Palmskog (Dec 07 2021 at 16:02):I'm not sure that very actively developed projects with strong leadership are good to put in coq-community. Usually strong leadership correlates with requirements for more control and so on, and we don't have a ton of that technically.
Karl Palmskog (Dec 07 2021 at 16:10):for example, my opinion of SerAPI for the moment would be something like: upstream Serlib to Coq, continue to maintain sertop + the API part of SerAPI in the current repo, spin off the Serlib-only tools to coq-community
Karl Palmskog (Dec 07 2021 at 16:13):something like PyCoq in my opinion needs strong leadership until it's more mature, so no obvious benefit from moving it to coq-community.
Karl Palmskog (Dec 08 2021 at 18:00):if anyone is following this, I opened the proposal for transferring bignums to coq-community: https://github.com/coq-community/manifesto/issues/136
Last updated: Oct 13 2024 at 01:02 UTC