Old versions of Coq alongside some Coq packages fail to build

[Coda-Coda]

Describe the bug

Old versions of Coq alongside some Coq packages listed in an opam file fail to install, the fix introduced in 5bfdc95 only works for newer versions of Coq. The fix doesn't work for older versions of Coq, see #48 and the resulting 34d74ca which disables it for Coq < 8.17.

To Reproduce

An opam file including, for example:

"coq" {>= "8.10" & < "8.12.0" }
"coq-ott" {>= "0.29"}

fails to build when following the standard instructions in the README of opam-nix with the error:

error: builder for '/nix/store/s5f9ss5b3i47fj85ik1k3ppv5nvv6fx4-coq-ott-dev.drv' failed with exit code 2;
       last 10 log lines:
       > install: cannot change permissions of '/nix/store/d75jswiprkwrmwm21xzv04rkjdxpwwmf-coq-8.11.2/lib/ocaml/4.11.2/site-lib/coq//user-contrib/Ott/': No such file or directory
       > install: cannot change permissions of '/nix/store/d75jswiprkwrmwm21xzv04rkjdxpwwmf-coq-8.11.2/lib/ocaml/4.11.2/site-lib/coq//user-contrib/Ott/': No such file or directory
       > install: cannot change permissions of '/nix/store/d75jswiprkwrmwm21xzv04rkjdxpwwmf-coq-8.11.2/lib/ocaml/4.11.2/site-lib/coq//user-contrib/Ott/': No such file or directory
       > install: cannot change permissions of '/nix/store/d75jswiprkwrmwm21xzv04rkjdxpwwmf-coq-8.11.2/lib/ocaml/4.11.2/site-lib/coq//user-contrib/Ott/': No such file or directory
       > install: cannot change permissions of '/nix/store/d75jswiprkwrmwm21xzv04rkjdxpwwmf-coq-8.11.2/lib/ocaml/4.11.2/site-lib/coq//user-contrib/Ott/': No such file or directory
       > install: cannot change permissions of '/nix/store/d75jswiprkwrmwm21xzv04rkjdxpwwmf-coq-8.11.2/lib/ocaml/4.11.2/site-lib/coq//user-contrib/Ott/': No such file or directory
       > make[1]: *** [Makefile.coq:490: install] Error 1
       > make[1]: Leaving directory '/build/source/coq'
       > make: *** [Makefile:5: install] Error 2
       > make: Leaving directory '/build/source/coq'
       For full logs, run 'nix log /nix/store/s5f9ss5b3i47fj85ik1k3ppv5nvv6fx4-coq-ott-dev.drv'.
error: 1 dependencies of derivation '/nix/store/ny29rycz6mqgskfmn8iv4sc57spmpv7x-coq-mi-cho-coq-dev-env.drv' failed to build

(Using nix develop --impure to trigger a build of Coq).

Expected behavior

Such an opam file would succeed at building Coq with coq-ott, following the instructions of the README.

Environment

OS name + version: NixOS
Version of the code: https://github.com/tweag/opam-nix/tree/34d74ca9d64339c453cbac3f85255644361937e2

Additional context

Removing the version constraints resulting in the following opam file, builds successfully. Giving: Coq v8.17.1

  "coq"
  "coq-ott"

I am trying to build the Coq specification of Michelson, Mi-Cho-Coq, with this .opam file.
This fails with:

error: builder for '/nix/store/cggr7bq1jzransryclk1k4k6mng60bhs-coq-error-handlers-1.2.0.drv' failed with exit code 2;
       last 10 log lines:
       > patching script interpreter paths in .
       > ./configure.sh: interpreter directive changed from "#!/usr/bin/env sh" to "/nix/store/zlf0f88vj30sc7567b80l52d19pbdmy2-bash-5.2-p15/bin/sh"
       > building
       > COQDEP VFILES
       > COQC src/All.v
       > installing
       > install: cannot change permissions of '/nix/store/d75jswiprkwrmwm21xzv04rkjdxpwwmf-coq-8.11.2/lib/ocaml/4.11.2/site-lib/coq//user-contrib/ErrorHandlers/': No such file or directory
       > install: cannot change permissions of '/nix/store/d75jswiprkwrmwm21xzv04rkjdxpwwmf-coq-8.11.2/lib/ocaml/4.11.2/site-lib/coq//user-contrib/ErrorHandlers/': No such file or directory
       > install: cannot change permissions of '/nix/store/d75jswiprkwrmwm21xzv04rkjdxpwwmf-coq-8.11.2/lib/ocaml/4.11.2/site-lib/coq//user-contrib/ErrorHandlers/': No such file or directory
       > make: *** [Makefile:490: install] Error 1
       For full logs, run 'nix log /nix/store/cggr7bq1jzransryclk1k4k6mng60bhs-coq-error-handlers-1.2.0.drv'.
error: 1 dependencies of derivation '/nix/store/7jx8n5nvn5pphwkd9xi9q9c7dwgwdmiw-coq-list-string-2.1.2.drv' failed to build
error (ignored): error: cannot unlink '/tmp/nix-build-coq-menhirlib-dev.drv-21/source/test/static/good': Directory not empty
error: 1 dependencies of derivation '/nix/store/s6f2rpr2df4lanmayilpin3npq7cfvdw-coq-mi-cho-coq-dev-env.drv' failed to build

I also tried the .opam file of the dev branch of Mi-Cho-Coq, which fails with a different error:

error: builder for '/nix/store/ldzavngayh84hm4a3z2bmib1vxd5f15r-coq-error-handlers-1.2.0.drv' failed with exit code 1;
       last 10 log lines:
       > unpacking sources
       > unpacking source archive /nix/store/qvd45x7m9a2hvnhm0fm8r7nyh4q8yl0y-1.2.0.tar.gz
       > source root is coq-error-handlers-1.2.0
       > setting SOURCE_DATE_EPOCH to timestamp 1437603510 of file coq-error-handlers-1.2.0/src/All.v
       > patching sources
       > configuring
       > patching script interpreter paths in .
       > ./configure.sh: interpreter directive changed from "#!/usr/bin/env sh" to "/nix/store/zlf0f88vj30sc7567b80l52d19pbdmy2-bash-5.2-p15/bin/sh"
       > building
       > Error: cannot find /nix/store/jcyy5nd5q4l576mm6m1z3i2kca6454za-coq-8.16.1/lib/ocaml/4.14.1/site-lib/coq/../coq-core/tools/CoqMakefile.in
       For full logs, run 'nix log /nix/store/ldzavngayh84hm4a3z2bmib1vxd5f15r-coq-error-handlers-1.2.0.drv'.
error: 1 dependencies of derivation '/nix/store/i1xx683iarcvdk14yskhaq7la1cxrs1j-coq-list-string-2.1.2.drv' failed to build
error: 1 dependencies of derivation '/nix/store/xbwp8ihlzwpgllcdib5dvdi7rp7r06k9-coq-mi-cho-coq-dev-env.drv' failed to build

The dev branch's .opam file builds successfully via opam.

[balsoft]

Hi! Should be fixed now. If you encounter more problems, please feel free to open corresponding issues.

[Coda-Coda]

Hi @balsoft, thank you very much for your efforts. I am still encountering an issue related to building Coq packages alongside Coq, though the error message is different to prior to 9c7e1be. I see you added a Coq Example which I've tried to use but may be using improperly.

My goal is to have a shell with the same dependencies loaded as if I'd used eval $(opam env --switch=mi-cho-coq) where the switch mi-cho-coq had been created as below (running from a clone of mi-cho-coq's dev branch):

opam switch create mi-cho-coq 4.13.1
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam install .

Currently, I'm using the following flake.nix file:

{
  inputs = {
    opam-nix.url = "github:tweag/opam-nix";
    flake-utils.url = "github:numtide/flake-utils";
    nixpkgs.follows = "opam-nix/nixpkgs";
    opam-repository = {
      url = "github:ocaml/opam-repository";
      flake = false;
    };
    opam-coq-archive = {
      url = "github:coq/opam-coq-archive";
      flake = false;
    };
  };
  outputs = { self, flake-utils, opam-nix, opam-repository, opam-coq-archive, nixpkgs }@inputs:
    # Don't forget to put the package name instead of `throw':
    let package = "coq-mi-cho-coq";
    in flake-utils.lib.eachDefaultSystem (system:
      let
        pkgs = nixpkgs.legacyPackages.${system};
        on = opam-nix.lib.${system};
        scope =
          on.buildOpamProject { repos = [ opam-repository
                        ("${opam-coq-archive}" + "/released")
                        ("${opam-coq-archive}" + "/extra-dev")
                      ];
            } package ./. { ocaml-base-compiler = "*"; };
        overlay = final: prev:
          {
            # Your overrides go here
          };
      in {
        legacyPackages = scope.overrideScope' overlay;

        packages.default = self.legacyPackages.${system}.${package};
      });
}

I think perhaps the above flake.nix is trying to make use of the .opam file from the coq-mi-cho-coq package in the coq-released or coq-extra-dev which is an issue. But the bigger issue is that regardless, it still fails to build.

The following error appears:

$ nix develop --impure
warning: Git tree '/home/daniel/Documents/Code/research/mi-cho-coq-nix' is dirty
error: builder for '/nix/store/6vmrc4cjjap71kknajmawyj8sfnikjgd-coq-list-string-2.1.2.drv' failed with exit code 2;
       last 10 log lines:
       > COQC src/Comparison.v
       > COQC src/Conversion.v
       > COQC src/Trim.v
       > File "./src/Conversion.v", line 6, characters 15-32:
       > Error: Cannot find a physical path bound to logical path matching suffix
       > ErrorHandlers.
       >
       > make[1]: *** [Makefile:677: src/Conversion.vo] Error 1
       > make[1]: *** Waiting for unfinished jobs....
       > make: *** [Makefile:327: all] Error 2
       For full logs, run 'nix log /nix/store/6vmrc4cjjap71kknajmawyj8sfnikjgd-coq-list-string-2.1.2.drv'.
error: 1 dependencies of derivation '/nix/store/djyz98q8l5h9nknjp0j0dk8psaiv5i70-coq-mi-cho-coq-dev-env.drv' failed to build

Thanks for your help once again. I feel this is still the current issue, but I cannot re-open it. If you'd prefer me to make it a new issue, that's fine too. Apologies for the delay in getting back to you.

[balsoft]

I can reproduce. In this particular case, relaxing the coq version requirement:

diff --git a/coq-mi-cho-coq.opam b/coq-mi-cho-coq.opam
index a202b28..34a2de6 100644
--- a/coq-mi-cho-coq.opam
+++ b/coq-mi-cho-coq.opam
@@ -22,7 +22,7 @@ depends: [
   "coq-list-string"
   "coq-menhirlib" {>= "20190626"}
   "coq-moment" {>= "1.2.0"}
-  "coq" {>= "8.14" & < "8.17.0" }
+  "coq" {>= "8.14" }
   "menhir"
   "ocaml" {>= "4.07.1"}
   "ocamlbuild"

Results in a successful build with the same flake as you have provided.

I'll try to figure out how to make it build with an older version.

[Coda-Coda]

Thanks @balsoft, I can also confirm that relaxing the coq version requirement allows it to be built. For me, this yields coqc --version = 8.17.1.

[balsoft]

Unfortunately, getting old versions of Coq to work seems to require more work than I'm able to put in at the moment; it's quite difficult to configure installation locations for Makefile.coq et al, while still allowing Coq to find its stdlib. If someone else is willing to step up (perhaps taking a look at nixpkgs would be of use), feel free.

[Coda-Coda]

Thanks for your efforts @balsoft!