1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
|
# 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_09" --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 ./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
python311
# coq-makefile timing tools
time
dune_3
]
++ optionals buildIde [
ocamlPackages.lablgtk3-sourceview3
glib
gnome.adwaita-icon-theme
wrapGAppsHook
]
++ optionals buildDoc [
# Sphinx doc dependencies
pkg-config (python311.withPackages
(ps: [ ps.sphinx 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/stdlib
'';
prefixKey = "-prefix ";
enableParallelBuilding = true;
buildFlags = [ "world" ];
# TODO, building of documentation package when not in dev mode
# https://github.com/coq/coq/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 coq-core coq-stdlib coq coqide-server coqide
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 = "ln -s $out/lib/coq-core $OCAMLFIND_DESTDIR/coq-core";
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;
};
}
|
