gentoo resync : 14.07.2018

8 files changed, 105 insertions, 14 deletions

diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz
index f415cee47683..7c4ec3675d15 100644
--- a/sci-mathematics/Manifest.gz
+++ b/sci-mathematics/Manifest.gz
diff --git a/sci-mathematics/calc/Manifest b/sci-mathematics/calc/Manifest
index f3a08fa4035a..9f10ce0c12d4 100644
--- a/sci-mathematics/calc/Manifest
+++ b/sci-mathematics/calc/Manifest
@@ -1,5 +1,4 @@
 AUX 2.12.4.0-ldflags.patch 4026 BLAKE2B 75aecbb3d8e3cc03ff8e2ef248d7b54adf7417c2de730fb8e1957a159e16d62b76a1116e08cfd13039a5770d216c962cd257f9ea07034ac6c2d1094dc8ba9bfe SHA512 d0e6ca66504962e9c6b037a598b06239475c8a1b2e9152945ebec70be60f3b4e43dfbec95ac46bcc15d79ea5f81622a499807d523ee3f4ffb2b1134a00829433
-AUX calc-2.12.2.2-libdir-fix.patch 570 BLAKE2B 20a50ab8c9c3715420f70e1fd83ac42db15543d7cb8de36563da1d2e00c787daf8a0f30e8be3885efa995dbbefecc59e64c7f7d29360c9c4f6b1a0c6f8cacfcb SHA512 ad15beeb3a52682e8119582b67abbecbe6de0aeac207b5cc88d085d986c34617b09e08678eae49a105577e415381ea99c6514a454d26c40cd77bfab8b375d79c
 AUX calc-2.12.4.13-prefix.patch 3189 BLAKE2B 888798c53afbbd85375ab01a0cbbf0e790de52f82481a4e26a1c54d349789662484e3def5a0d2fedb4c81bb36d7219f295354ea3cda33e1019cb5cd2928da61f SHA512 aedaf30a8837cc1ff545b502e60e3284e4d8df37dd9d98516fbed17788f3d9a497aa3ba66f4613bd237de6152c041b339f26c89ff20ccdc1fb15387f9dba166e
 AUX calc-2.12.5.4-as-needed.patch 6226 BLAKE2B cb75c4ffbc5fd916e6d94d00bd32f8170be6eb82f47f1fde3d2d5968853ac7c7719883844563df6b545aa7226b178f9f54f7adb89a843fdd9ab7b92701193276 SHA512 fd65cdc727b9859d8d1a55e4140bb74301dc1941f647f5d52026818a1da56f90d21eea26a578bfd4fb0988cb3c516985239e8a06a3de15a9109fbe77b9536466
 DIST calc-2.12.4.13.tar.bz2 970778 BLAKE2B 0e34df7d445a84de89e2c662ea7e8da4a350eaeef984b5027befe5947bf8e863180dd07bbe525c4bc04a6e3aa53bfbb2f3d719c8bfff3c238b16941b701d4b4d SHA512 7b7136c793917652ce2f2b3866b2db16a69dbead729d8a72b8c1359ebb8a4e1d4e7a3a8b214f8e85b9ccf41193ba6ffcb49926cc68f494e2b6cdff58559f2534
diff --git a/sci-mathematics/calc/files/calc-2.12.2.2-libdir-fix.patch b/sci-mathematics/calc/files/calc-2.12.2.2-libdir-fix.patch
deleted file mode 100644
index f265793ab871..000000000000
--- a/sci-mathematics/calc/files/calc-2.12.2.2-libdir-fix.patch
+++ /dev/null
@@ -1,12 +0,0 @@
-diff -Naur calc-2.12.2.2.old/Makefile calc-2.12.2.2/Makefile
---- calc-2.12.2.2.old/Makefile	2007-09-29 12:58:19.000000000 -0400
-+++ calc-2.12.2.2/Makefile	2007-10-24 06:40:10.000000000 -0400
-@@ -1131,7 +1131,7 @@
- BLD_TYPE= calc-dynamic-only
- #
- CC_SHARE= -fPIC
--DEFAULT_LIB_INSTALL_PATH= ${PWD}:/lib:/usr/lib:${LIBDIR}:/usr/local/lib
-+DEFAULT_LIB_INSTALL_PATH= /lib:/usr/lib:${LIBDIR}:/usr/local/lib
- LD_SHARE= "-Wl,-rpath,${DEFAULT_LIB_INSTALL_PATH}" \
-     "-Wl,-rpath-link,${DEFAULT_LIB_INSTALL_PATH}"
- LIBCALC_SHLIB= -shared "-Wl,-soname,libcalc${LIB_EXT_VERSION}"
diff --git a/sci-mathematics/glpk/Manifest b/sci-mathematics/glpk/Manifest
index 96ee6c8b58d6..f5e9c215c6fa 100644
--- a/sci-mathematics/glpk/Manifest
+++ b/sci-mathematics/glpk/Manifest
@@ -1,4 +1,4 @@
 AUX glpk-4.63-debundle-system-libs.patch 2240 BLAKE2B 5bd0d25768682a410159e3bf0eaf83dc038da8c6bda275c6994846516bb347caf6d4ea726e8635c77b84a463cb1ec32955f573589291486067c651a88d7f276c SHA512 186c1dd2197119b376a76a2db9a73d7fc1e43adc6ae54f5d3e39ad9114a9a406d45dd7bce4bcea31cfce94e71234b70872db22378e8312026912a93077488805
 DIST glpk-4.63.tar.gz 4131787 BLAKE2B 791fa1a1424011668019e180fc245c0319f601255f596affe87afa0df47d9d615a8accd794d51c15bff5fe4fe6409369362f6c9e82bdde67903177b8da55e891 SHA512 3ee9b9ec5322282a9c62b2ee209fc7760383a6a764ef3816445ffb66f15ed4d00309bff1b98d50c243b58aa74f83072afde45c389799e637e11e86f4db45276c
-EBUILD glpk-4.63.ebuild 1370 BLAKE2B dbccbe5e61a11564984550cf1f39f0658b0201442e0330b292468afd5212780a803e72b0c81ac91c9657cdc986d0efb5b6655724ec741afaba1a6dcfb4d2782b SHA512 a6661f6f70dbdd0d47bd37029b9b23c0227554cc76538a8f29a721e2543ab38c45e562585910093398bdf6feeea5e20d5ec94c96cb8af674057bdb60b15ff08d
+EBUILD glpk-4.63.ebuild 1482 BLAKE2B 481b980c053570f4c01fcd01ed1f25795afe60b17b3fa9dc2b81016658322bfa9f77b25a416c5a703ca5a2f207e7384664bb7ecd3acb1b8851b4014868307ec3 SHA512 5f6724c325437111f9d8ecfee98080c753104bbb546b7b9bec170321560c09a0d052d30dcca70ae595dc63092d04931ba68eafe20d7f6dbe6fd886fcebd0b573
 MISC metadata.xml 668 BLAKE2B 9dec50a5d6aa33f108651ed8fd891750fc8146eedf8df28abc0fa04a6db2f0d590073fe3606c658a99d56d283d7a24629503bbf11f6593ef1b90314d26a1ab69 SHA512 0c37b2854097a14a58070b1651ccdcdfae652e7d2b5afd62c617e22fa0256acee07aab0409f6621382151e1fb5e605002a3a809113693b2078054a4b16e72452
