update meta.yml

.gitattributes

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

.github/workflows/docker-action.yml

@@ -20,9 +20,10 @@ jobs:
           - 'mathcomp/mathcomp:1.12.0-coq-8.11'
           - 'mathcomp/mathcomp:1.12.0-coq-8.12'
           - 'mathcomp/mathcomp:1.12.0-coq-8.13'
+          - 'mathcomp/mathcomp:1.12.0-coq-dev'
           - 'mathcomp/mathcomp-dev:coq-8.11'
           - 'mathcomp/mathcomp-dev:coq-8.12'
-          - 'mathcomp/mathcomp-dev:coq-8.13'
+          - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

.github/workflows/nix-action.yml

@@ -0,0 +1,115 @@
+# 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-matrix:
+    runs-on: ubuntu-latest
+    outputs:
+      matrix: ${{ steps.set-matrix.outputs.matrix }}
+    steps:
+    - name: Cachix install
+      uses: cachix/install-nix-action@v12
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Git checkout
+      uses: actions/checkout@v2
+    - name: Print matrix
+      id: set-matrix
+      run: |
+        matrix=$(nix-shell --arg do-nothing true --run nixInputs)
+        echo ::set-output name=matrix::{\"input\":$(echo $matrix)}\"
+
+  dependencies:
+    runs-on: ubuntu-latest
+    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
+        signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
+    - name: Git checkout
+      uses: actions/checkout@v2
+    - name: Building/fetching dependencies
+      run: nix-build --argstr ci-step dependencies
+
+  main:
+    runs-on: ubuntu-latest
+    needs:
+    - dependencies
+    - setup-matrix
+    strategy:
+      matrix: ${{fromJson(needs.setup-matrix.outputs.matrix)}}
+    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
+        signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
+    - name: Git checkout
+      uses: actions/checkout@v2
+    - name: Building/fetching dependencies
+      run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-step dependencies
+    - name: Building/fetching current project
+      run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-step main
+
+  all:
+    runs-on: ubuntu-latest
+    needs:
+    - dependencies
+    - setup-matrix
+    - main
+    strategy:
+      matrix: ${{fromJson(needs.setup-matrix.outputs.matrix)}}
+    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
+        signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
+    - name: Git checkout
+      uses: actions/checkout@v2
+    - name: Building/fetching dependencies
+      run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-step dependencies
+    - name: Building/fetching current project
+      run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-step main
+    - name: Building/fetching current project
+      run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-step all

.nix/config.nix

@@ -0,0 +1,22 @@
+{
+  format = "1.0.0";
+  coq-attribute = "mathcomp-analysis";
+  pname = "analysis";
+  namespace = "mathcomp.analysis";
+  realpath = "theories";
+  select = "coq-8.13";
+  inputs."coq-8.13".coqPackages = {
+    coq.override.version = "8.13";
+    mathcomp.override.version = "1.12.0";
+    mathcomp-real-closed.override.version = "1.1";
+    mathcomp-finmap.override.version = "1.5";
+    hierarchy-builder.override.version = "1.0.0";
+    coq-elpi.override.version = "1.8.1"; };
+  inputs."coq-8.12".coqPackages = {
+    coq.override.version = "8.12";
+    mathcomp.override.version = "1.12.0"; };
+  inputs."coq-8.11+multinomials".coqPackages = {
+    coq.override.version = "8.11";
+    mathcomp.override.version = "1.12.0";
+    multinomials.ci = "all"; };
+}

.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/coq-overlays/multinomials/default.nix

@@ -0,0 +1,34 @@
+{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough,
+  lib, version ? null }:
+with lib; mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "multinomials";
+  owner = "math-comp";
+  inherit version;
+  defaultVersion =  with versions; switch [ coq.version mathcomp.version ] [
+      { cases = [ (range "8.7" "8.13")  "1.11.0" ];             out = "1.5.2"; }
+      { cases = [ (range "8.7" "8.11")  (range "1.8" "1.10") ]; out = "1.5.0"; }
+      { cases = [ (range "8.7" "8.10")  (range "1.8" "1.10") ]; out = "1.4"; }
+      { cases = [ "8.6"                 (range "1.6" "1.7") ];  out = "1.1"; }
+    ] null;
+  release = {
+    "1.5.2".sha256 = "15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s";
+    "1.5.1".sha256 = "13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3";
+    "1.5.0".sha256 = "064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw";
+    "1.5.0".rev    = "1.5";
+    "1.4".sha256   = "0vnkirs8iqsv8s59yx1fvg1nkwnzydl42z3scya1xp1b48qkgn0p";
+    "1.3".sha256   = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4";
+    "1.2".sha256   = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq";
+    "1.1".sha256   = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s";
+    "1.0".sha256   = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
+  };
+
+  propagatedBuildInputs =
+    [ mathcomp.ssreflect mathcomp.algebra mathcomp-finmap mathcomp-bigenough ];
+
+  meta = {
+    description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
+    license = licenses.cecill-c;
+  };
+}

.nix/nixpkgs.nix

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

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