coq: making sure coq master and 9.0 compile

[CohenCyril]

Things done

• Built on platform(s)
  • x86_64-linux
  • aarch64-linux
  • x86_64-darwin
  • aarch64-darwin
• For non-Linux: Is sandboxing enabled in nix.conf? (See Nix manual)
  • sandbox = relaxed
  • sandbox = true
• Tested, as applicable:
  • NixOS test(s) (look inside nixos/tests)
  • and/or package tests
  • or, for functions and "core" functionality, tests in lib/tests or pkgs/test
  • made sure NixOS tests are linked to the relevant packages
• Tested compilation of all packages that depend on this change using nix-shell -p nixpkgs-review --run "nixpkgs-review rev HEAD". Note: all changes have to be committed, also see nixpkgs-review usage
• Tested basic functionality of all binary files (usually in ./result/bin/)
• 25.05 Release Notes (or backporting 24.11 and 25.05 Release notes)
  • (Package updates) Added a release notes entry if the change is major or breaking
  • (Module updates) Added a release notes entry if the change is significant
  • (Module addition) Added a release notes entry if adding a new NixOS module
• Fits CONTRIBUTING.md.

---

Add a 👍 reaction to pull requests you find important.

[CohenCyril]

For now this errors with the following message when running ./result/bin/coqtop 😕

Welcome to Coq 9.0+alpha
Error:
Findlib error: zarith not found in:
/nix/store/c2hwnp5ryalzz1rwldp7a87lzxaq1329-coq-dev/lib/coq/../coq-core/..
/nix/store/c2hwnp5ryalzz1rwldp7a87lzxaq1329-coq-dev/lib/coq/user-contrib/Ltac2
/nix/store/c2hwnp5ryalzz1rwldp7a87lzxaq1329-coq-dev/lib/coq/user-contrib/Ltac2/Compat
/nix/store/bj6kj93sbg5j0vgv5yrxfcq91fj9pqfi-ocaml4.14.2-findlib-1.9.8/lib/ocaml/4.14.2/site-lib
required by `coq-core.interp'

[vbgl]

Thanks Cyril for working on this! Regarding the coqtop failure, did you try wrapping the binary (like, e.g., rtop):

nixpkgs/pkgs/development/compilers/reason/rtop.nix

Lines 23 to 28 in b343873

	postInstall = ''
	wrapProgram $out/bin/rtop \
	--prefix PATH : "${utop}/bin" \
	--prefix CAML_LD_LIBRARY_PATH : "$CAML_LD_LIBRARY_PATH" \
	--prefix OCAMLPATH : "$OCAMLPATH:$OCAMLFIND_DESTDIR"
	'';

[vbgl]

This was wrong advice. Sorry about that.

I guess this PR can be closed, thanks to the nice work by Pierre.

[CohenCyril]

Subsumed by #364617