# 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;
  };

}