diff options
| -rw-r--r-- | .github/workflows/nix.yml | 30 | ||||
| -rw-r--r-- | config.nix | 3 | ||||
| -rw-r--r-- | default.nix | 70 | ||||
| -rw-r--r-- | package.nix | 1 |
4 files changed, 86 insertions, 18 deletions
diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml new file mode 100644 index 0000000..bd399a8 --- /dev/null +++ b/.github/workflows/nix.yml @@ -0,0 +1,30 @@ +name: Cachix +on: + push: +jobs: + cachix: + name: Cachix branch + runs-on: ubuntu-latest + strategy: + fail-fast: false + matrix: + coq: [ "8.11", "8.10", "8.9", "8.8", "8.7" ] + steps: + - name: Get branch shortname + run: echo "##[set-output name=branch;]$(echo ${GITHUB_REF#refs/heads/})" + id: branch-short-name + - name: Get repo name + run: echo "##[set-output name=repo;]$(echo $GITHUB_REPOSITORY | cut -d/ -f1)" + id: repo-name + - name: Get repo lowercase name + run: echo "##[set-output name=repo;]$(echo $GITHUB_REPOSITORY | cut -d/ -f1 | tr '[:upper:]' '[:lower:]')" + id: repo-lowercase-name + - uses: cachix/install-nix-action@v8 + - uses: cachix/cachix-action@v6 + with: + # Name of a cachix cache to push and pull/substitute + name: ${{ steps.repo-lowercase-name.outputs.repo }} + # Authentication token for Cachix, needed only for private cache access + signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}' + # building fake mathcomp-fast target + - run: nix-build https://github.com/math-comp/math-comp-nix/archive/master.tar.gz --arg config '{coq = "${{ matrix.coq }}"; mathcomp = "${{ steps.repo-name.outputs.repo }}/${{ steps.branch-short-name.outputs.branch }}";}' --argstr package mathcomp diff --git a/config.nix b/config.nix new file mode 100644 index 0000000..7660dde --- /dev/null +++ b/config.nix @@ -0,0 +1,3 @@ +{ + coq = "8.10"; +} diff --git a/default.nix b/default.nix index 1ab1783..82542c8 100644 --- a/default.nix +++ b/default.nix @@ -1,15 +1,19 @@ { - nixpkgs ? (fetchTarball https://github.com/CohenCyril/nixpkgs/archive/mathcomp-1.11.tar.gz), - config ? (pkgs: {}), + nixpkgs ? (if builtins.pathExists ./nixpkgs.nix then import ./nixpkgs.nix + else fetchTarball https://github.com/CohenCyril/nixpkgs/archive/mathcomp-fix-rec.tar.gz), + config ? (if builtins.pathExists ./config.nix then import ./config.nix else {}), withEmacs ? false, print-env ? false, - package ? "mathcomp.single" + 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); - pkgs = import nixpkgs { - config.packageOverrides = pkgs: with pkgs.lib; + 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; @@ -18,32 +22,59 @@ let "8.11" = coqPackages_8_11; "default" = coqPackages_8_10; }.${(cfg-fun pkgs).coq or "default"}.overrideScope' - (self: super: + (coqPackages: super-coqPackages: let - all-pkgs = pkgs // { coqPackages = self; }; - cfg = { ${if package == "mathcomp.single" then "mathcomp" else package} = ./.; } // { + all-pkgs = pkgs // { inherit coqPackages; }; + cfg = pkg-src // { mathcomp-fast = { src = ./.; - propagatedBuildInputs = with self; ([ mathcomp ] ++ mathcomp-extra-fast); + propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-fast); }; mathcomp-full = { src = ./.; - propagatedBuildInputs = with self; ([ mathcomp ] ++ mathcomp-extra-all); + propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-all); }; } // (cfg-fun all-pkgs); in { - # mathcomp-extra-config = lib.recursiveUpdate super.mathcomp-extra-config { - # for-coq-and-mc.${self.coq.coq-version}.${self.mathcomp.version} = - # removeAttrs cfg ["mathcomp" "coq"]; - # }; - mathcomp = if cfg?mathcomp then self.mathcomp_ cfg.mathcomp else super.mathcomp; + 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 // ( + if elem version [ "master" "cauchy_etoile" "holomorphy" ] + then { + propagatedBuildInputs = mca.propagatedBuildInputs ++ + [coqPackages.mathcomp-real-closed]; + } 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 = ./.; @@ -57,10 +88,13 @@ let 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" - for x in $buildInputs; do printf " "; echo $x | cachix push math-comp; done - for x in $propagatedBuildInputs; do printf " "; echo $x | cachix push math-comp; done + printEnv | cachix push math-comp } nixDefault () { cat $mathcompnix/default.nix diff --git a/package.nix b/package.nix new file mode 100644 index 0000000..661824d --- /dev/null +++ b/package.nix @@ -0,0 +1 @@ +"mathcomp.single" |