Stream: Coq users

Topic: ✔ Nix flake setup


view this post on Zulip Sebastian Ertel (Feb 07 2023 at 19:37):

Hi,

I'm trying to setup a Nix flake to build a project that has another Coq project , SSProve as a git submodule.
Hence, the flake is supposed to load the proper setup to compile SSProve successfully such that I can use SSProve in my actual project.
But I get an error when Nix is trying to load mathcomp.

Any help on this would be highly appreciated.

Here is my flake.nix:

{
  inputs = {
    nixpkgs.url = github:nixos/nixpkgs;
    flake-utils.url = github:numtide/flake-utils;
  };
  outputs = { self, nixpkgs, flake-utils }:
    flake-utils.lib.eachDefaultSystem (system:
      let
        pkgs = nixpkgs.legacyPackages.${system};
        ocamlPackages = pkgs.ocaml-ng.ocamlPackages_4_09;
        coq = pkgs.coq_8_14.override {
          customOCamlPackages = ocamlPackages;
        };
        coqPackages = pkgs.coqPackages_8_14.overrideScope'
          (self: super: {
            equations          = super.equations.override { version = "1.3"; };
            mathcomp-analysis  = super.mathcomp-analysis.override { version = "0.3.12"; };
            mathcomp-ssreflect = super.mathcomp-ssreflect.override { version = "1.13.0"; };
            extructures        = super.extructures.override { version = "0.3.1"; };
            deriving           = super.deriving.override { version = "0.1"; };
         });
      in {
        devShell = pkgs.mkShell {
          packages =
            (with pkgs; [ coq gnumake ])
            ++
            (with coqPackages; [ equations  mathcomp-analysis  mathcomp-ssreflect  extructures  deriving ]);
        };
      }
    );
}

The error message that I receive when calling nix develop is:

error: in pure evaluation mode, 'fetchTarball' requires a 'sha256' argument

With --show-trace I see:

       ...
       at /nix/store/i29856bzbvv3aczf09rmvkniagv7pgw0-source/pkgs/build-support/coq/meta-fetch/default.nix:58:7:

           57|       inherit version;
           58|       src = fetcher (location // { inherit rev; } //
             |       ^
           59|         (optionalAttrs has-owner { owner = head splitted; }));

        while evaluating the attribute 'src' of the derivation 'coq8.14-mathcomp1.15-mathcomp-classical-dev'

       at /nix/store/i29856bzbvv3aczf09rmvkniagv7pgw0-source/pkgs/stdenv/generic/make-derivation.nix:286:7:

          285|     // (lib.optionalAttrs (attrs ? name || (attrs ? pname && attrs ? version)) {
          286|       name =
             |       ^
          287|         let

        while evaluating the attribute 'propagatedBuildInputs' of the derivation 'coq8.14-mathcomp1.15-mathcomp-analysis-dev'

       at /nix/store/i29856bzbvv3aczf09rmvkniagv7pgw0-source/pkgs/stdenv/generic/make-derivation.nix:286:7:

          285|     // (lib.optionalAttrs (attrs ? name || (attrs ? pname && attrs ? version)) {
          286|       name =
             |       ^
          287|         let

        while evaluating the attribute 'nativeBuildInputs' of the derivation 'nix-shell'

       at /nix/store/i29856bzbvv3aczf09rmvkniagv7pgw0-source/pkgs/stdenv/generic/make-derivation.nix:286:7:

          285|     // (lib.optionalAttrs (attrs ? name || (attrs ? pname && attrs ? version)) {
          286|       name =
             |       ^
          287|         let

view this post on Zulip Ali Caglayan (Feb 07 2023 at 19:46):

Something you are using is using fetch tar which needs the exact sha for the commit to be reproducable (pure). You can override this requirement by passing --impure to nix develop or whatever command you are using.

view this post on Zulip Ali Caglayan (Feb 07 2023 at 19:47):

I don't know if it is possible to manually override the sha being passed to fetch tar.

view this post on Zulip Sebastian Ertel (Feb 07 2023 at 20:05):

I tried that too and it fails with:

error: unable to download 'https://github.com/math-comp/math-comp/archive/0.3.12.tar.gz': HTTP error 404

view this post on Zulip Sebastian Ertel (Feb 07 2023 at 20:15):

It seems to confuse the version numbers at this point. It uses the one from mathcomp-analysis to fetch mathcomp.

view this post on Zulip Sebastian Ertel (Feb 08 2023 at 07:17):

I found the problem.
The version number for mathcomp-analysis was wrong. There is no version 0.3.12. I meant to write 0.3.2.
But there is no such version in Nix:
https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coq-modules/mathcomp-analysis/default.nix
Setting the version to 0.3.1 solves at least this problem.

view this post on Zulip Sebastian Ertel (Feb 08 2023 at 12:59):

But now its stuck trying to fetch mathcomp-analysis or mathcomp-ssreflect:

trying https://github.com/math-comp/math-comp/archive/0.3.1.zip

It again tries the totally wrong version number.

view this post on Zulip Théo Zimmermann (Feb 08 2023 at 15:38):

Try replacing super.mathcomp-ssreflect.override with super.mathcomp.override.

view this post on Zulip Théo Zimmermann (Feb 08 2023 at 15:38):

(mathcomp-ssreflect is exported by mathcomp, so I think you have to override the latter directly)

view this post on Zulip Sebastian Ertel (Feb 08 2023 at 16:20):

Thanks for your inputs.
I solved the problem. In nix you have to explicitly specify the mathcomp version. Apparently in opam this is not necessary.
So adding the following (as suggested by @Théo Zimmermann ) solved all the problems:

mathcomp  = super.mathcomp.override { version = "1.13.0"; };

view this post on Zulip Notification Bot (Feb 08 2023 at 16:20):

Sebastian Ertel has marked this topic as resolved.


Last updated: May 24 2024 at 21:01 UTC