Generated nix CI

.gitattributes

@@ -1 +1,3 @@
+.git* export-ignore
+.nix export-ignore
 CHANGELOG_UNRELEASED.md merge=union

.github/workflows/nix-action.yml

@@ -0,0 +1,165 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+name: Nix CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  setup:
+    runs-on: ubuntu-latest
+    steps:
+    - name: Do nothing
+      run: echo "No setup, using meta.yml tasks"
+
+  "_deps":
+    runs-on: ubuntu-latest
+    needs:
+      - setup
+    strategy:
+      matrix:
+        task:
+          - "coq-8.13"
+          - "coq-8.12"
+          - "coq-8.11+multinomials"
+    steps:
+    - name: Cachix install
+      uses: cachix/install-nix-action@v12
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: coq
+    - name: Cachix setup math-comp
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: math-comp
+        authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+    - name: Git checkout
+      uses: actions/checkout@v2
+      with:
+        fetch-depth: 0
+    - name: Building/fetching current CI target
+      run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "_deps"
+
+  "mathcomp-analysis":
+    runs-on: ubuntu-latest
+    needs:
+      - setup
+      - "_deps"
+    strategy:
+      matrix:
+        task:
+          - "coq-8.13"
+          - "coq-8.12"
+          - "coq-8.11+multinomials"
+    steps:
+    - name: Cachix install
+      uses: cachix/install-nix-action@v12
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: coq
+    - name: Cachix setup math-comp
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: math-comp
+        authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+    - name: Git checkout
+      uses: actions/checkout@v2
+      with:
+        fetch-depth: 0
+    - name: Building/fetching previous target _deps
+      run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "_deps"
+    - name: Building/fetching current CI target
+      run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "mathcomp-analysis"
+
+  "multinomials":
+    runs-on: ubuntu-latest
+    needs:
+      - setup
+      - "_deps"
+    strategy:
+      matrix:
+        task:
+          - "coq-8.13"
+          - "coq-8.12"
+          - "coq-8.11+multinomials"
+    steps:
+    - name: Cachix install
+      uses: cachix/install-nix-action@v12
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: coq
+    - name: Cachix setup math-comp
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: math-comp
+        authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+    - name: Git checkout
+      uses: actions/checkout@v2
+      with:
+        fetch-depth: 0
+    - name: Building/fetching previous target _deps
+      run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "_deps"
+    - name: Building/fetching current CI target
+      run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "multinomials"
+
+  "_allJobs":
+    runs-on: ubuntu-latest
+    needs:
+      - setup
+      - "_deps"
+      - "multinomials"
+      - "mathcomp-analysis"
+    strategy:
+      matrix:
+        task:
+          - "coq-8.13"
+          - "coq-8.12"
+          - "coq-8.11+multinomials"
+    steps:
+    - name: Cachix install
+      uses: cachix/install-nix-action@v12
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: coq
+    - name: Cachix setup math-comp
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: math-comp
+        authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+    - name: Git checkout
+      uses: actions/checkout@v2
+      with:
+        fetch-depth: 0
+    - name: Building/fetching previous target _deps
+      run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "_deps"
+    - name: Building/fetching previous target multinomials
+      run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "multinomials"
+    - name: Building/fetching previous target mathcomp-analysis
+      run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "mathcomp-analysis"
+    - name: Building/fetching current CI target
+      run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "_allJobs"

.nix/coq-nix-toolbox.nix

@@ -0,0 +1,5 @@
+# This file was generated from meta.yml, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+# However, this rev was not handled by mustache, but by a special eval command
+# because you picked the option nix-default: ... in meta.yml
+"0ea896bc753c0770331911381d78b2fcdfa48c66"

.nix/coq-overlays/mathcomp-analysis/default.nix

@@ -0,0 +1,31 @@
+{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap,
+  mathcomp-bigenough, mathcomp-real-closed,
+  hierarchy-builder,
+  stdenv, lib, fetchFromGitHub, version ? null }:
+
+with lib; mkCoqDerivation {
+
+  prefix-list = [ "coq" "mathcomp" ];
+  pname = "analysis";
+  owner = "math-comp";
+
+  release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8";
+  release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
+
+  inherit version;
+  default-version = with versions; switch [ coq.version mathcomp.version ]  [
+      { cases = [ (range "8.10" "8.12~") "1.11.0" ]; out = "0.3.1"; }
+      { cases = [ (range "8.9"  "8.12~") "1.10.0" ]; out = "0.3.0"; }
+      { cases = [ (range "8.8"  "8.11~") (range "1.8.0" "1.11~") ];
+        out = "0.2.3"; }
+    ] null;
+
+  propagatedBuildInputs =
+    [ mathcomp.ssreflect mathcomp.field hierarchy-builder
+      mathcomp-finmap mathcomp-bigenough mathcomp-real-closed ];
+
+  meta = {
+    description = "Analysis library compatible with Mathematical Components";
+    license = licenses.cecill-c;
+  };
+}

