Stream: Coq devs & plugin devs

Topic: Bignums maintenance


view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Théo Zimmermann (Dec 07 2021 at 15:03):

So...

view this post on Zulip Théo Zimmermann (Dec 07 2021 at 15:03):

Moving bignums out of Coq was a huge mistake.

view this post on Zulip Théo Zimmermann (Dec 07 2021 at 15:03):

Done for stupid reasons (speed up the build).

view this post on Zulip Théo Zimmermann (Dec 07 2021 at 15:04):

Since then, bignums maintenance has taken a serious hit.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Dec 07 2021 at 15:05):

I've proposed moving bignums to coq-community but there was a bit of backlash.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Dec 07 2021 at 15:25):

It's more of a process and infrastructure problem.

view this post on Zulip 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:

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2021 at 15:28):

Not easy tho, due to our own constraints a researchers

view this post on Zulip 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).

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2021 at 15:56):

_à la mathlib_ ?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2021 at 15:59):

serapi / pycoq should certainly move at some point I guess

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2021 at 15:59):

or even to the main coq repos? I dunno

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Dec 07 2021 at 16:01):

this is both a strength and also arguably a weakness sometimes

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: Feb 06 2023 at 00:03 UTC