New nix infrastructure

.nix/auto-config.nix

@@ -0,0 +1,149 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+# this config parser reads a config file with its format attributes
+# (or default to the last available format)
+prefix:
+with builtins;
+let
+  optionalImport = f: d:
+    if (isPath f || isString f) && pathExists f then import f else d;
+  get-path = f: let local = prefix + "/.nix/${f}"; in
+    if pathExists local then local else ./. + "/${f}";
+in
+{
+  config-file ? get-path "config.nix",
+  fallback-file ? get-path "fallback-config.nix",
+  nixpkgs-file ? get-path "nixpkgs.nix",
+  shellHook-file ? get-path "shellHook.sh",
+  overlays-dir ? get-path "overlays",
+  coq-overlays-dir ? get-path "coq-overlays",
+  ocaml-overlays-dir ? get-path "ocaml-overlays",
+  config ? {},
+  withEmacs ? false,
+  print-env ? false,
+  do-nothing ? false,
+  update-nixpkgs ? false,
+  ci ? false,
+  inNixShell ? null
+}@args:
+let
+  do-nothing = (args.do-nothing or false) || update-nixpkgs;
+  input = {
+    config = optionalImport config-file (optionalImport fallback-file {}) ;
+    nixpkgs = optionalImport nixpkgs-file (throw "cannot find nixpkgs");
+  };
+in
+let tmp-pkgs = import input.nixpkgs {}; in
+with (tmp-pkgs.coqPackages.lib or tmp-pkgs.lib);
+if (input.config.format or "1.0.0") == "1.0.0" then
+  let
+    inNixShell = args.inNixShell or trivial.inNixShell;
+    attribute-from = coq-attribute: "coqPackages.${coq-attribute}";
+    logpath-from = namespace: concatStringsSep "/" (splitString "." namespace);
+    config = rec {
+      format = "1.0.0";
+      coq-attribute = input.config.coq-attribute or "template";
+      attribute = input.config.attribute or (attribute-from coq-attribute);
+      nixpkgs = input.config.nixpkgs or input.nixpkgs;
+      ppath = input.config.ppath or (splitString "." attribute);
+      pname = input.config.pname or (last ppath);
+      namespace = input.config.namespace or ".";
+      logpath = input.config.logpath or (logpath-from namespace);
+      realpath = input.config.realpath or ".";
+      select = input.config.select or 0;
+      inputs = input.config.inputs or [ {} ];
+      override = input.config.override or {};
+      src = input.config.src or fetchGit (
+        if false # replace by a version check when supported
+                 # cf https://github.com/NixOS/nix/issues/1837
+        then { url = prefix; shallow = true; } else prefix); };
+  in
+  with config; switch-if [
+    { cond = attribute-from coq-attribute != attribute;
+      out = throw "One cannot set both `coq-attribute` and `attribute`."; }
+    { cond = logpath-from namespace != config.logpath;
+      out = throw "One cannot set both `namespace` and `logpath`."; }
+  ] (let
+    mk-overlays = path: callPackage:
+      if !pathExists path then {}
+      else mapAttrs (x: _v: callPackage (path + "/${x}") {}) (readDir path);
+      # preparing inputs
+    inputs = forEach config.inputs
+      (i: foldl recursiveUpdate {} [
+        (setAttrByPath ppath { override.version = "${src}"; ci = true; })
+        i config.override
+      ]);
+    do-override = pkg: cfg:
+      let pkg' = if cfg?override
+          then pkg.override or (x: pkg) cfg.override else pkg; in
+        if cfg?overrideAttrs
+        then pkg'.overrideAttrs cfg.overrideAttrs else pkg';
+    mk-instance = input: let
+      nixpkgs-overrides =
+        self: super: mapAttrs (n: ov: do-override super.${n} ov)
+          (removeAttrs input [ "coqPackages" "ocamlPackages" ]);
+      ocaml-overrides =
+        self: super: mapAttrs (n: ov: do-override super.${n} ov)
+          (input.ocamlPackages or {});
+      coq-overrides =
+        self: super: mapAttrs
+          (n: ov: do-override (super.${n} or
+            (makeOverridable self.mkCoqDerivation {
+              pname = "${n}"; version = "${src}";
+            })) ov)
+          (input.coqPackages or {});
+      fold-override = foldl (fpkg: override: fpkg.overrideScope' override);
+      overlays = [
+        (self: super: mk-overlays overlays-dir self.callPackage)
+        nixpkgs-overrides
+        (self: super: { coqPackages = fold-override super.coqPackages ([
+          (self: super: mk-overlays coq-overlays-dir self.callPackage)
+          coq-overrides
+          (self: super: { coq = super.coq.override {
+            customOCamlPackages = fold-override super.coq.ocamlPackages [
+              (self: super: mk-overlays ocaml-overlays-dir self.callPackage)
+              ocaml-overrides
+            ];};})
+        ]);})
+        (self: super: { coqPackages =
+          super.coqPackages.filterPackages
+            (! (super.coqPackages.coq.dontFilter or false)); })
+      ]; in rec {
+        inherit input;
+        pkgs = import config.nixpkgs { inherit overlays; };
+        default-coq-derivation =
+          makeOverridable pkgs.coqPackages.mkCoqDerivation
+            { inherit pname; version = "${src}"; };
+        this-pkg = attrByPath ppath default-coq-derivation pkgs;
+        emacs = with pkgs; emacsWithPackages
+          (epkgs: with epkgs.melpaStablePackages; [proof-general]);
+        ci-coqpkgs =
+          filterAttrs (n: v: input.coqPackages.${n}.ci or false)
+            pkgs.coqPackages;
+        json_input = toJSON input;
+      };
+    instances = map mk-instance inputs;
+    selected-instance = elemAt instances select;
+    shellHook = readFile shellHook-file
+        + optionalString print-env "nixEnv"
+        + optionalString update-nixpkgs "updateNixPkgs; exit";
+    nix-shell = with selected-instance; this-pkg.overrideAttrs (old: {
+      inherit json_input shellHook;
+      currentdir = prefix;
+      coq_version = pkgs.coqPackages.coq.coq-version;
+      inherit nixpkgs logpath realpath;
+
+      buildInputs = optionals (!do-nothing)
+        (old.buildInputs or [] ++ optional withEmacs pkgs.emacs);
+
+      propagatedBuildInputs = optionals (!do-nothing)
+        (old.propagatedBuildInputs or []);
+    });
+    nix-ci = map (b: b.ci-coqpkgs) instances;
+    nix-default = selected-instance.this-pkg;
+    nix-auto = if inNixShell then nix-shell else
+      if ci then nix-ci else nix-default;
+    in {inherit nixpkgs config selected-instance instances shellHook
+                nix-shell nix-default nix-ci nix-auto; }
+  )
+else throw "Current config.format (${input.config.format}) not implemented"

.nix/nixpkgs.nix

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

.nix/shellHook.sh

@@ -0,0 +1,104 @@
+#! /usr/bin/bash
+
+printNixEnv () {
+  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\"; ...}' to nix-shell to change packages versions"
+}
+catNixEnv () {
+  for x in $buildInputs; do echo $x; done
+  for x in $propagatedBuildInputs; do echo $x; done
+}
+
+upateNixDefault () {
+  cat $currentdir/default.nix
+} > default.nix
+
+updateNixPkgs (){
+  HASH=$(git ls-remote https://github.com/NixOS/nixpkgs refs/heads/nixpkgs-unstable | cut -f1);
+  URL=https://github.com/NixOS/nixpkgs/archive/$HASH.tar.gz
+  SHA256=$(nix-prefetch-url --unpack $URL)
+  echo "fetchTarball {
+    url = $URL;
+    sha256 = \"$SHA256\";
+  }" > .nix/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\";
+  }" > .nix/nixpkgs.nix
+}
+
+updateNixPkgsCustom (){
+  if [[ -n "$1" ]]
+  then if [[ -n "$2" ]]; then B=$2; else B="master"; fi
+       HASH=$(git ls-remote https://github.com/$1/nixpkgs refs/heads/$B | cut -f1)
+       URL=https://github.com/$1/nixpkgs/archive/$HASH.tar.gz
+       SHA256=$(nix-prefetch-url --unpack $URL)
+       echo "fetchTarball {
+         url = $URL;
+         sha256 = \"$SHA256\";
+       }" > .nix/nixpkgs.nix
+  else echo "error: usage: updateNixPkgsCustom <github username> [branch]"
+  fi
+}
+
+printNixInputs (){
+    echo current input: $json_input
+}
+
+initNixConfig (){
+  F=./.nix/config.nix;
+  if [[ -f $F ]]
+    then echo "$F already exists"
+    else if [[ -n "$1" ]]
+      then echo "{" > $F
+           echo "  coq-attribute = \"$1\";" >> $F
+           echo "  overrides = {};" >> $F
+           echo "}" >> $F
+           chmod u+w $F
+      else echo "usage: initNixConfig pname"
+    fi
+  fi
+}
+
+fetchCoqOverlay (){
+  F=$nixpkgs/pkgs/development/coq-modules/$1/default.nix
+  D=./.nix/coq-overlays/$1/
+  if [[ -f "$F" ]]
+    then mkdir -p $D; cp $F $D; chmod u+w ${D}default.nix;
+         git add ${D}default.nix
+         echo "You may now amend ${D}default.nix"
+    else echo "usage: fetchCoqOverlay pname"
+  fi
+}
+
+cachedMake (){
+  vopath="$(env -i nix-build)/lib/coq/$coq_version/user-contrib/$logpath"
+  dest="$(git rev-parse --show-toplevel)/$realpath"
+  echo "Compiling/Fetching and copying vo from $vopath to $realpath"
+  rsync -r --ignore-existing --include=*/ $vopath/* $dest
+}
+
+nixHelp (){
+  cat <<END
+Available commands:
+  printNixEnv
+  catNixEnv
+  upateNixDefault
+  updateNixPkgs
+  updateNixPkgsCustom
+  printNixInputs
+  initNixConfig name
+  fetchCoqOverlay
+  cachedMake
+END
+}

default.nix.mustache

@@ -1,36 +1,6 @@
 # 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 ? false, inNixShell ? null
+}@args: (import https://raw.githubusercontent.com/coq-community/templates/nix-toolbox/.nix/auto-config.nix ./. args).nix-auto
 
-{ pkgs ? (import <nixpkgs> {}), coq-version-or-url, shell ? false }:
-
-let
-  coq-version-parts = builtins.match "([0-9]+).([0-9]+)" coq-version-or-url;
-  coqPackages =
-    if coq-version-parts == null then
-      pkgs.mkCoqPackages (import (fetchTarball coq-version-or-url) {})
-    else
-      pkgs."coqPackages_${builtins.concatStringsSep "_" coq-version-parts}";
-in
-
-with coqPackages;
-
-pkgs.stdenv.mkDerivation {
-
-  name = "{{ shortname }}";
-
-{{# plugin }}
-  buildInputs = with coq.ocamlPackages; [ ocaml findlib ]
-    ++ pkgs.lib.optionals shell [ merlin ocp-indent ocp-index ];
-
-{{/ plugin }}
-  propagatedBuildInputs = [
-    coq
-{{# dependencies }}
-    {{ nix }}
-{{/ dependencies }}
-  ];
-
-  src = if shell then null else ./.;
-
-  installFlags = "COQMF_COQLIB=$(out)/lib/coq/${coq.coq-version}/";
-}

fallback-config.nix.mustache

@@ -0,0 +1,3 @@
+{
+  coq-attribute = "{{nix_name}}";
+}

generate.sh

@@ -95,20 +95,29 @@ for f in "$srcdir"/{,.}*.mustache; do
                 continue
             fi
             ;;
-	config.yml)
-	    mustache='{{ circleci }}'
-	    bool=$(get_yaml meta.yml <<<"$mustache")
+        config.yml)
+	        mustache='{{ circleci }}'
+	        bool=$(get_yaml meta.yml <<<"$mustache")
+                if [ -n "$bool" ] && [ "$bool" != false ]; then
+                    mkdir -p -v .circleci && target=".circleci/$target"
+                else
+                    continue
+                fi
+                ;;
+        default.nix)
+            mustache='{{ nix }}'
+            bool=$(get_yaml meta.yml <<<"$mustache")
             if [ -n "$bool" ] && [ "$bool" != false ]; then
-                mkdir -p -v .circleci && target=".circleci/$target"
+                : noop
             else
                 continue
             fi
             ;;
-        default.nix)
+        fallback-config.nix)
             mustache='{{ nix }}'
             bool=$(get_yaml meta.yml <<<"$mustache")
             if [ -n "$bool" ] && [ "$bool" != false ]; then
-                : noop
+                mkdir -p -v .nix && target=".nix/$target"
             else
                 continue
             fi

nix-action.yml.mustache

@@ -13,27 +13,31 @@ on:
 jobs:
   build:
     runs-on: ubuntu-latest
-    strategy:
-      matrix:
-        version_or_url:
-{{# tested_coq_nix_versions }}
-          - '{{ version_or_url }}'
-{{/ tested_coq_nix_versions }}{{^ tested_coq_nix_versions }}          - 'https://github.com/coq/coq-on-cachix/tarball/master'
-{{/ tested_coq_nix_versions }}
-      fail-fast: false
     steps:
       - uses: cachix/install-nix-action@v12
         with:
           nix_path: nixpkgs=channel:nixpkgs-unstable
+{{# cachix}}
       - uses: cachix/cachix-action@v8
         with:
           # Name of a cachix cache to pull/substitute
-          name: coq
+          name: {{name}}
+{{=<% %>=}}
+<%# key%>
+          signingKey: '${{ secrets.<%key%> }}'
+<%/ key%>
+<%# token%>
+          authToken: '${{ secrets.<%token%> }}'
+<%/ token%>
+<%={{ }}=%>
+{{/ cachix}}
       - uses: actions/checkout@v2
+        with:
+          fetch-depth: 0
 {{# submodule }}
       - name: Checkout submodules
         uses: textbook/git-checkout-submodule-action@2.1.1
 {{/ submodule }}
 {{! Change delimiters to avoid the next line being parsed as mustache syntax. }}
 {{=<% %>=}}
-      - run: nix-build --argstr coq-version-or-url "${{ matrix.version_or_url }}"
+      - run: nix-build --arg ci true