Cannot build Coq projects that depend on the Coq package index

[dunnl]

Describe the bug I am not able to build the Coq package Verdi (or other Coq projects that depend on the Coq package index) using buildOpamProject, even though Verdi is an opam project.

To Reproduce

1. Clone my fork of Verdi that adds a flake.nix and checkout the branch opam-nix-issue

2. Run nix build --show-trace

3. Be met with the following trace

   error:
      … while evaluating the attribute 'buildInputs' of the derivation 'coq-verdi-dev'
   
      at /nix/store/q3l9x3ncgi0hppw0i65ki9jrxj8kmgac-source/pkgs/stdenv/generic/make-derivation.nix:302:7:
   
         301|     // (lib.optionalAttrs (attrs ? name || (attrs ? pname && attrs ? version)) {
         302|       name =
            |       ^
         303|         let
   
      … while evaluating the attribute 'src' of the derivation 'coq-inf-seq-ext-dev'
   
      at /nix/store/q3l9x3ncgi0hppw0i65ki9jrxj8kmgac-source/pkgs/stdenv/generic/make-derivation.nix:302:7:
   
         301|     // (lib.optionalAttrs (attrs ? name || (attrs ? pname && attrs ? version)) {
         302|       name =
            |       ^
         303|         let
   
      … while evaluating the attribute 'src'
   
      at /nix/store/hd3481707v5r6prhf52y8gyk9x048d00-source/src/evaluator/default.nix:444:17:
   
         443|         pkgdef.src or pkgs.pkgsBuildBuild.emptyDirectory;
         444|     in { inherit archive src; };
            |                 ^
         445|
   
      error: in pure evaluation mode, 'fetchTarball' requires a 'sha256' argument

4. Just for fun, run nix build --impure --show-trace to see if that fixes anything

5. Be met with the following trace

   
   error:
      … while evaluating the attribute 'buildInputs' of the derivation 'coq-verdi-dev'
   
      at /nix/store/q3l9x3ncgi0hppw0i65ki9jrxj8kmgac-source/pkgs/stdenv/generic/make-derivation.nix:302:7:
   
         301|     // (lib.optionalAttrs (attrs ? name || (attrs ? pname && attrs ? version)) {
         302|       name =
            |       ^
         303|         let
   
      … while evaluating the attribute 'src' of the derivation 'coq-inf-seq-ext-dev'
   
      at /nix/store/q3l9x3ncgi0hppw0i65ki9jrxj8kmgac-source/pkgs/stdenv/generic/make-derivation.nix:302:7:
   
         301|     // (lib.optionalAttrs (attrs ? name || (attrs ? pname && attrs ? version)) {
         302|       name =
            |       ^
         303|         let
   
      … while evaluating the attribute 'src'
   
      at /nix/store/hd3481707v5r6prhf52y8gyk9x048d00-source/src/evaluator/default.nix:444:17:
   
         443|         pkgdef.src or pkgs.pkgsBuildBuild.emptyDirectory;
         444|     in { inherit archive src; };
            |                 ^
         445|
   
      error: unable to download 'git+https://github.com/DistributedComponents/InfSeqExt.git#master': Unsupported protocol (1)

The error appears to stem from [this line](https://github.com/coq/opam-coq-archive/blob/608e0fa62974c27b86deeaeff412a139452fa662/extra-dev/packages/coq-inf-seq-ext/coq-inf-seq-ext.dev/opam#L35). Building other Coq projects with similar dependencies also leads to the same sort of "Unsupported protocol" error, so I do not believe this is specific to Coq's distributed components library, nor to Verdi. But I don't understand `opam-nix` well enough to know what is happening here.

**Expected behavior**
Because Verdi is an opam project, the first `nix build` should succeed and build Verdi for me.

**Environment**
 - NixOS following the 23.05 release branch

**Additional context**
The `flake.nix` contains a line like

      on.buildOpamProject
        { repos = [ opam-repository
                    ("${opam-coq-archive}" + "/extra-dev")
                  ];
        }

The string interpolation is because opam-coq-archive contains multiple opam repos (unfortunately), so I have to specify the `extra-dev` repo in particular.

[balsoft]

Because Verdi is an opam project, the first nix build should succeed and build Verdi for me.

That's just not possible if a dependency of that package has a "moving" source (and a git branch is a moving source). Nix guarantees reproducibility (in a particular sense), and it requires that all the inputs to a derivation must have a corresponding checksum, which this doesn't. I believe it's a bad idea to put a package like this into any repository, so it should probably be fixed upstream (with either a particular git revision or a stable link with a checksum locking it).

As for the second error (when ran with --impure), it is indeed fixable on the opam-nix side. I will look into it.

[balsoft]

For now, as a workaround, you can override the src argument of the offending packages with something like src = builtins.fetchGit "https://github.com/DistributedComponents/InfSeqExt.git"; or similar. Note that this will require --impure.

[balsoft]

That particular error should be fixed in f4aa535d3d266ddd5bbd3c63156135a825fc6d52 . The flake still doesn't build, but it's a separate issue.

[balsoft]

As of 5bfdc95cfb7662cac808eb1baa70ae3fff0cab4f, your flake builds fine now. Thanks for reporting!

[dunnl]

Can confirm both of these fixes. Checksums are evidently not common in Coq's core-dev and extra-dev repos:

$ cd opam-coq-archive/extra-dev
$ find . -iname 'opam' | wc -l
316
$ grep --files-with-matches "checksum" . -R | wc -l
30

So --impure will be required for the foreseeable future here, which is indeed an upstream issue. Cheers!