sci-mathematics/coq: revbump for newer ocaml + num
authorJason A. Donenfeld <zx2c4@gentoo.org>
Tue, 7 Jan 2020 20:57:56 +0000 (15:57 -0500)
committerJason A. Donenfeld <zx2c4@gentoo.org>
Tue, 7 Jan 2020 21:00:55 +0000 (16:00 -0500)
Fixes: https://bugs.gentoo.org/704928
Package-Manager: Portage-2.3.84, Repoman-2.3.20
Signed-off-by: Jason A. Donenfeld <zx2c4@gentoo.org>
sci-mathematics/coq/coq-8.9.1-r2.ebuild [new file with mode: 0644]

diff --git a/sci-mathematics/coq/coq-8.9.1-r2.ebuild b/sci-mathematics/coq/coq-8.9.1-r2.ebuild
new file mode 100644 (file)
index 0000000..75d3af5
--- /dev/null
@@ -0,0 +1,86 @@
+# Copyright 1999-2020 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI="7"
+
+inherit desktop multilib
+
+MY_PV=${PV/_p/pl}
+MY_P=${PN}-${MY_PV}
+
+DESCRIPTION="Proof assistant written in O'Caml"
+HOMEPAGE="http://coq.inria.fr/"
+SRC_URI="https://github.com/coq/coq/archive/V${MY_PV}.tar.gz -> ${P}.tar.gz"
+
+LICENSE="LGPL-2.1"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+IUSE="gtk debug +ocamlopt doc"
+
+RESTRICT=test
+
+RDEPEND="
+       >=dev-lang/ocaml-4.0.7:=[ocamlopt?]
+       dev-ml/camlp5:=[ocamlopt?]
+       dev-ml/num:=
+       gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )"
+DEPEND="${RDEPEND}
+       dev-ml/findlib
+       doc? (
+               media-libs/netpbm[png,zlib]
+               virtual/latex-base
+               dev-tex/hevea
+               dev-texlive/texlive-latexrecommended
+               dev-texlive/texlive-pictures
+               dev-texlive/texlive-mathscience
+               dev-texlive/texlive-latexextra
+               )"
+
+S=${WORKDIR}/${MY_P}
+
+src_configure() {
+       ocaml_lib=$(ocamlc -where)
+       local myconf=(
+               -prefix /usr
+               -bindir /usr/bin
+               -libdir /usr/$(get_libdir)/coq
+               -mandir /usr/share/man
+               -coqdocdir /usr/$(get_libdir)/coq/coqdoc
+               -docdir /usr/share/doc/${PF}
+               -configdir /etc/xdg/${PN}
+               -lablgtkdir ${ocaml_lib}/lablgtk2
+               )
+
+       use debug && myconf+=( -debug )
+       use doc || myconf+=( -with-doc no )
+
+       if use gtk; then
+               if use ocamlopt; then
+                       myconf+=( -coqide opt )
+               else
+                       myconf+=( -coqide byte )
+               fi
+       else
+               myconf+=( -coqide no )
+       fi
+
+       use ocamlopt || myconf+=( -byte-only )
+
+       export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/"
+       ./configure ${myconf[@]} || die "configure failed"
+}
+
+src_compile() {
+       emake STRIP="true" -j1 world VERBOSE=1
+}
+
+src_test() {
+       emake STRIP="true" check VERBOSE=1
+}
+
+src_install() {
+       emake STRIP="true" COQINSTALLPREFIX="${D}" install VERBOSE=1
+       dodoc README.md CREDITS CHANGES.md
+
+       use gtk && make_desktop_entry "coqide" "Coq IDE" "${EPREFIX}/usr/share/coq/coq.png"
+}