gmp is something that comes in via opam, we don't even use it directly -- it's somewhere in Rocq's dependency tree. If the usual opam package doesn...

I've fixed coq-lint.sh in the repo.

Well, it also instructs the user that the gmp should be installed as a shell rather than globally, though I do see your point. I'll close the MR.

With the changed shell file, NixOS.md seems to just say "use opam", which we recommend anyway. So I don't quite see the point.

It works

I'll test it out, but isn't the bigger issue the shell.nix? What I'm thinking is to just remove the shell.nix, replace /bin/bash with /bin/sh, and ...

Apparently /bin/sh exists on NixOS. I think we can change it to that.

You can have a branch in your fork, you don't need my permission for that.

@jung I understand. Rather than it being merged into main, can it be it's own branch?

Thanks for the MR! However, I don't think we want to have some odd shell.nix file here that nobody in the team understands -- this repo is portable...

@jung Thanks

Forking repos requires manual approval of the account. We're being flooded by spambots so sadly this has become necessary....

Probably just nix shenanigans