From f37210c50071b7ea6d815c5b84d74445b128455b Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 9 Mar 2021 19:40:37 +0100 Subject: [PATCH] Switching to the new CoqPackages infrastructure --- .../mathcomp-core-shell/default.nix | 6 + .../mathcomp-full-shell/default.nix | 9 + Makefile | 2 + default.nix | 160 ++---------------- 4 files changed, 34 insertions(+), 143 deletions(-) create mode 100644 .nix/coq-overlays/mathcomp-core-shell/default.nix create mode 100644 .nix/coq-overlays/mathcomp-full-shell/default.nix diff --git a/.nix/coq-overlays/mathcomp-core-shell/default.nix b/.nix/coq-overlays/mathcomp-core-shell/default.nix new file mode 100644 index 0000000..e06ac66 --- /dev/null +++ b/.nix/coq-overlays/mathcomp-core-shell/default.nix @@ -0,0 +1,6 @@ +{ stdenv, coq, mathcomp, version ? null }@args: +stdenv.mkDerivation { + name = "mathcomp-core-shell"; + buildInputs = [ coq mathcomp ]; + src = version; +} diff --git a/.nix/coq-overlays/mathcomp-full-shell/default.nix b/.nix/coq-overlays/mathcomp-full-shell/default.nix new file mode 100644 index 0000000..b467e72 --- /dev/null +++ b/.nix/coq-overlays/mathcomp-full-shell/default.nix @@ -0,0 +1,9 @@ +{ stdenv, coq, mathcomp, mathcomp-finmap, mathcomp-bigenough, + mathcomp-real-closed, mathcomp-analysis, multinomials, + mathcomp-abel, version ? null }@args: +stdenv.mkDerivation { + name = "mathcomp-full-shell"; + buildInputs = builtins.attrValues + (builtins.removeAttrs args ["stdenv" "version"]); + src = version; +} diff --git a/Makefile b/Makefile index d211b79..9d96754 100644 --- a/Makefile +++ b/Makefile @@ -1,3 +1,5 @@ .PHONY: err err: echo "Use --arg src /your/path to provide a source path" +install: + echo "No install" diff --git a/default.nix b/default.nix index 9c4336c..132972f 100644 --- a/default.nix +++ b/default.nix @@ -1,144 +1,18 @@ -{ - nixpkgs ? (if builtins.pathExists ./nixpkgs.nix then import ./nixpkgs.nix - else fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/502845c3e31ef3de0e424f3fcb09217df2ce6df6.tar.gz), - config ? (if builtins.pathExists ./config.nix then import ./config.nix else {}), - withEmacs ? false, - print-env ? false, - do-nothing ? false, - package ? (if builtins.pathExists ./package.nix then import ./package.nix else "mathcomp-fast"), - src ? (if builtins.pathExists ./package.nix then ./. else false) -}: -with builtins; -let - cfg-fun = if isFunction config then config else (pkgs: config); - pkg-src = if src == false then {} - else { ${if package == "mathcomp.single" then "mathcomp" else package} = src; }; - pkgs = if isAttrs nixpkgs then nixpkgs else import nixpkgs { - overlays = [ (pkgs: super-pkgs: with pkgs.lib; - let coqPackages = with pkgs; { - "8.7" = coqPackages_8_7; - "8.8" = coqPackages_8_8; - "8.9" = coqPackages_8_9; - "8.10" = coqPackages_8_10; - "8.11" = coqPackages_8_11; - "8.12" = coqPackages_8_12; - "default" = coqPackages_8_10; - }.${(cfg-fun pkgs).coq or "default"}.overrideScope' - (coqPackages: super-coqPackages: - let - all-pkgs = pkgs // { inherit coqPackages; }; - cfg = pkg-src // { - mathcomp-fast = { - src = ./.; - propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-fast); - }; - mathcomp-full = { - src = ./.; - propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-all); - }; - } // (cfg-fun all-pkgs); - in { - mathcomp-extra-config = - let mec = super-coqPackages.mathcomp-extra-config; in - lib.recursiveUpdate mec { - initial = { - # fixing mathcomp analysis to depend on real-closed - mathcomp-analysis = {version, coqPackages} @ args: - let mca = mec.initial.mathcomp-analysis args; in - mca // { - propagatedBuildInputs = mca.propagatedBuildInputs ++ - (if builtins.elem coq.version ["8.10" "8.11" "8.12"] then (with coqPackages; [ coq-elpi hierarchy-builder ]) else []); - }; - }; - for-coq-and-mc.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} = - (super-coqPackages.mathcomp-extra-config.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} or {}) // - (removeAttrs cfg [ "mathcomp" "coq" "mathcomp-fast" "mathcomp-full" ]); - }; - mathcomp = if cfg?mathcomp then coqPackages.mathcomp_ cfg.mathcomp else super-coqPackages.mathcomp; - } // mapAttrs - (package: version: coqPackages.mathcomp-extra package version) - (removeAttrs cfg ["mathcomp" "coq"]) - ); in { - coqPackages = coqPackages.filterPackages coqPackages.coq coqPackages; - coq = coqPackages.coq; - mc-clean = src: { - version = baseNameOf src; - src = cleanSourceWith { - src = cleanSource src; - filter = path: type: let baseName = baseNameOf (toString path); in ! ( - hasSuffix ".aux" baseName || - hasSuffix ".d" baseName || - hasSuffix ".vo" baseName || - hasSuffix ".glob" baseName || - elem baseName ["Makefile.coq" "Makefile.coq.conf" ".mailmap" ".git"] - ); - }; - }; - })]; - }; - - mathcompnix = ./.; - - shellHook = '' - nixEnv () { - echo "Here is your work environement" - echo "buildInputs:" - for x in $buildInputs; do printf " "; echo $x | cut -d "-" -f "2-"; done - echo "propagatedBuildInputs:" - for x in $propagatedBuildInputs; do printf " "; echo $x | cut -d "-" -f "2-"; done - echo "you can pass option --arg config '{coq = \"x.y\"; math-comp = \"x.y.z\";}' to nix-shell to change coq and/or math-comp versions" - } - - printEnv () { - for x in $buildInputs; do echo $x; done - for x in $propagatedBuildInputs; do echo $x; done - } - - cachixEnv () { - echo "Pushing environement to cachix" - printEnv | cachix push math-comp - } - - nixDefault () { - cat $mathcompnix/default.nix - } > default.nix - - updateNixPkgs (){ - HASH=$(git ls-remote https://github.com/NixOS/nixpkgs-channels refs/heads/nixpkgs-unstable | cut -f1); - URL=https://github.com/NixOS/nixpkgs-channels/archive/$HASH.tar.gz - SHA256=$(nix-prefetch-url --unpack $URL) - echo "fetchTarball { - url = $URL; - sha256 = \"$SHA256\"; - }" > nixpkgs.nix - } - updateNixPkgsMaster (){ - HASH=$(git ls-remote https://github.com/NixOS/nixpkgs refs/heads/master | cut -f1); - URL=https://github.com/NixOS/nixpkgs/archive/$HASH.tar.gz - SHA256=$(nix-prefetch-url --unpack $URL) - echo "fetchTarball { - url = $URL; - sha256 = \"$SHA256\"; - }" > nixpkgs.nix - } - '' - + pkgs.lib.optionalString print-env "nixEnv"; - - emacs = with pkgs; emacsWithPackages - (epkgs: with epkgs.melpaStablePackages; [proof-general]); - - pkg = with pkgs; - if package == "mathcomp.single" then coqPackages.mathcomp.single - else coqPackages.${package} or (coqPackages.current-mathcomp-extra package); +{ core ? false, + config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false, + update-nixpkgs ? false, ci-matrix ? false, ci-step ? null, + override ? {}, ocaml-override ? {}, global-override ? {}, + ci ? (!isNull ci-step), inNixShell ? null +}@args: +let src = fetchGit { + url = "https://github.com/coq-community/nix-toolbox.git"; + ref = "8b8ed7f4fc38ae218d99fe9909142b30e6a0733f"; +}; in -if pkgs.lib.trivial.inNixShell then pkg.overrideAttrs (old: { - inherit shellHook mathcompnix; - - buildInputs = if do-nothing then [] - else (old.buildInputs ++ - (if pkgs.lib.trivial.inNixShell then pkgs.lib.optional withEmacs pkgs.emacs - else [])); - - propagatedBuildInputs = if do-nothing then [] else old.propagatedBuildInputs; - -}) else pkg +(import src ./. + ({config = { + coq-attribute = if core then "mathcomp-core-shell" + else "mathcomp-full-shell"; + src = ./.; + }; + } // removeAttrs args ["core"])).nix-auto