From f7e231ccdaaad267812708793138a3ec712120a6 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 10 Oct 2024 22:35:14 +0900 Subject: [PATCH] add dep to algebra-tactics in nix --- .github/workflows/nix-action-8.19.yml | 12 +++ .github/workflows/nix-action-8.20.yml | 12 +++ .github/workflows/nix-action-master.yml | 5 + .../mathcomp-analysis/default.nix | 93 +++++++++++++++++++ 4 files changed, 122 insertions(+) create mode 100644 .nix/coq-overlays/mathcomp-analysis/default.nix diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml index 3cce5d97e..0a8341cfa 100644 --- a/.github/workflows/nix-action-8.19.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -186,6 +186,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra-tactics' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-algebra-tactics" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr @@ -250,6 +254,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-finmap' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "mathcomp-finmap" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "hierarchy-builder" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr @@ -258,6 +266,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra-tactics' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-algebra-tactics" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr diff --git a/.github/workflows/nix-action-8.20.yml b/.github/workflows/nix-action-8.20.yml index eb81d5274..44b5a7783 100644 --- a/.github/workflows/nix-action-8.20.yml +++ b/.github/workflows/nix-action-8.20.yml @@ -186,6 +186,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra-tactics' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp-algebra-tactics" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr @@ -250,6 +254,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-finmap' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr job "mathcomp-finmap" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "hierarchy-builder" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr @@ -258,6 +266,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra-tactics' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp-algebra-tactics" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr diff --git a/.github/workflows/nix-action-master.yml b/.github/workflows/nix-action-master.yml index 327cb360a..41563f1e1 100644 --- a/.github/workflows/nix-action-master.yml +++ b/.github/workflows/nix-action-master.yml @@ -310,6 +310,7 @@ jobs: needs: - coq - mathcomp-finmap + - hierarchy-builder - mathcomp-bigenough - hierarchy-builder runs-on: ubuntu-latest @@ -365,6 +366,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-finmap' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "mathcomp-finmap" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" diff --git a/.nix/coq-overlays/mathcomp-analysis/default.nix b/.nix/coq-overlays/mathcomp-analysis/default.nix new file mode 100644 index 000000000..4e527a820 --- /dev/null +++ b/.nix/coq-overlays/mathcomp-analysis/default.nix @@ -0,0 +1,93 @@ +{ lib, + mkCoqDerivation, recurseIntoAttrs, + mathcomp, mathcomp-finmap, mathcomp-bigenough, + hierarchy-builder, mathcomp-algebra-tactics, + single ? false, + coqPackages, coq, version ? null }@args: +with builtins // lib; +let + repo = "analysis"; + owner = "math-comp"; + + release."0.6.1".sha256 = "sha256-1VyNXu11/pDMuH4DmFYSUF/qZ4Bo+/Zl3Y0JkyrH/r0="; + release."0.6.0".sha256 = "sha256-0msICcIrK6jbOSiBu0gIVU3RHwoEEvB88CMQqW/06rg="; + release."0.5.3".sha256 = "sha256-1NjFsi5TITF8ZWx1NyppRmi8g6YaoUtTdS9bU/sUe5k="; + release."0.5.2".sha256 = "0yx5p9zyl8jv1vg7rgkyq8dqzkdnkqv969mi62whmhkvxbavgzbw"; + release."0.5.1".sha256 = "1hnzqb1gxf88wgj2n1b0f2xm6sxg9j0735zdsv6j12hlvx5lwk68"; + release."0.3.13".sha256 = "sha256-Yaztew79KWRC933kGFOAUIIoqukaZOdNOdw4XszR1Hg="; + release."0.3.10".sha256 = "sha256-FBH2c8QRibq5Ycw/ieB8mZl0fDiPrYdIzZ6W/A3pIhI="; + release."0.3.9".sha256 = "sha256-uUU9diBwUqBrNRLiDc0kz0CGkwTZCUmigPwLbpDOeg4="; + release."0.3.6".sha256 = "0g2j7b2hca4byz62ssgg90bkbc8wwp7xkb2d3225bbvihi92b4c5"; + release."0.3.4".sha256 = "18mgycjgg829dbr7ps77z6lcj03h3dchjbj5iir0pybxby7gd45c"; + release."0.3.3".sha256 = "1m2mxcngj368vbdb8mlr91hsygl430spl7lgyn9qmn3jykack867"; + release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8"; + release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966"; + + defaultVersion = with versions; lib.switch [ coq.version mathcomp.version ] [ + { cases = [ (isGe "8.14") (isGe "1.13.0") ]; out = "0.6.1"; } + { cases = [ (isGe "8.14") (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.11" "8.12") "1.11.0" ]; out = "0.3.4"; } + { 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 + packages = [ "classical" "analysis" ]; + + mathcomp_ = package: let + classical-deps = [ mathcomp.algebra mathcomp-finmap hierarchy-builder ]; + analysis-deps = [ mathcomp.field mathcomp-bigenough ]; + intra-deps = if package == "single" then [] + else map mathcomp_ (head (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" + else "mathcomp-${package}"; + derivation = mkCoqDerivation ({ + inherit version pname defaultVersion release repo owner; + + namePrefix = [ "coq" "mathcomp" ]; + + propagatedBuildInputs = + intra-deps + ++ optionals (elem package [ "classical" "single" ]) classical-deps + ++ optionals (elem package [ "analysis" "single" ]) analysis-deps + ++ optionals (elem package [ "analysis" "single" ]) [mathcomp-algebra-tactics]; + + preBuild = '' + cd ${pkgpath} + ''; + + meta = { + description = "Analysis library compatible with Mathematical Components"; + maintainers = [ maintainers.cohencyril ]; + license = licenses.cecill-c; + }; + + passthru = 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) + { 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) + { preBuild = ""; } + ); + patched-derivation = patched-derivation2.overrideAttrs (o: + optionalAttrs (o.version != null + && (o.version == "dev" || versions.isGe "0.3.4" o.version)) + { + propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ]; + } + ); + in patched-derivation; +in +mathcomp_ (if single then "single" else "analysis")