diff --git a/.gitattributes b/.gitattributes
index 035f68b71..ef19d53db 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -1 +1,3 @@
+.git* export-ignore
+.nix export-ignore
 CHANGELOG_UNRELEASED.md merge=union
\ No newline at end of file
diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
deleted file mode 100644
index e57449e75..000000000
--- a/.github/workflows/coq-action.yml
+++ /dev/null
@@ -1,30 +0,0 @@
-name: CI
-
-on:
-  push:
-    branches:
-      - master
-  pull_request:
-    branches:
-      - '**'
-
-jobs:
-  build:
-    # the OS must be GNU/Linux to be able to use the docker-coq-action
-    runs-on: ubuntu-latest
-    strategy:
-      matrix:
-        image:
-          - 'mathcomp/mathcomp:1.12.0-coq-8.11'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.12'
-      fail-fast: false
-    steps:
-      - uses: actions/checkout@v2
-      - uses: coq-community/docker-coq-action@v1
-        with:
-          opam_file: 'coq-mathcomp-analysis.opam'
-          custom_image: ${{ matrix.image }}
-
-# See also:
-# https://github.com/coq-community/docker-coq-action#readme
-# https://github.com/erikmd/docker-coq-github-action-demo
diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml
new file mode 100644
index 000000000..0d7a0843f
--- /dev/null
+++ b/.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"
diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml
deleted file mode 100644
index fa42fead9..000000000
--- a/.github/workflows/nix.yml
+++ /dev/null
@@ -1,18 +0,0 @@
-name: Cachix
-on:
-  push:
-jobs:
-  cachix:
-    name: Cachix branch
-    runs-on: ubuntu-latest
-    steps:
-    - uses: cachix/install-nix-action@v12
-    - uses: cachix/cachix-action@v8
-      with:
-        # Name of a cachix cache to push and pull/substitute
-        name:  math-comp
-        # Authentication token for Cachix, needed only for private cache access
-        authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
-    - uses: actions/checkout@v2
-    - run: nix-build
-    # - run: export CACHIX_SIGNING_KEY=${{ secrets.CACHIX_SIGNING_KEY }} cachix push math-comp result
diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix
new file mode 100644
index 000000000..632ecf6e3
--- /dev/null
+++ b/.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"
diff --git a/.nix/coq-overlays/mathcomp-analysis/default.nix b/.nix/coq-overlays/mathcomp-analysis/default.nix
new file mode 100644
index 000000000..a3170a899
--- /dev/null
+++ b/.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;
+  };
+}
diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix
new file mode 100644
index 000000000..e10c47339
--- /dev/null
+++ b/.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";
+  };
+}
diff --git a/.nix/nixpkgs.nix b/.nix/nixpkgs.nix
new file mode 100644
index 000000000..197902d24
--- /dev/null
+++ b/.nix/nixpkgs.nix
@@ -0,0 +1,4 @@
+fetchTarball {
+    url = https://github.com/NixOS/nixpkgs/archive/0e1a8cc3ec6fd5844d30a24d99e44ad4a6971235.tar.gz;
+    sha256 = "1gsvr0h0rmc0vx0x9vabrcfdndl5kcd617i5wxy5r35nr68rbvaj";
+  }
diff --git a/README.md b/README.md
index cc08603c0..a1233288d 100644
--- a/README.md
+++ b/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
 
