From 9ab423efec908ac94dc39d5742c4b1b86c89897c Mon Sep 17 00:00:00 2001 From: Philip Taron Date: Thu, 14 Mar 2024 14:57:15 -0700 Subject: [PATCH 1/4] coqPackages.metacoq: avoid top-level `with ...;` --- .../coq-modules/metacoq/default.nix | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/pkgs/development/coq-modules/metacoq/default.nix b/pkgs/development/coq-modules/metacoq/default.nix index 174f44b7702a..bfd5baf97d4c 100644 --- a/pkgs/development/coq-modules/metacoq/default.nix +++ b/pkgs/development/coq-modules/metacoq/default.nix @@ -1,11 +1,11 @@ { lib, fetchzip, - mkCoqDerivation, recurseIntoAttrs, single ? false, + mkCoqDerivation, single ? false, coqPackages, coq, equations, version ? null }@args: -with builtins // lib; + let repo = "metacoq"; owner = "MetaCoq"; - defaultVersion = with versions; switch coq.coq-version [ + defaultVersion = lib.switch coq.coq-version [ { case = "8.11"; out = "1.0-beta2-8.11"; } { case = "8.12"; out = "1.0-beta2-8.12"; } # Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3) @@ -36,14 +36,14 @@ let releaseRev = v: "v${v}"; # list of core metacoq packages sorted by dependency order - packages = if versionAtLeast coq.coq-version "8.17" + packages = if lib.versionAtLeast coq.coq-version "8.17" then [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ] else [ "template-coq" "pcuic" "safechecker" "erasure" "all" ]; template-coq = metacoq_ "template-coq"; metacoq_ = package: let - metacoq-deps = lib.optionals (package != "single") (map metacoq_ (head (splitList (lib.pred.equal package) packages))); + metacoq-deps = lib.optionals (package != "single") (map metacoq_ (lib.head (lib.splitList (lib.pred.equal package) packages))); pkgpath = if package == "single" then "./" else "./${package}"; pname = if package == "all" then "metacoq" else "metacoq-${package}"; pkgallMake = '' @@ -57,7 +57,7 @@ let mlPlugin = true; propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps; - patchPhase = if versionAtLeast coq.coq-version "8.17" then '' + patchPhase = if lib.versionAtLeast coq.coq-version "8.17" then '' patchShebangs ./configure.sh patchShebangs ./template-coq/update_plugin.sh patchShebangs ./template-coq/gen-src/to-lower.sh @@ -76,11 +76,11 @@ let sed -i -e 's/mv $i $newi;/mv $i tmp; mv tmp $newi;/' ./template-coq/gen-src/to-lower.sh ./pcuic/clean_extraction.sh ./safechecker/clean_extraction.sh ./erasure/clean_extraction.sh '' ; - configurePhase = optionalString (package == "all") pkgallMake + '' + configurePhase = lib.optionalString (package == "all") pkgallMake + '' touch ${pkgpath}/metacoq-config - '' + optionalString (elem package ["safechecker" "erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin"]) '' + '' + lib.optionalString (lib.elem package ["safechecker" "erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin"]) '' echo "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config - '' + optionalString (package == "single") '' + '' + lib.optionalString (package == "single") '' ./configure.sh local ''; @@ -90,17 +90,17 @@ let meta = { homepage = "https://metacoq.github.io/"; - license = licenses.mit; - maintainers = with maintainers; [ cohencyril ]; + license = lib.licenses.mit; + maintainers = with lib.maintainers; [ cohencyril ]; }; - } // optionalAttrs (package != "single") - { passthru = genAttrs packages metacoq_; }) + } // lib.optionalAttrs (package != "single") + { passthru = lib.genAttrs packages metacoq_; }) ).overrideAttrs (o: - let requiresOcamlStdlibShims = versionAtLeast o.version "1.0-8.16" || - (o.version == "dev" && (versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev")) ; + let requiresOcamlStdlibShims = lib.versionAtLeast o.version "1.0-8.16" || + (o.version == "dev" && (lib.versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev")) ; in { - propagatedBuildInputs = o.propagatedBuildInputs ++ optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims; + propagatedBuildInputs = o.propagatedBuildInputs ++ lib.optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims; }); in derivation; in From 94112e3ae57edb91e33f01fe7f46f02c47d728cc Mon Sep 17 00:00:00 2001 From: Philip Taron Date: Thu, 14 Mar 2024 14:51:49 -0700 Subject: [PATCH 2/4] coqPackages.mathcomp: avoid top-level `with ...;` --- .../coq-modules/mathcomp/default.nix | 41 ++++++++++--------- 1 file changed, 21 insertions(+), 20 deletions(-) diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix index 50fc63de4cc4..7f132768ff88 100644 --- a/pkgs/development/coq-modules/mathcomp/default.nix +++ b/pkgs/development/coq-modules/mathcomp/default.nix @@ -11,14 +11,15 @@ ############################################################################ { lib, ncurses, graphviz, lua, fetchzip, - mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false, + mkCoqDerivation, withDoc ? false, single ? false, coqPackages, coq, hierarchy-builder, version ? null }@args: -with builtins // lib; + let repo = "math-comp"; owner = "math-comp"; withDoc = single && (args.withDoc or false); - defaultVersion = with versions; lib.switch coq.coq-version [ + defaultVersion = let inherit (lib.versions) range; in + lib.switch coq.coq-version [ { case = range "8.19" "8.19"; out = "1.19.0"; } { case = range "8.17" "8.18"; out = "1.18.0"; } { case = range "8.15" "8.18"; out = "1.17.0"; } @@ -63,7 +64,7 @@ let packages = [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ]; mathcomp_ = package: let - mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ (head (splitList (lib.pred.equal package) packages))); + mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ (lib.head (lib.splitList (lib.pred.equal package) packages))); pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}"; pname = if package == "single" then "mathcomp" else "mathcomp-${package}"; pkgallMake = '' @@ -74,12 +75,12 @@ let derivation = mkCoqDerivation ({ inherit version pname defaultVersion release releaseRev repo owner; - mlPlugin = versions.isLe "8.6" coq.coq-version; - nativeBuildInputs = optionals withDoc [ graphviz lua ]; + mlPlugin = lib.versions.isLe "8.6" coq.coq-version; + nativeBuildInputs = lib.optionals withDoc [ graphviz lua ]; buildInputs = [ ncurses ]; propagatedBuildInputs = mathcomp-deps; - buildFlags = optional withDoc "doc"; + buildFlags = lib.optional withDoc "doc"; preBuild = '' if [[ -f etc/utils/ssrcoqdep ]] @@ -90,16 +91,16 @@ let fi '' + '' cd ${pkgpath} - '' + optionalString (package == "all") pkgallMake; + '' + lib.optionalString (package == "all") pkgallMake; meta = { homepage = "https://math-comp.github.io/"; - license = licenses.cecill-b; - maintainers = with maintainers; [ vbgl jwiegley cohencyril ]; + license = lib.licenses.cecill-b; + maintainers = with lib.maintainers; [ vbgl jwiegley cohencyril ]; }; - } // optionalAttrs (package != "single") - { passthru = genAttrs packages mathcomp_; } - // optionalAttrs withDoc { + } // lib.optionalAttrs (package != "single") + { passthru = lib.genAttrs packages mathcomp_; } + // lib.optionalAttrs withDoc { htmldoc_template = fetchzip { url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip"; @@ -111,7 +112,7 @@ let ''; postInstall = let tgt = "$out/share/coq/${coq.coq-version}/"; in - optionalString withDoc '' + lib.optionalString withDoc '' mkdir -p ${tgt} cp -r htmldoc ${tgt} cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/ @@ -120,20 +121,20 @@ let extraInstallFlags = [ "-f Makefile.coq" ]; }); patched-derivation1 = derivation.overrideAttrs (o: - optionalAttrs (o.pname != null && o.pname == "mathcomp-all" && - o.version != null && o.version != "dev" && versions.isLt "1.7" o.version) + lib.optionalAttrs (o.pname != null && o.pname == "mathcomp-all" && + o.version != null && o.version != "dev" && lib.versions.isLt "1.7" o.version) { preBuild = ""; buildPhase = ""; installPhase = "echo doing nothing"; } ); patched-derivation2 = patched-derivation1.overrideAttrs (o: - optionalAttrs (versions.isLe "8.7" coq.coq-version || - (o.version != "dev" && versions.isLe "1.7" o.version)) + lib.optionalAttrs (lib.versions.isLe "8.7" coq.coq-version || + (o.version != "dev" && lib.versions.isLe "1.7" o.version)) { installFlags = o.installFlags ++ [ "-f Makefile.coq" ]; } ); patched-derivation = patched-derivation2.overrideAttrs (o: - optionalAttrs (o.version != null - && (o.version == "dev" || versions.isGe "2.0.0" o.version)) + lib.optionalAttrs (o.version != null + && (o.version == "dev" || lib.versions.isGe "2.0.0" o.version)) { propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ]; } From e8955041c3a107525bc2eb3d118337cce37ac758 Mon Sep 17 00:00:00 2001 From: Philip Taron Date: Thu, 14 Mar 2024 14:53:57 -0700 Subject: [PATCH 3/4] coqPackages.mathcomp-analysis: avoid top-level `with ...;` --- .../coq-modules/mathcomp-analysis/default.nix | 47 ++++++++++--------- 1 file changed, 24 insertions(+), 23 deletions(-) diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix index abd300f947a9..97e8a7698a90 100644 --- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix +++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix @@ -1,10 +1,10 @@ { lib, - mkCoqDerivation, recurseIntoAttrs, + mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough, hierarchy-builder, single ? false, coqPackages, coq, version ? null }@args: -with builtins // lib; + let repo = "analysis"; owner = "math-comp"; @@ -30,20 +30,21 @@ let release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8"; release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966"; - defaultVersion = with versions; lib.switch [ coq.version mathcomp.version ] [ - { cases = [ (range "8.17" "8.19") (range "2.0.0" "2.2.0") ]; out = "1.1.0"; } + defaultVersion = let inherit (lib.versions) range; in + lib.switch [ coq.version mathcomp.version ] [ + { cases = [ (range "8.17" "8.19") (range "2.0.0" "2.2.0") ]; out = "1.1.0"; } { cases = [ (range "8.17" "8.19") (range "1.17.0" "1.19.0") ]; out = "0.7.0"; } { cases = [ (range "8.17" "8.18") (range "1.15.0" "1.18.0") ]; out = "0.6.7"; } { cases = [ (range "8.17" "8.18") (range "1.15.0" "1.18.0") ]; out = "0.6.6"; } { cases = [ (range "8.14" "8.18") (range "1.15.0" "1.17.0") ]; out = "0.6.5"; } { cases = [ (range "8.14" "8.18") (range "1.13.0" "1.16.0") ]; out = "0.6.1"; } - { cases = [ (range "8.14" "8.18") (range "1.13" "1.15") ]; out = "0.5.2"; } - { cases = [ (range "8.13" "8.15") (range "1.13" "1.14") ]; out = "0.5.1"; } - { cases = [ (range "8.13" "8.15") (range "1.12" "1.14") ]; out = "0.3.13"; } - { cases = [ (range "8.11" "8.14") (range "1.12" "1.13") ]; out = "0.3.10"; } - { cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "0.3.3"; } - { cases = [ (range "8.10" "8.11") "1.11.0" ]; out = "0.3.1"; } - { cases = [ (range "8.8" "8.11") (range "1.8" "1.10") ]; out = "0.2.3"; } + { cases = [ (range "8.14" "8.18") (range "1.13" "1.15") ]; out = "0.5.2"; } + { cases = [ (range "8.13" "8.15") (range "1.13" "1.14") ]; out = "0.5.1"; } + { cases = [ (range "8.13" "8.15") (range "1.12" "1.14") ]; out = "0.3.13"; } + { cases = [ (range "8.11" "8.14") (range "1.12" "1.13") ]; out = "0.3.10"; } + { cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "0.3.3"; } + { cases = [ (range "8.10" "8.11") "1.11.0" ]; out = "0.3.1"; } + { cases = [ (range "8.8" "8.11") (range "1.8" "1.10") ]; out = "0.2.3"; } ] null; # list of analysis packages sorted by dependency order @@ -52,7 +53,7 @@ let mathcomp_ = package: let classical-deps = [ mathcomp.algebra mathcomp-finmap ]; analysis-deps = [ mathcomp.field mathcomp-bigenough ]; - intra-deps = lib.optionals (package != "single") (map mathcomp_ (head (splitList (lib.pred.equal package) packages))); + intra-deps = lib.optionals (package != "single") (map mathcomp_ (lib.head (lib.splitList (lib.pred.equal package) packages))); pkgpath = if package == "single" then "." else if package == "analysis" then "theories" else "${package}"; pname = if package == "single" then "mathcomp-analysis-single" @@ -64,8 +65,8 @@ let propagatedBuildInputs = intra-deps - ++ optionals (elem package [ "classical" "single" ]) classical-deps - ++ optionals (elem package [ "analysis" "single" ]) analysis-deps; + ++ lib.optionals (lib.elem package [ "classical" "single" ]) classical-deps + ++ lib.optionals (lib.elem package [ "analysis" "single" ]) analysis-deps; preBuild = '' cd ${pkgpath} @@ -73,26 +74,26 @@ let meta = { description = "Analysis library compatible with Mathematical Components"; - maintainers = [ maintainers.cohencyril ]; - license = licenses.cecill-c; + maintainers = [ lib.maintainers.cohencyril ]; + license = lib.licenses.cecill-c; }; - passthru = genAttrs packages mathcomp_; + passthru = lib.genAttrs packages mathcomp_; }); # split packages didn't exist before 0.6, so bulding nothing in that case patched-derivation1 = derivation.overrideAttrs (o: - optionalAttrs (o.pname != null && o.pname != "mathcomp-analysis" && - o.version != null && o.version != "dev" && versions.isLt "0.6" o.version) + lib.optionalAttrs (o.pname != null && o.pname != "mathcomp-analysis" && + o.version != null && o.version != "dev" && lib.versions.isLt "0.6" o.version) { preBuild = ""; buildPhase = "echo doing nothing"; installPhase = "echo doing nothing"; } ); patched-derivation2 = patched-derivation1.overrideAttrs (o: - optionalAttrs (o.pname != null && o.pname == "mathcomp-analysis" && - o.version != null && o.version != "dev" && versions.isLt "0.6" o.version) + lib.optionalAttrs (o.pname != null && o.pname == "mathcomp-analysis" && + o.version != null && o.version != "dev" && lib.versions.isLt "0.6" o.version) { preBuild = ""; } ); patched-derivation = patched-derivation2.overrideAttrs (o: - optionalAttrs (o.version != null - && (o.version == "dev" || versions.isGe "0.3.4" o.version)) + lib.optionalAttrs (o.version != null + && (o.version == "dev" || lib.versions.isGe "0.3.4" o.version)) { propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ]; } From 3aaf29fe2271f969ad26bf63883dd0cf72faeab2 Mon Sep 17 00:00:00 2001 From: Philip Taron Date: Thu, 14 Mar 2024 14:45:58 -0700 Subject: [PATCH 4/4] coqPackages.coq-elpi: avoid top-level `with ...;` --- pkgs/development/coq-modules/coq-elpi/default.nix | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix index 04dea2feaf60..fe577a149d71 100644 --- a/pkgs/development/coq-modules/coq-elpi/default.nix +++ b/pkgs/development/coq-modules/coq-elpi/default.nix @@ -1,6 +1,6 @@ { lib, mkCoqDerivation, which, coq, version ? null }: -with builtins; with lib; let +let elpi = coq.ocamlPackages.elpi.override (lib.switch coq.coq-version [ { case = "8.11"; out = { version = "1.11.4"; };} { case = "8.12"; out = { version = "1.12.0"; };} @@ -71,7 +71,7 @@ in mkCoqDerivation { meta = { description = "Coq plugin embedding ELPI"; - maintainers = [ maintainers.cohencyril ]; - license = licenses.lgpl21Plus; + maintainers = [ lib.maintainers.cohencyril ]; + license = lib.licenses.lgpl21Plus; }; }