diff --git a/sci-mathematics/glpk/glpk-4.63.ebuild b/sci-mathematics/glpk/glpk-4.63.ebuild
index 4721b1832852..b32475f03a75 100644
--- a/sci-mathematics/glpk/glpk-4.63.ebuild
+++ b/sci-mathematics/glpk/glpk-4.63.ebuild
@@ -29,6 +29,7 @@ PATCHES=(
 )
 
 src_prepare() {
+	sed -e 's#CPPFLAGS="-I/usr/include/mysql#CPPFLAGS="-I'"${EPREFIX}"'/usr/include/mysql#' -i configure.ac || die
 	use odbc && [[ -z $(type -P odbc_config) ]] && \
 		append-cppflags $($(tc-getPKG_CONFIG) --cflags libiodbc)
 
diff --git a/sci-mathematics/why3-for-spark/Manifest b/sci-mathematics/why3-for-spark/Manifest
index d1fd3138ac77..acf43503242f 100644
--- a/sci-mathematics/why3-for-spark/Manifest
+++ b/sci-mathematics/why3-for-spark/Manifest
@@ -1,4 +1,7 @@
 AUX why3-for-spark-2017-gentoo.patch 1300 BLAKE2B 616ed7cf1d5c8494a0b9f724ef1b011ad51e9f7edfb8bc88892902ad0cdc23793c8f8cd0e491757be08d90cb1159878d8bd3a34e1ebba62c927b9f676f58c241 SHA512 7ec992b1d0f0f285903b69876b853a8d368c73f4ed3dfccc25f5ae18e72e0c6f71ce9b81e18f2a685d19a7bfa8e69571cb71d4faa5ec67e0fbf2231202c2ea3d
+AUX why3-for-spark-2018-gentoo.patch 1015 BLAKE2B 201846ae0ef17bc6d777b7c1a8baddd1f684e82b811b16d2cce447423189a899f3e599cbf5cbd01630e2b246f8257ba5a890b20aaf62b0c1bc24e46642a37600 SHA512 871534c90f4f7c680f07dcd0bcacc4ce75c43b3132e8570b73e66316fe4333c244b9c443998916af7ff8fd297c20f7079ec5e8bf4c97207d0b7537722cd010a6
 DIST why3-for-spark-gpl-2017-src.tar.gz 9248235 BLAKE2B d9eb7201dfd5962c88ac8995e3cd800bf318f575a5e6ff7d0219941c0f0c9052e6b2c95c7c16fcd81b90cac647d503041bf16560bd44b58e7e0ced1ef2314bd2 SHA512 8f444402f6c1744cd7c565117732935791b1ae7996a94314c40a66d125eae8a81f2257314246c94fd29d3cd16abcff6a50a152a1191a4aae39a2c8a8d7c3b9e1
+DIST why3-for-spark-gpl-2018-src.tar.gz 7682767 BLAKE2B 0b0272ca4d5519ca402990b234d0847378bcd2a0949fea78ea10e355233a16aebe79b938cdf8e4daadabb909171cab83b9d6ccacf9f2dc1c0b57bb6da6fd1fe0 SHA512 fc798acf343484fd8e70f470a318753c9a0e9967ff579f20ec185bf3c2a75e7a4a556388fc86a378610ce4a467f3e722c6f610da34d4c33bc3d6b10551731f07
 EBUILD why3-for-spark-2017.ebuild 1797 BLAKE2B 8ca7d6ea2787bbe271924d1cecb1807da5c26f7e6342cac62c53d3c9f451c21eb892b8528900ea61fc54aa00bf5fa503dc4a77c7a13fcfceb342c6344d7d3bdc SHA512 b033c9f507637dfd10b759f9f7ffe89a1e7516d43fba2b1ad5e2cf4769d61fce9c6c61c6743ef54f5277994e9aec1656c981eac540b777d085232bcb79d2bd37
+EBUILD why3-for-spark-2018.ebuild 1709 BLAKE2B ed0f018d0025ef7d7c01624eb21387fb2ba506d3a5c08012ad9ec01afd8cacc2f4e2525ba197dc2308584a9e7cc931a7286844459c299385aebeb6e1394327e9 SHA512 a61b98a07a0e939be7ef65266df80be84e898dda3342d51c2e135300a1f3030b6b660de71023b3007805adc1a5ab016c652c05787380ee4e25c3a4599db76339
 MISC metadata.xml 1363 BLAKE2B 820bfc974ca6984f78340f223f8f19d12f0313016118110a35cfe149129c2dc189d6f03f34bf3d30c9d3e5d9c9ab90bba33dca4320c034821a7a89f97b92a7f9 SHA512 ee8323cc37fdea800e355fc14ba67cac66c3ec3c41528d481a7e938b1d3e23859bdddfb06d3b6653725cdcfcc0d07e66ba1d3cc80b3637a781db7bab5f7dc677
diff --git a/sci-mathematics/why3-for-spark/files/why3-for-spark-2018-gentoo.patch b/sci-mathematics/why3-for-spark/files/why3-for-spark-2018-gentoo.patch
new file mode 100644
index 000000000000..9d7165cbed78
--- /dev/null
+++ b/sci-mathematics/why3-for-spark/files/why3-for-spark-2018-gentoo.patch
@@ -0,0 +1,25 @@
+--- why3-for-spark-gpl-2017-src/src/gnat/gnat_config.ml.old	2017-10-18 09:07:03.118919785 +0200
++++ why3-for-spark-gpl-2017-src/src/gnat/gnat_config.ml	2017-10-18 09:07:45.198216939 +0200
+@@ -12,10 +12,7 @@
+   | Limit_Check of Gnat_expl.check
+   | Limit_Line of Gnat_loc.loc
+ 
+-let spark_prefix =
+-  (Filename.dirname
+-          (Filename.dirname (Filename.dirname
+-          (Filename.dirname Sys.executable_name))))
++let spark_prefix = "/usr"
+ 
+ let rec file_concat l =
+   match l with
+--- why3-for-spark-gpl-2017-src/src/coq-tactic/why3tac.ml4.old	2017-10-26 22:25:55.289094778 +0200
++++ why3-for-spark-gpl-2017-src/src/coq-tactic/why3tac.ml4	2017-10-26 22:26:10.719807270 +0200
+@@ -1352,7 +1352,7 @@
+     let limit =
+     { Call_provers.empty_limit with Call_provers.limit_time = timelimit } in
+     let call = Driver.prove_task ~command ~limit drv !task in
+-    wait_on_call call
++    wait_on_call (ServerCall call)
+   with
+     | NotFO ->
+         if debug then Printexc.print_backtrace stderr; flush stderr;
diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
new file mode 100644
index 000000000000..e766cce4ade3
--- /dev/null
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
@@ -0,0 +1,75 @@
+# Copyright 1999-2018 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=6
+
+inherit autotools
+
+MYP=${PN}-gpl-${PV}-src
+
+DESCRIPTION="Platform for deductive program verification"
+HOMEPAGE="http://why3.lri.fr/"
+SRC_URI="http://mirrors.cdn.adacore.com/art/5b0819dec7a447df26c27a43
+	-> ${MYP}.tar.gz"
+
+LICENSE="GPL-3"
+SLOT="0"
+KEYWORDS="~amd64"
+IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt profiling zarith zip"
+RESTRICT=strip
+
+DEPEND=">=dev-lang/ocaml-4.02.3[ocamlopt?]
+	dev-ml/menhir
+	coq? ( sci-mathematics/coq )
+	doc? ( dev-tex/rubber )
+	gtk? ( dev-ml/lablgtk[sourceview] )
+	emacs? ( app-editors/emacs:* )
+	html? ( dev-tex/hevea )
+	hypothesis-selection? ( dev-ml/ocamlgraph )
+	zarith? ( dev-ml/zarith )
+	zip? ( >=dev-ml/camlzip-1.07 )"
+RDEPEND="${DEPEND}"
+
+S="${WORKDIR}"/${MYP}
+
+PATCHES=( "${FILESDIR}"/${P}-gentoo.patch )
+
+REQUIRED_USE="html? ( doc )"
+
+src_configure() {
+	econf \
+		--disable-pvs-libs \
+		--disable-isabelle-libs \
+		$(use_enable coq coq-libs) \
+		$(use_enable coq coq-tactic) \
+		$(use_enable doc) \
+		$(use_enable emacs emacs-compilation) \
+		$(use_enable gtk ide) \
+		$(use_enable html html-doc) \
+		$(use_enable hypothesis-selection) \
+		$(use_enable ocamlopt native-code) \
+		$(use_enable profiling) \
+		$(use_enable zarith) \
+		$(use_enable zip)
+}
+
+src_compile() {
+	emake -j1
+	if use ocamlopt; then
+		emake byte
+	fi
+	use doc && emake doc
+}
+
+src_install() {
+	emake DESTDIR="${D}" -j1 install
+	emake DESTDIR="${D}" -j1 install-lib
+	emake DESTDIR="${D}" install_spark2014_dev
+	einstalldocs
+	docompress -x /usr/share/doc/${PF}/examples
+	dodoc -r examples
+	if use doc; then
+		dodoc doc/manual.pdf
+		use html && dodoc -r doc/html
+	fi
+}