.nix/fallback-config.nix

@@ -0,0 +1,62 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+# *However*, you may copy paste it to `config.nix`
+# in the same subdirectory .nix and extend it as needed.
+# Note that this would completely deactivate this file.
+
+{
+  ## DO NOT CHANGE THE format
+  format = "1.0.0";
+  ## unless you made an automated or manual update
+  ## to another supported format.
+
+  ## The attribute to build, either from nixpkgs
+  ## of from the overlays located in `.nix/coq-overlays`
+  attribute = "mathcomp-analysis";
+
+  ## If you want to select a different attribute
+  ## to serve as a basis for nix-shell edit this
+  # shell-attribute = "mathcomp-analysis";
+
+  ## Maybe the shortname of the library is different from
+  ## the name of the nixpkgs attribute, if so, set it here:
+  pname = "analysis";
+
+  ## Lists the dependencies, phrased in terms of nix attributes.
+  ## No need to list Coq, it is already included.
+  ## These dependencies will systematically be added to the currently
+  ## known dependencies, if any more than Coq.
+  ## /!\ Remove this field as soon as the package is available on nixpkgs.
+  ## /!\ Manual overlays in `.nix/coq-overlays` should be preferred then.
+  #buildInputs = [ ];
+
+  ## Indicate the relative location of your _CoqProject
+  ## If not specified, it defaults to "_CoqProject"
+  coqproject = "_CoqProject";
+
+  ## Select a task to build by default in the following `tasks` set
+  ## It will be used when typing nix-shell or nix-build without argument
+  ## defaults to "default"
+  default-task = "coq-8.13";
+  tasks."coq-8.13" = {};
+
+  tasks."coq-8.13" = {
+      coqPackages."coq".override.version = "8.13";
+      coqPackages."mathcomp".override.version = "1.12.0";
+      coqPackages."mathcomp".job = "_excluded";
+      coqPackages."mathcomp-real-closed".override.version = "1.1";
+      coqPackages."mathcomp-finmap".override.version = "1.5";
+      coqPackages."hierarchy-builder".override.version = "1.0.0";
+      coqPackages."coq-elpi".override.version = "1.9.3";
+  };
+  tasks."coq-8.12" = {
+      coqPackages."coq".override.version = "8.12";
+      coqPackages."mathcomp".override.version = "1.12.0";
+  };
+  tasks."coq-8.11+multinomials" = {
+      coqPackages."coq".override.version = "8.11";
+      coqPackages."mathcomp".override.version = "1.12.0";
+      coqPackages."multinomials".override.version = "1.5.4";
+  };
+}

.nix/nixpkgs.nix

@@ -0,0 +1,4 @@
+fetchTarball {
+    url = https://github.com/NixOS/nixpkgs/archive/0e1a8cc3ec6fd5844d30a24d99e44ad4a6971235.tar.gz;
+    sha256 = "1gsvr0h0rmc0vx0x9vabrcfdndl5kcd617i5wxy5r35nr68rbvaj";
+  }

README.md

@@ -5,10 +5,14 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 # Analysis library compatible with Mathematical Components
 
 [![Docker CI][docker-action-shield]][docker-action-link]
+[![Nix CI][nix-action-shield]][nix-action-link]
 [![Chat][chat-shield]][chat-link]
 
 [docker-action-shield]: https://github.com/math-comp/analysis/workflows/Docker%20CI/badge.svg?branch=master
 [docker-action-link]: https://github.com/math-comp/analysis/actions?query=workflow:"Docker%20CI"
+
+[nix-action-shield]: https://github.com/math-comp/analysis/workflows/Nix%20CI/badge.svg?branch=master
+[nix-action-link]: https://github.com/math-comp/analysis/actions?query=workflow:"Nix%20CI"
 [chat-shield]: https://img.shields.io/badge/zulip-join_chat-brightgreen.svg
 [chat-link]: https://coq.zulipchat.com/login/#narrow/stream/237666-math-comp-analysis
 

coq-nix-toolbox.nix

@@ -0,0 +1 @@
+"e54b920493f0494ede95b5f7d083cc8b20b1f5a6"