Test against Rocq 9.1.0 in CI.

[rlepigre]

I have no idea what I am doing (not a nix user), so help would be appreciated.

[Alizter]

Looks like rocq isn't a valid package name in nixpkgs. Likely they haven't committed to switching to the new name just yet. I think coq would work here instead IIUC.

[rlepigre]

Let's try!

[Alizter]

Looks like the nix part is working. However as you can see, the test suite will need to be updated which will probably entail a lot of work.

I don't mind bumping the coq/rocq version to 9.1 and stopping the testing of 8.16. There is little point of us testing an older version anyway if most potential users are using something else.

This PR will likely have to be drafted until the fixes are done.

[rlepigre]

Yeah, it indeed looks non-trivial... On the other hand, it'd be nice if we could have have the test suite work for both versions for a while, to notice regressions when we move to using the rocq command instead of coq on newer versions for example.

I'll experiment a bit more to see what it would take. If that's too hard, I guess we can just bump to using Rocq 9.

[ejgallego]

Hi folks, I did look into this back when we were writing #12035 , and indeed it'd be a bit complex.

IMHO I prefer to go ahead with #12035 , which will CI against 9.1 , and keep the legacy (lang coq) testing as it is.

But if you would like to improve CI for (lang coq) so it can test against newer coq packages please feel welcome to do so.