diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix deleted file mode 100644 index eb2363285f49..000000000000 --- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix +++ /dev/null @@ -1,255 +0,0 @@ -{ - lib, - mkCoqDerivation, - mathcomp, - mathcomp-finmap, - mathcomp-bigenough, - hierarchy-builder, - stdlib, - single ? false, - coq, - version ? null, -}@args: - -let - repo = "analysis"; - owner = "math-comp"; - - release."1.14.0".hash = "sha256-FFcfxnF1wtz2e9Rdqu4Wd0rtLW0DYoXswCTji//RSCQ="; - release."1.13.0".hash = "sha256-nn2gl6cAO93QEdMvLGlB9WAPddQiOdeRtk1pLO+gxII="; - release."1.12.0".hash = "sha256-PF10NlZ+aqP3PX7+UsZwgJT9PEaDwzvrS/ZGzjP64Wo="; - release."1.11.0".hash = "sha256-1apbzBvaLNw/8ARLUhGGy89CyXW+/6O4ckdxKPraiVc="; - release."1.9.0".hash = "sha256-zj7WSDUg8ISWxcipGpjEwvvnLp1g8nm23BZiib/15+g="; - release."1.8.0".hash = "sha256-2ZafDmZAwGB7sxdUwNIE3xvwBRw1kFDk0m5Vz+onWZc="; - release."1.7.0".hash = "sha256-GgsMIHqLkWsPm2VyOPeZdOulkN00IoBz++qA6yE9raQ="; - release."1.5.0".hash = "sha256-EWogrkr5TC5F9HjQJwO3bl4P8mij8U7thUGJNNI+k88="; - release."1.4.0".hash = "sha256-eDggeuEU0fMK7D5FbxvLkbAgpLw5lwL/Rl0eLXAnJeg="; - release."1.2.0".hash = "sha256-w6BivDM4dF4Iv4rUTy++2feweNtMAJxgGExPfYGhXxo="; - release."1.1.0".hash = "sha256-wl4kZf4mh9zbFfGcqaFEgWRyp0Bj511F505mYodpS6o="; - release."1.0.0".hash = "sha256-KiXyaWB4zQ3NuXadq4BSWfoN1cIo1xiLVSN6nW03tC4="; - release."0.7.0".hash = "sha256-JwkyetXrFsFHqz8KY3QBpHsrkhmEFnrCGuKztcoen60="; - release."0.6.7".hash = "sha256-3i2PBMEwihwgwUmnS0cmrZ8s+aLPFVq/vo0aXMUaUyA="; - release."0.6.6".hash = "sha256-tWtv6yeB5/vzwpKZINK9OQ0yQsvD8qu9zVSNHvLMX5Y="; - release."0.6.5".hash = "sha256-oJk9/Jl1SWra2aFAXRAVfX7ZUaDfajqdDksYaW8dv8E="; - release."0.6.1".hash = "sha256-1VyNXu11/pDMuH4DmFYSUF/qZ4Bo+/Zl3Y0JkyrH/r0="; - release."0.6.0".hash = "sha256-0msICcIrK6jbOSiBu0gIVU3RHwoEEvB88CMQqW/06rg="; - release."0.5.3".hash = "sha256-1NjFsi5TITF8ZWx1NyppRmi8g6YaoUtTdS9bU/sUe5k="; - release."0.5.2".hash = "sha256:0yx5p9zyl8jv1vg7rgkyq8dqzkdnkqv969mi62whmhkvxbavgzbw"; - release."0.5.1".hash = "sha256:1hnzqb1gxf88wgj2n1b0f2xm6sxg9j0735zdsv6j12hlvx5lwk68"; - release."0.3.13".hash = "sha256-Yaztew79KWRC933kGFOAUIIoqukaZOdNOdw4XszR1Hg="; - release."0.3.10".hash = "sha256-FBH2c8QRibq5Ycw/ieB8mZl0fDiPrYdIzZ6W/A3pIhI="; - release."0.3.9".hash = "sha256-uUU9diBwUqBrNRLiDc0kz0CGkwTZCUmigPwLbpDOeg4="; - release."0.3.6".hash = "sha256:0g2j7b2hca4byz62ssgg90bkbc8wwp7xkb2d3225bbvihi92b4c5"; - release."0.3.4".hash = "sha256:18mgycjgg829dbr7ps77z6lcj03h3dchjbj5iir0pybxby7gd45c"; - release."0.3.3".hash = "sha256:1m2mxcngj368vbdb8mlr91hsygl430spl7lgyn9qmn3jykack867"; - release."0.3.1".hash = "sha256:1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8"; - release."0.2.3".hash = "sha256:0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966"; - - defaultVersion = - let - case = coq: mc: out: { - cases = [ - coq - mc - ]; - inherit out; - }; - in - with lib.versions; - lib.switch - [ coq.coq-version mathcomp.version ] - [ - (case (range "8.20" "9.1") (range "2.4.0" "2.5.0") "1.14.0") - (case (range "8.20" "9.1") (range "2.1.0" "2.4.0") "1.13.0") - (case (range "8.20" "9.1") (range "2.1.0" "2.4.0") "1.12.0") - (case (range "8.19" "8.20") (range "2.1.0" "2.3.0") "1.9.0") - (case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "1.1.0") - (case (range "8.17" "8.19") (range "1.17.0" "1.19.0") "0.7.0") - (case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.7") - (case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.6") - (case (range "8.14" "8.18") (range "1.15.0" "1.17.0") "0.6.5") - (case (range "8.14" "8.18") (range "1.13.0" "1.16.0") "0.6.1") - (case (range "8.14" "8.18") (range "1.13" "1.15") "0.5.2") - (case (range "8.13" "8.15") (range "1.13" "1.14") "0.5.1") - (case (range "8.13" "8.15") (range "1.12" "1.14") "0.3.13") - (case (range "8.11" "8.14") (range "1.12" "1.13") "0.3.10") - (case (range "8.10" "8.12") "1.11.0" "0.3.3") - (case (range "8.10" "8.11") "1.11.0" "0.3.1") - (case (range "8.8" "8.11") (range "1.8" "1.10") "0.2.3") - ] - null; - - # list of analysis packages sorted by dependency order - packages = { - "classical" = [ ]; - "reals" = [ "classical" ]; - "experimental-reals" = [ "reals" ]; - "analysis" = [ "reals" ]; - "reals-stdlib" = [ "reals" ]; - "analysis-stdlib" = [ - "analysis" - "reals-stdlib" - ]; - }; - - mathcomp_ = - package: - let - classical-deps = [ - mathcomp.ssreflect - mathcomp.algebra - mathcomp-finmap - ]; - experimental-reals-deps = [ mathcomp-bigenough ]; - analysis-deps = [ - mathcomp.field - mathcomp-bigenough - ]; - intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package}); - pkgpath = lib.switch package [ - { - case = "single"; - out = "."; - } - { - case = "analysis"; - out = "theories"; - } - { - case = "experimental-reals"; - out = "experimental_reals"; - } - { - case = "reals-stdlib"; - out = "reals_stdlib"; - } - { - case = "analysis-stdlib"; - out = "analysis_stdlib"; - } - ] package; - pname = if package == "single" then "mathcomp-analysis-single" else "mathcomp-${package}"; - derivation = mkCoqDerivation { - inherit - version - pname - defaultVersion - release - repo - owner - ; - - namePrefix = [ - "coq" - "mathcomp" - ]; - - propagatedBuildInputs = - intra-deps - ++ lib.optionals (lib.elem package [ - "classical" - "single" - ]) classical-deps - ++ lib.optionals (lib.elem package [ - "experimental-reals" - "single" - ]) experimental-reals-deps - ++ lib.optionals (lib.elem package [ - "analysis" - "single" - ]) analysis-deps - ++ lib.optional (lib.elem package [ - "reals-stdlib" - "analysis-stdlib" - "single" - ]) stdlib; - - preBuild = '' - cd ${pkgpath} - ''; - - meta = { - description = "Analysis library compatible with Mathematical Components"; - maintainers = [ lib.maintainers.cohencyril ]; - license = lib.licenses.cecill-c; - }; - - passthru = lib.mapAttrs (package: deps: mathcomp_ package) packages; - }; - # split packages didn't exist before 0.6, so building nothing in that case - patched-derivation1 = derivation.overrideAttrs ( - o: - 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: - lib.optionalAttrs ( - o.pname != null - && o.pname == "mathcomp-analysis" - && o.version != null - && o.version != "dev" - && lib.versions.isLt "0.6" o.version - ) { preBuild = ""; } - ); - # only packages classical and analysis existed before 1.7, so building nothing in that case - patched-derivation3 = patched-derivation2.overrideAttrs ( - o: - lib.optionalAttrs - ( - o.pname != null - && o.pname != "mathcomp-classical" - && o.pname != "mathcomp-analysis" - && o.version != null - && o.version != "dev" - && lib.versions.isLt "1.7" o.version - ) - { - preBuild = ""; - buildPhase = "echo doing nothing"; - installPhase = "echo doing nothing"; - } - ); - patched-derivation = patched-derivation3.overrideAttrs ( - o: - lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "0.3.4" o.version)) - { - propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ]; - } - ); - in - patched-derivation; -in -# this is just a wrapper for rocqPackages.mathcomp-analysis for Rocq >= 9.0 -if - coq.rocqPackages ? mathcomp-analysis - && !(lib.elem version [ - "1.12.0" - "1.13.0" - "1.14.0" - "1.15.0" - ]) -then - coq.rocqPackages.mathcomp-analysis.override { - inherit version single; - inherit - mathcomp - mathcomp-finmap - mathcomp-bigenough - stdlib - ; - inherit (coq.rocqPackages) rocq-core; - } -else - mathcomp_ (if single then "single" else "analysis") diff --git a/pkgs/development/rocq-modules/mathcomp-analysis/default.nix b/pkgs/development/rocq-modules/mathcomp-analysis/default.nix index a1da2f0868b4..10b32be2a9b2 100644 --- a/pkgs/development/rocq-modules/mathcomp-analysis/default.nix +++ b/pkgs/development/rocq-modules/mathcomp-analysis/default.nix @@ -5,6 +5,7 @@ mathcomp-finmap, mathcomp-bigenough, mathcomp-real-closed, + hierarchy-builder, stdlib, single ? false, rocq-core, @@ -16,6 +17,35 @@ let owner = "math-comp"; release."1.16.0".sha256 = "sha256-L0dCbxEqxI8rFv6OOEoIT/U3GKX37ageU9yw2H6hrWY="; + release."1.14.0".hash = "sha256-FFcfxnF1wtz2e9Rdqu4Wd0rtLW0DYoXswCTji//RSCQ="; + release."1.13.0".hash = "sha256-nn2gl6cAO93QEdMvLGlB9WAPddQiOdeRtk1pLO+gxII="; + release."1.12.0".hash = "sha256-PF10NlZ+aqP3PX7+UsZwgJT9PEaDwzvrS/ZGzjP64Wo="; + release."1.11.0".hash = "sha256-1apbzBvaLNw/8ARLUhGGy89CyXW+/6O4ckdxKPraiVc="; + release."1.9.0".hash = "sha256-zj7WSDUg8ISWxcipGpjEwvvnLp1g8nm23BZiib/15+g="; + release."1.8.0".hash = "sha256-2ZafDmZAwGB7sxdUwNIE3xvwBRw1kFDk0m5Vz+onWZc="; + release."1.7.0".hash = "sha256-GgsMIHqLkWsPm2VyOPeZdOulkN00IoBz++qA6yE9raQ="; + release."1.5.0".hash = "sha256-EWogrkr5TC5F9HjQJwO3bl4P8mij8U7thUGJNNI+k88="; + release."1.4.0".hash = "sha256-eDggeuEU0fMK7D5FbxvLkbAgpLw5lwL/Rl0eLXAnJeg="; + release."1.2.0".hash = "sha256-w6BivDM4dF4Iv4rUTy++2feweNtMAJxgGExPfYGhXxo="; + release."1.1.0".hash = "sha256-wl4kZf4mh9zbFfGcqaFEgWRyp0Bj511F505mYodpS6o="; + release."1.0.0".hash = "sha256-KiXyaWB4zQ3NuXadq4BSWfoN1cIo1xiLVSN6nW03tC4="; + release."0.7.0".hash = "sha256-JwkyetXrFsFHqz8KY3QBpHsrkhmEFnrCGuKztcoen60="; + release."0.6.7".hash = "sha256-3i2PBMEwihwgwUmnS0cmrZ8s+aLPFVq/vo0aXMUaUyA="; + release."0.6.6".hash = "sha256-tWtv6yeB5/vzwpKZINK9OQ0yQsvD8qu9zVSNHvLMX5Y="; + release."0.6.5".hash = "sha256-oJk9/Jl1SWra2aFAXRAVfX7ZUaDfajqdDksYaW8dv8E="; + release."0.6.1".hash = "sha256-1VyNXu11/pDMuH4DmFYSUF/qZ4Bo+/Zl3Y0JkyrH/r0="; + release."0.6.0".hash = "sha256-0msICcIrK6jbOSiBu0gIVU3RHwoEEvB88CMQqW/06rg="; + release."0.5.3".hash = "sha256-1NjFsi5TITF8ZWx1NyppRmi8g6YaoUtTdS9bU/sUe5k="; + release."0.5.2".hash = "sha256:0yx5p9zyl8jv1vg7rgkyq8dqzkdnkqv969mi62whmhkvxbavgzbw"; + release."0.5.1".hash = "sha256:1hnzqb1gxf88wgj2n1b0f2xm6sxg9j0735zdsv6j12hlvx5lwk68"; + release."0.3.13".hash = "sha256-Yaztew79KWRC933kGFOAUIIoqukaZOdNOdw4XszR1Hg="; + release."0.3.10".hash = "sha256-FBH2c8QRibq5Ycw/ieB8mZl0fDiPrYdIzZ6W/A3pIhI="; + release."0.3.9".hash = "sha256-uUU9diBwUqBrNRLiDc0kz0CGkwTZCUmigPwLbpDOeg4="; + release."0.3.6".hash = "sha256:0g2j7b2hca4byz62ssgg90bkbc8wwp7xkb2d3225bbvihi92b4c5"; + release."0.3.4".hash = "sha256:18mgycjgg829dbr7ps77z6lcj03h3dchjbj5iir0pybxby7gd45c"; + release."0.3.3".hash = "sha256:1m2mxcngj368vbdb8mlr91hsygl430spl7lgyn9qmn3jykack867"; + release."0.3.1".hash = "sha256:1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8"; + release."0.2.3".hash = "sha256:0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966"; defaultVersion = let @@ -32,6 +62,23 @@ let [ rocq-core.rocq-version mathcomp.version ] [ (case (range "9.0" "9.3") (range "2.4.0" "2.6.0") "1.16.0") + (case (range "8.20" "9.1") (range "2.4.0" "2.5.0") "1.14.0") + (case (range "8.20" "9.1") (range "2.1.0" "2.4.0") "1.13.0") + (case (range "8.20" "9.1") (range "2.1.0" "2.4.0") "1.12.0") + (case (range "8.19" "8.20") (range "2.1.0" "2.3.0") "1.9.0") + (case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "1.1.0") + (case (range "8.17" "8.19") (range "1.17.0" "1.19.0") "0.7.0") + (case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.7") + (case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.6") + (case (range "8.14" "8.18") (range "1.15.0" "1.17.0") "0.6.5") + (case (range "8.14" "8.18") (range "1.13.0" "1.16.0") "0.6.1") + (case (range "8.14" "8.18") (range "1.13" "1.15") "0.5.2") + (case (range "8.13" "8.15") (range "1.13" "1.14") "0.5.1") + (case (range "8.13" "8.15") (range "1.12" "1.14") "0.3.13") + (case (range "8.11" "8.14") (range "1.12" "1.13") "0.3.10") + (case (range "8.10" "8.12") "1.11.0" "0.3.3") + (case (range "8.10" "8.11") "1.11.0" "0.3.1") + (case (range "8.8" "8.11") (range "1.8" "1.10") "0.2.3") ] null; @@ -113,6 +160,8 @@ let cd ${pkgpath} ''; + useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLe "1.15.0" v; + meta = { description = "Analysis library compatible with Mathematical Components"; maintainers = [ lib.maintainers.cohencyril ]; @@ -121,7 +170,59 @@ let passthru = lib.mapAttrs (package: deps: mathcomp_ package) packages; }; + # split packages didn't exist before 0.6, so building nothing in that case + patched-derivation1 = derivation.overrideAttrs ( + o: + 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: + lib.optionalAttrs ( + o.pname != null + && o.pname == "mathcomp-analysis" + && o.version != null + && o.version != "dev" + && lib.versions.isLt "0.6" o.version + ) { preBuild = ""; } + ); + # only packages classical and analysis existed before 1.7, so building nothing in that case + patched-derivation3 = patched-derivation2.overrideAttrs ( + o: + lib.optionalAttrs + ( + o.pname != null + && o.pname != "mathcomp-classical" + && o.pname != "mathcomp-analysis" + && o.version != null + && o.version != "dev" + && lib.versions.isLt "1.7" o.version + ) + { + preBuild = ""; + buildPhase = "echo doing nothing"; + installPhase = "echo doing nothing"; + } + ); + patched-derivation = patched-derivation3.overrideAttrs ( + o: + lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "0.3.4" o.version)) + { + propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ]; + } + ); in - derivation; + patched-derivation; in mathcomp_ (if single then "single" else "analysis") diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index 24868a76ba33..b5af3ce604ee 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -168,7 +168,7 @@ let mathcomp-character = self.mathcomp.group-representation; mathcomp-abel = callPackage ../development/coq-modules/mathcomp-abel { }; mathcomp-algebra-tactics = callPackage ../development/coq-modules/mathcomp-algebra-tactics { }; - mathcomp-analysis = callPackage ../development/coq-modules/mathcomp-analysis { }; + mathcomp-analysis = callPackage ../development/rocq-modules/mathcomp-analysis { }; mathcomp-analysis-stdlib = self.mathcomp-analysis.analysis-stdlib; mathcomp-apery = callPackage ../development/coq-modules/mathcomp-apery { }; mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough { };