Mathcomp 2.1.0 support

[sertel]

This PR contains the port of the codebase to mathcomp 2.1.0.

Pending work:

1. OVN is now commented out and still needs to be ported.
2. mathcomp-analysis deprecation warnings need to be fixed. (The SSProve code uses certain lemmas from mathcomp-analysis that in turn us admitted and as such are deprecated. I could not see a replacement. Hence, the proofs need to be redone without these lemmas.)

This PR also contains a flake.nix to

• develop SSProve via nix develop and
• load SSProve flake-style using ssprove.url = github:ssprove/ssprove and calling mkDrv to build it against the selected version of Coq and its packages

[sertel]

I'm sorry, I forgot to update the opam file. I develop via nix only. So if this opam update does not work then a little bit of help would be very much appreciated.

[cmester0]

I already have a PR (#39) for porting to Coq 18 and mathcomp 2, however I did not spend much time on it. You might benefit from comparing to it.

We should probably also update the versions in the workflow files in the .github folder

[sertel]

Ah yes, thanks.
It seems like my opam updates should work now.

[sertel]

I have a passing CI now: https://github.com/sertel/ssprove/actions/runs/8158634434
But I saw in the log that I missed to fix some of the warnings. Let me fix these first and then report back a valid CI run such that this PR can then be merged.

[sertel]

Here you go: https://github.com/sertel/ssprove/actions/runs/8169103098/job/22332488642
Is there anything else that I can/need to do before this PR can be merged?

[haselwarter]

@sertel Thank you for the effort! What is the status of the two open TODOs you mention?

[cmester0]

I might have a working version of OVN.

[sertel]

Thanks @cmester0 for taking a look at OVN.

I'm not sure about the fixes for the mathcomp-analysis warnings. I was hoping that somebody else with a bit more knowledge on that could take a look.

On that note, there is another minor TODO:
The example constructions for deriving in concrete_groups.v did not work anymore.
I can take a closer look at those ones if you think they are worth keeping.

[sertel]

I have adapted most of the examples in concrete_groups.v. I dropped the last 2 because I believe that they are not possible anymore.
Yet, there are many more warnings now about redundant definitions. I'm not yet sure how to get rid of them.

A more general comment/question:
Should concrete_groups.v really be part of SSProve?
Looks to me more like a tutorial on mathcomp and deriving. It does not use any of the SSProve files.

[haselwarter]

Fair enough. I'm not particularly attached to concrete_groups.v ; it can be laid to rest in the project's git history.

The situation for OVN might be a bit different ; @spitters , is there anyone working on (something related to) this?

[spitters]

@cmester0 and @4ever2 are working on OVN. I believe it works again.

[sertel]

I asked the mathcomp-analysis community on how to handle the admitted lemma here.
There seems to be a (migration?) plan with respect to the whole distr.v file. But I did not yet receive an answer that allows me to derive any further steps on this.

[sertel]

According to the authors of mathcomp-analysis, distr.v may go away eventually. So it makes no sense to invest time in fixing these warnings now.

[cmester0]

Some minor comments, otherwise I think this should just be merged.

[TheoWinterhalter]

I don't see anything suspicious going on, thanks. :)

[sertel]

Hi @haselwarter,
Do you have any further comments on the PR?
I have another PR forthcoming which would be based on this one ;)

[spitters]

@haselwarter about the todos:

1. Will fix OVN in a later PR.
2. as @sertel says the warnings about distr will be fixed by the MC team at a later point.

So, I'll merge this now.

[spitters]

@sertel what's the status of putting SSProve in MC CI?
One reason I'm asking is that there's a new release of MC analysis, so it would be good if we'd automatically check that that one also compiles.
https://github.com/math-comp/analysis/blob/master/CHANGELOG.md

[sertel]

Could you please start versioning SSProve as we discussed on Zulip?

[spitters]

Yes, could you send a PR for the 0.2.0 release?
@TheoWinterhalter has done the other releases, so he should be able to provide some guidance if needed.
https://github.com/SSProve/ssprove/releases

[sertel]

I'm sorry but I did not get that. What would that PR do?
Someone with the appropriate permissions needs to tag the commit before and after this PR with 0.1.0 and 0.2.0 respectively (via the Github UI).

[spitters]

Of course...
@TheoWinterhalter could you do that? I'd need to search for the precise buttons to push...

[sertel]

https://docs.github.com/en/repositories/releasing-projects-on-github/managing-releases-in-a-repository

[TheoWinterhalter]

Done.

[sertel]

Great, thanks a lot @TheoWinterhalter.
I will take care of putting SSProve on the Nix-Mathcomp-CI by the end of the week.

[sertel]

I'm on it but need to resolve some Nix problems first.