blob: ff918e6d5e4046f2af6c434498fab30b65838c66 (
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
|
# Copyright 1999-2025 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
ADA_COMPAT=( gcc_14 )
PYTHON_COMPAT=( python3_{10..13} pypy3 )
inherit ada python-any-r1 multiprocessing
commitId=ce5fad038790d5dc18f9b5345dc604f1ccf45b06
why3Id=fb4ca6cd8c7d888d3e8d281e6de87c66ec20f084
DESCRIPTION="Software development for high-reliability applications"
HOMEPAGE="http://libre.adacore.com"
SRC_URI="https://github.com/AdaCore/spark2014/archive/${commitId}.tar.gz
-> ${P}.tar.gz
http://mirror.koddos.net/gcc/releases/gcc-14.2.0/gcc-14.2.0.tar.xz"
S="${WORKDIR}"/spark2014-${commitId}
LICENSE="GPL-3"
SLOT="0"
KEYWORDS="~amd64 ~arm64"
IUSE="doc"
RDEPEND="
dev-ada/gnatcoll-core[${ADA_USEDEP},shared]
~dev-ada/gpr-24.2.0[${ADA_USEDEP}]
sci-mathematics/alt-ergo
sci-mathematics/why3-for-spark"
DEPEND="${RDEPEND}
dev-ada/gprbuild[${ADA_USEDEP}]"
BDEPEND="doc? (
$(python_gen_any_dep '
dev-python/sphinx[${PYTHON_USEDEP}]
dev-python/sphinx-rtd-theme[${PYTHON_USEDEP}]
')
)"
REQUIRED_USE="${ADA_REQUIRED_USE}"
PATCHES=( "${FILESDIR}"/${P}-gentoo.patch )
python_check_deps() {
python_has_version "dev-python/sphinx[${PYTHON_USEDEP}]" &&
python_has_version "dev-python/sphinx-rtd-theme[${PYTHON_USEDEP}]"
}
pkg_setup() {
use doc && python-any-r1_pkg_setup
ada_pkg_setup
}
src_prepare() {
ln -s "${WORKDIR}"/gcc-14.2.0/gcc/ada gnat2why/gnat_src || die
default
}
src_compile() {
emake -j1 -C gnat2why \
GPRARGS="-XLIBRARY_TYPE=relocatable -XBuild=Production -v" \
PROCS=$(makeopts_jobs)
gprbuild -j$(makeopts_jobs) -p -XLIBRARY_TYPE=relocatable -v \
-P gnatprove.gpr \
-largs ${LDFLAGS} -cargs ${ADAFLAGS} || die
if use doc; then
emake -C docs/lrm html
fi
}
src_install() {
dodir /usr/bin
dodir /usr/include/spark
dodir /usr/lib/spark
dodir /usr/share/spark/explain_codes
dodir /usr/share/spark/theories
dodir /usr/share/spark/runtimes
gcc -c -gnats spark2014vsn.ads -gnatet="${D}"/usr/bin/target.atp
insinto /usr/share/spark
doins share/spark/help.txt
doins -r share/spark/config
doins -r share/spark/explain_codes
insinto /usr/share/spark/theories
doins share/spark/theories/*why
doins share/spark/theories/*mlw
insinto /usr/share/spark/runtimes
doins share/spark/runtimes/README
insinto /usr/include/spark
doins src/spark/*.ad?
# Create the fake prover scripts to help extract benchmarks.
insinto /usr/libexec/spark/bin
doins benchmark_script/fake_*
dobin install/bin/gnatprove
exeinto /usr/libexec/spark/bin
doexe install/bin/gnat2why
doexe install/bin/spark_memcached_wrapper
doexe install/bin/spark_report
doexe install/bin/spark_semaphore_wrapper
use doc && HTML_DOCS=( docs/lrm/_build/html/* )
einstalldocs
}
|
