Merge PR #7973: Add a test build on NixOS to GitLab CI.

4 files changed, 60 insertions, 50 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index e6f08b8c6..773a89a46 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -236,6 +236,22 @@ windows32:
   variables:
     ARCH: "32"
 
+pkg:nix:
+  image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git
+  stage: test
+  variables:
+    GIT_STRATEGY: none
+  dependencies: [] # We don't need to download build artifacts
+  before_script: [] # We don't want to use the shared 'before_script'
+  script:
+    - export TMPDIR=$PWD
+    - nix-build "$CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz" -K
+  artifacts:
+    name: "$CI_JOB_NAME.logs"
+    when: on_failure
+    paths:
+      - nix-build-coq.drv-0/*/test-suite/logs
+
 warnings:base:
   <<: *warnings-template
 
diff --git a/default.nix b/default.nix
index a2645f4fc..1be274081 100644
--- a/default.nix
+++ b/default.nix
@@ -9,23 +9,27 @@
 
 # nix-shell supports the --arg option (see Nix doc) that allows you for
 # instance to do this:
-# $ nix-shell --arg ocamlPackages "(import <nixpkgs> {}).ocamlPackages_latest" --arg buildIde false
+# $ nix-shell --arg ocamlPackages "(import <nixpkgs> {}).ocaml-ng.ocamlPackages_4_05" --arg buildIde false
 
 # You can also compile Coq and "install" it by running:
 # $ make clean # (only needed if you have left-over compilation files)
 # $ nix-build
 # at the root of the Coq repository.
 # nix-build also supports the --arg option, so you will be able to do:
-# $ nix-build --arg doCheck false
+# $ nix-build --arg doInstallCheck false
 # if you want to speed up things by not running the test-suite.
 # Once the build is finished, you will find, in the current directory,
 # a symlink to where Coq was installed.
 
-{ pkgs ? (import <nixpkgs> {})
+{ pkgs ?
+    (import (fetchTarball {
+      url = "https://github.com/NixOS/nixpkgs/archive/060a98e9f4ad879492e48d63e887b0b6db26299e.tar.gz";
+      sha256 = "1lzvp3md0hf6kp2bvc6dbzh40navlyd51qlns9wbkz6lqk3lgf6j";
+    }) {})
 , ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06
 , buildIde ? true
 , buildDoc ? true
-, doCheck ? true
+, doInstallCheck ? true
 }:
 
 with pkgs;
@@ -36,64 +40,50 @@ stdenv.mkDerivation rec {
   name = "coq";
 
   buildInputs = [
-
-    # Coq dependencies
     hostname
-  ] ++ (with ocamlPackages; [
-    ocaml
-    findlib
-    camlp5_strict
-    num
-
-  ]) ++ (if buildIde then [
-
-    # CoqIDE dependencies
-    ocamlPackages.lablgtk
-
-  ] else []) ++ (if buildDoc then [
-
+    python2 time # coq-makefile timing tools
+  ]
+  ++ (with ocamlPackages; [ ocaml findlib camlp5_strict num ])
+  ++ optional buildIde ocamlPackages.lablgtk
+  ++ optionals buildDoc [
     # Sphinx doc dependencies
     pkgconfig (python3.withPackages
       (ps: [ ps.sphinx ps.sphinx_rtd_theme ps.pexpect ps.beautifulsoup4
              ps.antlr4-python3-runtime ps.sphinxcontrib-bibtex ]))
-     antlr4
-
-  ] else []) ++ (if doCheck then
-
+    antlr4
+  ]
+  ++ optionals doInstallCheck (
     # Test-suite dependencies
     # ncurses is required to build an OCaml REPL
     optional (!versionAtLeast ocaml.version "4.07") ncurses
-    ++ [
-    python
-    rsync
-    which
-    ocamlPackages.ounit
-
-  ] else []) ++ (if lib.inNixShell then [
-    ocamlPackages.merlin
-    ocamlPackages.ocp-indent
-    ocamlPackages.ocp-index
-
-    # Dependencies of the merging script
-    jq
-    curl
-    git
-    gnupg
-
-  ] else []);
+    ++ [ ocamlPackages.ounit rsync which ]
+  )
+  ++ optionals lib.inNixShell (
+    [ jq curl git gnupg ] # Dependencies of the merging script
+    ++ (with ocamlPackages; [ merlin ocp-indent ocp-index ]) # Dev tools
+  );
 
   src =
     if lib.inNixShell then null
     else
       with builtins; filterSource
-        (path: _: !elem (baseNameOf path) [".git" "result" "bin"]) ./.;
+        (path: _:
+           !elem (baseNameOf path) [".git" "result" "bin" "_build_ci"]) ./.;
 
   prefixKey = "-prefix ";
 
-  buildFlags = [ "world" ] ++ optional buildDoc "doc-html";
+  buildFlags = [ "world" "byte" ] ++ optional buildDoc "doc-html";
+
+  installTargets =
+    [ "install" "install-byte" ] ++ optional buildDoc "install-doc-html";
+
+  inherit doInstallCheck;
 
-  installTargets = [ "install" ] ++ optional buildDoc "install-doc-html";
+  preInstallCheck = ''
+    patchShebangs tools/
+    patchShebangs test-suite/
+  '';
 
-  inherit doCheck;
+  installCheckTarget = [ "check" ];
 
 }
diff --git a/shell.nix b/shell.nix
new file mode 100644
index 000000000..45070b2ba
--- /dev/null
+++ b/shell.nix
@@ -0,0 +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> {}; }
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 8e60d3932..7aa2d0a5a 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -65,20 +65,20 @@ VERBOSE ?=
 # Time the Coq process (set to non empty), and how (see default value)
 TIMED?=
 TIMECMD?=
-# Use /usr/bin/env time on linux, gtime on Mac OS
+# Use command time on linux, gtime on Mac OS
 TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)"
 ifneq (,$(TIMED))
-ifeq (0,$(shell /usr/bin/env time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
-STDTIME?=/usr/bin/env time -f $(TIMEFMT)
+ifeq (0,$(shell command time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+STDTIME?=command time -f $(TIMEFMT)
 else
 ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
 STDTIME?=gtime -f $(TIMEFMT)
 else
-STDTIME?=time
+STDTIME?=command time
 endif
 endif
 else
-STDTIME?=/usr/bin/env time -f $(TIMEFMT)
+STDTIME?=command time -f $(TIMEFMT)
 endif
 
 # Coq binaries