diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml index de429af..f8f7287 100644 --- a/.github/workflows/nix.yml +++ b/.github/workflows/nix.yml @@ -1,32 +1,66 @@ name: Cachix on: - push: + pull_request: + branches: + - master + - v2 jobs: - cachix: - name: Cachix branch + setup: + name: Computing matrix of tested versions runs-on: ubuntu-latest + outputs: + matrix: ${{ steps.set-matrix.outputs.matrix }} + steps: + - name: Checkout + uses: actions/checkout@v2.1.1 + - uses: cachix/install-nix-action@v12 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Setup build matrix + id: set-matrix + run: "echo ::set-output name=matrix::$(./ci-matrix.sh)" + + builds: + name: Build mathcomp and coq combination + runs-on: ubuntu-latest + needs: setup strategy: fail-fast: false - matrix: - mc: [ "1.11.0", "1.10.0", "1.9.0", "1.8.0" ] - coq: [ "8.12", "8.11", "8.10", "8.9", "8.8", "8.7" ] - exclude: - - mc: "1.8.0" - coq: "8.10" - - mc: "1.8.0" - coq: "8.11" - - mc: "1.9.0" - coq: "8.11" - - mc: "1.8.0" - coq: "8.12" - - mc: "1.9.0" - coq: "8.12" - - mc: "1.10.0" - coq: "8.12" + matrix: ${{fromJson(needs.setup.outputs.matrix)}} steps: + - uses: cachix/install-nix-action@v12 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - uses: cachix/cachix-action@v8 + with: + # Name of a cachix cache to push and pull/substitute + name: math-comp + extraPullNames: coq + # Authentication token for Cachix, needed only for private cache access + authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' - name: Checkout uses: actions/checkout@v2.1.1 + - name: Building mathcomp-full-shell target if required + run: | + overrides="{coq = \"${{ matrix.coq }}\"; mathcomp = \"${{ matrix.mc }}\";}" + storepath=$(nix eval "(\"\${import ./. {override = $overrides;}}\")") + hash=$(echo $storepath | sed "s/\"//mg" | xargs basename | cut -d- -f1) + url=https://math-comp.cachix.org/$hash.narinfo + if curl --output /dev/null --silent --head --fail "$url"; then + echo "In cache: $url, doing nothing" + else + echo "Not in cache, compiling" + nix-build --no-out-link --arg override "$overrides" + fi + + summary: + name: Generate summary + runs-on: ubuntu-latest + needs: builds + steps: - uses: cachix/install-nix-action@v12 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable - uses: cachix/cachix-action@v8 with: # Name of a cachix cache to push and pull/substitute @@ -34,5 +68,15 @@ jobs: extraPullNames: coq # Authentication token for Cachix, needed only for private cache access authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' - # building fake mathcomp-fast target - - run: nix-build --arg config '{coq = "${{ matrix.coq }}"; mathcomp = "${{ matrix.mc }}";}' + ## does not work because the PR is updated only once + - name: Checkout + uses: actions/checkout@v2.1.1 + - name: Update README.md + id: set-nixenv + run: | + ./update-readme.sh + - name: Commit README.md + uses: EndBug/add-and-commit@v7 + with: + message: 'Updating README.md' + add: 'README.md' diff --git a/README_TEMPLATE.md b/README_TEMPLATE.md new file mode 100644 index 0000000..a6646ec --- /dev/null +++ b/README_TEMPLATE.md @@ -0,0 +1,37 @@ +# Nix support, build and caching for mathcomp packages + +![Cachix](https://github.com/math-comp/math-comp-nix/workflows/Cachix/badge.svg) + +This caches the builds needed to call +``` +nix-shell https://github.com/math-comp/math-comp-nix/archive/v2.tar.gz + +``` + +Which can also be called (with some delays in updates) +``` +nix-shell https://math-comp.github.io/nix +``` + +See [Mathcomp on nix Wiki page](https://github.com/math-comp/math-comp/wiki/Using-nix) for a short manual. + +## Summary + +Here is a synthesis of all available mathcomp packages. + +If a mathcomp-coq combination is missing, please add it to the `mc-coq-set` attribute in the file [`matrix/default.nix`](https://github.com/math-comp/math-comp-nix/blob/v2/mstrix/default.nix). + +If some mathcomp extra package is missing, there might be two reasons: +- Either the (upadate of the) package has not been pushed on [NixOS/nixpkgs](https://github.com/NixOS/nixpkgs). + If that's the case you can either + + open a pull request to add it, or + + open an issue and tag @CohenCyril to prompt for the addition of the package. +- Or the nixpkgs commit has not been updated in https://github.com/coq-nix-toolbox/. + In which case, you should go there and run `nix-shell --arg update-nixpkgs true`, commit and push **there**. + + This command is also applicable in the current directory but is strongly discouraged + outside of development purpose, since it would desynchronize the nixpkgs versions at use + between https://github.com/coq-nix-toolbox/ and https://math-comp.github.io/nix. + + It can take some time for a package pushed to NixOS/nixpkgs to reach the unstable branch. + If you are too impatient you can run `nix-shell --arg do-nothing true --run updateNixpkgsMaster` + **on your own projects**. + diff --git a/ci-matrix.sh b/ci-matrix.sh new file mode 100755 index 0000000..b4dbd4c --- /dev/null +++ b/ci-matrix.sh @@ -0,0 +1,3 @@ +#!/usr/bin/env bash + +cat $(nix-build --no-build-output matrix) \ No newline at end of file diff --git a/default.nix b/default.nix index 9c4336c..71c3300 100644 --- a/default.nix +++ b/default.nix @@ -1,144 +1,20 @@ -{ - 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 auto = fetchGit { + url = "https://github.com/coq-community/nix-toolbox.git"; + ref = "master"; + rev = "b1e5c52bdc1d79b7cd220476ebd9bc552a2331c7"; +}; 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 auto ( + { src = ./shells; + config = { + coq-attribute = if core then "mathcomp-core-shell" + else "mathcomp-full-shell"; + + }; + } // removeAttrs args ["core"])).nix-auto diff --git a/matrix/default.nix b/matrix/default.nix new file mode 100644 index 0000000..7d5bbc9 --- /dev/null +++ b/matrix/default.nix @@ -0,0 +1,36 @@ +{ run ? null }: +with import {}; with builtins; with lib; +let + old-coq = [ "8.9" "8.8" "8.7" ]; + mc-coq-set = { + "1.12.0" = [ "8.13" "8.12" "8.11" "8.10" ]; + "1.11.0" = [ "8.12" "8.11" "8.10" ] ++ old-coq; + "1.10.0" = [ "8.11" "8.10" ] ++ old-coq; + "1.9.0" = [ "8.10" ] ++ old-coq; + "1.8.0" = old-coq; + }; + + mcs = sort versionAtLeast (attrNames mc-coq-set); + pairs = mc: map (coq: { inherit mc coq; }) + (sort versionAtLeast mc-coq-set.${mc}); + matrix.include = flatten (map pairs mcs); + + # Generating an expanded script + coq-loop = coq: '' + export coq="${coq}" + '' + run + "\n"; + mc-loop = mc: '' + export mc="${mc}" + '' + foldl (sh: coq: sh + coq-loop coq) "" mc-coq-set.${mc}; +in + +if !isString run then + writeTextFile { + name = "JSONMatrix"; + text = toJSON matrix; + } +else +writeScriptBin "run" ('' + #!/usr/bin/env bash + '' + foldl (sh: mc: sh + mc-loop mc) "" mcs) + diff --git a/matrix/report.sh b/matrix/report.sh new file mode 100755 index 0000000..fe0b414 --- /dev/null +++ b/matrix/report.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +echo "### Mathematical Components $mc and Coq $coq" +nix-shell ./. --arg override "{coq = \"$coq\"; mathcomp = \"$mc\";}" --run ppNixEnv \ No newline at end of file diff --git a/shells/.nix/coq-overlays/mathcomp-core-shell/default.nix b/shells/.nix/coq-overlays/mathcomp-core-shell/default.nix new file mode 100644 index 0000000..e06ac66 --- /dev/null +++ b/shells/.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/shells/.nix/coq-overlays/mathcomp-full-shell/default.nix b/shells/.nix/coq-overlays/mathcomp-full-shell/default.nix new file mode 100644 index 0000000..7e5ee01 --- /dev/null +++ b/shells/.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 = with builtins; filter (x: !(x.meta.broken or false)) + (attrValues (removeAttrs args ["stdenv" "version"])); + src = version; +} diff --git a/Makefile b/shells/Makefile similarity index 72% rename from Makefile rename to shells/Makefile index d211b79..9d96754 100644 --- a/Makefile +++ b/shells/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/Makefile.coq b/shells/Makefile.coq similarity index 100% rename from Makefile.coq rename to shells/Makefile.coq diff --git a/update-readme.sh b/update-readme.sh new file mode 100755 index 0000000..2407efc --- /dev/null +++ b/update-readme.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +cat README_TEMPLATE.md > README.md +$(nix-build matrix --no-build-output --argstr run "bash matrix/report.sh")/bin/run >> README.md \ No newline at end of file