1 files changed, 134 insertions, 0 deletions
diff --git a/default.nix b/default.nix
new file mode 100644
index 0000000000..89d69cc40f
--- /dev/null
+++ b/default.nix
@@ -0,0 +1,134 @@
+# How to use?
+
+# If you have Nix installed, you can get in an environment with everything
+# needed to compile Coq and CoqIDE by running:
+# $ nix-shell
+# at the root of the Coq repository.
+
+# How to tweak default arguments?
+
+# nix-shell supports the --arg option (see Nix doc) that allows you for
+# instance to do this:
+# $ 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 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 (fetchTarball {
+      url = "https://github.com/NixOS/nixpkgs/archive/958a6c6dd39b0d6628e1408e798a8f1308f2f3e1.tar.gz";
+      sha256 = "0vs6k4jn0rbdfzaxmh3xh64q213326680i9g3cjgr7l9y6h6m5sy";
+    }) {})
+, ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06
+, 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.
+, coq-version ? "8.10-git"
+}:
+
+with pkgs;
+with stdenv.lib;
+
+stdenv.mkDerivation rec {
+
+  name = "coq";
+
+  buildInputs = [
+    hostname
+    python2 time # coq-makefile timing tools
+    dune
+  ]
+  ++ (with ocamlPackages; [ ocaml findlib 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
+    ocamlPackages.odoc
+  ]
+  ++ optionals doInstallCheck (
+    # Test-suite dependencies
+    # ncurses is required to build an OCaml REPL
+    optional (!versionAtLeast ocaml.version "4.07") ncurses
+    ++ [ ocamlPackages.ounit rsync which ]
+  )
+  ++ optionals shell (
+    [ jq curl gitFull gnupg ] # Dependencies of the merging script
+    ++ (with ocamlPackages; [ merlin ocp-indent ocp-index utop ]) # Dev tools
+    ++ [ graphviz ] # Useful for STM debugging
+  );
+
+  src =
+    if shell then null
+    else
+      with builtins; filterSource
+        (path: _:
+           !elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci"]) ./.;
+
+  preConfigure = ''
+    patchShebangs kernel/
+    patchShebangs dev/tools/
+  '';
+
+  prefixKey = "-prefix ";
+
+  buildFlags = [ "world" "byte" ] ++ optional buildDoc "doc-html";
+
+  installTargets =
+    [ "install" "install-byte" ] ++ optional buildDoc "install-doc-html";
+
+  createFindlibDestdir = !shell;
+
+  postInstall = "ln -s $out/lib/coq $OCAMLFIND_DESTDIR/coq";
+
+  inherit doInstallCheck;
+
+  preInstallCheck = ''
+    patchShebangs tools/
+    patchShebangs test-suite/
+    export OCAMLPATH=$OCAMLFIND_DESTDIR:$OCAMLPATH
+  '';
+
+  installCheckTarget = [ "check" ];
+
+  passthru = {
+    inherit coq-version ocamlPackages;
+    dontFilter = true; # Useful to use mkCoqPackages from <nixpkgs>
+  };
+
+  setupHook = writeText "setupHook.sh" "
+    addCoqPath () {
+      if test -d \"$1/lib/coq/${coq-version}/user-contrib\"; then
+        export COQPATH=\"$COQPATH\${COQPATH:+:}$1/lib/coq/${coq-version}/user-contrib/\"
+      fi
+    }
+
+    addEnvHooks \"$targetOffset\" addCoqPath
+  ";
+
+  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;
+    platforms = platforms.unix;
+  };
+
+}