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.

Let's try!

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.

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.