blob: 888c5c48f865b05d49efe5dc84bdc9f13fcbe30e (
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
|
# Copyright 1999-2024 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
inherit autotools findlib
DESCRIPTION="Platform for deductive program verification"
HOMEPAGE="https://why3.lri.fr/"
SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
LICENSE="LGPL-2"
SLOT="0/${PV}"
KEYWORDS="~amd64"
IUSE="coq doc emacs gtk +ocamlopt re sexp stackify +zarith zip"
RDEPEND="
!sci-mathematics/why3-for-spark
>=dev-lang/ocaml-4.05.0:=[ocamlopt?]
>=dev-ml/menhir-20170418:=
dev-ml/num:=
coq? ( >=sci-mathematics/coq-8.7:= )
emacs? ( app-editors/emacs:* )
gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )
re? ( dev-ml/re:= )
sexp? (
dev-ml/ppx_deriving:=[ocamlopt?]
dev-ml/ppx_sexp_conv:=[ocamlopt?]
dev-ml/sexplib:=[ocamlopt?]
)
stackify? ( dev-ml/ocamlgraph:=[ocamlopt?] )
zarith? ( dev-ml/zarith:= )
zip? ( dev-ml/camlzip:= )
"
DEPEND="${RDEPEND}"
BDEPEND="
doc? (
dev-python/sphinx
dev-python/sphinxcontrib-bibtex
media-gfx/graphviz
dev-texlive/texlive-latex
dev-texlive/texlive-fontsrecommended
dev-texlive/texlive-latexextra
)
"
DOCS=( CHANGES.md README.md )
PATCHES=( "${FILESDIR}"/${P}-signum.patch )
src_prepare() {
mv configure.in configure.ac || die
sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
-e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
-e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \
-i Makefile.in || die
# remove QA warning about duplicated compressed file:
rm examples/mlcfg/basic/why3shapes.gz || die
eautoreconf
default
}
src_configure() {
local -a myconf=(
--enable-verbose-make
--disable-frama-c
--disable-hypothesis-selection
--disable-infer
--disable-isabelle-libs
--disable-pvs-libs
--disable-web-ide
$(use_enable coq coq-libs)
$(use_enable doc)
$(use_enable emacs emacs-compilation)
$(use_enable gtk ide)
$(use_enable ocamlopt native-code)
$(use_enable re)
$(use_enable sexp)
$(use_enable stackify)
$(use_enable zarith)
$(use_enable zip)
)
econf "${myconf[@]}"
}
src_compile() {
emake
emake plugins
use doc && emake doc
}
src_install(){
findlib_src_preinst
emake install install-lib DESTDIR="${ED}"
einstalldocs
docompress -x /usr/share/doc/${PF}/examples
dodoc -r examples
if use doc; then
dodoc doc/latex/manual.pdf
dodoc -r doc/html
fi
}
|
