From fcbb16841aa036d029a7336bca9afcda9081bdee Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 2 Jul 2018 13:43:17 +0200 Subject: Adapt default.nix to allow nix-build to run the test-suite. --- default.nix | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/default.nix b/default.nix index a2645f4fc..e4834ae3a 100644 --- a/default.nix +++ b/default.nix @@ -9,14 +9,14 @@ # nix-shell supports the --arg option (see Nix doc) that allows you for # instance to do this: -# $ nix-shell --arg ocamlPackages "(import {}).ocamlPackages_latest" --arg buildIde false +# $ nix-shell --arg ocamlPackages "(import {}).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. @@ -25,7 +25,7 @@ , ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06 , buildIde ? true , buildDoc ? true -, doCheck ? true +, doInstallCheck ? true }: with pkgs; @@ -58,13 +58,13 @@ stdenv.mkDerivation rec { ps.antlr4-python3-runtime ps.sphinxcontrib-bibtex ])) antlr4 - ] else []) ++ (if doCheck then + ] else []) ++ (if doInstallCheck then # Test-suite dependencies # ncurses is required to build an OCaml REPL optional (!versionAtLeast ocaml.version "4.07") ncurses ++ [ - python + python2 rsync which ocamlPackages.ounit @@ -90,10 +90,18 @@ stdenv.mkDerivation rec { prefixKey = "-prefix "; - buildFlags = [ "world" ] ++ optional buildDoc "doc-html"; + buildFlags = [ "world" "byte" ] ++ optional buildDoc "doc-html"; - installTargets = [ "install" ] ++ optional buildDoc "install-doc-html"; + installTargets = + [ "install" "install-byte" ] ++ optional buildDoc "install-doc-html"; - inherit doCheck; + inherit doInstallCheck; + + preInstallCheck = '' + patchShebangs tools/ + patchShebangs test-suite/ + ''; + + installCheckTarget = [ "check" ]; } -- cgit v1.2.3 From 89d8674c6ac2c826f157ff0a007cc5eecda9b313 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Sun, 1 Jul 2018 18:42:50 +0200 Subject: Add a test build of Nix package to GitLab CI. We pin default.nix again to make the CI build predictable. As in Windows builds, we need to override the default before_script. As in other test-suite jobs, we export logs as artifacts on failure. --- .gitlab-ci.yml | 16 ++++++++++++++++ default.nix | 6 +++++- 2 files changed, 21 insertions(+), 1 deletion(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8469d6119..f54171412 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -233,6 +233,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 e4834ae3a..d5e7674d4 100644 --- a/default.nix +++ b/default.nix @@ -21,7 +21,11 @@ # Once the build is finished, you will find, in the current directory, # a symlink to where Coq was installed. -{ pkgs ? (import {}) +{ 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 -- cgit v1.2.3 From 5239af30618d3c23666cc75078bf269172b6d3df Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 3 Jul 2018 11:34:18 +0200 Subject: Fix timing tools on NixOS. --- default.nix | 12 ++++-------- tools/CoqMakefile.in | 10 +++++----- 2 files changed, 9 insertions(+), 13 deletions(-) diff --git a/default.nix b/default.nix index d5e7674d4..2bf0409d6 100644 --- a/default.nix +++ b/default.nix @@ -40,9 +40,9 @@ stdenv.mkDerivation rec { name = "coq"; buildInputs = [ - - # Coq dependencies hostname + python2 time # coq-makefile timing tools + ] ++ (with ocamlPackages; [ ocaml findlib @@ -67,13 +67,9 @@ stdenv.mkDerivation rec { # Test-suite dependencies # ncurses is required to build an OCaml REPL optional (!versionAtLeast ocaml.version "4.07") ncurses - ++ [ - python2 - rsync - which - ocamlPackages.ounit + ++ [ ocamlPackages.ounit rsync which ] - ] else []) ++ (if lib.inNixShell then [ + else []) ++ (if lib.inNixShell then [ ocamlPackages.merlin ocamlPackages.ocp-indent ocamlPackages.ocp-index 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 -- cgit v1.2.3 From 81c3b2003d3d9b1492949773ed69e0c0ddac8316 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 3 Jul 2018 13:43:02 +0200 Subject: Refactor default.nix to use optionals. --- default.nix | 46 ++++++++++++++-------------------------------- 1 file changed, 14 insertions(+), 32 deletions(-) diff --git a/default.nix b/default.nix index 2bf0409d6..1be274081 100644 --- a/default.nix +++ b/default.nix @@ -42,51 +42,33 @@ stdenv.mkDerivation rec { buildInputs = [ hostname python2 time # coq-makefile timing tools - - ] ++ (with ocamlPackages; [ - ocaml - findlib - camlp5_strict - num - - ]) ++ (if buildIde then [ - - # CoqIDE dependencies - ocamlPackages.lablgtk - - ] else []) ++ (if buildDoc then [ - + ] + ++ (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 doInstallCheck then - + antlr4 + ] + ++ optionals doInstallCheck ( # Test-suite dependencies # ncurses is required to build an OCaml REPL optional (!versionAtLeast ocaml.version "4.07") ncurses ++ [ ocamlPackages.ounit rsync which ] - - else []) ++ (if lib.inNixShell then [ - ocamlPackages.merlin - ocamlPackages.ocp-indent - ocamlPackages.ocp-index - - # Dependencies of the merging script - jq - curl - git - gnupg - - ] else []); + ) + ++ 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 "; -- cgit v1.2.3 From def875bd55053957fb28bc6004576b6ca20dad7a Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 3 Jul 2018 16:53:27 +0200 Subject: Add a shell.nix that is not pinned to satisfy some developers' preference. --- shell.nix | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 shell.nix 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 {}; } -- cgit v1.2.3