search

coq-community / coq-nix-toolbox

Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]
MIT License
32 stars 9 forks source link

Adding SSProve to the CI #213

Closed sertel closed 4 months ago

sertel commented 4 months ago

This PR adds SSProve to the CI.

sertel commented 4 months ago

Also for helping with this PR, thanks a lot @vbgl !

proux01 commented 4 months ago

@sertel sorry for the late review, if you want ssprove added in mathcomp CI, feel free to open a PR there to update coq-nix-toolbox

sertel commented 4 months ago

Hi @proux01 , this PR was already merged, so it is already part of the Coq Nix-based CI in the Coq-nix-toolbox.

proux01 commented 4 months ago

@sertel sure but ssprove won't be tested in mathcomp CI until coq-nix-toolbox is updated there

sertel commented 4 months ago

I see. Can you please me again what the mathcomp CI ensures and the Coq CI doesn't? Upon a new mathcomp release, does it check for compatibility automatically?

proux01 commented 4 months ago

Can you please me again what the mathcomp CI ensures and the Coq CI doesn't?

Well, the CI of mathcomp is testing that changes to mathcomp don't break its reverse dependencies. The CI of Coq is for changes in Coq.

Upon a new mathcomp release, does it check for compatibility automatically?

Nothing automatic, but the goal of a CI is that things shouldn't get merged until it's green.

sertel commented 4 months ago

Well, yes. Looking at the nix-script in mathcomp I can see that the CI for mathcomp checks whether it would break the packages that are listed there.

My question is: When mathcomp changes are breaking SSProve, then, by definition of a CI, as you correctly pointed out, these changes can not be pushed. Who is in this case responsible for fixing SSProve? Or is mathcomp always trying to provide backward compatibility?

proux01 commented 4 months ago

When mathcomp changes are breaking SSProve, [...] Who is in this case responsible for fixing SSProve?

SSProve maintainers, but legitimate breaking changes are pretty rare

Or is mathcomp always trying to provide backward compatibility?

We don't have any strict policy but we try our best to avoid breaking changes as much as possible. And most of the time we provide deprecation notations that we keep for a few versions (usually three) to let users some time to adapt.

sertel commented 4 months ago

Fair enough. Thanks for your responses! I will add SSProve to the mathcomp CI then as well soon.