diff --git a/config.nix b/config.nix
deleted file mode 100644
index 1daa16d79..000000000
--- a/config.nix
+++ /dev/null
@@ -1,6 +0,0 @@
-{
-  coq = "8.11";
-  mathcomp = "mathcomp-1.12.0";
-  mathcomp-real-closed = "1.1.2";
-  mathcomp-finmap = "1.5.1";
-}
diff --git a/coq-nix-toolbox.nix b/coq-nix-toolbox.nix
new file mode 100644
index 000000000..ba2d94364
--- /dev/null
+++ b/coq-nix-toolbox.nix
@@ -0,0 +1 @@
+"e54b920493f0494ede95b5f7d083cc8b20b1f5a6"
diff --git a/default.nix b/default.nix
index 1f6bda078..446181f1a 100644
--- a/default.nix
+++ b/default.nix
@@ -1,149 +1,16 @@
-{
-  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;
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+{ config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false,
+  update-nixpkgs ? false, ci-matrix ? false,
+  override ? {}, ocaml-override ? {}, global-override ? {},
+  task ? null, job ? null, inNixShell ? null, src ? ./.,
+}@args:
 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_11;
-      }.${(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 // (
-                      if elem version [ "master" "cauchy_etoile" "holomorphy" ]
-                      then {
-                        propagatedBuildInputs = mca.propagatedBuildInputs ++
-                                                [ coqPackages.mathcomp-real-closed coqPackages.hierarchy-builder ];
-                      } else {
-                        propagatedBuildInputs = mca.propagatedBuildInputs ++
-                                                (with coqPackages; [ coq-elpi hierarchy-builder ]);
-                      });
-                };
-                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"]
-              );
-            };
-          };
-        })];
+  auto = fetchGit {
+    url = "https://github.com/coq-community/coq-nix-toolbox.git";
+    ref = "simplify_allJobs";
+    rev = import ./.nix/coq-nix-toolbox.nix;
   };
-
-  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);
 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;
+(import auto ({inherit src;} // args)).nix-auto
 
-}) else pkg
diff --git a/index.md b/index.md
new file mode 100644
index 000000000..95b589783
--- /dev/null
+++ b/index.md
@@ -0,0 +1,54 @@
+---
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+title: Analysis library compatible with Mathematical Components
+lang: en
+header-includes:
+  - |
+    <style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>
+    <style type="text/css"> h1 {margin-left: 0em; padding: 0px; text-align: center} </style>
+    <style type="text/css"> h2 {margin-left: 0em; padding: 0px; color: #580909} </style>
+    <style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>
+    <style type="text/css"> body { width: 1100px; margin-left: 30px; }</style>
+---
+
+<div style="text-align:left"><img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px">
+<a href="https://github.com/math-comp/analysis">View the project on GitHub</a>
+<img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px"></div>
+
+## About
+
+Welcome to the Analysis library compatible with Mathematical Components project website!
+
+This repository contains an experimental library for real analysis for
+the Coq proof-assistant and using the Mathematical Components library.
+
+This is an open source project, licensed under the CeCILL-C.
+
+## Get the code
+
+The current stable release of Analysis library compatible with Mathematical Components can be [downloaded from GitHub](https://github.com/math-comp/analysis/releases).
+
+## Documentation
+
+
+Related publications, if any, are listed below.
+
+- [Formalization Techniques for Asymptotic Reasoning in Classical Analysis](https://jfr.unibo.it/article/view/8124) doi:[10.6092/issn.1972-5787/8124](https://doi.org/10.6092/issn.1972-5787/8124)
+- [Competing inheritance paths in dependent type theory---a case study in functional analysis](https://hal.inria.fr/hal-02463336) doi:[10.1007/978-3-030-51054-1_1](https://doi.org/10.1007/978-3-030-51054-1_1)
+- [Formalisation Tools for Classical Analysis](http://www-sop.inria.fr/members/Damien.Rouhling/data/phd/thesis.pdf) 
+
+## Help and contact
+
+- Report issues on [GitHub](https://github.com/math-comp/analysis/issues)
+
+## Authors and contributors
+
+- Reynald Affeldt
+- Cyril Cohen
+- Marie Kerjean
+- Assia Mahboubi
+- Damien Rouhling
+- Kazuhiko Sakaguchi
+- Pierre-Yves Strub
+
diff --git a/meta.yml b/meta.yml
index 2e286e9ac..e317c36ec 100644
--- a/meta.yml
+++ b/meta.yml
@@ -2,10 +2,66 @@ fullname: Analysis library compatible with Mathematical Components
 shortname: analysis
 organization: math-comp
 opam_name: coq-mathcomp-analysis
+nix_name: mathcomp-analysis
 community: false
 action: true
 coqdoc: false
 
+nix: true
+nix-default:
+  ref: simplify_allJobs
+
+cachix:
+- name: coq
+- name: math-comp
+  token: CACHIX_AUTH_TOKEN
+
+nix-jobs:
+- job: _deps
+- job: mathcomp-analysis
+  needs:
+    - _deps
+- job: multinomials
+  needs:
+    - _deps
+- job: _allJobs
+  needs:
+    - _deps
+    - multinomials
+    - mathcomp-analysis
+
+nix-default-task: coq-8.13
+nix-tasks:
+- task: coq-8.13
+  packages:
+    - name: coq
+      version: 8.13
+    - name: mathcomp
+      version: 1.12.0
+      job: _excluded
+    - name: mathcomp-real-closed
+      version: 1.1
+    - name: mathcomp-finmap
+      version: 1.5
+    - name: hierarchy-builder
+      version: 1.0.0
+    - name: coq-elpi
+      version: 1.9.3
+- task: coq-8.12
+  packages:
+    - name: coq
+      version: 8.12
+    - name: mathcomp
+      version: 1.12.0
+- task: coq-8.11+multinomials
+  packages:
+    - name: coq
+      version: 8.11
+    - name: mathcomp
+      version: 1.12.0
+    - name: multinomials
+      version: 1.5.4
+
 synopsis: >-
   An analysis library for mathematical components
 description: |-
@@ -103,7 +159,7 @@ keywords:
 publications:
 - pub_url: https://jfr.unibo.it/article/view/8124
   pub_title:  Formalization Techniques for Asymptotic Reasoning in Classical Analysis
-  pub_doi: 10.6092/issn.1972-5787/8124 
+  pub_doi: 10.6092/issn.1972-5787/8124
 - pub_url: https://hal.inria.fr/hal-02463336
   pub_title: Competing inheritance paths in dependent type theory---a case study in functional analysis
   pub_doi: 10.1007/978-3-030-51054-1_1
@@ -112,7 +168,7 @@ publications:
 
 documentation: |-
   ## Disclaimer
- 
+
   This library is still at an experimental stage.  Contents may
   change, definitions and theorems may be renamed, and inference
   mechanisms may be replaced at any major version bump.  Use at your
@@ -124,7 +180,7 @@ documentation: |-
 
   Changes are documented in [CHANGELOG.md](CHANGELOG.md) and
   [CHANGELOG_UNRELEASED.md](CHANGELOG_UNRELEASED.md).
-  
+
   Overview presentation: [Classical Analysis with Coq](https://perso.crans.org/cohen/CoqWS2018.pdf) (2018)
 
   Other work using MathComp-Analysis: [A Formal Classical Proof of Hahn-Banach in Coq](https://lipn.univ-paris13.fr/~kerjean/slides/slidesTYPES19.pdf) (2019)
diff --git a/package.nix b/package.nix
index e8e708431..f5b0de146 100644
--- a/package.nix
+++ b/package.nix
@@ -1 +1,36 @@
-"mathcomp-analysis"
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to
+# regenerate.
+{
+  config-file ? ./.nix/config.nix,
+  config ? {},
+  withEmacs ? false,
+  print-env ? false,
+  do-nothing ? false,
+  update-nixpkgs ? false,
+  ci ? false,
+}@args:
+let do-nothing = (args.do-nothing or false) || update-nixpkgs; in
+with builtins;
+let result = (import ./.nix/auto-config.nix {inherit config config-file;}); in
+with result;
+with selected-instance.pkgs.coqPackages.lib;
+if trivial.inNixShell then
+  with selected-instance; this-pkg.overrideAttrs (old: {
+    inherit json_input;
+    shellHook = result.shellHook
+      + optionalString print-env "nixEnv"
+      + optionalString update-nixpkgs "updateNixPkgs";
+    currentdir = "./.";
+    coq_version = pkgs.coqPackages.coq.coq-version;
+    inherit (result.config) nixpkgs logpath realpath;
+
+    buildInputs = optionals (!do-nothing)
+      (old.buildInputs or [] ++ optional withEmacs pkgs.emacs);
+
+    propagatedBuildInputs = optionals (!do-nothing)
+      (old.propagatedBuildInputs or []);
+  })
+else
+  if ci then map (b: b.ci-coqpkgs) instances
+  else selected-instance.this-pkg