coq fails

[quinn-dougherty]

Hi! I was having some issues with coq in an opam2nix project, namely nix-shell default.nix --pure --run "coqc --version" after following instructions would fail. I was drawing up a minimal replicator to file an issue to learn more about how I'm supposed to be using the tool, when I couldn't even get that far and the larger project that previously at least had a successfully built shell stopped working too somehow.

$ cat opam2nix.nix 
import (builtins.fetchTarball "https://github.com/timbertson/opam2nix/archive/v1.tar.gz")

$ cat mytest.opam
opam-version: "2.0"

depends: [
         "coq" { >= "8.13.0" & < "8.14" }
]

build: [ "dune" "build" "-p" name "-j" jobs ]

$ cat default.nix
{ pkgs ? import (builtins.fetchTarball {
    url = "https://github.com/NixOS/nixpkgs/archive/refs/tags/21.05.tar.gz";
  }) {} }:
let
  opam2nix = import ./opam2nix.nix {};
  ocaml = pkgs.ocaml;
  selection = opam2nix.build {
    inherit ocaml;
    selection = ./opam-selection.nix;
    src = ./.;
  };
in selection.mytest

$ "$(nix-build --no-out-link ./opam2nix.nix)"/bin/opam2nix resolve --ocaml-version 4.12.0 ./mytest.opam 

$ nix-shell default.nix
...
<OCAMLC trying to compile coq>
...
OCAMLC    checker/votour.mli
OCAMLC -a bin/doc_grammar
"/nix/store/zxwc73n4pjcvl8bv4pw695wn6z12a5w3-ocamlfind-1.9.1/bin/ocamlfind" ocamlc -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67   -safe-string -strict-sequence  ide/coqide/default_bindings_src.ml -o ide/coqide/default_bindings_src.exe
CHECK revision
sh: ./dev/tools/make_git_revision.sh: /usr/bin/env: bad interpreter: No such file or directory
make[1]: *** [Makefile.dev:34: revision] Error 126
make[1]: *** Waiting for unfinished jobs....
make[1]: Leaving directory '/build/coq-8.13.2'
make: *** [Makefile.make:178: submake] Error 2
Command failed.
error: builder for '/nix/store/48bpq8irly0wwm0ja5rz3xmhqwjqsq8a-coq-8.13.2.drv' failed with exit code 2                                            

Any ideas?

[Zimmi48]

I have no idea what opam2nix does, but from the error message, it looks like there was no step to patch shebangs in scripts that are run during the build. See the corresponding code from the nixpkgs derivation: https://github.com/NixOS/nixpkgs/blob/e74894146a42ba552ebafa19ab2d1df7ccbc1738/pkgs/applications/science/logic/coq/default.nix#L153-L159