Merge PR #8001: Cache the build of the Nix package using Cachix.

3 files changed, 35 insertions, 5 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 773a89a46..11614bc38 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -240,12 +240,25 @@ pkg:nix:
   image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git
   stage: test
   variables:
+    # By default we use coq.cachix.org as an extra substituter but this can be overridden
+    EXTRA_SUBSTITUTERS: https://coq.cachix.org
+    EXTRA_PUBLIC_KEYS: coq.cachix.org-1:Jgt0DwGAUo+wpxCM52k2V+E0hLoOzFPzvg94F65agtI=
+    # The following variables should not be overridden
     GIT_STRATEGY: none
+    CACHIX_PUBLIC_KEY: cachix.cachix.org-1:eWNHQldwUO7G2VkjpnjDbWwy4KQ/HNxht7H4SSoMckM=
+    NIXOS_PUBLIC_KEY: cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
+
   dependencies: [] # We don't need to download build artifacts
   before_script: [] # We don't want to use the shared 'before_script'
   script:
+    # Use current worktree as tmpdir to allow exporting artifacts in case of failure
     - export TMPDIR=$PWD
-    - nix-build "$CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz" -K
+    # Install Cachix as documented at https://github.com/cachix/cachix
+    - nix-env -if https://github.com/cachix/cachix/tarball/master --substituters https://cachix.cachix.org --trusted-public-keys "$CACHIX_PUBLIC_KEY"
+    # We build an expression rather than a direct URL to not be dependent on
+    # the URL location; we are forced to put the public key of cache.nixos.org
+    # because there is no --extra-trusted-public-key option.
+    - nix-build -E "import (fetchTarball $CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz) {}" -K --extra-substituters "$EXTRA_SUBSTITUTERS" --trusted-public-keys "$NIXOS_PUBLIC_KEY $EXTRA_PUBLIC_KEYS" | if [ ! -z "$CACHIX_SIGNING_KEY" ]; then cachix push coq; fi
   artifacts:
     name: "$CI_JOB_NAME.logs"
     when: on_failure
diff --git a/default.nix b/default.nix
index 1be274081..d9317bcca 100644
--- a/default.nix
+++ b/default.nix
@@ -30,6 +30,9 @@
 , buildIde ? true
 , buildDoc ? true
 , doInstallCheck ? true
+, shell ? false
+  # We don't use lib.inNixShell because that would also apply
+  # when in a nix-shell of some package depending on this one.
 }:
 
 with pkgs;
@@ -58,13 +61,13 @@ stdenv.mkDerivation rec {
     optional (!versionAtLeast ocaml.version "4.07") ncurses
     ++ [ ocamlPackages.ounit rsync which ]
   )
-  ++ optionals lib.inNixShell (
+  ++ optionals shell (
     [ jq curl git gnupg ] # Dependencies of the merging script
     ++ (with ocamlPackages; [ merlin ocp-indent ocp-index ]) # Dev tools
   );
 
   src =
-    if lib.inNixShell then null
+    if shell then null
     else
       with builtins; filterSource
         (path: _:
@@ -86,4 +89,18 @@ stdenv.mkDerivation rec {
 
   installCheckTarget = [ "check" ];
 
+  passthru = { inherit ocamlPackages; };
+
+  meta = {
+    description = "Coq proof assistant";
+    longDescription = ''
+      Coq is a formal proof management system.  It provides a formal language
+      to write mathematical definitions, executable algorithms and theorems
+      together with an environment for semi-interactive development of
+      machine-checked proofs.
+    '';
+    homepage = http://coq.inria.fr;
+    license = licenses.lgpl21;
+  };
+
 }
diff --git a/shell.nix b/shell.nix
index 45070b2ba..3201c5050 100644
--- a/shell.nix
+++ b/shell.nix
@@ -1,4 +1,4 @@
 # Some developers don't want a pinned nix-shell by default.
 # If you want to use the pin nix-shell or a more sophisticated set of arguments:
-# $ nix-shell default.nix
-import ./default.nix { pkgs = import <nixpkgs> {}; }
+# $ nix-shell default.nix --arg shell true
+import ./default.nix { pkgs = import <nixpkgs> {}; shell = true; }