Sebastian Ertel (Feb 07 2023 at 19:37): 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
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.
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.
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
It seems to confuse the version numbers at this point. It uses the one from mathcomp-analysis to fetch mathcomp.
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.
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.
Théo Zimmermann (Feb 08 2023 at 15:38):Try replacing super.mathcomp-ssreflect.override with super.mathcomp.override.
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)
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"; };
Sebastian Ertel has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC