Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

coqPackages: refactor #59217

Merged
merged 1 commit into from
Apr 16, 2019
Merged

coqPackages: refactor #59217

merged 1 commit into from
Apr 16, 2019

Conversation

CohenCyril
Copy link
Contributor

Motivation for this change

Coq packages that depend on other need to be recompiled when the dependencies are updated,
so we make the whole coqPackage overridable by overrideScope', using lib.makeScope.

Things done
  • Tested using sandboxing (nix.useSandbox on NixOS, or option sandbox in nix.conf on non-NixOS)
  • Built on platform(s)
    • NixOS
    • macOS
    • other Linux distributions
  • Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
  • Tested compilation of all pkgs that depend on this change using nix-shell -p nix-review --run "nix-review wip"
  • Tested execution of all binary files (usually in ./result/bin/)
  • Determined the impact on package closure size (by running nix path-info -S before and after)
  • Assured whether relevant documentation is up to date
  • Fits CONTRIBUTING.md.

@GrahamcOfBorg GrahamcOfBorg added 10.rebuild-darwin: 0 This PR does not cause any packages to rebuild on Darwin 10.rebuild-linux: 0 This PR does not cause any packages to rebuild on Linux labels Apr 9, 2019
Coq packages that depend on others need to be recompiled when the dependencies are updated, so we make the whole `coqPackages` overridable by `overrideScope'`, using `lib.makeScope`.
@vbgl vbgl added the 6.topic: coq "A formal proof management system" label Apr 15, 2019
@CohenCyril
Copy link
Contributor Author

Before this PR

The following shell will lead to an inconsistent state of the Coq libraries:
(name this shell-nofix.nix)

let
  config.packageOverrides = pkgs:
    with pkgs; {
      coqPackages = let super = coqPackages; in super // rec {

        mathcomp = super.mathcomp.overrideDerivation (o: rec {
          version = "1.8.0";
          name = "coq${pkgs.coq.coq-version}-mathcomp-${version}";
          src = fetchFromGitHub {
            owner = "math-comp";
            repo = "math-comp";
            rev = "mathcomp-1.8.0";
            sha256 = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
          };
         });
        
        ## Uncomment to fix! 
        # mathcomp-bigenough = super.mathcomp-bigenough.overrideDerivation (oldAttrs: {
        #   propagatedBuildInputs = [mathcomp];
        # });
       };
    };
in
with import <nixpkgs> {inherit config;};
stdenv.mkDerivation rec {
  name = "env";
  env = buildEnv { name = name; paths = buildInputs; };
  
  buildInputs = [ coq ] ++ (with coqPackages; [ mathcomp mathcomp-bigenough ]);
}

Indeed, when we do

echo "From mathcomp Require Import all_ssreflect bigenough." > test.v
nix-shell shell-nofix.nix --run "coqtop -l test.v"

Coq fails with the following error message

Welcome to Coq 8.8.2 (April 2019)
File "[...]/test.v", line 1, characters 0-53:
Error:
Compiled library mathcomp.bigenough.bigenough (in file /nix/store/cdznaylb54c9ixhdgg30xqphlrc10pni-coq8.8-mathcomp-bigenough-1.0.0/lib/coq/8.8/user-contrib/mathcomp/bigenough/bigenough.vo) makes inconsistent assumptions over library mathcomp.ssreflect.eqtype

And I know no other way that propagating the dependencies by hand in the current state of the library.

With this PR

We can now write shell-fix.nix:

let
  config.packageOverrides = pkgs:
    with pkgs; {
      coqPackages = pkgs.coqPackages.overrideScope' (self: super: {

        mathcomp = super.mathcomp.overrideDerivation (o: rec {
          version = "1.8.0";
          name = "coq${pkgs.coq.coq-version}-mathcomp-${version}";
          src = fetchFromGitHub {
            owner = "math-comp";
            repo = "math-comp";
            rev = "mathcomp-1.8.0";
            sha256 = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
          };
         });
       });
    };
in
with import <nixpkgs> {inherit config;};
stdenv.mkDerivation rec {
  name = "env";
  env = buildEnv { name = name; paths = buildInputs; };
  
  buildInputs = [ coq ] ++ (with coqPackages; [ mathcomp mathcomp-bigenough ]);
}

and then

nix-shell shell-fix.nix --run "coqtop -l test.v"

succeeds.

@vbgl vbgl merged commit c46811b into NixOS:master Apr 16, 2019
@vbgl
Copy link
Contributor

vbgl commented Apr 16, 2019

Thank you very much!

@CohenCyril CohenCyril deleted the coq-modules-fix branch May 23, 2019 13:12
@Janik-Haag Janik-Haag added the 12. first-time contribution This PR is the author's first one; please be gentle! label Jun 12, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
6.topic: coq "A formal proof management system" 10.rebuild-darwin: 0 This PR does not cause any packages to rebuild on Darwin 10.rebuild-linux: 0 This PR does not cause any packages to rebuild on Linux 12. first-time contribution This PR is the author's first one; please be gentle!
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants