| 1 |
|
# Copyright 1999-2025 Gentoo Authors
|
|
1 |
# Copyright 1999-2026 Gentoo Authors
|
| 2 |
2 |
# Distributed under the terms of the GNU General Public License v2
|
| 3 |
3 |
|
| 4 |
|
EAPI=7
|
|
4 |
EAPI=8
|
| 5 |
5 |
|
| 6 |
6 |
inherit autotools findlib
|
| 7 |
7 |
|
| 8 |
|
ADAMIRROR=https://community.download.adacore.com/v1
|
| 9 |
|
ID=dd74ae7ecfd7d56aff7b17cee7a35559384a600f
|
| 10 |
|
MYP=why3-${PV}-20210519-19ADF-src
|
|
8 |
ID=fb4ca6cd8c7d888d3e8d281e6de87c66ec20f084
|
| 11 |
9 |
|
| 12 |
|
DESCRIPTION="Platform for deductive program verification"
|
|
10 |
DESCRIPTION="SPARK 2014 repository for the Why3 verification platform"
|
| 13 |
11 |
HOMEPAGE="https://www.why3.org/ https://github.com/AdaCore/why3"
|
| 14 |
|
SRC_URI="${ADAMIRROR}/${ID}?filename=${MYP}.tar.gz -> ${MYP}.tar.gz"
|
|
12 |
SRC_URI="https://github.com/AdaCore/why3/archive/${ID}.tar.gz
|
|
13 |
-> ${P}.tar.gz"
|
| 15 |
14 |
|
| 16 |
|
S="${WORKDIR}"/${MYP}
|
|
15 |
S="${WORKDIR}"/why3-${ID}
|
| 17 |
16 |
|
| 18 |
17 |
LICENSE="GPL-3"
|
| 19 |
18 |
SLOT="0"
|
| 20 |
|
KEYWORDS="amd64"
|
|
19 |
KEYWORDS="amd64 ~arm64"
|
| 21 |
20 |
IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt sexp zarith zip"
|
| 22 |
21 |
RESTRICT="strip"
|
| 23 |
22 |
|
| 24 |
23 |
RDEPEND="
|
| 25 |
24 |
dev-ml/menhir:=[ocamlopt?]
|
| 26 |
25 |
dev-ml/num:=[ocamlopt?]
|
|
26 |
dev-ml/re:=[ocamlopt?]
|
| 27 |
27 |
dev-ml/yojson:=
|
| 28 |
|
coq? ( sci-mathematics/coq )
|
|
28 |
coq? ( <=sci-mathematics/coq-8.18 )
|
| 29 |
29 |
emacs? ( app-editors/emacs:* )
|
| 30 |
30 |
gtk? ( dev-ml/lablgtk:=[sourceview] )
|
| 31 |
31 |
html? ( dev-tex/hevea:= )
|
| 32 |
32 |
hypothesis-selection? ( dev-ml/ocamlgraph:= )
|
| 33 |
|
sexp? (
|
| 34 |
|
dev-ml/ppx_deriving:=[ocamlopt?]
|
| 35 |
|
dev-ml/ppx_sexp_conv:=[ocamlopt?]
|
| 36 |
|
dev-ml/sexplib:=[ocamlopt?]
|
| 37 |
|
)
|
|
33 |
dev-ml/ppx_deriving:=[ocamlopt?]
|
|
34 |
dev-ml/ppx_sexp_conv:=[ocamlopt?]
|
|
35 |
dev-ml/sexplib:=[ocamlopt?]
|
| 38 |
36 |
zarith? ( dev-ml/zarith:=[ocamlopt?] )
|
| 39 |
37 |
zip? ( dev-ml/camlzip:=[ocamlopt?] )
|
| 40 |
38 |
"
|
| ... | ... | |
| 51 |
49 |
PATCHES=(
|
| 52 |
50 |
"${FILESDIR}"/${PN}-2020-gentoo.patch
|
| 53 |
51 |
"${FILESDIR}"/${P}-flags.patch
|
| 54 |
|
"${FILESDIR}"/${P}-make.patch #Bug #883167
|
|
52 |
"${FILESDIR}"/${PN}-2021-make.patch #Bug #883167
|
| 55 |
53 |
"${FILESDIR}"/${PN}-2020-bibtex.patch
|
| 56 |
|
"${FILESDIR}"/${P}-sighandler.patch
|
|
54 |
"${FILESDIR}"/${P}-spark.patch
|
|
55 |
"${FILESDIR}"/${PN}-2021-sighandler.patch
|
| 57 |
56 |
)
|
| 58 |
57 |
|
| 59 |
58 |
QA_FLAGS_IGNORED=(
|
| ... | ... | |
| 74 |
73 |
|
| 75 |
74 |
src_prepare() {
|
| 76 |
75 |
find examples -name \*gz | xargs gunzip
|
|
76 |
sed -i \
|
|
77 |
-e 's:configure.in:configure.ac:g' \
|
|
78 |
Makefile.in || die
|
|
79 |
sed -i \
|
|
80 |
-e 's: effect: effekt:g' \
|
|
81 |
-e 's:(effect:(effekt:g' \
|
|
82 |
-e 's:\.effect:\.effekt:g' \
|
|
83 |
src/extract/mltree.ml \
|
|
84 |
src/extract/mltree.mli \
|
|
85 |
src/mlw/expr.ml \
|
|
86 |
src/mlw/expr.mli \
|
|
87 |
src/mlw/ity.ml \
|
|
88 |
src/mlw/ity.mli \
|
|
89 |
|| die
|
|
90 |
sed -i \
|
|
91 |
-e 's:Pervasives:Stdlib:g' \
|
|
92 |
src/gnat/gnat_loc.ml \
|
|
93 |
src/gnat/gnat_expl.ml \
|
|
94 |
|| die
|
|
95 |
mv configure.{in,ac} || die
|
| 77 |
96 |
eautoreconf
|
| 78 |
97 |
default
|
| 79 |
98 |
}
|
| ... | ... | |
| 83 |
102 |
--disable-pvs-libs
|
| 84 |
103 |
--disable-isabelle-libs
|
| 85 |
104 |
--enable-verbose-make
|
|
105 |
--enable-sexp
|
| 86 |
106 |
$(use_enable coq coq-libs)
|
| 87 |
107 |
$(use_enable doc)
|
| 88 |
108 |
$(use_enable emacs emacs-compilation)
|
| ... | ... | |
| 90 |
110 |
$(use_enable html html-pdf)
|
| 91 |
111 |
$(use_enable hypothesis-selection)
|
| 92 |
112 |
$(use_enable ocamlopt native-code)
|
| 93 |
|
$(use_enable sexp pp-sexp)
|
| 94 |
113 |
$(use_enable zarith)
|
| 95 |
114 |
$(use_enable zip)
|
| 96 |
115 |
)
|
| ... | ... | |
| 106 |
125 |
}
|
| 107 |
126 |
|
| 108 |
127 |
src_install() {
|
| 109 |
|
emake DESTDIR="${D}" -j1 install
|
| 110 |
|
emake DESTDIR="${D}" -j1 install-lib
|
| 111 |
128 |
emake DESTDIR="${D}" install_spark2014_dev
|
| 112 |
129 |
local cmdPath=/usr/$(get_libdir)/why3/commands
|
| 113 |
130 |
dosym ../why3server ${cmdPath}/why3server
|
| 114 |
131 |
# Remove duplicated files
|
| 115 |
132 |
for filename in config.cmxs ide.cmxs realize.cmxs server session.cmxs; do
|
| 116 |
133 |
if [[ -e "${D}"${cmdPath}/why3${filename} ]]; then
|
| 117 |
|
rm "${D}"${cmdPath}/why3${filename}
|
|
134 |
rm "${D}"${cmdPath}/why3${filename} || die
|
| 118 |
135 |
dosym ../../../bin/why3${filename} ${cmdPath}/why3${filename}
|
| 119 |
136 |
fi
|
| 120 |
137 |
done
|
