diff options
Diffstat (limited to 'default.nix')
-rw-r--r-- | default.nix | 98 |
1 files changed, 53 insertions, 45 deletions
diff --git a/default.nix b/default.nix index 91d963604..d9317bcca 100644 --- a/default.nix +++ b/default.nix @@ -9,23 +9,30 @@ # 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 +, 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; @@ -36,63 +43,64 @@ 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.ocpIndent - - # Dependencies of the merging script - jq - curl - git - gnupg - - ] else []); + ++ [ ocamlPackages.ounit rsync which ] + ) + ++ 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: _: !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; + + preInstallCheck = '' + patchShebangs tools/ + patchShebangs test-suite/ + ''; + + installCheckTarget = [ "check" ]; - installTargets = [ "install" ] ++ optional buildDoc "install-doc-html"; + passthru = { inherit ocamlPackages; }; - inherit doCheck; + 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; + }; } |