blob: ac81887a2d4a0f49123a37cbe957d4b043ff513a (
plain)
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
|
# Copyright 1999-2025 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
inherit check-reqs desktop dune edo
DESCRIPTION="Coq/Rocq is a proof assistant written in O'Caml"
HOMEPAGE="https://coq.inria.fr/
https://github.com/coq/coq/"
if [[ "${PV}" == *9999* ]] ; then
inherit git-r3
EGIT_REPO_URI="https://github.com/coq/coq"
else
SRC_URI="https://github.com/coq/coq/archive/V${PV}.tar.gz
-> ${P}.tar.gz"
KEYWORDS="~amd64 ~arm64"
fi
LICENSE="LGPL-2.1"
SLOT="0/${PV}"
IUSE="debug gui native-compiler +ocamlopt test"
# TODO: Lots of failing tests.
# RESTRICT="!test? ( test )"
RESTRICT="test"
RDEPEND="
dev-ml/camlzip:=
dev-ml/num:=
dev-ml/zarith:=
gui? (
>=dev-ml/lablgtk-3.1.2:3=[sourceview,ocamlopt?]
>=dev-ml/lablgtk-sourceview-3.1.2:3=[ocamlopt?]
)
native-compiler? (
<dev-lang/ocaml-5:=
)
"
DEPEND="
${RDEPEND}
"
BDEPEND="
dev-ml/findlib
test? (
dev-ml/ounit2
)
"
PDEPEND="
sci-mathematics/coq-stdlib
"
CHECKREQS_DISK_BUILD="2G"
DOCS=( CODE_OF_CONDUCT.md CONTRIBUTING.md CREDITS INSTALL.md README.md )
DUNE_PACKAGES=()
src_prepare() {
# Remove bad tests (recursive).
local -a bad_tests=(
coq-makefile/timing-aggregate
coq-makefile/timing-error
coq-makefile/timing-per-file
coq-makefile/timing-per-line
coq-makefile/timing-template
)
local bad_test=""
for bad_test in "${bad_tests[@]}" ; do
if [[ -e "test-suite/${bad_test}" ]] ; then
rm -r "test-suite/${bad_test}" || die "failed to remove test ${bad_test}"
else
ewarn "Test file ${bad_test} does not exist"
fi
done
default
}
src_configure() {
local -x CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/"
DUNE_PACKAGES=(
coq
coq-core
rocq-core
rocq-prover
rocq-runtime
)
if use gui ; then
DUNE_PACKAGES+=(
coqide-server
rocqide
)
fi
local -a myconf=(
-prefix /usr
-libdir "/usr/$(get_libdir)/coq"
-mandir /usr/share/man
-docdir "/usr/share/doc/${PF}"
-datadir /usr/share/coq
-configdir "/etc/xdg/${PN}"
-native-compiler "$(usex native-compiler yes no)"
)
if use debug ; then
myconf+=(
-debug
)
fi
emake clean
edo sh ./configure "${myconf[@]}"
}
src_compile() {
emake DUNEOPT="--display=short --profile release" VERBOSE="1" dunestrap
dune-compile "${DUNE_PACKAGES[@]}"
}
src_install() {
dune-install "${DUNE_PACKAGES[@]}"
if use gui ; then
make_desktop_entry rocqide "Coq IDE" "${EPREFIX}/usr/share/coq/coq.png"
fi
local ocamlc_where="$(ocamlc -where)"
# Dune installs into /usr/<libdir>/ocaml/<coq> but
# Coq wants /usr/<libdir>/<coq> ; symlink those directories
local sym=""
for sym in "${DUNE_PACKAGES[@]}" ; do
dosym "${ocamlc_where}/${sym}" "/usr/$(get_libdir)/${sym}"
done
einstalldocs
}
|
