Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185# How to use?
# If you have Nix installed, you can get in an environment with everything# needed to compile Rocq and RocqIDE by running:# $ nix-shell# at the root of the Rocq 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_14" --arg buildIde false
# You can also compile Rocq and "install" it by running:# $ make clean # (only needed if you have left-over compilation files)# $ nix-build# at the root of the Rocq 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 Rocq was installed.
{ pkgs ? import ./dev/nixpkgs.nix {}, ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_14, 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.14-git"}:
with pkgs;with pkgs.lib;
stdenv.mkDerivation rec {
name = "coq";
buildInputs = [ hostname python312 ocamlPackages.yojson ocamlPackages.camlzip # coq-makefile timing tools time dune_3 ] ++ optionals buildIde [ ocamlPackages.lablgtk3-sourceview3 glib (pkgs.adwaita-icon-theme or gnome.adwaita-icon-theme) (pkgs.wrapGAppsHook3 or wrapGAppsHook) ] ++ optionals buildDoc [ # Sphinx doc dependencies pkg-config (python312.withPackages (ps: [ ps.sphinx (ps."sphinx-rtd-theme" or ps.sphinx_rtd_theme) ps.pexpect ps.beautifulsoup4 (ps.antlr4-python3-runtime.override {antlr4 = pkgs.antlr4_9;}) ps.sphinxcontrib-bibtex ])) antlr4_9 ocamlPackages.odoc ] ++ optionals doInstallCheck [ # Test-suite dependencies ocamlPackages.ounit rsync which ] ++ optionals shell ( [ # Dependencies of the merging script jq curl gitFull gnupg ] ++ (with ocamlPackages; [ # Dev tools ocaml-lsp merlin ocp-indent ocp-index utop ocamlformat ]) ++ [ # Useful for STM debugging graphviz ] );
# OCaml and findlib are needed so that native_compute works # This follows a similar change in the nixpkgs repo (cf. NixOS/nixpkgs#101058) # ocamlfind looks for zarith when building plugins # This follows a similar change in the nixpkgs repo (cf. NixOS/nixpkgs#94230) propagatedBuildInputs = with ocamlPackages; [ ocaml findlib zarith ];
propagatedUserEnvPkgs = with ocamlPackages; [ ocaml findlib ];
src = if shell then null else with builtins; filterSource (path: _: !elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci" "_build_vo" "nix"]) ./.;
preConfigure = '' patchShebangs dev/tools/ doc/corelib '';
prefixKey = "-prefix ";
enableParallelBuilding = true;
buildFlags = [ "world" ] ++ optional buildIde "rocqide";
# TODO, building of documentation package when not in dev mode # https://github.com/rocq-prover/rocq/issues/16198 # buildFlags = [ "world" ] ++ optional buildDoc "refman-html";
# From https://github.com/NixOS/nixpkgs/blob/master/pkgs/build-support/ocaml/dune.nix installPhase = '' runHook preInstall dune install --prefix $out --libdir $OCAMLFIND_DESTDIR rocq-runtime coq-core rocq-core rocqide-server ${optionalString buildIde "rocqide"} runHook postInstall '';
# installTargets = # [ "install" ]; # fixme, do we have to do a target, or can we just do a copy? # ++ optional buildDoc "install-doc-html";
createFindlibDestdir = !shell;
postInstall = '' for pkg in rocq-runtime coq-core; do if [ -e "$out/lib/$pkg" ] && [ ! -e "$OCAMLFIND_DESTDIR/$pkg" ]; then ln -s "$out/lib/$pkg" "$OCAMLFIND_DESTDIR/$pkg" elif [ -e "$OCAMLFIND_DESTDIR/$pkg" ] && [ ! -e "$out/lib/$pkg" ]; then ln -s "$OCAMLFIND_DESTDIR/$pkg" "$out/lib/$pkg" fi done '';
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 ROCQPATH=\"\${ROCQPATH-}\${ROCQPATH:+:}$1/lib/coq/${coq-version}/user-contrib/\" fi }
addEnvHooks \"$targetOffset\" addCoqPath ";
meta = { description = "Rocq Prover"; longDescription = '' The Rocq Prover is an interactive theorem prover, or proof assistant. 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 = https://rocq-prover.org; license = licenses.lgpl21; platforms = platforms.unix; };
}