aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--dev-libs/simclist/ChangeLog8
-rw-r--r--dev-libs/simclist/Manifest3
-rw-r--r--dev-libs/simclist/metadata.xml17
-rw-r--r--dev-libs/simclist/simclist-1.6.ebuild6
-rw-r--r--dev-ml/mlgmpidl/ChangeLog2
-rw-r--r--dev-ml/mlgmpidl/Manifest4
-rw-r--r--dev-ml/mlgmpidl/metadata.xml23
-rw-r--r--dev-ml/mlgmpidl/mlgmpidl-1.1.ebuild6
-rw-r--r--dev-ml/ocamlgraph/ChangeLog22
-rw-r--r--dev-ml/ocamlgraph/Manifest6
-rw-r--r--dev-ml/ocamlgraph/metadata.xml47
-rw-r--r--dev-ml/ocamlgraph/ocamlgraph-1.8.5.ebuild (renamed from dev-ml/ocamlgraph/ocamlgraph-1.8.2.ebuild)14
-rw-r--r--dev-ml/zarith/ChangeLog9
-rw-r--r--dev-ml/zarith/Manifest5
-rw-r--r--dev-ml/zarith/metadata.xml20
-rw-r--r--dev-ml/zarith/zarith-1.1.ebuild41
-rw-r--r--dev-ml/zarith/zarith-1.2.1.ebuild40
-rw-r--r--sci-mathematics/alt-ergo/ChangeLog21
-rw-r--r--sci-mathematics/alt-ergo/Manifest5
-rw-r--r--sci-mathematics/alt-ergo/alt-ergo-0.95.2.ebuild35
-rw-r--r--sci-mathematics/alt-ergo/metadata.xml22
-rw-r--r--sci-mathematics/apron/ChangeLog14
-rw-r--r--sci-mathematics/apron/Manifest6
-rw-r--r--sci-mathematics/apron/apron-0.9.10-r1.ebuild79
-rw-r--r--sci-mathematics/apron/apron-0.9.10.ebuild6
-rw-r--r--sci-mathematics/apron/metadata.xml31
-rw-r--r--sci-mathematics/flocq/ChangeLog14
-rw-r--r--sci-mathematics/flocq/Manifest5
-rw-r--r--sci-mathematics/flocq/flocq-2.1.0.ebuild21
-rw-r--r--sci-mathematics/flocq/flocq-2.3.0.ebuild36
-rw-r--r--sci-mathematics/flocq/metadata.xml17
-rw-r--r--sci-mathematics/frama-c/ChangeLog28
-rw-r--r--sci-mathematics/frama-c/Manifest7
-rw-r--r--sci-mathematics/frama-c/files/frama-c-make.patch12
-rw-r--r--sci-mathematics/frama-c/files/frama-c-ocaml-4.01.patch145
-rw-r--r--sci-mathematics/frama-c/files/ocamlgraph185_compat.patch254
-rw-r--r--sci-mathematics/frama-c/frama-c-20130601.ebuild65
-rw-r--r--sci-mathematics/frama-c/frama-c-20140301.ebuild (renamed from sci-mathematics/frama-c/frama-c-20120901.ebuild)29
-rw-r--r--sci-mathematics/frama-c/metadata.xml28
-rw-r--r--sci-mathematics/gappa/ChangeLog32
-rw-r--r--sci-mathematics/gappa/Manifest5
-rw-r--r--sci-mathematics/gappa/gappa-1.0.0.ebuild37
-rw-r--r--sci-mathematics/gappa/gappa-1.1.1.ebuild42
-rw-r--r--sci-mathematics/gappalib-coq/ChangeLog30
-rw-r--r--sci-mathematics/gappalib-coq/Manifest5
-rw-r--r--sci-mathematics/gappalib-coq/files/gappalib-coq-coq84.patch71
-rw-r--r--sci-mathematics/gappalib-coq/gappalib-coq-0.18.0.ebuild35
-rw-r--r--sci-mathematics/gappalib-coq/gappalib-coq-1.0.0.ebuild35
-rw-r--r--sci-mathematics/giac/ChangeLog15
-rw-r--r--sci-mathematics/giac/Manifest5
-rw-r--r--sci-mathematics/giac/giac-1.1.0.ebuild (renamed from sci-mathematics/giac/giac-1.0.0.ebuild)37
-rw-r--r--sci-mathematics/giac/metadata.xml24
-rw-r--r--sci-mathematics/ltl2ba/Manifest3
-rw-r--r--sci-mathematics/ltl2ba/ltl2ba-1.1.ebuild4
-rw-r--r--sci-mathematics/ltl2ba/metadata.xml3
-rw-r--r--sci-mathematics/pff/ChangeLog17
-rw-r--r--sci-mathematics/pff/Manifest3
-rw-r--r--sci-mathematics/pff/metadata.xml17
-rw-r--r--sci-mathematics/pff/pff-8.4.ebuild18
-rw-r--r--sci-mathematics/why/ChangeLog19
-rw-r--r--sci-mathematics/why/Manifest6
-rw-r--r--sci-mathematics/why/files/why-2.30.patch36
-rw-r--r--sci-mathematics/why/files/why-flocq23.patch11
-rw-r--r--sci-mathematics/why/metadata.xml35
-rw-r--r--sci-mathematics/why/why-2.30.ebuild73
-rw-r--r--sci-mathematics/why/why-2.34.ebuild66
-rw-r--r--sci-mathematics/why3/ChangeLog7
-rw-r--r--sci-mathematics/why3/Manifest4
-rw-r--r--sci-mathematics/why3/metadata.xml23
-rw-r--r--sci-mathematics/why3/why3-0.83.ebuild55
70 files changed, 1087 insertions, 839 deletions
diff --git a/dev-libs/simclist/ChangeLog b/dev-libs/simclist/ChangeLog
index 92a97991a..2184e626b 100644
--- a/dev-libs/simclist/ChangeLog
+++ b/dev-libs/simclist/ChangeLog
@@ -2,14 +2,14 @@
# Copyright 1999-2012 Gentoo Foundation; Distributed under the GPL v2
# $Header: $
- 17 Mar 2012; J.-C. Demay <jcdemay@gmail.com>
+ 17 Mar 2012; Jonathan-Christofer Demay <jcdemay@gmail.com>
-simclist-1.5.ebuild, +simclist-1.6.ebuild:
version bump
-
- 24 Nov 2010; J.-C. Demay <jcdemay@gmail.com>
+
+ 24 Nov 2010; Jonathan-Christofer Demay <jcdemay@gmail.com>
-simclist-1.4.4_rc4.ebuild, +simclist-1.5.ebuild:
version bump
-
+
23 Jun 2010; Andreas K. Huettel (dilfridge) <mail@akhuettel.de>
simclist-1.4.4_rc3.ebuild:
QA fixes
diff --git a/dev-libs/simclist/Manifest b/dev-libs/simclist/Manifest
index edd77050a..7acf87ae8 100644
--- a/dev-libs/simclist/Manifest
+++ b/dev-libs/simclist/Manifest
@@ -1 +1,4 @@
DIST simclist-1.6.tar.bz2 44280 SHA256 63b47211215466ddfba1643582cb3aaa7b5e9ca1cc5f247290e3199c4e29f147
+EBUILD simclist-1.6.ebuild 814 SHA256 9ac9188534ad3990ec55dcc78aa8e9515e007fc62253bf3bb77ae6071c153937 SHA512 0b2ef20c083dd7169c44285d68897616cc4da7eb4868163dd91f422ce210bd535c032e3d1012ef643472e27a5a41838e990464be2e9d7db256579519aea66ba3 WHIRLPOOL 46f4ae3fac5fb2fbffe9930b32759d3bff44fe2a6a4eca617fc8d757aa1f9799f3d491010df6a3930299c2c2b65a088735281291cffb76400c76b91ab7dace23
+MISC ChangeLog 599 SHA256 aa1ef92eac7b1c44e251691bddbca45fbe6d938b332e268a1389d7866dff4463 SHA512 452658e17bb276b9c80c9ef051111248529daeaf0be9bd7a5712acb4c89d1046f4f72b5d9a9beedea10f18887eec6f9de2e30684778741f7c25cf47e8274b85d WHIRLPOOL c3265ac6af1e707555a5898e8592808bd006dfd5a9068a05de26bb6893473b38fb0998808890a77de7890fbeae66b256185cd9b6f0f80175d565cfbea6c5d9a1
+MISC metadata.xml 535 SHA256 cabdc9cb6f6bc4af60eb13a5bac8a914354fef222730840e051c42ab5f70bba0 SHA512 a33e71708bc18a62fd1009eddc60c3930ab5b81b806f921b2eeddd706c6b0887bdc831df819774fbab2c305f3c6a5289e167e89fe89bb5e555446a18a7611f3c WHIRLPOOL 5955a3f3b3d09938dab20f2b2a23c9c6a1ffc540904129c2f34308761758b6a07571ff414c90879fb705dd8262826b3181b0f655c88ef8aa2265231f9fbb59cf
diff --git a/dev-libs/simclist/metadata.xml b/dev-libs/simclist/metadata.xml
index 1da3891dc..49fb6b89c 100644
--- a/dev-libs/simclist/metadata.xml
+++ b/dev-libs/simclist/metadata.xml
@@ -1,11 +1,14 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
<pkgmetadata>
-<herd>sci</herd>
-<longdescription>
- SimCList is a high quality C (C++ embeddable) library for handling
- lists. It exploits several advanced techniques for improving
- performance, including freelists, sentinels, automatic sort algorithm
- selection, sort randomization, mid pointer and optional multithreading.
-</longdescription>
+ <herd>sci</herd>
+ <longdescription>
+ SimCList is a high quality C (C++ embeddable) library for handling
+ lists. It exploits several advanced techniques for improving
+ performance, including freelists, sentinels, automatic sort algorithm
+ selection, sort randomization, mid pointer and optional multithreading.
+ </longdescription>
+ <maintainer>
+ <email>sci@gentoo.org</email>
+ </maintainer>
</pkgmetadata>
diff --git a/dev-libs/simclist/simclist-1.6.ebuild b/dev-libs/simclist/simclist-1.6.ebuild
index aecf21fd5..0df95c3a4 100644
--- a/dev-libs/simclist/simclist-1.6.ebuild
+++ b/dev-libs/simclist/simclist-1.6.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2014 Gentoo Foundation
+# Copyright 1999-2012 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Header: $
@@ -6,13 +6,13 @@ EAPI=3
inherit cmake-utils
-DESCRIPTION="SimCList is a high quality C (C++ embeddable) library for handling lists."
+DESCRIPTION="SimCList is a high quality C (C++ embeddable) library for handling lists"
HOMEPAGE="http://mij.oltrelinux.com/devel/simclist"
SRC_URI="${HOMEPAGE}/${P/_/}.tar.bz2"
LICENSE="BSD"
SLOT="0"
-KEYWORDS="~amd64 ~ppc ~sparc ~x86"
+KEYWORDS="~amd64 ~x86"
IUSE="doc examples"
S="${WORKDIR}/${P/_/}"
diff --git a/dev-ml/mlgmpidl/ChangeLog b/dev-ml/mlgmpidl/ChangeLog
index 7fb3a3c06..0b8e69c49 100644
--- a/dev-ml/mlgmpidl/ChangeLog
+++ b/dev-ml/mlgmpidl/ChangeLog
@@ -2,7 +2,7 @@
# Copyright 1999-2010 Gentoo Foundation; Distributed under the GPL v2
# $Header: $
- 03 Jul 2010; J.-C. Demay <jcdemay@gmail.com>
+ 03 Jul 2010; Jonathan-Christofer Demay <jcdemay@gmail.com>
mlgmpidl-1.1.ebuild, +files/mlgmpidl-1.1-mpfr-3_compat.patch:
dev-libs/mpfr-3.0.0 compatibility
diff --git a/dev-ml/mlgmpidl/Manifest b/dev-ml/mlgmpidl/Manifest
index e3fb55977..81f2b7f30 100644
--- a/dev-ml/mlgmpidl/Manifest
+++ b/dev-ml/mlgmpidl/Manifest
@@ -1 +1,5 @@
+AUX mlgmpidl-1.1-mpfr-3_compat.patch 496 SHA256 d888a1ad0930895ef2ec83bef6eef5a39ed18a38aa3a637f33b61b9a20d19e2b SHA512 b4979e4dbf1cc5aa1fba5ffb08557c6c32d16e4d2c3ae1fc14d999e52231efb344524e1dc2d6612021a0b4dba4b5f6d1394316abff4698f58d5decc3ff417cbf WHIRLPOOL a3f1c218c2de8413042f56f1de2a6257a895a44edd16daa0e301a20426da0c0275685e440d039d8db39b79853617c54b68002c4d5dd2b63a9d22a9341d987a7d
DIST mlgmpidl-1.1.tgz 194002 SHA256 8990a56f4c1ff701bb922bacf7f23b40539d123216ac5f9fe0f35967735d6fc9
+EBUILD mlgmpidl-1.1.ebuild 1311 SHA256 756c0655b0045c2e8c2c4072f113023dd70d6e27dd31059db234df7ca586d188 SHA512 493266916193940b1701aea85cbb447e154820113b87ec87319d3ffd11689c08b3a77d5fd8e8c9290b05141ac83707f68ff97e2ba6b5050796b58aa11bc68c1e WHIRLPOOL 1861032f03cf71ec5c6d025c0f2f17964cf07822425d8fca1d1e19c1755ee9d985bc689f49ce123ebdd95f1b682c1c1a00d818900cb6ddae3cf550ae2596010d
+MISC ChangeLog 394 SHA256 ec34f25ee458e0ce79b7209a31cfbb9e40975cc3e22e7b97fc9fc57372c9a549 SHA512 eafca747c958cb036ae7dfbd068d8be9c6db76342d42d458c886fc8dc1677d6b5d9bb758da7e138bc89c87816a58ddc50eabf115b5b9a41dfdca8ff3d5bd73eb WHIRLPOOL da7983220947c85972e778061bff3b0612a2de7a39a343a88ef204a6235050b32b8b3a791f485ba187b819f97adb88811c7437cc47096b5f723644ffabd3364b
+MISC metadata.xml 629 SHA256 c430bdc6e03131ed1ce7f991f1ad0d9fd641be877a5bd089da1179fa8d10eb1a SHA512 a5c827b6e812cc96befabb965377723eae2468e8d7ad8f3ae00c6c3ad70d459301225b8f76105ed8f02bdd2f261407b4d2dbd4fab1b1d17806fba0d14f1663b2 WHIRLPOOL 1fb51759a7409d3d3cc8178c3f4db215fb7fbb350bbe6c5314292f303749f1a655bcf0375c3960e9d86506a7981bbede2b9d2beffb5bd2fe861d02a9c7b081d9
diff --git a/dev-ml/mlgmpidl/metadata.xml b/dev-ml/mlgmpidl/metadata.xml
index a3fac8132..c6107f8e5 100644
--- a/dev-ml/mlgmpidl/metadata.xml
+++ b/dev-ml/mlgmpidl/metadata.xml
@@ -1,14 +1,17 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
<pkgmetadata>
-<herd>sci-mathematics</herd>
-<longdescription>
- MLGMPIDL is a package offering an interface to the GMP and MPFR
- libraries for OCaml version 3.07 or higher. The interface offers access
- to almost all the functions of the library, and is decomposed into 7
- submodules.
-</longdescription>
-<use>
- <flag name="mpfr">Add support for <pkg>dev-libs/mpfr</pkg></flag>
-</use>
+ <herd>sci</herd>
+ <longdescription>
+ MLGMPIDL is a package offering an interface to the GMP and MPFR
+ libraries for OCaml version 3.07 or higher. The interface offers access
+ to almost all the functions of the library, and is decomposed into 7
+ submodules.
+ </longdescription>
+ <maintainer>
+ <email>sci@gentoo.org</email>
+ </maintainer>
+ <use>
+ <flag name="mpfr">add support for mpfr, the library for multiple-precision floating-point computations with exact rounding</flag>
+ </use>
</pkgmetadata>
diff --git a/dev-ml/mlgmpidl/mlgmpidl-1.1.ebuild b/dev-ml/mlgmpidl/mlgmpidl-1.1.ebuild
index a2bf2eec4..6efca0c5f 100644
--- a/dev-ml/mlgmpidl/mlgmpidl-1.1.ebuild
+++ b/dev-ml/mlgmpidl/mlgmpidl-1.1.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2014 Gentoo Foundation
+# Copyright 1999-2010 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Header: $
@@ -12,7 +12,7 @@ SRC_URI="https://gforge.inria.fr/frs/download.php/20228/${PN}-${PV}.tgz"
LICENSE="LGPL-2"
SLOT="0"
-KEYWORDS="~amd64 ~ppc ~x86"
+KEYWORDS="~amd64 ~x86"
IUSE="doc +mpfr"
DEPEND=">=dev-lang/ocaml-3.09
@@ -49,7 +49,7 @@ src_compile() {
}
src_install(){
- emake install DESTDIR="${D}" || die "emake install failed"
+ DESTDIR="${D}" emake install || die "emake install failed"
dodoc README
if use doc; then
diff --git a/dev-ml/ocamlgraph/ChangeLog b/dev-ml/ocamlgraph/ChangeLog
index 18e109637..42f0c5b82 100644
--- a/dev-ml/ocamlgraph/ChangeLog
+++ b/dev-ml/ocamlgraph/ChangeLog
@@ -1,24 +1,32 @@
# ChangeLog for dev-ml/ocamlgraph
-# Copyright 1999-2013 Gentoo Foundation; Distributed under the GPL v2
+# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2
# $Header: $
- 14 Jan 2013; J.-C. Demay <jcdemay@gmail.com>
- +ocamlgraph-1.8.2.ebuild, +ocamlgraph-1.8.1.ebuild:
+ 21 Jun 2014; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -ocamlgraph-1.8.3.ebuild, +ocamlgraph-1.8.5.ebuild:
version bump
- 21 Dec 2011; J.-C. Demay <jcdemay@gmail.com>
+ 10 Jan 2014; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -ocamlgraph-1.8.2.ebuild, +ocamlgraph-1.8.3.ebuild:
+ version bump
+
+ 14 Jan 2013; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -ocamlgraph-1.8.1.ebuild, +ocamlgraph-1.8.2.ebuild:
+ version bump
+
+ 21 Dec 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
-ocamlgraph-1.7.ebuild, +ocamlgraph-1.8.1.ebuild:
version bump
- 06 May 2011; J.-C. Demay <jcdemay@gmail.com>
+ 06 May 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
-ocamlgraph-1.6.ebuild, +ocamlgraph-1.7.ebuild:
version bump
- 13 Jul 2010; J.-C. Demay <jcdemay@gmail.com>
+ 13 Jul 2010; Jonathan-Christofer Demay <jcdemay@gmail.com>
-files/ocamlgraph-1.5-makefile.patch, +files/ocamlgraph-makefile.patch, -ocamlgraph-1.5.ebuild, +ocamlgraph-1.6.ebuild:
version bump
- 04 Jul 2010; J.-C. Demay <jcdemay@gmail.com>
+ 04 Jul 2010; Jonathan-Christofer Demay <jcdemay@gmail.com>
-files/ocamlgraph-1.2-makefile.patch, +files/ocamlgraph-1.5-makefile.patch, -ocamlgraph-1.2.ebuild, +ocamlgraph-1.5.ebuild:
version bump
diff --git a/dev-ml/ocamlgraph/Manifest b/dev-ml/ocamlgraph/Manifest
index 4b4f6d4f0..123489c97 100644
--- a/dev-ml/ocamlgraph/Manifest
+++ b/dev-ml/ocamlgraph/Manifest
@@ -1 +1,5 @@
-DIST ocamlgraph-1.8.2.tar.gz 249253 SHA256 e54ae60cd977a032854166dad56348d0fb76c6cd8e03e960af455268f0c8b5a6 SHA512 93995dbacc571569a3f168ae141808ac5053ad895ad3ee4dddd311f1e5b3123a8096a5a4b4d10695b5c02d41efa15a92c425987836a5db6ef6469ef77cd23750 WHIRLPOOL 7d36a4b33fb1e981b5ae7b94627de918ad60610ecc8f364b1895593da98f78cfdb606325e862534ecdb9ef53b00de50d31df1e67a5e4fa5325327d8d1e4588a8
+AUX ocamlgraph-makefile.patch 1564 SHA256 c36612f740033a3d158f5d2a458697b1a41dacf2d1964484c1fd0c0f39fd276b SHA512 a0251220741069e729ffebdf7d9f2b3f02119dec48c09321cc9cbc8b82286d4081ccd89dbe5c1fe634ea415aa5e48d162f522ce6509812847dba2909c7572adb WHIRLPOOL 56765554649d5e5d38016ad22183b7b0d46c3780beeffb7f79d46c30e33967a3fd5f8ed92335dd8b5dd727743d25d8975c52d839817e276d13f595b25b7d82f4
+DIST ocamlgraph-1.8.5.tar.gz 269438 SHA256 d167466435a155c779d5ec25b2db83ad851feb42ebc37dca8ffa345ddaefb82f SHA512 e3bf7f43f7b5167cbd23ea44a510d1a569d35771882ab7ae83bacc73822c5f4c944f62c95e0efa813b765e1e385a6b3ebff342cbf1c5589c73d022b8591a52dc WHIRLPOOL d25e124c2814e3196a441e706ca91a0429ab48669309c5dec2ae6697e48064ce54efc9d24440d9e52f3a1af8cfdd5c3ae04cd549fde4e9abc860a3506bd2de8d
+EBUILD ocamlgraph-1.8.5.ebuild 1086 SHA256 3f0b493eb204938e5fbe27db188f1c0d2aaf697a78d1964178e79d2eac5a27e2 SHA512 cc8bf450cfd95177d417e638ad082f7f13a84bf7f0b2059ab5aa10b63d4ad3e87998b35c6d4fca6714bb981ea08180b77c2297e8b74693f93968d74bcd31346e WHIRLPOOL 205b37506e016e9f27158720ea828a71000dfeafa2da331a0145cb524abb27517e7053ee13afb6239ea7c2bd0aef0967872b8cc9eb86fafb188399a6ba8ceb14
+MISC ChangeLog 1288 SHA256 e6b9aa482e6272815905a96ebeb959b8333947336de304fc75ed8bc1bc3ba361 SHA512 7718a1990e660bf8f5194b7aa3a1b7bf0203b27f35c9e6d614cd8fecf055d1a92072ae1829148b98322dce8f6ea5c13112d30a58bf97396ae5a283dcb60edf47 WHIRLPOOL ebfc633797de5dfe2952c5e07d8edfa3d3dfe009bda6e5fc505c7054a152a205e32bca24ddef2a403ebacc8a2afb65c531da8fc5b6d61d6d19ccfc1b1358c7c3
+MISC metadata.xml 1550 SHA256 cf29ffe695398a61363b2f993b7e904ae259447488f14e072f77a098798ed1e0 SHA512 a824c62089e03b1c8936930100b893b25706cbcb5747e218d72120332e14597f2823ac1da64b59a62637d66295679202eb7142867145e2ae28b0667492587103 WHIRLPOOL a91552ca140d206fb80768b25999f38047e8a82904a949c724ba188c8682222709dd9cb3ec3b662c8573b568a97d64e3a64b4dfeb415d212ab6d94209b0f6a78
diff --git a/dev-ml/ocamlgraph/metadata.xml b/dev-ml/ocamlgraph/metadata.xml
index 87fc10d58..763c1cd36 100644
--- a/dev-ml/ocamlgraph/metadata.xml
+++ b/dev-ml/ocamlgraph/metadata.xml
@@ -1,23 +1,32 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
<pkgmetadata>
-<herd>sci-mathematics</herd>
-<longdescription>
- It provides an easy-to-use graph data structure together with several
- operations and algorithms over graphs, in Graph.Pack. It is a reasonably
- efficient imperative data structure for directed graphs with vertices
- and edges labeled with integers. Several other graph implementations
- are proposed for those not satisfied with the one above. Some are
- persistent (imutable) and other imperative (mutable). Some are directed
- and other are not. Some have labels for vertices, or labels for edges,
- or both. Some have abstract types for vertices. etc. These
- implementations are written as functors: you give the types of vertices
- labels, edge labels, etc. and you get the data structure as a result.
- it also provides several classic operations and algorithms over graphs.
- They are also written as functors i.e. independently of the data
- structure for graphs. One consequence is that you can define your own
- data structure for graphs and yet re-use all the algorithms from this
- library: you only need to provide a few operations such as iterating
- over all vertices, over the successors of a vertex, etc.
-</longdescription>
+ <herd>sci</herd>
+ <longdescription>
+ It provides an easy-to-use graph data structure together with several
+ operations and algorithms over graphs, in Graph.Pack. It is a reasonably
+ efficient imperative data structure for directed graphs with vertices
+ and edges labeled with integers. Several other graph implementations
+ are proposed for those not satisfied with the one above. Some are
+ persistent (imutable) and other imperative (mutable). Some are directed
+ and other are not. Some have labels for vertices, or labels for edges,
+ or both. Some have abstract types for vertices. etc. These
+ implementations are written as functors: you give the types of vertices
+ labels, edge labels, etc. and you get the data structure as a result.
+ it also provides several classic operations and algorithms over graphs.
+ They are also written as functors i.e. independently of the data
+ structure for graphs. One consequence is that you can define your own
+ data structure for graphs and yet re-use all the algorithms from this
+ library: you only need to provide a few operations such as iterating
+ over all vertices, over the successors of a vertex, etc.
+ </longdescription>
+ <maintainer>
+ <email>sci@gentoo.org</email>
+ </maintainer>
+ <use>
+ <flag name="doc">?doc?</flag>
+ <flag name="examples">?examples?</flag>
+ <flag name="gtk">?gtk?</flag>
+ <flag name="ocamlopt">?ocamlopt?</flag>
+ </use>
</pkgmetadata>
diff --git a/dev-ml/ocamlgraph/ocamlgraph-1.8.2.ebuild b/dev-ml/ocamlgraph/ocamlgraph-1.8.5.ebuild
index 1442073be..d950b6f2d 100644
--- a/dev-ml/ocamlgraph/ocamlgraph-1.8.2.ebuild
+++ b/dev-ml/ocamlgraph/ocamlgraph-1.8.5.ebuild
@@ -7,12 +7,12 @@ EAPI="2"
inherit eutils autotools
DESCRIPTION="A graph library for Objective Caml"
-HOMEPAGE="http://ocamlgraph.lri.fr/"
-SRC_URI="http://ocamlgraph.lri.fr/download/${P}.tar.gz"
+HOMEPAGE="http://ocamlgraph.lri.fr"
+SRC_URI="${HOMEPAGE}/download/${P}.tar.gz"
LICENSE="LGPL-2"
SLOT="0"
-KEYWORDS="~amd64 ~ppc ~sparc ~x86"
+KEYWORDS="~amd64 ~x86"
IUSE="doc examples gtk +ocamlopt"
DEPEND=">=dev-lang/ocaml-3.10.2[ocamlopt?]
@@ -21,11 +21,15 @@ RDEPEND="${DEPEND}"
src_prepare() {
epatch "${FILESDIR}/${PN}-makefile.patch"
+
+ #dirty fix for doc building
+ sed -i Makefile.in -e "s/-d doc -html \$(DGRAPH_INCLUDES) \$(DOC_SRC)/-d doc -html \$(DGRAPH_INCLUDES) \$(DOC_SRC:src\/merge.mli=)/g"
+
eautoreconf
}
src_compile() {
- emake -j1 DESTDIR="/" || die "emake failed"
+ DESTDIR="/" emake -j1 || die "emake failed"
if use doc; then
emake doc || die "emake doc failed"
@@ -33,7 +37,7 @@ src_compile() {
}
src_install() {
- emake install DESTDIR="${D}" || die "emake install failed"
+ DESTDIR="${D}" emake install || die "emake install failed"
dodoc CHANGES CREDITS FAQ README
if use doc; then
diff --git a/dev-ml/zarith/ChangeLog b/dev-ml/zarith/ChangeLog
index aab4931c7..a521a070e 100644
--- a/dev-ml/zarith/ChangeLog
+++ b/dev-ml/zarith/ChangeLog
@@ -1,11 +1,12 @@
# ChangeLog for dev-ml/zarith
-# Copyright 1999-2013 Gentoo Foundation; Distributed under the GPL v2
+# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2
# $Header: $
- 03 Mar 2013; Justin Lecher <jlec@gentoo.org> zarith-1.1.ebuild, metadata.xml:
- Clean wrong space and blank lines; move EAPI=5
+ 10 Jun 2014; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -zarith-1.1.ebuild, +zarith-1.2.1.ebuild:
+ version bump
- 14 Jan 2013; J.-C. Demay <jcdemay@gmail.com>
+ 14 Jan 2013; Jonathan-Christofer Demay <jcdemay@gmail.com>
+zarith-1.1.ebuild:
initial commit
diff --git a/dev-ml/zarith/Manifest b/dev-ml/zarith/Manifest
index 5ba03d9d8..8dbf2f331 100644
--- a/dev-ml/zarith/Manifest
+++ b/dev-ml/zarith/Manifest
@@ -1 +1,4 @@
-DIST zarith-1.1.tgz 68383 SHA256 a0ba322c8d4f5bffa43f1c571e839baa0c7b155b67630bbd8481df21eb636b6e SHA512 60f36282eb5721df164437a0b24f36b601639914b4369ed0b9ca089fda1e75191163c1c57a3890f6f9c92c64eb99f9092f045822223c448298eccf9baed535e5 WHIRLPOOL 5671caa5f942084215d52f691257fb40229607f6394ad1a1e4c932df3cf3c0bcf598caf72dc16a23c849e2bba4e9caaad659a186475ea0173b78fad6799bd859
+DIST zarith-1.2.1.tgz 68654 SHA256 916801cc39599d3fca07384fbfeec4bfaa5ffcb497d68ef89320af40ba5e4144 SHA512 5c053e259469bf6a2d4aaa3e653da42d18015e815a0b922a4e317db091a54c560e7ed32f5cb1faae7df1e8a6d81ba3913d71e5b500ace1bd45d69e69858467a1 WHIRLPOOL e31770c23e7f77bff8f084eeb3e0a9cab7c1413f2da64926c403720df2351bb84598953ad1bae0436d9b3ba6e66c1543aee0dbd9151a3708d793abe5506f1e00
+EBUILD zarith-1.2.1.ebuild 992 SHA256 247562941f50638da74a08fd033a38a2366f9f896ab4983c0d1c2a19e67fe589 SHA512 4a5bfa400ac5f0804c06b42e488cf8ec54c0674fc4224bc19c8e7d845bbd8c25458cc776790da91b1764df1be0094813603d71ea04c32a0016d442107d134aee WHIRLPOOL b5cbbaa432b53df50051a97fd4679be1d884ad19dbcddc331e827ae6e4cc6bc148deb54394a946dba8cf8550d8aad75d376c51551b412cc3e34e6ff2340b13e6
+MISC ChangeLog 336 SHA256 dd82e831bb0b21ef3c9917dc50b16b10b21e66561794ca0b59eb2ae07cda49aa SHA512 471d19d844981cff8dab5738d5366922de22a658a652956214304f7a47f431c39086ab488cc9c5b79ce22562170cdedd67b58a879ade9e8cfdce47a7d14037e0 WHIRLPOOL 15b849caba4bd8c03a9d1d6f1f8682956cac874c1cf918635c08e8919fa398bc76cf237c4b26b49cb4fa2225355d377c73142af24ee77ee97dda521b903a035e
+MISC metadata.xml 576 SHA256 f2e3b72798b53b5cc8de7f84bb15a4f936b202798dff0924a8dc3153fc02eba3 SHA512 fabad704c895e72ced7561f1e5db01869f3b5b7ecca6d96d3a1474e7febad1170a8ad9087346aa8caf8741a5cd719290567581297ef452cb1eb94f706cb14e6e WHIRLPOOL 15466f22d6b3f39bc2c294a642dccc215a34c84325443b385a9e4aeccef0e8a178b389ce76380769edd55992d6e665b8f440236a132141b85a8885d26d2de108
diff --git a/dev-ml/zarith/metadata.xml b/dev-ml/zarith/metadata.xml
index 1ff321877..d2e969145 100644
--- a/dev-ml/zarith/metadata.xml
+++ b/dev-ml/zarith/metadata.xml
@@ -1,11 +1,17 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
<pkgmetadata>
-<herd>sci-mathematics</herd>
-<longdescription>
- The Zarith library implements arithmetic and logical operations over
- arbitrary-precision integers. It uses GMP to efficiently implement
- arithmetic over big integers. Small integers are represented as Caml
- unboxed integers, for speed and space economy.
-</longdescription>
+ <herd>sci</herd>
+ <longdescription>
+ The Zarith library implements arithmetic and logical operations over
+ arbitrary-precision integers. It uses GMP to efficiently implement
+ arithmetic over big integers. Small integers are represented as Caml
+ unboxed integers, for speed and space economy.
+ </longdescription>
+ <maintainer>
+ <email>sci@gentoo.org</email>
+ </maintainer>
+ <use>
+ <flag name="ocamlopt">?ocamlopt?</flag>
+ </use>
</pkgmetadata>
diff --git a/dev-ml/zarith/zarith-1.1.ebuild b/dev-ml/zarith/zarith-1.1.ebuild
deleted file mode 100644
index dc8c685cb..000000000
--- a/dev-ml/zarith/zarith-1.1.ebuild
+++ /dev/null
@@ -1,41 +0,0 @@
-# Copyright 1999-2014 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-# $Header: $
-
-EAPI=5
-
-DESCRIPTION="The Zarith library implements arithmetic and logical operations over arbitrary-precision integers"
-HOMEPAGE="http://forge.ocamlcore.org/projects/zarith"
-SRC_URI="http://forge.ocamlcore.org/frs/download.php/835/${P}.tgz"
-
-LICENSE="GPL-2"
-SLOT="0"
-KEYWORDS="~amd64 ~ppc ~x86"
-IUSE="+ocamlopt"
-
-DEPEND="
- >=dev-lang/ocaml-3.10.2[ocamlopt?]
- dev-libs/gmp"
-RDEPEND="${DEPEND}"
-
-pkg_setup() {
- OCAMLDIR=$(ocamlc -where)
-}
-
-src_prepare(){
- sed \
- -e "s:(OCAMLFIND) install:(OCAMLFIND) install -ldconf \$(INSTALLDIR)/ld.conf:g" \
- -i "${S}"/project.mak || die
-}
-
-src_configure(){
- ./configure -installdir "${D}${OCAMLDIR}" || die
-}
-
-src_install(){
- dodir "${OCAMLDIR}"
- cp "${OCAMLDIR}/ld.conf" "${D}${OCAMLDIR}/ld.conf" || die
- emake install
- rm "${D}${OCAMLDIR}/ld.conf" || die
- dodoc Changes README
-}
diff --git a/dev-ml/zarith/zarith-1.2.1.ebuild b/dev-ml/zarith/zarith-1.2.1.ebuild
new file mode 100644
index 000000000..2822592e2
--- /dev/null
+++ b/dev-ml/zarith/zarith-1.2.1.ebuild
@@ -0,0 +1,40 @@
+# Copyright 1999-2014 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: $
+
+EAPI=4
+
+DESCRIPTION="The Zarith library implements arithmetic and logical operations over arbitrary-precision integers"
+HOMEPAGE="http://forge.ocamlcore.org/projects/zarith"
+SRC_URI="http://forge.ocamlcore.org/frs/download.php/1199/${P}.tgz"
+
+LICENSE="GPL-2"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+IUSE="+ocamlopt"
+
+OCAMLDIR=`ocamlc -where`
+
+DEPEND=">=dev-lang/ocaml-3.12.1[ocamlopt?]
+ dev-libs/gmp"
+RDEPEND="${DEPEND}"
+
+src_prepare(){
+ sed -i ${S}/project.mak -e "s:(OCAMLFIND) install:(OCAMLFIND) install -ldconf \$(INSTALLDIR)/ld.conf:g"
+}
+
+src_configure(){
+ ./configure -installdir "${D}${OCAMLDIR}" || die "configure failed"
+}
+
+src_compile(){
+ emake || die "emake failed"
+}
+
+src_install(){
+ mkdir -p "${D}${OCAMLDIR}"
+ cp "${OCAMLDIR}/ld.conf" "${D}${OCAMLDIR}/ld.conf"
+ emake install || die "emake install failed"
+ rm "${D}${OCAMLDIR}/ld.conf"
+ dodoc Changes README
+}
diff --git a/sci-mathematics/alt-ergo/ChangeLog b/sci-mathematics/alt-ergo/ChangeLog
index b396eaafb..e1becf1b1 100644
--- a/sci-mathematics/alt-ergo/ChangeLog
+++ b/sci-mathematics/alt-ergo/ChangeLog
@@ -2,24 +2,11 @@
# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2
# $Header: $
-*alt-ergo-0.95.2 (16 Jun 2014)
+ 10 Jan 2014; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -alt-ergo-0.95.ebuild, +alt-ergo-0.95.2.ebuild:
+ version bump
- 16 Jun 2014; Jauhien Piatlicki <jauhien@gentoo.org> -alt-ergo-0.95.1.ebuild,
- +alt-ergo-0.95.2.ebuild:
- fix bug #479994: move sources to my dev space
-
-*alt-ergo-0.95.1 (25 Aug 2013)
-
- 25 Aug 2013; Andrew Savchenko <bircoph@gmail.com> -alt-ergo-0.95.ebuild,
- +alt-ergo-0.95.1.ebuild, metadata.xml:
- Version bump for a bugfix release. Cleanup metadata.
- This also fixes bug 479994 (wrong manifest for alt-ergo-0.95).
-
- 03 Mar 2013; Justin Lecher <jlec@gentoo.org> alt-ergo-0.95.ebuild,
- metadata.xml:
- Move to EAPI=5; clean quoting and ebuild syntax and indention
-
- 14 Jan 2013; J.-C. Demay <jcdemay@gmail.com>
+ 14 Jan 2013; Jonathan-Christofer Demay <jcdemay@gmail.com>
+alt-ergo-0.95.ebuild:
initial commit
diff --git a/sci-mathematics/alt-ergo/Manifest b/sci-mathematics/alt-ergo/Manifest
index ad6a8ca8d..f3610fbad 100644
--- a/sci-mathematics/alt-ergo/Manifest
+++ b/sci-mathematics/alt-ergo/Manifest
@@ -1 +1,4 @@
-DIST alt-ergo-0.95.2.tar.gz 233778 SHA256 5a6cd4349c144653be19a1ba4c254bbf626bdfd97c54d1c13ba63e396006eeac SHA512 e4bb73719d67e44bac058ea53082879534c93d47fd931ec927e7f1e59330a60915ae73c662153207e6229ae914a5c0b8b16c04763f1ae3e251668a336a11d382 WHIRLPOOL aa5f8f0bf46eb93d4e8e4be4e6a30facd7b97d35fd110e4081a61826edb1def7dc5724db08c05f714c3bc1a70add9aaa961e9757492aa47f9c97ad48069f5ae9
+DIST download_manager.php?target=alt-ergo-0.95.2.tar.gz 233778 SHA256 5a6cd4349c144653be19a1ba4c254bbf626bdfd97c54d1c13ba63e396006eeac SHA512 e4bb73719d67e44bac058ea53082879534c93d47fd931ec927e7f1e59330a60915ae73c662153207e6229ae914a5c0b8b16c04763f1ae3e251668a336a11d382 WHIRLPOOL aa5f8f0bf46eb93d4e8e4be4e6a30facd7b97d35fd110e4081a61826edb1def7dc5724db08c05f714c3bc1a70add9aaa961e9757492aa47f9c97ad48069f5ae9
+EBUILD alt-ergo-0.95.2.ebuild 996 SHA256 f21ffd478f413f6c1c64563429942bd81fc7ee4b5089e118f546f6c0a34cb8dc SHA512 0c304baf0809a9493e9ebb5ba8750b03978eb72065a4e7ad2131ae66b1327bba8f569a4695f77054299e42f4720b0e255b542bb47d01a2db4362235cf1768823 WHIRLPOOL b81c27cd79ece6a8dd4936bedeaf8a2aa8b5195de9452660871d5a924793d36195f75882342e6b13df3842168c26c73cf2299641ec075307db42679fa8d263d7
+MISC ChangeLog 356 SHA256 aa57e6b9bd4954e27d5dcf7e4f6a5553c66c28b2e685492b65923fce765272c3 SHA512 746bb5a06accb524caa1248847eb6e45d23b1be3afaef74b98b24f163b254517f184aa83b574c4ae25e61e936c5b60f57aeb028dc27c592364773a3b1f54f69c WHIRLPOOL 6e92d14aacb458f3791d0ee6e91b8a5c6ec902a735532ee4397e1acb7a99ea81ec4b4f672d974f63bbc7ada505e394ece55dc00ef17c35fe307c8ac2efc89d99
+MISC metadata.xml 723 SHA256 995ef23d0edbbcdc7b9b6e775fc393bcea0aae1d6b98ad577b23f577389c397d SHA512 f388963e5ebe117d3f382434dad98f53080906a73a19cdc7667f377e2a65f9dc75e43cf5c358a2badd769218cfc975305e50f0584152ccc4b906cfe56b7762f4 WHIRLPOOL be335909c18f8037bf3dd63649a8591b328f7ed72d7e45b5944f8322ce1d02c9972415fd9ccbbc7496f5d692ce2b3fe14b6f1d2ed3460d54d8f1089ddc0efdf3
diff --git a/sci-mathematics/alt-ergo/alt-ergo-0.95.2.ebuild b/sci-mathematics/alt-ergo/alt-ergo-0.95.2.ebuild
index ce0fcc70a..9bd6f6b1c 100644
--- a/sci-mathematics/alt-ergo/alt-ergo-0.95.2.ebuild
+++ b/sci-mathematics/alt-ergo/alt-ergo-0.95.2.ebuild
@@ -2,37 +2,38 @@
# Distributed under the terms of the GNU General Public License v2
# $Header: $
-EAPI=5
+EAPI=4
inherit eutils
DESCRIPTION="Alt-Ergo is an automatic theorem prover"
-HOMEPAGE="http://alt-ergo.lri.fr"
-SRC_URI="http://dev.gentoo.org/~jauhien/distfiles/${P}.tar.gz"
+HOMEPAGE="http://alt-ergo.ocamlpro.com"
+SRC_URI="${HOMEPAGE}/download_manager.php?target=${P}.tar.gz"
LICENSE="CeCILL-C"
SLOT="0"
KEYWORDS="~amd64 ~x86"
IUSE="+ocamlopt gtk"
-DEPEND="
- >=dev-lang/ocaml-3.10.2[ocamlopt?]
- >=dev-ml/ocamlgraph-1.8.2[gtk?,ocamlopt?]
- dev-ml/zarith
- gtk? (
- x11-libs/gtksourceview:2.0
- >=dev-ml/lablgtk-2.14[sourceview,ocamlopt?]
- )"
+DEPEND=">=dev-lang/ocaml-3.12.1[ocamlopt?]
+ >=dev-ml/ocamlgraph-1.8.2[gtk?,ocamlopt?]
+ gtk? ( >=x11-libs/gtksourceview-2.8
+ >=dev-ml/lablgtk-2.14[sourceview,ocamlopt?] )"
RDEPEND="${DEPEND}"
src_prepare(){
- sed \
+ sed -i ${S}/Makefile.in \
-e "s: /usr/share/: \$(DESTDIR)/usr/share/:g" \
- -e "s:cp -f altgr-ergo.opt:mkdir -p \$(DESTDIR)/usr/share/gtksourceview-2.0/language-specs/\n\tcp -f altgr-ergo.opt:g" \
- -i "${S}"/Makefile.in || die
+ -e "s:cp -f altgr-ergo.opt:mkdir -p \$(DESTDIR)/usr/share/gtksourceview-2.0/language-specs/\n\tcp -f altgr-ergo.opt:g"
}
-
src_compile(){
- emake
- use gtk && emake gui
+ emake || die "emake failed"
+ if use gtk; then
+ emake gui || die "emake gui failed"
+ fi
+}
+
+src_install(){
+ DESTDIR="${D}" emake install || die "emake install failed"
+ dodoc README.md CHANGES
}
diff --git a/sci-mathematics/alt-ergo/metadata.xml b/sci-mathematics/alt-ergo/metadata.xml
index 947fde0ac..4ac4fb5dc 100644
--- a/sci-mathematics/alt-ergo/metadata.xml
+++ b/sci-mathematics/alt-ergo/metadata.xml
@@ -1,11 +1,19 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
<pkgmetadata>
-<herd>sci-mathematics</herd>
-<longdescription>
- Alt-Ergo is an open source automatic theorem prover dedicated to program verification.
- It is an SMT solver based on CC(X): a congruence closure algorithm parameterized by an
- equational theory X. Alt-Ergo is based on a home-made SAT-solver and implements an
- instantiation mechanism for quantified formulas.
-</longdescription>
+ <herd>sci</herd>
+ <longdescription>
+ Alt-Ergo is an open source automatic theorem prover dedicated to program verification.
+ It is an SMT solver based on CC(X): a congruence closure algorithm parameterized by an
+ equational theory X. Alt-Ergo is based on a home-made SAT-solver and implements an
+ instantiation mechanism for quantified formulas. Its architecture is summarized by the
+ the following picture.
+ </longdescription>
+ <maintainer>
+ <email>sci@gentoo.org</email>
+ </maintainer>
+ <use>
+ <flag name="gtk">?gtk?</flag>
+ <flag name="ocamlopt">?ocamlopt?</flag>
+ </use>
</pkgmetadata>
diff --git a/sci-mathematics/apron/ChangeLog b/sci-mathematics/apron/ChangeLog
index 0eb1de48a..ffe53b5f8 100644
--- a/sci-mathematics/apron/ChangeLog
+++ b/sci-mathematics/apron/ChangeLog
@@ -1,21 +1,25 @@
# ChangeLog for sci-mathematics/apron
-# Copyright 1999-2011 Gentoo Foundation; Distributed under the GPL v2
+# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2
# $Header: $
- 13 Feb 2011; J.C. Demay <jcdemay@gmail.com>
+ 21 Jun 2014; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ +apron-0.9.10-r1.ebuild:
+ dropping cxx and ppl support
+
+ 13 Feb 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
apron-0.9.10.ebuild:
- doc generation for cxx fixed using dev-tex/rubber
+ doc generation for cxx fixed using dev-tex/rubber
04 Jul 2010; Andreas K. Huettel (dilfridge) <mail@akhuettel.de>
apron-0.9.10.ebuild, metadata.xml:
Silence repoman; drop ~sparc since dependencies cannot be fulfilled; move
doc generation dependencies to RDEPEND
- 04 Jul 2010; J.-C. Demay <jcdemay@gmail.com>
+ 04 Jul 2010; Jonathan-Christofer Demay <jcdemay@gmail.com>
-files/apron-0.9.10-pkgrid_manager.patch, apron-0.9.10.ebuild:
building process fixed for the latest sources
- 03 Jul 2010; J.-C. Demay <jcdemay@gmail.com>
+ 03 Jul 2010; Jonathan-Christofer Demay <jcdemay@gmail.com>
+metadata.xml, +ChangeLog:
QA fixes
diff --git a/sci-mathematics/apron/Manifest b/sci-mathematics/apron/Manifest
index e9d2c4184..1407aeebb 100644
--- a/sci-mathematics/apron/Manifest
+++ b/sci-mathematics/apron/Manifest
@@ -1 +1,5 @@
-DIST apron-0.9.10.tgz 1694989 SHA256 b108de2f4a8c4ecac1ff76a6d282946fd3bf1466a126cf5344723955f305ec8e
+DIST apron-0.9.10.tgz 1694989 SHA256 b108de2f4a8c4ecac1ff76a6d282946fd3bf1466a126cf5344723955f305ec8e SHA512 9b84bf6b5d34ee34558e8224ecd09d48ff2013b7a301a8749512aaea8b8c99da394bb0550055b9bc37692187ca8956bf25e74535c1d41ac1907e161163bc6e8a WHIRLPOOL 5a3eef9ae6387a55f898fdb336a41ccb64a0ea628a8992c2adce28a7168de549c17816f9313f06561d29d512a9ce90ad3b39ddbd76559421a107d0088b4c8279
+EBUILD apron-0.9.10-r1.ebuild 2101 SHA256 d5889ea44dcfe4b46adbabc6d696eb2217140543b9a629d764d8c85fb9346481 SHA512 37aefe19d5b10b20490fc32e60902bfeb17d6aefd0f051ef3647fb86d683d34e5a9f565b72f2271ac54d51c40aba089d7fa4e9b62661c297f07f9085facb88df WHIRLPOOL 8f9d0b6aa24f68028bc6de67b980d283184150f1fd65debb9caaf7ea2c736b6b7aeaa9b16bd80b4a9488bdf4a695fb5351e74adfd661594fcb8a8beacc49a468
+EBUILD apron-0.9.10.ebuild 2428 SHA256 f95f644a80dc742f8fd5637c4b7f3f35dd4226b9b8323b277c4ad03304c8f8a5 SHA512 55d95bfe3a93f58c5cafd139c8f1b15615f4db4cbadd093821d6b7bb04e90607c9f39c64358356d18728f2dc2ebdd771c67dd6a007dd77d4ce39cd494ff289ef WHIRLPOOL d421cf006dea3c8356bb8b636a6b667871778fb55dba8210a41acd67371c7ad0ff6320400115e6b58e29f8b40cb0a0da85581fc04f60a029ca2a93f0e83012a1
+MISC ChangeLog 877 SHA256 15fc1ab32c5ef6c7a8fe25aece31d2ea2203cee540afd91d4a40deb0c1aab6a7 SHA512 ea0cc38a53f99bd9cc0517bfcc33d344d96466df4867601453ceeebd546a0a362d7311a2f9b519393816f61ececc05382bca1322e59252057d0196b11b4ff907 WHIRLPOOL c57b153cd0903ffc184a3cc795b40d7e69cb8dacc718807d502a58d99581aead199641afd5ea62a17ab73c2829efa50275f5f3eecc64205039e75cdc5f74257f
+MISC metadata.xml 817 SHA256 5867fca0c661c85733f41114cdc60300cc1222272d41196390c7fc6e21e1fe27 SHA512 fdb2f51196edf3ab3d1d92c61b52c988cf816d3c17459e835aef84e9343306170004065dfb4d66cdce0c6dee31227b47ed60d46a5d5369cd6f5be17cb840dee9 WHIRLPOOL bda55109cebd30ceec84595bd1b3ec328dcb367fdaba7b5c6be514e5efc3092dcdc3d8da99b6130d014533292a1b9364b2fb9afc34efa0a7d13f48afab8c4bd5
diff --git a/sci-mathematics/apron/apron-0.9.10-r1.ebuild b/sci-mathematics/apron/apron-0.9.10-r1.ebuild
new file mode 100644
index 000000000..40791e2dc
--- /dev/null
+++ b/sci-mathematics/apron/apron-0.9.10-r1.ebuild
@@ -0,0 +1,79 @@
+# Copyright 1999-2010 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: $
+
+EAPI="2"
+
+inherit eutils toolchain-funcs
+
+DESCRIPTION="Library for static analysis of the numerical variables of a program by Abstract Interpretation"
+HOMEPAGE="http://apron.cri.ensmp.fr/library/"
+SRC_URI="http://apron.cri.ensmp.fr/library/${P}.tgz"
+
+LICENSE="LGPL-2 GPL-2"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+IUSE="doc ocaml"
+
+RDEPEND="ocaml? ( >=dev-lang/ocaml-3.09
+ dev-ml/camlidl
+ dev-ml/mlgmpidl )
+ dev-libs/gmp
+ dev-libs/mpfr"
+DEPEND="${RDEPEND}
+ doc? ( app-text/texlive
+ app-text/ghostscript-gpl )"
+
+src_prepare() {
+ mv Makefile.config.model Makefile.config
+
+ #fix compile process
+ sed -i Makefile.config \
+ -e "s/FLAGS = \\\/FLAGS += \\\/g" \
+ -e "s/-O3 -DNDEBUG/-DNDEBUG/g" \
+ -e "s/APRON_PREFIX =.*/APRON_PREFIX = \${DESTDIR}\/usr/g" \
+ -e "s/MLGMPIDL_PREFIX =.*/MLGMPIDL_PREFIX = \${DESTDIR}\/usr/g"
+
+ #fix doc building process
+ sed -i Makefile -e "s/; make html/; make/g"
+ sed -i apronxx/Makefile \
+ -e "s:cd doc/latex && make:cd doc/latex; rubber refman.tex; dvipdf refman.dvi:g"
+ sed -i apronxx/doc/Doxyfile \
+ -e "s/OUTPUT_DIRECTORY = \/.*/OUTPUT_DIRECTORY = .\//g" \
+ -e "s/STRIP_FROM_PATH = \/.*/STRIP_FROM_PATH = .\//g"
+
+ #fix ppl install for 32 platforms
+ sed -i ppl/Makefile -e "s/libap_ppl_caml\*\./libap_ppl\*\./g"
+
+ if [[ "$(gcc-major-version)" == "4" ]]; then
+ sed -i -e "s/# HAS_LONG_DOUBLE = 1/HAS_LONG_DOUBLE = 1/g" Makefile.config
+ fi
+ if use !ocaml; then
+ sed -i -e "s/HAS_OCAML = 1/#HAS_OCAML = 0/g" Makefile.config
+ fi
+}
+
+src_compile() {
+ #damn crappy Makefile
+ emake || emake || die "emake failed"
+
+ if use doc && use cxx; then
+ emake -C apronxx doc || "emake doc failed"
+ fi
+}
+
+src_install(){
+ DESTDIR="${D}" emake install || die "emake install failed"
+ dodoc AUTHORS Changes README
+
+ if use doc; then
+ dodoc apron/apron.pdf
+ if use ocaml; then
+ dodoc mlapronidl/mlapronidl.pdf
+ fi
+ if use cxx; then
+ mv apronxx/doc/latex/refman.pdf apronxx/apronxx.pdf
+ dodoc ./apronxx/apronxx.pdf
+ fi
+ fi
+}
diff --git a/sci-mathematics/apron/apron-0.9.10.ebuild b/sci-mathematics/apron/apron-0.9.10.ebuild
index c4f78c05d..2752070f7 100644
--- a/sci-mathematics/apron/apron-0.9.10.ebuild
+++ b/sci-mathematics/apron/apron-0.9.10.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2014 Gentoo Foundation
+# Copyright 1999-2010 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Header: $
@@ -12,7 +12,7 @@ SRC_URI="http://apron.cri.ensmp.fr/library/${P}.tgz"
LICENSE="LGPL-2 GPL-2"
SLOT="0"
-KEYWORDS="~amd64 ~ppc ~x86"
+KEYWORDS="~amd64 ~x86"
IUSE="cxx doc ocaml ppl"
RDEPEND="ocaml? ( >=dev-lang/ocaml-3.09
@@ -76,7 +76,7 @@ src_compile() {
}
src_install(){
- emake install DESTDIR="${D}" || die "emake install failed"
+ DESTDIR="${D}" emake install || die "emake install failed"
dodoc AUTHORS Changes README
if use doc; then
diff --git a/sci-mathematics/apron/metadata.xml b/sci-mathematics/apron/metadata.xml
index 75f2ae704..f87ceb90a 100644
--- a/sci-mathematics/apron/metadata.xml
+++ b/sci-mathematics/apron/metadata.xml
@@ -1,18 +1,21 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
<pkgmetadata>
-<herd>sci-mathematics</herd>
-<longdescription>
- The APRON library is dedicated to the static analysis of the numerical
- variables of a program by Abstract Interpretation. The aim of such an
- analysis is to infer invariants about these variables. The APRON library
- is intended to be a common interface to various underlying
- libraries/abstract domains and to provide additional services that can
- be implemented independently from the underlying library/abstract
- domain, as shown by the poster on the right (presented at the SAS 2007
- conference.
-</longdescription>
-<use>
- <flag name="ppl">Enable optional interface to the Parma Polyhedra Library</flag>
-</use>
+ <herd>sci</herd>
+ <longdescription>
+ The APRON library is dedicated to the static analysis of the numerical
+ variables of a program by Abstract Interpretation. The aim of such an
+ analysis is to infer invariants about these variables. The APRON library
+ is intended to be a common interface to various underlying
+ libraries/abstract domains and to provide additional services that can
+ be implemented independently from the underlying library/abstract
+ domain, as shown by the poster on the right (presented at the SAS 2007
+ conference.
+ </longdescription>
+ <maintainer>
+ <email>sci@gentoo.org</email>
+ </maintainer>
+ <use>
+ <flag name="ocaml">?ocaml?</flag>
+ </use>
</pkgmetadata>
diff --git a/sci-mathematics/flocq/ChangeLog b/sci-mathematics/flocq/ChangeLog
index ffc9d3dcc..e3076b83e 100644
--- a/sci-mathematics/flocq/ChangeLog
+++ b/sci-mathematics/flocq/ChangeLog
@@ -1,20 +1,20 @@
# ChangeLog for sci-mathematics/flocq
-# Copyright 1999-2013 Gentoo Foundation; Distributed under the GPL v2
+# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2
# $Header: $
- 03 Mar 2013; Justin Lecher <jlec@gentoo.org> flocq-2.1.0.ebuild,
- metadata.xml:
- Move to EAPI=5; assign RDEPEND explicitatly
+ 21 Jun 2014; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -flocq-2.1.0.ebuild, +flocq-2.3.0.ebuild:
+ version bump
- 14 Jan 2013; J.-C. Demay <jcdemay@gmail.com>
+ 14 Jan 2013; Jonathan-Christofer Demay <jcdemay@gmail.com>
-flocq-1.4.0.ebuild, +flocq-2.1.0.ebuild:
version bump
- 06 May 2011; J.-C. Demay <jcdemay@gmail.com>
+ 06 May 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
-flocq-1.2.ebuild, +flocq-1.4.0.ebuild:
version bump
- 13 Feb 2011; J.-C. Demay <jcdemay@gmail.com>
+ 13 Feb 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
+metadata.xml, +ChangeLog:
QA fixes
diff --git a/sci-mathematics/flocq/Manifest b/sci-mathematics/flocq/Manifest
index 789fb75fe..4d73f691c 100644
--- a/sci-mathematics/flocq/Manifest
+++ b/sci-mathematics/flocq/Manifest
@@ -1 +1,4 @@
-DIST flocq-2.1.0.tar.gz 139831 SHA256 d9af741f648d56a6dc2a8e368e47b003c170403a4cf71ffd49b3af4f6a902dfe SHA512 9871dd0fbddb0036819c71ae0a25f89c1b2ec0c51fe0a3aaf9b4716fb8ec602dbd77c18918664781d67562e292595bac8a3530cfff87d84177ce609cd8c9e1f5 WHIRLPOOL b267daaaaa3c9b8cd1472cdc9d32ab2cea6bbe1790ba823c5df559bd3c9b11f4564d9e58b25e02270ad3f5b847c25d719e41206685aad02be1e91b56d3e1634e
+DIST flocq-2.3.0.tar.gz 155465 SHA256 b2b2474df966975b7a00310031b122aa31489d96f06b2d5b62156acc687730dd SHA512 964b87f3df3ab76549dace5d8c16c7e7890dc70b64f54db3555023dcd6b32648b19030ad25ecb5b6e99bca5139f289a2ecfd3a1fe8bc1e1dfe7429f3d4f1ebc3 WHIRLPOOL c8b4c3e57e3753d245ae01a2fb93d3dcaef9cabbf21c1afa04568137555dc21d087a7faec6df3d3db2cb497a0985ed3344d7f748f32f9670f640b6cec28fdbc8
+EBUILD flocq-2.3.0.ebuild 793 SHA256 2eb59d5a58c64c6fd23195713c925a68ef59ff792e4ae680324d2a0e660f060d SHA512 4b769ff19abbab261d16ab6d0e672bc9a879b2e5892feada75f7736acec39b8a909d5dabf38e94a3957355dc26768762dd56fe7baa2890209ee3f7f5186fd8bb WHIRLPOOL 9acc0f225e16fe74dec637b342c943e267b2aad5cb4e5b3fefd2bd4620bb35597ffd907c1e711db749e5ebc70c285a0ad13e3fa71d67e14008addff8d3d2653e
+MISC ChangeLog 585 SHA256 999b9bc1c42b76d63b38287b73e1435956ff1f17fc5fb7c344f3f3395b4b7f2a SHA512 7ef9130eb278cf02608af839c35af86dcab9f8ad72dc9875761452c189a1fc1e2374128de962b7107d3b8ef02e9adad6aefd8843ff6e2ab4cdd5aa24470bc3cc WHIRLPOOL b5c64422b524d04eb97e15bb580127bc818735b209c53040077bee8ab50fa7a3465a297d96ab11f7683677abeedaec33e1470e51d2b0231be9778a41290a1091
+MISC metadata.xml 497 SHA256 888cc1091b03da5c749d586bccafc4eaa063c08a9273458b17026a6c8c91626a SHA512 c997254c2771af0ef2010b0f0664e6be22f7f35e6929c5596e80d159216c004f28e620e82e87a1a5c5f54568390594375650dffde79f0c3c4ddbe4978975261d WHIRLPOOL 95a8d99484e7968048f995d67ca454ab9a79723d76528cd75465804aae3c4c029a1fd01e4aae42adcb2341b932a8d47b694473c2e5c1571964e420795f471504
diff --git a/sci-mathematics/flocq/flocq-2.1.0.ebuild b/sci-mathematics/flocq/flocq-2.1.0.ebuild
deleted file mode 100644
index 5c274dc8e..000000000
--- a/sci-mathematics/flocq/flocq-2.1.0.ebuild
+++ /dev/null
@@ -1,21 +0,0 @@
-# Copyright 1999-2014 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-# $Header: $
-
-EAPI=5
-
-DESCRIPTION="A floating-point formalization for the Coq system"
-HOMEPAGE="http://flocq.gforge.inria.fr/"
-SRC_URI="https://gforge.inria.fr/frs/download.php/30884/${P}.tar.gz"
-
-LICENSE="LGPL-3"
-SLOT="0"
-KEYWORDS="~amd64 ~ppc ~x86"
-IUSE=""
-
-DEPEND="sci-mathematics/coq"
-RDEPEND="${DEPEND}"
-
-src_configure() {
- econf --libdir="$(coqc -where)/user-contrib/Flocq"
-}
diff --git a/sci-mathematics/flocq/flocq-2.3.0.ebuild b/sci-mathematics/flocq/flocq-2.3.0.ebuild
new file mode 100644
index 000000000..6c32445dc
--- /dev/null
+++ b/sci-mathematics/flocq/flocq-2.3.0.ebuild
@@ -0,0 +1,36 @@
+# Copyright 1999-2014 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: $
+
+EAPI="3"
+
+DESCRIPTION="A floating-point formalization for the Coq system"
+HOMEPAGE="http://flocq.gforge.inria.fr/"
+SRC_URI="https://gforge.inria.fr/frs/download.php/33502/${P}.tar.gz"
+
+LICENSE="LGPL-3"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+IUSE=""
+
+DEPEND="sci-mathematics/coq"
+
+src_prepare() {
+ sed -i Remakefile.in \
+ -e "s:mkdir -p @libdir@:mkdir -p \$(DESTDIR)@libdir@:g" \
+ -e "s:cp \$f @libdir@:cp \$f \$(DESTDIR)@libdir@:g"
+}
+
+src_configure() {
+ econf --libdir="`coqc -where`/user-contrib/Flocq"
+}
+
+src_compile() {
+ ./remake || die "emake failed"
+}
+
+src_install() {
+ DESTDIR="${D}" ./remake install || die "emake install failed"
+ dodoc NEWS README AUTHORS ChangeLog
+}
+
diff --git a/sci-mathematics/flocq/metadata.xml b/sci-mathematics/flocq/metadata.xml
index dad568b86..c8feb0fc1 100644
--- a/sci-mathematics/flocq/metadata.xml
+++ b/sci-mathematics/flocq/metadata.xml
@@ -1,11 +1,14 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
<pkgmetadata>
-<herd>sci-mathematics</herd>
-<longdescription>
- Flocq (Floats for Coq) is a floating-point formalization for the Coq
- system. It provides a comprehensive library of theorems on a multi-radix
- multi-precision arithmetic. It also supports efficient numerical
- computations inside Coq.
-</longdescription>
+ <herd>sci</herd>
+ <longdescription>
+ Flocq (Floats for Coq) is a floating-point formalization for the Coq
+ system. It provides a comprehensive library of theorems on a multi-radix
+ multi-precision arithmetic. It also supports efficient numerical
+ computations inside Coq.
+ </longdescription>
+ <maintainer>
+ <email>sci@gentoo.org</email>
+ </maintainer>
</pkgmetadata>
diff --git a/sci-mathematics/frama-c/ChangeLog b/sci-mathematics/frama-c/ChangeLog
index 6ece89419..3188d4785 100644
--- a/sci-mathematics/frama-c/ChangeLog
+++ b/sci-mathematics/frama-c/ChangeLog
@@ -2,33 +2,35 @@
# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2
# $Header: $
-*frama-c-20130601 (24 Feb 2014)
+ 21 Jun 2014; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -frama-c-20130601.ebuild, +frama-c-20140301.ebuild:
+ version bump
- 24 Feb 2014; Andrew Savchenko <bircoph@gmail.com> +frama-c-20130601.ebuild,
- +files/frama-c-ocaml-4.01.patch, +files/frama-c-make.patch:
- Version bump. Fix build with make >= 4.x, add ocaml-4.01 support.
+ 19 Jul 2013; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -frama-c-20120901.ebuild, +frama-c-20130601.ebuild:
+ version bump
- 14 Jan 2013; J.-C. Demay <jcdemay@gmail.com>
- +frama-c-20120901.ebuild, -frama-c-20111001.ebuild:
+ 14 Jan 2013; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -frama-c-20111001.ebuild, +frama-c-20120901.ebuild:
version bump
- 21 Dec 2011; J.-C. Demay <jcdemay@gmail.com>
- +frama-c-20111001.ebuild, -frama-c-20110201.ebuild:
+ 21 Dec 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -frama-c-20110201.ebuild, +frama-c-20111001.ebuild:
version bump
- 06 may 2011; J.-C. Demay <jcdemay@gmail.com>
- +frama-c-20110201.ebuild, -frama-c-20101202_beta2.ebuild:
+ 06 may 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -frama-c-20101202_beta2.ebuild, +frama-c-20110201.ebuild:
version bump
- 14 Feb 2011; J.-C. Demay <jcdemay@gmail.com>
- +frama-c-20101202_beta2.ebuild, -frama-c-20100401.ebuild, -files/frama-c-20100401-plugin_install.patch:
+ 14 Feb 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -frama-c-20100401.ebuild, -files/frama-c-20100401-plugin_install.patch, +frama-c-20101202_beta2.ebuild:
version bump
11 Jul 2010; Andreas K. Huettel (dilfridge) <mail@akhuettel.de>
frama-c-20100401.ebuild:
Dropped ~sparc since dependencies cannot be fulfilled.
- 08 Jul 2010; J.-C. Demay <jcdemay@gmail.com>
+ 08 Jul 2010; Jonathan-Christofer Demay <jcdemay@gmail.com>
+frama-c-20100401.ebuild:
version bump
diff --git a/sci-mathematics/frama-c/Manifest b/sci-mathematics/frama-c/Manifest
index 35cc1df0e..5bdb52046 100644
--- a/sci-mathematics/frama-c/Manifest
+++ b/sci-mathematics/frama-c/Manifest
@@ -1,2 +1,5 @@
-DIST frama-c-Fluorine-20130601.tar.gz 9729343 SHA256 137006b4168933cf412da8b3a35f8b0d0c3bf8d5991b4fcd1b13a9090d9819bf SHA512 ecfcd3839733630df053f36d8b6e12177fcb6f3befdcb6f7a9d3e650cab4a511f86570bb2c1018f45e575d46eab74564e8f7c05129a1c22db5b96c77e35c51a6 WHIRLPOOL f709108f47ada543393925502551b8c08f50fc8ad4266aa20250f437020bf488324284465314774cbb3832860572d937c84897c2639712a7968ee3719403f819
-DIST frama-c-Oxygen-20120901.tar.gz 10815011 SHA256 f749870a2451f97d24da886c0cc7708e3ec57ad3f169f6b79f9b52be1f47c216 SHA512 fcf96dd2c0e50c4f125050b677f55d960d3a78d2d827cbb6f9ddd98892162cb1181053202ce46f74911b29ad895489d51939a2bb52dafed440ee2abcbde41224 WHIRLPOOL 7f226eac21aa3bdddd42a85819559745444855b116a89a849d32a57f652d3e3dd001e60d1b3ac6388ebed29a7b0c43a1190b4dafec959273d560b6d58e2f2694
+AUX ocamlgraph185_compat.patch 10397 SHA256 49b231062e23c71535e2ecd451e34852249b4a8fdd07f6db6cb899eada901a0e SHA512 3813119616ce801d391d0ac6000b84244ede25709f7bc09d657e95a76a42220418ef7c3b668252822798f5b8f7b7c5ec32cbccb2109f94aabcc76894ff659921 WHIRLPOOL 99ea959621f81ebdc706ebe0aa061d836d1a8a6b055d1c42677ab64d2ebb018c1c8cc1726802ef671f007125ea5261a28620ea7ff1630d5b6ef7eb5aedc775de
+DIST frama-c-Neon-20140301.tar.gz 3122492 SHA256 c5a0606f5c2d56280fd90f979c07ff398acb1e6a661323438b8d0cbd8f9f4731 SHA512 9cfe4c986004b4b991dbd2d7dc31777100bf85910c488d575c670d40d53b3e309667dfee75f22d121a6351f23753ed31decffbee08929ea129daf56f0c9a01e8 WHIRLPOOL 06935a38cc43f7472dd88a96b8fdd3d94f7393caed927b3f1870b8b911bcbdf6006aa325d0e30b6f58eb736dd8ea0102e41632d372f5205801af5c85146b2d4a
+EBUILD frama-c-20140301.ebuild 1506 SHA256 b3e6c5b677088ea2a7cdefad1f196a9d74a005dce7dfd36aceab1b238655b819 SHA512 1896ddb8c6bab105cfca33b8e1c608d500eab562053b7b26219f912cc3e5a6260e7f4ddc432aa4d2de36136c76e63674cc966b95c3040d403fadc6cf5094555e WHIRLPOOL 6173eff9a90cfea2c6359d3906167407b7405e9bd5a8f27e5e2b70b346c648daf871f04e2c2299aab3266943480a9c49ae01ab5cdeb66554b9e96ad93769667b
+MISC ChangeLog 1344 SHA256 6632d43186a227c2a1af9bf5628ca19ca6d040364f64583fa4dfc83c4b0d8b5c SHA512 f5827b23797399bc5cf635020fcd4b3957cde04bc238b802763caee1a5758c58564990edffad30c2fe47cd3eac85ae85c97c50b5defae2f3c39c4a2f66b94386 WHIRLPOOL ca3cf955d112d9ec164c6a6f6511a3cb50cd1e00ff8e6aa7851d390b14834de194eeb3ed9ca8618b1a5154d9abe41c4a17181a84890ccbc2a6d5bed44ee66ec0
+MISC metadata.xml 821 SHA256 03eed3b99543c4497d69633fbb76362faacc117ffa9b27a15709d21b6c47a7cf SHA512 5a9980d08aea9605dab7f45a6ef9ffb40f95c68a98ef65f17d88edb7a660da38f5d28a6cb7eadad00d5e9597f371539099233e36d794f759b094b5a5f0c76993 WHIRLPOOL b10f8efeb50c036440d79bb832fbe9d3dd7d4f38cddcfc8fb6d2288ac8471abc206ee709cef86ba3ab4250ce90ca9c5f1b689f882b3c8c241389ded46a7f92ef
diff --git a/sci-mathematics/frama-c/files/frama-c-make.patch b/sci-mathematics/frama-c/files/frama-c-make.patch
deleted file mode 100644
index 7e0b1d97d..000000000
--- a/sci-mathematics/frama-c/files/frama-c-make.patch
+++ /dev/null
@@ -1,12 +0,0 @@
---- frama-c-Oxygen-20120901/configure.in.orig 2012-09-19 15:56:17.000000000 +0400
-+++ frama-c-Oxygen-20120901/configure.in 2014-02-24 19:02:44.616467203 +0400
-@@ -61,7 +61,8 @@
- MAKE_MAJOR=`$MAKE -v | sed -n -f bin/sed_get_make_major `
- MAKE_MINOR=`$MAKE -v | sed -n -f bin/sed_get_make_minor `
- echo $ECHO_N "make version is $MAKE_DISTRIB Make $MAKE_MAJOR.$MAKE_MINOR: $ECHO_C"
--if test "$MAKE_DISTRIB" != GNU -o "$MAKE_MAJOR" -lt 3 -o "$MAKE_MINOR" -lt 81;
-+if test "$MAKE_DISTRIB" != GNU -o \( "$MAKE_MAJOR" -eq 3 -a "$MAKE_MINOR" -lt 81 \)
-+ -o "$MAKE_MAJOR" -lt 3;
- then
- echo "${ECHO_T}"
- AC_MSG_ERROR([unsupported version; GNU Make version 3.81
diff --git a/sci-mathematics/frama-c/files/frama-c-ocaml-4.01.patch b/sci-mathematics/frama-c/files/frama-c-ocaml-4.01.patch
deleted file mode 100644
index 44b86b363..000000000
--- a/sci-mathematics/frama-c/files/frama-c-ocaml-4.01.patch
+++ /dev/null
@@ -1,145 +0,0 @@
-https://raw.github.com/vprevosto/opam-repository/2e0db18a822eb1818cd39a02e2ca8dde071e5d51/packages/frama-c.20130601/files/4.01-compat.patch
-diff -Naur frama-c-Fluorine-20130601/external/hptmap.ml frama-c-Fluorine-20130601.new/external/hptmap.ml
---- frama-c-Fluorine-20130601/external/hptmap.ml 2013-06-11 18:15:19.000000000 +0400
-+++ frama-c-Fluorine-20130601.new/external/hptmap.ml 2014-02-24 20:17:10.749247061 +0400
-@@ -357,6 +357,21 @@
- find htr
-
-
-+ let find_key key htr =
-+ let id = Key.id key in
-+ let rec find htr =
-+ match htr with
-+ | Empty ->
-+ raise Not_found
-+ | Leaf (key', _, _) ->
-+ if Key.equal key key' then
-+ key'
-+ else
-+ raise Not_found
-+ | Branch (_, mask, tree0, tree1, _) ->
-+ find (if (id land mask) = 0 then tree0 else tree1)
-+ in
-+ find htr
-
-
- let mem key htr =
-diff -Naur frama-c-Fluorine-20130601/external/hptmap.mli frama-c-Fluorine-20130601.new/external/hptmap.mli
---- frama-c-Fluorine-20130601/external/hptmap.mli 2013-06-11 18:15:19.000000000 +0400
-+++ frama-c-Fluorine-20130601.new/external/hptmap.mli 2014-02-24 20:17:10.769246098 +0400
-@@ -84,6 +84,9 @@
- for [k], it is overridden. *)
-
- val find : key -> t -> V.t
-+
-+ val find_key: key -> t -> key
-+
- val remove : key -> t -> t
- (** [remove k m] returns the map [m] deprived from any binding involving
- [k]. *)
-diff -Naur frama-c-Fluorine-20130601/src/kernel/file.ml frama-c-Fluorine-20130601.new/src/kernel/file.ml
---- frama-c-Fluorine-20130601/src/kernel/file.ml 2013-06-11 18:13:13.000000000 +0400
-+++ frama-c-Fluorine-20130601.new/src/kernel/file.ml 2014-02-24 20:17:10.773245905 +0400
-@@ -322,6 +322,7 @@
- Printer.pp_logic_var lv Printer.pp_varinfo v
-
- method vlogic_info_decl li =
-+ Logic_var.Hashtbl.add known_logic_info li.l_var_info li;
- List.iter
- (fun lv ->
- if lv.lv_kind <> LVFormal then
-@@ -769,10 +770,6 @@
- DoChildren
- | _ -> DoChildren
-
-- method vlogic_info_decl li =
-- Logic_var.Hashtbl.add known_logic_info li.l_var_info li;
-- DoChildren
--
- method vlogic_info_use li =
- let unknown () =
- check_abort "logic function %s has no information" li.l_var_info.lv_name
-diff -Naur frama-c-Fluorine-20130601/src/lib/hptset.ml frama-c-Fluorine-20130601.new/src/lib/hptset.ml
---- frama-c-Fluorine-20130601/src/lib/hptset.ml 2013-06-11 18:13:42.000000000 +0400
-+++ frama-c-Fluorine-20130601.new/src/lib/hptset.ml 2014-02-24 20:17:10.773245905 +0400
-@@ -26,6 +26,7 @@
- val empty: t
- val is_empty: t -> bool
- val mem: elt -> t -> bool
-+ val find: elt -> t -> elt
- val add: elt -> t -> t
- val singleton: elt -> t
- val remove: elt -> t -> t
-@@ -71,6 +72,7 @@
- type elt = X.t
-
- let add k = add k ()
-+ let find = find_key
- let iter f = iter (fun x () -> f x)
- let fold f = fold (fun x () -> f x)
-
-diff -Naur frama-c-Fluorine-20130601/src/lib/hptset.mli frama-c-Fluorine-20130601.new/src/lib/hptset.mli
---- frama-c-Fluorine-20130601/src/lib/hptset.mli 2013-06-11 18:13:42.000000000 +0400
-+++ frama-c-Fluorine-20130601.new/src/lib/hptset.mli 2014-02-24 20:17:10.777245712 +0400
-@@ -50,6 +50,8 @@
- val mem: elt -> t -> bool
- (** [mem x s] tests whether [x] belongs to the set [s]. *)
-
-+ val find: elt -> t -> elt
-+
- val add: elt -> t -> t
- (** [add x s] returns a set containing all elements of [s],
- plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
-diff -Naur frama-c-Fluorine-20130601/src/lib/setWithNearest.ml frama-c-Fluorine-20130601.new/src/lib/setWithNearest.ml
---- frama-c-Fluorine-20130601/src/lib/setWithNearest.ml 2013-06-11 18:13:42.000000000 +0400
-+++ frama-c-Fluorine-20130601.new/src/lib/setWithNearest.ml 2014-02-24 20:17:10.781245519 +0400
-@@ -165,6 +165,14 @@
- let c = Ord.compare x v in
- c = 0 || mem x (if c < 0 then l else r)
-
-+ let rec find x = function
-+ | Empty -> raise Not_found
-+ | Node(l, v, r, _) ->
-+ match Ord.compare x v with
-+ | c when c < 0 -> find x l
-+ | 0 -> v
-+ | _ -> find x r
-+
- let singleton x = Node(Empty, x, Empty, 1)
-
- let rec remove x = function
-diff -Naur frama-c-Fluorine-20130601/src/memory_state/cvalue.mli frama-c-Fluorine-20130601.new/src/memory_state/cvalue.mli
---- frama-c-Fluorine-20130601/src/memory_state/cvalue.mli 2013-06-11 18:13:51.000000000 +0400
-+++ frama-c-Fluorine-20130601.new/src/memory_state/cvalue.mli 2014-02-24 20:17:10.781245519 +0400
-@@ -35,8 +35,8 @@
- include module type of Location_Bytes
- (* Too many aliases, and OCaml module system is not able to keep track
- of all of them. Use some shortcuts *)
-- with type z = Location_Bytes.z
-- and type M.t = Location_Bytes.M.t
-+ with type M.t = Location_Bytes.M.t
-+ and type z = Location_Bytes.z
-
- include Lattice_With_Isotropy.S
- with type t := t
-diff -Naur frama-c-Fluorine-20130601/src/wp/qed/src/idxset.ml frama-c-Fluorine-20130601.new/src/wp/qed/src/idxset.ml
---- frama-c-Fluorine-20130601/src/wp/qed/src/idxset.ml 2013-06-11 18:13:23.000000000 +0400
-+++ frama-c-Fluorine-20130601.new/src/wp/qed/src/idxset.ml 2014-02-24 20:17:10.785245326 +0400
-@@ -59,6 +59,8 @@
-
- let mem e s = mem_k (E.id e) s
-
-+ let find e s = if mem e s then e else raise Not_found
-+
- let lowest_bit x = x land (-x)
-
- let branching_bit p0 p1 = lowest_bit (p0 lxor p1)
-@@ -360,6 +362,8 @@
-
- let mem e s = mem_k (index e) s
-
-+ let find e s = if mem e s then e else raise Not_found
-+
- let mask k m = (k lor (m-1)) land (lnot m)
-
- (* we first write a naive implementation of [highest_bit]
diff --git a/sci-mathematics/frama-c/files/ocamlgraph185_compat.patch b/sci-mathematics/frama-c/files/ocamlgraph185_compat.patch
new file mode 100644
index 000000000..798d17fd3
--- /dev/null
+++ b/sci-mathematics/frama-c/files/ocamlgraph185_compat.patch
@@ -0,0 +1,254 @@
+From: Mehdi Dogguy <mehdi@debian.org>
+Date: Sun, 27 Apr 2014 13:46:16 +0200
+Subject: Port to OCamlgraph 1.8.5
+
+---
+ src/impact/reason_graph.ml | 2 +-
+ src/kernel/stmts_graph.ml | 10 +++++-----
+ src/logic/property_status.ml | 8 ++++----
+ src/misc/service_graph.ml | 4 ++--
+ src/pdg_types/pdgTypes.ml | 6 +++---
+ src/postdominators/print.ml | 2 +-
+ src/semantic_callgraph/register.ml | 4 ++--
+ src/slicing/printSlice.ml | 10 +++++-----
+ src/syntactic_callgraph/register.ml | 4 ++--
+ src/wp/cil2cfg.ml | 12 ++++++------
+ 10 files changed, 31 insertions(+), 31 deletions(-)
+
+diff --git a/src/impact/reason_graph.ml b/src/impact/reason_graph.ml
+index eabacb0..ce19b4a 100644
+--- a/src/impact/reason_graph.ml
++++ b/src/impact/reason_graph.ml
+@@ -139,7 +139,7 @@ module Printer (X: AdditionalInfo) = struct
+
+ let graph_attributes _ = [`Label "Impact graph"]
+
+- let default_vertex_attributes _g = [`Style [`Filled]; `Shape `Box]
++ let default_vertex_attributes _g = [`Style `Filled; `Shape `Box]
+ let default_edge_attributes _g = []
+
+ let vertex_attributes v =
+diff --git a/src/kernel/stmts_graph.ml b/src/kernel/stmts_graph.ml
+index a8fe121..16059c3 100644
+--- a/src/kernel/stmts_graph.ml
++++ b/src/kernel/stmts_graph.ml
+@@ -157,12 +157,12 @@ module TP = struct
+
+ let vertex_attributes s =
+ match s.skind with
+- | Loop _ -> [`Color 0xFF0000; `Style [`Filled]]
+- | If _ -> [`Color 0x00FF00; `Style [`Filled]; `Shape `Diamond]
+- | Return _ -> [`Color 0x0000FF; `Style [`Filled]]
++ | Loop _ -> [`Color 0xFF0000; `Style `Filled]
++ | If _ -> [`Color 0x00FF00; `Style `Filled; `Shape `Diamond]
++ | Return _ -> [`Color 0x0000FF; `Style `Filled]
+ | Block _ -> [`Shape `Box; `Fontsize 8]
+- | Goto _ -> [`Shape `Diamond; `Color 0x00FFFF ; `Style [`Filled]]
+- | Instr (Skip _) -> [`Color 0x00FFFF ; `Style [`Filled]]
++ | Goto _ -> [`Shape `Diamond; `Color 0x00FFFF ; `Style `Filled]
++ | Instr (Skip _) -> [`Color 0x00FFFF ; `Style `Filled]
+ | _ -> []
+ let default_vertex_attributes _ = []
+
+diff --git a/src/logic/property_status.ml b/src/logic/property_status.ml
+index f7c278d..47485f6 100644
+--- a/src/logic/property_status.ml
++++ b/src/logic/property_status.ml
+@@ -1481,12 +1481,12 @@ module Consolidation_graph = struct
+ let s = get_status p in
+ let color = status_color p s in
+ let style = match s with
+- | Never_tried -> [`Style [`Bold]; `Width 0.8 ]
+- | _ -> [`Style [`Filled]]
++ | Never_tried -> [`Style `Bold; `Width 0.8 ]
++ | _ -> [`Style `Filled]
+ in
+ style @ [ label v; `Color color; `Shape `Box ]
+ | Emitter _ as v ->
+- [ label v; `Shape `Diamond; `Color 0xb0c4de; `Style [`Filled] ]
++ [ label v; `Shape `Diamond; `Color 0xb0c4de; `Style `Filled ]
+ | Tuning_parameter _ as v ->
+ [ label v; (*`Style `Dotted;*) `Color 0xb0c4de; ]
+ (*| Correctness_parameter _ (*as v*) -> assert false (*[ label v; `Color 0xb0c4de ]*)*)
+@@ -1495,7 +1495,7 @@ module Consolidation_graph = struct
+ | None -> []
+ | Some s ->
+ let c = emitted_status_color s in
+- [ `Color c; `Fontcolor c; `Style [`Bold] ]
++ [ `Color c; `Fontcolor c; `Style `Bold ]
+
+ let default_vertex_attributes _ = []
+ let default_edge_attributes _ = []
+diff --git a/src/misc/service_graph.ml b/src/misc/service_graph.ml
+index 4f866c5..d158028 100644
+--- a/src/misc/service_graph.ml
++++ b/src/misc/service_graph.ml
+@@ -289,7 +289,7 @@ Src root:%s in %s (is_root:%b) Dst:%s in %s (is_root:%b) [2d case]"
+ color e
+ else
+ match CallG.E.label e with
+- | Inter_services -> [ `Style [`Invis] ]
++ | Inter_services -> [ `Style `Invis ]
+ | Inter_functions | Both -> color e
+
+ let default_edge_attributes _ = []
+@@ -303,7 +303,7 @@ Src root:%s in %s (is_root:%b) Dst:%s in %s (is_root:%b) [2d case]"
+ sg_attributes =
+ [ `Label ("S " ^ cs);
+ `Color (Extlib.number_to_color id);
+- `Style [`Bold] ] }
++ `Style `Bold ] }
+
+ end
+
+diff --git a/src/pdg_types/pdgTypes.ml b/src/pdg_types/pdgTypes.ml
+index 05754e4..74cdebf 100644
+--- a/src/pdg_types/pdgTypes.ml
++++ b/src/pdg_types/pdgTypes.ml
+@@ -626,7 +626,7 @@ module Pdg = struct
+
+ let graph_attributes _ = [`Rankdir `TopToBottom ]
+
+- let default_vertex_attributes _ = [`Style [`Filled]]
++ let default_vertex_attributes _ = [`Style `Filled]
+ let vertex_name v = string_of_int (Node.id v)
+
+ let vertex_attributes v =
+@@ -711,13 +711,13 @@ module Pdg = struct
+ if Dpd.is_ctrl d then (`Arrowtail `Odot)::attrib else attrib
+ in
+ let attrib =
+- if Dpd.is_addr d then (`Style [`Dotted])::attrib else attrib
++ if Dpd.is_addr d then (`Style `Dotted)::attrib else attrib
+ in
+ attrib
+
+ let get_subgraph v =
+ let mk_subgraph name attrib =
+- let attrib = (`Style [`Filled]) :: attrib in
++ let attrib = (`Style `Filled) :: attrib in
+ Some { Graph.Graphviz.DotAttributes.sg_name= name;
+ sg_parent = None;
+ sg_attributes = attrib }
+diff --git a/src/postdominators/print.ml b/src/postdominators/print.ml
+index f2e3a25..15f4ff2 100644
+--- a/src/postdominators/print.ml
++++ b/src/postdominators/print.ml
+@@ -63,7 +63,7 @@ module Printer = struct
+
+ let graph_attributes (title, _) = [`Label title]
+
+- let default_vertex_attributes _g = [`Style [`Filled]]
++ let default_vertex_attributes _g = [`Style `Filled]
+ let default_edge_attributes _g = []
+
+ let vertex_attributes (s, has_postdom) =
+diff --git a/src/semantic_callgraph/register.ml b/src/semantic_callgraph/register.ml
+index 1c79dcc..071f061 100644
+--- a/src/semantic_callgraph/register.ml
++++ b/src/semantic_callgraph/register.ml
+@@ -102,8 +102,8 @@ module Service =
+ let name = Kernel_function.get_name
+ let attributes v =
+ [ `Style
+- [if Kernel_function.is_definition v then `Bold
+- else `Dotted] ]
++ (if Kernel_function.is_definition v then `Bold
++ else `Dotted) ]
+ let entry_point () =
+ try Some (fst (Globals.entry_point ()))
+ with Globals.No_such_entry_point _ -> None
+diff --git a/src/slicing/printSlice.ml b/src/slicing/printSlice.ml
+index c5363f9..211e0bb 100644
+--- a/src/slicing/printSlice.ml
++++ b/src/slicing/printSlice.ml
+@@ -227,7 +227,7 @@ module PrintProject = struct
+
+ let graph_attributes (name, _) = [`Label name]
+
+- let default_vertex_attributes _ = [`Style [`Filled]]
++ let default_vertex_attributes _ = [`Style `Filled]
+
+ let vertex_name v = match v with
+ | Src fi -> SlicingMacros.fi_name fi
+@@ -280,16 +280,16 @@ module PrintProject = struct
+
+ let edge_attributes (e, call) =
+ let attrib = match e with
+- | (Src _, Src _) -> [`Style [`Invis]]
+- | (OptSliceCallers _, _) -> [`Style [`Invis]]
+- | (_, OptSliceCallers _) -> [`Style [`Invis]]
++ | (Src _, Src _) -> [`Style `Invis]
++ | (OptSliceCallers _, _) -> [`Style `Invis]
++ | (_, OptSliceCallers _) -> [`Style `Invis]
+ | _ -> []
+ in match call with None -> attrib
+ | Some call -> (`Label (string_of_int call.sid)):: attrib
+
+ let get_subgraph v =
+ let mk_subgraph name attrib =
+- let attrib = (*(`Label name) ::*) (`Style [`Filled]) :: attrib in
++ let attrib = (*(`Label name) ::*) (`Style `Filled) :: attrib in
+ Some { Graph.Graphviz.DotAttributes.sg_name= name;
+ sg_parent = None;
+ sg_attributes = attrib }
+diff --git a/src/syntactic_callgraph/register.ml b/src/syntactic_callgraph/register.ml
+index d4669c4..d41980e 100644
+--- a/src/syntactic_callgraph/register.ml
++++ b/src/syntactic_callgraph/register.ml
+@@ -37,8 +37,8 @@ module Service =
+ let name v = nodeName v.cnInfo
+ let attributes v =
+ [ match v.cnInfo with
+- | NIVar (_,b) when not !b -> `Style [`Dotted]
+- | _ -> `Style [`Bold] ]
++ | NIVar (_,b) when not !b -> `Style `Dotted
++ | _ -> `Style `Bold ]
+ let equal v1 v2 = id v1 = id v2
+ let compare v1 v2 =
+ let i1 = id v1 in
+diff --git a/src/wp/cil2cfg.ml b/src/wp/cil2cfg.ml
+index 6d8cf09..ba5f410 100644
+--- a/src/wp/cil2cfg.ml
++++ b/src/wp/cil2cfg.ml
+@@ -1278,9 +1278,9 @@ module Printer (PE : sig val edge_txt : edge -> string end) = struct
+ | Vstart | Vend | Vexit -> [`Color 0x0000FF; `Shape `Doublecircle]
+ | VfctIn | VfctOut -> [`Color 0x0000FF; `Shape `Box]
+ | VblkIn _ | VblkOut _ -> [`Shape `Box]
+- | Vloop _ | Vloop2 _ -> [`Color 0xFF0000; `Style [`Filled]]
++ | Vloop _ | Vloop2 _ -> [`Color 0xFF0000; `Style `Filled]
+ | Vtest _ | Vswitch _ ->
+- [`Color 0x00FF00; `Style [`Filled]; `Shape `Diamond]
++ [`Color 0x00FF00; `Style `Filled; `Shape `Diamond]
+ | Vcall _ | Vstmt _ -> []
+ in (`Label (String.escaped label))::attr
+
+@@ -1290,15 +1290,15 @@ module Printer (PE : sig val edge_txt : edge -> string end) = struct
+ let attr = [] in
+ let attr = (`Label (String.escaped (PE.edge_txt e)))::attr in
+ let attr =
+- if is_back_edge e then (`Constraint false)::(`Style [`Bold])::attr
++ if is_back_edge e then (`Constraint false)::(`Style `Bold)::attr
+ else attr
+ in
+ let attr = match (edge_type e) with
+ | Ethen | EbackThen -> (`Color 0x00FF00)::attr
+ | Eelse | EbackElse -> (`Color 0xFF0000)::attr
+- | Ecase [] -> (`Color 0x0000FF)::(`Style [`Dashed])::attr
++ | Ecase [] -> (`Color 0x0000FF)::(`Style `Dashed)::attr
+ | Ecase _ -> (`Color 0x0000FF)::attr
+- | Enext -> (`Style [`Dotted])::attr
++ | Enext -> (`Style `Dotted)::attr
+ | Eback -> attr (* see is_back_edge above *)
+ | Enone -> attr
+ in
+@@ -1308,7 +1308,7 @@ module Printer (PE : sig val edge_txt : edge -> string end) = struct
+
+ let get_subgraph v =
+ let mk_subgraph name attrib =
+- let attrib = (`Style [`Filled]) :: attrib in
++ let attrib = (`Style `Filled) :: attrib in
+ Some { Graph.Graphviz.DotAttributes.sg_name= name;
+ sg_parent = None;
+ sg_attributes = attrib }
+--
diff --git a/sci-mathematics/frama-c/frama-c-20130601.ebuild b/sci-mathematics/frama-c/frama-c-20130601.ebuild
deleted file mode 100644
index 09cfe9644..000000000
--- a/sci-mathematics/frama-c/frama-c-20130601.ebuild
+++ /dev/null
@@ -1,65 +0,0 @@
-# Copyright 1999-2014 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-# $Header: $
-
-EAPI="5"
-
-inherit autotools eutils
-
-DESCRIPTION="Framework for analysis of source codes written in C"
-HOMEPAGE="http://frama-c.com"
-NAME="Fluorine"
-SRC_URI="http://frama-c.com/download/${PN/-c/-c-$NAME}-${PV/_/-}.tar.gz"
-
-LICENSE="LGPL-2"
-SLOT="0"
-KEYWORDS="~amd64 ~ppc ~x86"
-IUSE="doc gtk +ocamlopt"
-RESTRICT="strip"
-
-DEPEND=">=dev-lang/ocaml-3.10.2[ocamlopt?]
- >=dev-ml/ocamlgraph-1.8.2[gtk?,ocamlopt?]
- dev-ml/zarith
- sci-mathematics/ltl2ba
- sci-mathematics/alt-ergo
- gtk? ( >=x11-libs/gtksourceview-2.8
- >=gnome-base/libgnomecanvas-2.26
- >=dev-ml/lablgtk-2.14[sourceview,gnomecanvas,ocamlopt?] )"
-RDEPEND="${DEPEND}"
-
-S="${WORKDIR}/${PN/-c/-c-$NAME}-${PV/_/-}"
-
-src_prepare(){
- rm share/libc/test.c
- touch config_file
- epatch "${FILESDIR}/${PN}-make.patch" \
- "${FILESDIR}/${PN}-ocaml-4.01.patch"
-
- eautoreconf
-}
-
-src_configure(){
- if use gtk; then
- myconf="--enable-gui"
- else
- myconf="--disable-gui"
- fi
-
- econf ${myconf}
-}
-
-src_compile(){
- # dependencies can not be processed in parallel,
- # this is the intended behavior.
- emake -j1 depend
- emake all top DESTDIR="/"
-}
-
-src_install(){
- emake install DESTDIR="${D}"
- dodoc Changelog doc/README
-
- if use doc; then
- dodoc doc/manuals/*.pdf
- fi
-}
diff --git a/sci-mathematics/frama-c/frama-c-20120901.ebuild b/sci-mathematics/frama-c/frama-c-20140301.ebuild
index 2568ba4fc..f93062cc5 100644
--- a/sci-mathematics/frama-c/frama-c-20120901.ebuild
+++ b/sci-mathematics/frama-c/frama-c-20140301.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2014 Gentoo Foundation
+# Copyright 1999-2013 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Header: $
@@ -8,18 +8,19 @@ inherit autotools eutils
DESCRIPTION="Framework for analysis of source codes written in C"
HOMEPAGE="http://frama-c.com"
-NAME="Oxygen"
+NAME="Neon"
SRC_URI="http://frama-c.com/download/${PN/-c/-c-$NAME}-${PV/_/-}.tar.gz"
LICENSE="LGPL-2"
SLOT="0"
-KEYWORDS="~amd64 ~ppc ~x86"
+KEYWORDS="~amd64 ~x86"
IUSE="doc gtk +ocamlopt"
RESTRICT="strip"
-DEPEND=">=dev-lang/ocaml-3.10.2[ocamlopt?]
- >=dev-ml/ocamlgraph-1.8.2[gtk?,ocamlopt?]
+DEPEND=">=dev-lang/ocaml-3.12.1[ocamlopt?]
+ >=dev-ml/ocamlgraph-1.8.5[gtk?,ocamlopt?]
dev-ml/zarith
+ sci-mathematics/coq
sci-mathematics/ltl2ba
sci-mathematics/alt-ergo
gtk? ( >=x11-libs/gtksourceview-2.8
@@ -30,9 +31,9 @@ RDEPEND="${DEPEND}"
S="${WORKDIR}/${PN/-c/-c-$NAME}-${PV/_/-}"
src_prepare(){
- rm share/libc/test.c
touch config_file
-
+ rm -f ocamlgraph.tar.gz
+ epatch "${FILESDIR}/ocamlgraph185_compat.patch"
eautoreconf
}
@@ -42,7 +43,6 @@ src_configure(){
else
myconf="--disable-gui"
fi
-
econf ${myconf} || die "econf failed"
}
@@ -50,14 +50,19 @@ src_compile(){
# dependencies can not be processed in parallel,
# this is the intended behavior.
emake -j1 depend || die "emake depend failed"
- emake all top DESTDIR="/" || die "emake failed"
+ DESTDIR="/" emake all top || die "emake failed"
+
+ if use doc; then
+ emake -j1 doc doc-tgz
+ tar -xzf frama-c-api.tar.gz -C doc/
+ fi
}
src_install(){
- emake install DESTDIR="${D}" || die "emake install failed"
- dodoc Changelog doc/README
+ DESTDIR="${D}" emake install || die "emake install failed"
+ dodoc Changelog
if use doc; then
- dodoc doc/manuals/*.pdf
+ dohtml -A svg -r doc/frama-c-api/*
fi
}
diff --git a/sci-mathematics/frama-c/metadata.xml b/sci-mathematics/frama-c/metadata.xml
index e429e6192..59797bca3 100644
--- a/sci-mathematics/frama-c/metadata.xml
+++ b/sci-mathematics/frama-c/metadata.xml
@@ -1,14 +1,22 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
<pkgmetadata>
-<herd>sci-mathematics</herd>
-<longdescription>
- Frama-C is a suite of tools dedicated to the analysis of the source code
- of software written in C. It gathers several static analysis techniques
- in a single collaborative framework. The collaborative approach of
- Frama-C allows static analyzers to build upon the results already
- computed by other analyzers in the framework. Thanks to this approach,
- Frama-C provides sophisticated tools, such as a slicer and dependency
- analysis.
-</longdescription>
+ <herd>sci</herd>
+ <longdescription>
+ Frama-C is a suite of tools dedicated to the analysis of the source code
+ of software written in C. It gathers several static analysis techniques
+ in a single collaborative framework. The collaborative approach of
+ Frama-C allows static analyzers to build upon the results already
+ computed by other analyzers in the framework. Thanks to this approach,
+ Frama-C provides sophisticated tools, such as a slicer and dependency
+ analysis.
+ </longdescription>
+ <maintainer>
+ <email>sci@gentoo.org</email>
+ </maintainer>
+ <use>
+ <flag name="doc">?doc?</flag>
+ <flag name="gtk">?gtk?</flag>
+ <flag name="ocamlopt">?ocamlopt?</flag>
+ </use>
</pkgmetadata>
diff --git a/sci-mathematics/gappa/ChangeLog b/sci-mathematics/gappa/ChangeLog
index 963d8474a..cb7576ddc 100644
--- a/sci-mathematics/gappa/ChangeLog
+++ b/sci-mathematics/gappa/ChangeLog
@@ -1,23 +1,25 @@
# ChangeLog for sci-mathematics/gappa
-# Copyright 1999-2013 Gentoo Foundation; Distributed under the GPL v2
+# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2
# $Header: $
-*gappa-1.0.0 (12 Aug 2013)
+ 21 Jun 2014; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -gappa-0.16.6.ebuild, +gappa-1.1.1.ebuild:
+ version bump
- 12 Aug 2013; Sébastien Fabbro <bicatali@gentoo.org> +gappa-1.0.0.ebuild,
- -gappa-0.16.3.ebuild:
- sci-mathematics/gappa: Version bump
+ 11 Dec 2013; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -gappa-0.16.3.ebuild, +gappa-0.16.6.ebuild:
+ version bump
- 14 Jan 2013; J.-C. Demay <jcdemay@gmail.com>
- +gappa-0.16.3.ebuild, -gappa-0.15.1.ebuild:
+ 14 Jan 2013; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -gappa-0.15.1.ebuild, +gappa-0.16.3.ebuild:
version bump
- 21 Dec 2011; J.-C. Demay <jcdemay@gmail.com>
- +gappa-0.15.1.ebuild, -gappa-0.14.0.ebuild:
+ 21 Dec 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -gappa-0.14.0.ebuild, +gappa-0.15.1.ebuild:
version bump
- 13 Feb 2011; J.-C. Demay <jcdemay@gmail.com>
- +gappa-0.14.0.ebuild, -gappa-0.13.0.ebuild:
+ 13 Feb 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -gappa-0.13.0.ebuild, +gappa-0.14.0.ebuild:
version bump
04 Jul 2010; Andreas K. Huettel (dilfridge) <mail@akhuettel.de>
@@ -25,10 +27,10 @@
Silence repoman; improve license description; move doc generation
dependencies to RDEPEND
- 04 Jul 2010; J.-C. Demay <jcdemay@gmail.com>
- +gappa-0.13.0.ebuild, -gappa-0.12.1.ebuild:
+ 04 Jul 2010; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -gappa-0.12.1.ebuild, +gappa-0.13.0.ebuild:
version bump
-
- 04 Jul 2010; J.-C. Demay <jcdemay@gmail.com>
+
+ 04 Jul 2010; Jonathan-Christofer Demay <jcdemay@gmail.com>
+metadata.xml, +ChangeLog:
QA fixes
diff --git a/sci-mathematics/gappa/Manifest b/sci-mathematics/gappa/Manifest
index 13ab58c82..9b992ad58 100644
--- a/sci-mathematics/gappa/Manifest
+++ b/sci-mathematics/gappa/Manifest
@@ -1 +1,4 @@
-DIST gappa-1.0.0.tar.gz 390329 SHA256 97b3e40343b12d3a938f69a50dad93f22bf94fff8368ec7359a3e9c23ff049e5 SHA512 75c86a4e2fcd58cec71854a8e40aeee65eceb0b2a9ede9642e91f2eb0a34ff5c64fe2b8c5ffdeb8000c425341e4809c278b869637fe90fc9bcec9339256a9980 WHIRLPOOL f2a244848c0127f152a459ba144eb36ec798305cb7df7e92fd941592457effc064b55be982242d266fa521ba9acf6198c9bc127a716344a524731c5a0a699d87
+DIST gappa-1.1.1.tar.gz 399606 SHA256 b03023d45d246d49fe57b0489cd3b11415b0cbf5aa96e03398d8f5c15284125c SHA512 95b01733554585729d73078522720f0c318f6e86eec02b869717e591bd1477a663c8f71d6c9362f8d5ec83d0a856be5771a27add426d8ac0eca429c4ded01a0e WHIRLPOOL e49860c5832a017a3eb0e8b8a607b56c947f6ce7c1c40c94187f5cfd2c35fd49ef293338b410a6f66ee7b711b0caf3b35d15d99d517a7e5f4c684ec6ca72d466
+EBUILD gappa-1.1.1.ebuild 973 SHA256 0473be6a798d4d201978f1268bc737b017b62e76a2efc0bb0f219cf3adebac64 SHA512 61b38344fda1c69663b577798a0577aeae27f4ebb3d4776df8d2ebebee9c044fbff95d680b86aa9404d2c4015a268f47f8eac2d18fcce0a6ed600a5308c5d2f5 WHIRLPOOL 8c1e2fc63e5ca01a1c073f0da887344cfa464f8a0594988bdba5c659d99f0f53a9dcaceb3c1a7f395c4b4e96739d4277b3b8fbd94769dd85d4afaf21ab50c19a
+MISC ChangeLog 1144 SHA256 7e4792dee61a159df670c0c3449b889282b7f3f4f31f47322a0125c21e5ff7af SHA512 bd90ecf294b538f5ae0a0c59a8eaccd7ef910c0bed10f98e62faa758d5643831da7316b21664dfd95f72be59378314091240907f85c6cc5dc163051c8cd2b0c8 WHIRLPOOL b2480f4a4a8950b2ee62c33ee30cd21db58e50b04d5969ade4c39c802928414e437fc534683e22183595007eb03a9d9ae4109668e9c3d9faf2936d60e62ca48f
+MISC metadata.xml 490 SHA256 0173cf09b7d6a481ce8fde3d4b8d1e56fdd0dc3d2d95e7804cab889043e444fa SHA512 8ea89f502a41f52b332fdd34f973ff6ef0dcd3bdd5da23740fcad179570b1dd7456f5582e714c9c0b93d436c8dd75a6cb304c69724771d209a3930e0a5684831 WHIRLPOOL a9ec88247b0b3c7f4a30909f2471d5d69f104950fae03edbd6fa3d25e3b36974c3248ed39efde50492bc7af86ccc0697f18f4b118d223f385348782ce88a8a13
diff --git a/sci-mathematics/gappa/gappa-1.0.0.ebuild b/sci-mathematics/gappa/gappa-1.0.0.ebuild
deleted file mode 100644
index 3d2c052b6..000000000
--- a/sci-mathematics/gappa/gappa-1.0.0.ebuild
+++ /dev/null
@@ -1,37 +0,0 @@
-# Copyright 1999-2014 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-# $Header: $
-
-EAPI=5
-
-PID=32744
-
-DESCRIPTION="A tool to help verifying and proving properties on floating-point or fixed-point arithmetic"
-HOMEPAGE="http://gappa.gforge.inria.fr/"
-SRC_URI="http://gforge.inria.fr/frs/download.php/${PID}/${P}.tar.gz"
-
-LICENSE="|| ( CeCILL-2 GPL-2 )"
-SLOT="0"
-KEYWORDS="~amd64 ~ppc ~sparc ~x86 ~amd64-linux ~x86-linux"
-IUSE="doc static-libs"
-
-RDEPEND="
- dev-libs/gmp
- dev-libs/mpfr
- dev-libs/boost"
-DEPEND="${RDEPEND}
- doc? ( app-doc/doxygen )"
-
-src_compile(){
- ./remake -d ${MAKEOPTS} || die
- if use doc; then
- cd doc/doxygen
- doxygen Doxyfile || die "doxygen failed"
- fi
-}
-
-src_install(){
- dobin src/gappa
- dodoc README AUTHORS ChangeLog NEWS TODO
- use doc && dohtml -r doc/doxygen/html/*
-}
diff --git a/sci-mathematics/gappa/gappa-1.1.1.ebuild b/sci-mathematics/gappa/gappa-1.1.1.ebuild
new file mode 100644
index 000000000..a817cbbd2
--- /dev/null
+++ b/sci-mathematics/gappa/gappa-1.1.1.ebuild
@@ -0,0 +1,42 @@
+# Copyright 1999-2014 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: $
+
+EAPI="3"
+
+DESCRIPTION="A tool to help verifying and proving properties on floating-point or fixed-point arithmetic"
+HOMEPAGE="http://gappa.gforge.inria.fr/"
+SRC_URI="http://gforge.inria.fr/frs/download.php/33486/${P}.tar.gz"
+
+LICENSE="|| ( CeCILL-2.0 GPL-2 )"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+IUSE="doc"
+
+RDEPEND="dev-libs/gmp
+ dev-libs/mpfr
+ dev-libs/boost"
+DEPEND="${RDEPEND}
+ doc? ( app-doc/doxygen )"
+
+src_prepare() {
+ sed -i Remakefile.in \
+ -e "s:mkdir -p @bindir@:mkdir -p \$(DESTDIR)@bindir@:g" \
+ -e "s:cp src/gappa @bindir@:cp src/gappa \$(DESTDIR)@bindir@:g"
+}
+
+src_compile() {
+ ./remake || die "emake failed"
+ if use doc; then
+ ./remake doc/html/index.html
+ fi
+}
+
+src_install() {
+ DESTDIR="${D}" ./remake install || die "emake install failed"
+ dodoc NEWS README AUTHORS ChangeLog
+ if use doc; then
+ dohtml -A png -r doc/html/*
+ fi
+}
+
diff --git a/sci-mathematics/gappalib-coq/ChangeLog b/sci-mathematics/gappalib-coq/ChangeLog
index a718c8bcd..c2d0ab4fa 100644
--- a/sci-mathematics/gappalib-coq/ChangeLog
+++ b/sci-mathematics/gappalib-coq/ChangeLog
@@ -1,28 +1,32 @@
# ChangeLog for sci-mathematics/gappalib-coq
-# Copyright 1999-2013 Gentoo Foundation; Distributed under the GPL v2
+# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2
# $Header: $
- 03 Mar 2013; Justin Lecher <jlec@gentoo.org> gappalib-coq-0.18.0.ebuild,
- metadata.xml:
+ 21 Jun 2014; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -gappalib-coq-0.18.0.ebuild, -files/gappalib-coq-coq84.patch, gappalib-coq-1.0.0.ebuild:
+ version bump
+
+ 03 Mar 2013; Justin Lecher <jlec@gentoo.org>
+ gappalib-coq-0.18.0.ebuild, metadata.xml:
Drop pcc and sparc keywords as deps are not keyworded; move to EAPI=5
- 14 Jan 2013; J.-C. Demay <jcdemay@gmail.com>
- +gappalib-coq-0.18.0.ebuild,+files/gappalib-coq-coq84.patch,-gappalib-coq-0.16.0.ebuild:
+ 14 Jan 2013; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -gappalib-coq-0.16.0.ebuild, +gappalib-coq-0.18.0.ebuild, +files/gappalib-coq-coq84.patch:
version bump
- 12 Dec 2011; J.-C. Demay <jcdemay@gmail.com>
- +gappalib-coq-0.16.0.ebuild, -gappalib-coq-0.14.1.ebuild:
+ 12 Dec 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -gappalib-coq-0.14.1.ebuild, -gappalib-coq-0.16.0.ebuild:
version bump
- 04 Jul 2010; J.-C. Demay <jcdemay@gmail.com>
- +gappalib-coq-0.14.1.ebuild, -gappalib-coq-0.13.ebuild:
+ 04 Jul 2010; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -gappalib-coq-0.13.ebuild, +gappalib-coq-0.14.1.ebuild:
version bump
- 04 Jul 2010; J.-C. Demay <jcdemay@gmail.com>
- +gappalib-coq-0.13.ebuild, -gappalib-coq-0.12.ebuild:
+ 04 Jul 2010; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -gappalib-coq-0.12.ebuild, +gappalib-coq-0.13.ebuild:
version bump
-
- 04 Jul 2010; J.-C. Demay <jcdemay@gmail.com>
+
+ 04 Jul 2010; Jonathan-Christofer Demay <jcdemay@gmail.com>
+metadata.xml, +ChangeLog:
QA fixes
diff --git a/sci-mathematics/gappalib-coq/Manifest b/sci-mathematics/gappalib-coq/Manifest
index 0af692089..07c2bc137 100644
--- a/sci-mathematics/gappalib-coq/Manifest
+++ b/sci-mathematics/gappalib-coq/Manifest
@@ -1 +1,4 @@
-DIST gappalib-coq-0.18.0.tar.gz 114679 SHA256 817c825ff02efaae88f0696f3e93aeeca854199f229d89ad8f18b16237b261b6 SHA512 b5781e3a35fc8f4a5349730790c815ba60a7cb3777d7be150803d63a57b615ef2f84e5e7c3c01b2a7184eb28c36bf75c8ad368e0818c1abdfda66905e60982d8 WHIRLPOOL 1f08fef5206f7a72afaff601f90e241ad9c984a8a03bad28070016024648032eac5eb8eee32498fdd18b043861f8e329085c893088fb164e5f88076fb07f1fad
+DIST gappalib-coq-1.0.0.tar.gz 118901 SHA256 3c7923b9f3bc9f43225f81e55540441abe76b776d3ca8d34b7898124523d91fb SHA512 1aed7eafc24d82fbb3431e267ae0882560b34864f443fa95b450f465fe571cae558bc0ddf31db96477092518dd20a9870a9f8360ad8a0b3967d6f912c2bd0b67 WHIRLPOOL 61227031eca402aca53ad20d34c74ea51dd4f42b79896e4898f233ee352be5848c087ff34b627ae6bbfbaf433c91fa131b37893bd89a70c97e44aa4c31e3033a
+EBUILD gappalib-coq-1.0.0.ebuild 842 SHA256 149658f79860e60e2940c6bff2c293a3d3793640cd98c5d841063d079a44279c SHA512 620425a8c135c3f8dfb05365a1dabe84cf1ca5210cae30c530fa1f5ad134153109d440c14a8edfc6c5b8916498e4be6997345daadec5f7459997661924ba2113 WHIRLPOOL ec49f8252864da8d4ed6de9ca5b8c3b5e4e9b2692d192dc4e3ec493bce2e4960e3c43f98b900d7a4599057e4620903a50bf50c267ed4fab90addeb5d0c76e4a5
+MISC ChangeLog 1138 SHA256 52a8807833fe0245f555f3dfcfc34590e6078378965a30de80b8be03dd143da7 SHA512 c158b0c6a1d9dc169e8e4fad26d042675020f5e66ab65d11d1491e6eeabd70fd2859cda63c85a07d2a1d67455de9b84b7b0c5b1bcd7ef523c73ecfdfdc4c16e4 WHIRLPOOL 1c865f0ddf8c242d20e1e12d0601f98765dda58309dc6f908f36a5bbf63e70af6772ec847d0258243ed5a90460a736cf0b50628dddde957943e1fd813193849c
+MISC metadata.xml 391 SHA256 e620622efa1a97573ca6acf6b6850c2fb8343a9cd3e176a5bbe4d4359a737e43 SHA512 be73357b6239636b5937fb58dc7d5735b3d87fbd41f696643a7e2975c706c30e4184654268e4ca68e498eb50995d627a3bf17e1b71fa0781f472d8456e386da2 WHIRLPOOL 2e94403f6439e6673062a1fab0e9a1c0038ab9adc9761738fb8fdc8b9ee03de46e958ec3a1e4c2bac0e4965014d36fa21535f826aaa402dbdd9be79e1d3c7b62
diff --git a/sci-mathematics/gappalib-coq/files/gappalib-coq-coq84.patch b/sci-mathematics/gappalib-coq/files/gappalib-coq-coq84.patch
deleted file mode 100644
index 8a6d07447..000000000
--- a/sci-mathematics/gappalib-coq/files/gappalib-coq-coq84.patch
+++ /dev/null
@@ -1,71 +0,0 @@
---- ./src/gappatac.ml.orig 2011-12-24 09:02:53.000000000 -0700
-+++ ./src/gappatac.ml 2012-08-22 16:57:48.106641575 -0600
-@@ -655,7 +655,7 @@ let no_glob f =
-
- (** replace all evars of any type [ty] by [(refl_equal true : ty)] *)
- let evars_to_vmcast sigma (emap, c) =
-- let emap = nf_evars emap in
-+ let emap = nf_evar_map emap in
- let change_exist evar =
- let ty = Reductionops.nf_betaiota emap (Evd.existential_type emap evar) in
- mkCast (mkApp (Lazy.force coq_refl_equal,
-@@ -717,7 +717,7 @@ let gappa_internal gl =
- (** {1 Packaging for [gappa_prepare; gappa_internal]: the [gappa] tactic} *)
- let gappa_prepare =
- let id = Ident (dummy_loc, id_of_string "gappa_prepare") in
-- lazy (Tacinterp.interp (Tacexpr.TacArg (Tacexpr.Reference id)))
-+ lazy (Tacinterp.interp (Tacexpr.TacArg (dummy_loc, Tacexpr.Reference id)))
-
- let gappa gl =
- Coqlib.check_required_library ["Gappa"; "Gappa_tactic"];
---- ./src/Gappa_round.v.orig 2011-12-08 03:17:56.000000000 -0700
-+++ ./src/Gappa_round.v 2012-08-22 16:57:48.106641575 -0600
-@@ -395,7 +395,7 @@ now apply Rlt_not_eq.
- revert H1.
- case rdir.
- intros H1.
--rewrite Nnat.Z_of_N_succ.
-+rewrite N2Z.inj_succ.
- rewrite Z_of_N_ZtoN.
- apply sym_eq.
- apply Zceil_floor_neq.
---- ./src/Gappa_float.v.orig 2011-12-27 15:10:54.000000000 -0700
-+++ ./src/Gappa_float.v 2012-08-22 16:57:48.112641551 -0600
-@@ -526,7 +526,7 @@ simpl (iter_nat (S (nat_of_P p)) positiv
- rewrite Zpos_xO.
- rewrite Zpos_xI.
- ring.
--rewrite Zneg_plus_distr.
-+rewrite <- Pos2Z.add_neg_neg.
- rewrite <- (Zopp_neg p).
- ring.
- apply Rplus_le_reg_r with (Rabs x).
---- ./src/Gappa_tactic.v.orig 2011-12-16 11:33:27.000000000 -0700
-+++ ./src/Gappa_tactic.v 2012-08-22 16:58:28.845476556 -0600
-@@ -567,7 +567,7 @@ destruct o ; try exact H.
- destruct v as [v|v|v w|v w|o v|o v w|v|v|v|v|v|v|f v] ; try exact H.
- destruct o ; try exact H.
- case_eq (RExpr_beq y v) ; intros Hb.
--rewrite <- RExpr_dec_bl with (1 := Hb).
-+rewrite <- internal_RExpr_dec_bl with (1 := Hb).
- 2: now rewrite Hb in H.
- simpl.
- apply <- change_rel_aux.
-@@ -609,7 +609,7 @@ rewrite Gappa_dyadic.Fopp2_correct.
- apply -> change_rel_aux.
- split.
- now apply (Gappa_dyadic.Fpos0_correct (Float2 (Zpos m) e)).
--rewrite <- RExpr_dec_bl with (1 := Hb) in H.
-+rewrite <- internal_RExpr_dec_bl with (1 := Hb) in H.
- simpl in H1.
- now rewrite H1.
- Qed.
-@@ -797,7 +797,7 @@ change (convert_goal_aux gc gh).
- destruct a as [l' v u'|v w l' u'|v w|v w|] ; try (apply IHgh ; try apply H ; easy).
- simpl in H.
- case_eq (RExpr_beq e v) ; intros H3 ; rewrite H3 in H.
--rewrite (RExpr_dec_bl _ _ H3) in H1, IHgh.
-+rewrite (internal_RExpr_dec_bl _ _ H3) in H1, IHgh.
- generalize (Gminmax_correct _ _ _ _ _ H1 H2).
- destruct (Gmax_lower l l') as [l''|].
- destruct (Gmin_upper u u') as [u''|].
diff --git a/sci-mathematics/gappalib-coq/gappalib-coq-0.18.0.ebuild b/sci-mathematics/gappalib-coq/gappalib-coq-0.18.0.ebuild
deleted file mode 100644
index 1ee9363fa..000000000
--- a/sci-mathematics/gappalib-coq/gappalib-coq-0.18.0.ebuild
+++ /dev/null
@@ -1,35 +0,0 @@
-# Copyright 1999-2014 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-# $Header: $
-
-EAPI=5
-
-inherit eutils
-
-DESCRIPTION="Allows the certificates Gappa generates to be imported by Coq"
-HOMEPAGE="http://gappa.gforge.inria.fr/"
-SRC_URI="http://gforge.inria.fr/frs/download.php/30081/${P}.tar.gz"
-
-LICENSE="LGPL-2"
-SLOT="0"
-KEYWORDS="~amd64 ~x86"
-IUSE=""
-
-DEPEND="
- sci-mathematics/gappa
- sci-mathematics/coq
- sci-mathematics/flocq"
-RDEPEND="${DEPEND}"
-
-src_prepare(){
- sed \
- -e "s/if test \"\$libdir\" = '\${exec_prefix}\/lib';/ \
- if test \"\$libdir\" = '\${exec_prefix}\/lib' -o "\$libdir" = \"\${prefix}\/lib64\";/g" \
- -i configure || die
-
- epatch "${FILESDIR}"/gappalib-coq-coq84.patch
-}
-
-src_compile(){
- emake DESTDIR="/"
-}
diff --git a/sci-mathematics/gappalib-coq/gappalib-coq-1.0.0.ebuild b/sci-mathematics/gappalib-coq/gappalib-coq-1.0.0.ebuild
new file mode 100644
index 000000000..01d90eede
--- /dev/null
+++ b/sci-mathematics/gappalib-coq/gappalib-coq-1.0.0.ebuild
@@ -0,0 +1,35 @@
+# Copyright 1999-2014 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: $
+
+EAPI="3"
+
+DESCRIPTION="Allows the certificates Gappa generates to be imported by the Coq"
+HOMEPAGE="http://gappa.gforge.inria.fr/"
+SRC_URI="http://gforge.inria.fr/frs/download.php/32743/${P}.tar.gz"
+
+LICENSE="LGPL-2"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+IUSE=""
+
+DEPEND="sci-mathematics/gappa
+ sci-mathematics/coq
+ sci-mathematics/flocq"
+RDEPEND="${DEPEND}"
+
+src_prepare() {
+ sed -i Remakefile.in \
+ -e "s:mkdir -p @libdir@:mkdir -p \${DESTDIR}@libdir@:g" \
+ -e "s:cp \$(OBJS) \$(MLTARGETS) @libdir@:cp \$(OBJS) \$(MLTARGETS) \${DESTDIR}@libdir@:g"
+}
+
+src_compile() {
+ ./remake || die "emake failed"
+}
+
+src_install() {
+ DESTDIR="${D}" ./remake install || die "emake install failed"
+ dodoc NEWS README AUTHORS ChangeLog
+}
+
diff --git a/sci-mathematics/giac/ChangeLog b/sci-mathematics/giac/ChangeLog
index a9a4fb63c..0d8189d5a 100644
--- a/sci-mathematics/giac/ChangeLog
+++ b/sci-mathematics/giac/ChangeLog
@@ -1,15 +1,16 @@
# ChangeLog for sci-mathematics/giac
-# Copyright 1999-2013 Gentoo Foundation; Distributed under the GPL v2
+# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2
# $Header: $
- 03 Mar 2013; Justin Lecher <jlec@gentoo.org> giac-1.0.0.ebuild, metadata.xml:
- Drop useless blank line
+ 21 Jun 2014; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -giac-1.0.0.ebuild, +giac-1.1.0.ebuild:
+ version bump
- 14 Jan 2013; J.-C. Demay <jcdemay@gmail.com>
- +giac-1.0.0.ebuild, -giac-0.9.2.ebuild:
+ 14 Jan 2013; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -giac-0.9.2.ebuild, +giac-1.0.0.ebuild:
version bump
-
- 16 May 2011; J.-C. Demay <jcdemay@gmail.com>
+
+ 16 May 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
giac-0.9.2.ebuild, +metadata.xml:
QA fixes
diff --git a/sci-mathematics/giac/Manifest b/sci-mathematics/giac/Manifest
index 44807076d..fa7199f58 100644
--- a/sci-mathematics/giac/Manifest
+++ b/sci-mathematics/giac/Manifest
@@ -1 +1,4 @@
-DIST giac-1.0.0.tar.gz 32734007 SHA256 09abe51f7caf14a925a46cee062c5918e765da6a9d30279eacc5ec177018d136 SHA512 15f3aa44ff9f48f78f868a5883b48804d95cce34661a77f3af6f105036ce90a6a4b820de62a283b0dabe3a2ddc367e1762e71e7c4ea9dab4dc8ce9455ad142dc WHIRLPOOL d79147da29b021e6deda67cfb83bd330aa642e0c81f279ab3b6476f55f62d9dd27cee3f481f047095c4cfe98eae5d725b9fa4ce8b61a75f36d6b0378742a1875
+DIST giac-1.1.0.tar.bz2 43295079 SHA256 8d4f96a577d526caa201d8311f462828b92eead2938b00e563b208b4e255a340 SHA512 2b34c7913a6a24aa770094bc839c01f7f3d16689ed9673d56b72ce39d07004e20218e039c85fb15e9f39f5f9e6993e6cfff62e755997f1107cddf7e601658434 WHIRLPOOL ca761a1f2bd6ad88655a079a29f54344d101542ba7a0c09fe7d8e0077e36ab06235341210a7b2a0ef98d09d416756be2725b9cc7be676957eaa199a67d67e375
+EBUILD giac-1.1.0.ebuild 1584 SHA256 3f6e83335d17450daa946c8fce064f3665a1a8f323d497000fb779c72fa86783 SHA512 08448895b4516b45d36d4f00660b7e5db0bcbff7aa3d54d1f6dfbffd958ff70c5a0861a3e0a954815627821308bd874f95c095aff989d63c30336cce945909e2 WHIRLPOOL 8b1a7d95b2cf471866cd10b25678c9062e00d9263f2b890c32c7748c945fb790b37daca944de565dac03e8ca08bd3b3219348506f9de0f17b468d84099df6968
+MISC ChangeLog 468 SHA256 945086ff54464166ef56ea6ce1e7f55cd196bbd80eaae6ad5c66a336c4a93729 SHA512 8f2159b346d1682d9661ea2d1bda9b05fefd3e79aa5563cd6e27fb4d8890d408abeb5bf0ca99429afd3c8203ab6bf7add2d10794c3e7a72879f5212a0e488b48 WHIRLPOOL 0df1e8f8553bdd02eef2341ac3f69cf58f39e0aa51118793f3d67d232b6dff6cd55afec7029f4ca42dc922474408afa4d6c350dfe9a2036e1a9bf78c2e999f47
+MISC metadata.xml 736 SHA256 cea04b87fc7389fe4e214ec7548e8234d1c81ac63022314ecfbfdbc48f7d3d08 SHA512 ae0a3ed705e0240f3d40b7e7375b59f3aaf68b1551da8dbff5d022748bf064c5b21f8e2c3cd673ab7e4915c97b0025c71f2c5340896405e87acd249e2b457201 WHIRLPOOL e3c03dd7218b1bff8b50a6f09691f88a14ba788221ff8c35db17952783bba4e101f3c80232d1af852c7ab44d56c2252f8b598a0df62e7021e1e9b5fd21f41530
diff --git a/sci-mathematics/giac/giac-1.0.0.ebuild b/sci-mathematics/giac/giac-1.1.0.ebuild
index 95fe44fda..d48ef0490 100644
--- a/sci-mathematics/giac/giac-1.0.0.ebuild
+++ b/sci-mathematics/giac/giac-1.1.0.ebuild
@@ -6,22 +6,20 @@ EAPI="4"
DESCRIPTION="A free C++ CAS (Computer Algebra System) library and its interfaces"
HOMEPAGE="http://www-fourier.ujf-grenoble.fr/~parisse/giac.html"
-SRC_URI="http://www-fourier.ujf-grenoble.fr/~parisse/giac/giac_frozen.tgz -> ${P}.tar.gz"
+SRC_URI="http://www-fourier.ujf-grenoble.fr/~parisse/${PN}/${P}.tar.bz2"
LICENSE="GPL-2"
SLOT="0"
KEYWORDS="~x86 ~amd64"
IUSE="doc examples fltk"
-RDEPEND="
- >=dev-libs/gmp-3
- >=sys-libs/readline-4.2
- dev-libs/mpfr
- sci-libs/gsl
- >=sci-mathematics/pari-2.3
- >=dev-libs/ntl-5.2
- fltk? ( >=x11-libs/fltk-1.1.9 )"
-DEPEND="${RDEPEND}"
+RDEPEND=">=dev-libs/gmp-3
+ >=sys-libs/readline-4.2
+ fltk? ( >=x11-libs/fltk-1.1.9 )
+ dev-libs/mpfr
+ sci-libs/gsl
+ >=sci-mathematics/pari-2.3
+ >=dev-libs/ntl-5.2"
src_prepare(){
sed -e "s:\$(prefix)/share:\$(DESTDIR)\$(prefix)/share:g" \
@@ -35,25 +33,26 @@ src_prepare(){
}
src_install() {
- emake DESTDIR="${D}" install || die "emake install failed"
- mv "${D}"/usr/bin/{aide,giac-help}
- rm "${D}"/usr/bin/*cas_help
- dodoc AUTHORS ChangeLog INSTALL NEWS README TROUBLES
+ DESTDIR="${D}" emake install || die "emake install failed"
+ mv ${D}/usr/bin/{aide,giac-help}
+ rm ${D}/usr/bin/*cas_help
+ dodoc AUTHORS ChangeLog COPYING INSTALL NEWS README TROUBLES
if use !fltk; then
- rm "${D}"/usr/bin/x*
+ rm ${D}/usr/bin/x*
fi
if use !doc; then
- rm -R "${D}"/usr/share/doc/giac "${D}"/usr/share/giac/doc/
+ rm -R ${D}/usr/share/doc/giac ${D}/usr/share/giac/doc/
else
for LANG in el en es fr pt; do
if echo ${LINGUAS} | grep -v $LANG &> /dev/null; then
- rm -R "${D}"/usr/share/giac/doc/$LANG
+ rm -R ${D}/usr/share/giac/doc/$LANG
else
- ln "${D}"/usr/share/giac/doc/aide_cas "${D}"/usr/share/giac/doc/$LANG/aide_cas
+ ln ${D}/usr/share/giac/doc/aide_cas ${D}/usr/share/giac/doc/$LANG/aide_cas
fi
done
fi
if use !examples; then
- rm -R "${D}"/usr/share/giac/examples
+ rm -R ${D}/usr/share/giac/examples
fi
}
+
diff --git a/sci-mathematics/giac/metadata.xml b/sci-mathematics/giac/metadata.xml
index f2342ef59..58559f4ee 100644
--- a/sci-mathematics/giac/metadata.xml
+++ b/sci-mathematics/giac/metadata.xml
@@ -1,12 +1,20 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
<pkgmetadata>
-<herd>sci</herd>
-<longdescription>
- Giac is a free computer algebra system that can be used to perform
- computer algebra, function graphs, interactive geometry (2-d and 3-d),
- spreadsheet and statistics, programmation. It may be used as a replacement
- for high end graphic calculators for example on netbooks (for about
- the same price as a calculator but with much more performances).
-</longdescription>
+ <herd>sci</herd>
+ <longdescription>
+ Giac is a free computer algebra system that can be used to perform
+ computer algebra, function graphs, interactive geometry (2-d and 3-d),
+ spreadsheet and statistics, programmation. It may be used as a replacement
+ for high end graphic calculators for example on netbooks (for about
+ the same price as a calculator but with much more performances).
+ </longdescription>
+ <maintainer>
+ <email>sci@gentoo.org</email>
+ </maintainer>
+ <use>
+ <flag name="doc">?doc?</flag>
+ <flag name="examples">?examples?</flag>
+ <flag name="fltk">?fltk?</flag>
+ </use>
</pkgmetadata>
diff --git a/sci-mathematics/ltl2ba/Manifest b/sci-mathematics/ltl2ba/Manifest
index f91bcb6ff..49e2867aa 100644
--- a/sci-mathematics/ltl2ba/Manifest
+++ b/sci-mathematics/ltl2ba/Manifest
@@ -1 +1,4 @@
DIST ltl2ba-1.1.tar.gz 29629 SHA256 a66bf05bc3fd030f19fd0114623d263870d864793b1b0a2ccf6ab6a40e7be09b
+EBUILD ltl2ba-1.1.ebuild 595 SHA256 35f637528fd4112b694d54cff4ab80713b8b6ddc2501b2b215c7e33675363f50 SHA512 5c91946ff3508944005ab386d6d09227eb45ce1bd11664954ae35ac084c8596802688935883aa7b5ab5b8850844a4dfee41f866632e041a193577b5fc4a97bde WHIRLPOOL 3334659acd69ca48612235188d44ea8ab052747a2f075c1fa6b1ae6edb4d63d2e1d407c40331ca6dcacd9608b87d0365c4e09714dc82b857532db0f5f2358d78
+MISC ChangeLog 244 SHA256 8c2728eab50fd614e4fa10da7e8a571d363594a89741f9f029b32e89c6134849 SHA512 4b896c379a4a22fb897b28c41db4e14db5ff6917fd3411b40e79e34b3e4d578b8bdb9fe86bed54d856f10cee1b93bff4d91196da61e588dc5e67a01725e85063 WHIRLPOOL 9d5f2a28da5b290ceb1e5c0f421abb8b2431c57e5b3b505b3f8120f3a8a2591cbd40e2d90a1a271def02959e2b9c7d1492429bc912e102cddc34de4d4bbc8d5b
+MISC metadata.xml 215 SHA256 13f32353652adbd3d934d41381cfc2cacc9e1127c508cebc73806cc1026ee80c SHA512 32f8ab6332992da04397ac0cbf0c632d6cb834e02b3f22e64fbd0147dcdf57052dc872b3118d2de1f95b81c735552db27fed40a750c55658944b38425393c674 WHIRLPOOL a1136483bd80ce0a497ea946c03e3d805d04fd7f6b0bdd6af73c96d043c1acd88a53d328256b62becff6fbb2c844562d9ceb3cfaab158ad39f7728617738035b
diff --git a/sci-mathematics/ltl2ba/ltl2ba-1.1.ebuild b/sci-mathematics/ltl2ba/ltl2ba-1.1.ebuild
index e3d9bdb69..c0bf64418 100644
--- a/sci-mathematics/ltl2ba/ltl2ba-1.1.ebuild
+++ b/sci-mathematics/ltl2ba/ltl2ba-1.1.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2014 Gentoo Foundation
+# Copyright 1999-2010 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Header: $
@@ -8,7 +8,7 @@ SRC_URI="http://www.lsv.ens-cachan.fr/~gastin/${PN}/${P}.tar.gz"
LICENSE="GPL-2"
SLOT="0"
-KEYWORDS="~amd64 ~ppc ~sparc ~x86"
+KEYWORDS="~amd64 ~x86"
IUSE=""
RDEPEND=""
diff --git a/sci-mathematics/ltl2ba/metadata.xml b/sci-mathematics/ltl2ba/metadata.xml
index b229aec85..efb490d78 100644
--- a/sci-mathematics/ltl2ba/metadata.xml
+++ b/sci-mathematics/ltl2ba/metadata.xml
@@ -2,4 +2,7 @@
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
<pkgmetadata>
<herd>sci</herd>
+<maintainer>
+ <email>sci@gentoo.org</email>
+</maintainer>
</pkgmetadata>
diff --git a/sci-mathematics/pff/ChangeLog b/sci-mathematics/pff/ChangeLog
index ab00b672e..1f0a01a14 100644
--- a/sci-mathematics/pff/ChangeLog
+++ b/sci-mathematics/pff/ChangeLog
@@ -1,19 +1,20 @@
# ChangeLog for sci-mathematics/pff
-# Copyright 1999-2013 Gentoo Foundation; Distributed under the GPL v2
+# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2
# $Header: $
- 03 Mar 2013; Justin Lecher <jlec@gentoo.org> pff-8.4.ebuild, metadata.xml:
- Drop pcc and sparc keywords as deps are not keyworded; move to EAPI=5
+ 21 Jun 2014; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ pff-8.4.ebuild:
+ install fixes
- 14 Jan 2013; J.-C. Demay <jcdemay@gmail.com>
- +pff-8.4.ebuild, -pff-8.3.ebuild:
+ 14 Jan 2013; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -pff-8.3.ebuild, +pff-8.4.ebuild:
version bump
- 21 Dec 2011; J.-C. Demay <jcdemay@gmail.com>
- +pff-8.3.ebuild, -pff-8.2.1.2.ebuild:
+ 21 Dec 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -pff-8.2.1.2.ebuild, +pff-8.3.ebuild:
version bump
- 04 Jul 2010; J.-C. Demay <jcdemay@gmail.com>
+ 04 Jul 2010; Jonathan-Christofer Demay <jcdemay@gmail.com>
+metadata.xml, +ChangeLog:
QA fixes
diff --git a/sci-mathematics/pff/Manifest b/sci-mathematics/pff/Manifest
index eabef8165..b0d27029f 100644
--- a/sci-mathematics/pff/Manifest
+++ b/sci-mathematics/pff/Manifest
@@ -1 +1,4 @@
DIST Float8.4.tgz 352313 SHA256 3436b4521ac8bb24850920f404994579174f5b20d1178d48dbd686ec109ef27c SHA512 4e53aad0a59d6875f071584a34b91029a51e8d797e2f5c1a51c772973b241ebda093463532653dbc54245bd03b2414d648648670c6658547c908403cbe6d1275 WHIRLPOOL 2bfe679b50a5ccb6aec88403a85766b774a416c56d94dd640d00577a35d2d3a06b7d91795285ba0e57c17f6bdcc19d71ffa2a7ab5f796b4e2e2366c195f557b5
+EBUILD pff-8.4.ebuild 819 SHA256 511ce39236b5927c89eb0ea178ecd223978c2698d4b7ba66dcd07c8d8c4e9153 SHA512 a006a4c0456ed38253af10fbf68028096d8dd35444bda2d939aa21df1e2fb486ccd9c7aee9c90618b34a26b79dcf90a1e932f5ad01b65bc3db96f6caf396dc35 WHIRLPOOL 8a161cec44c6885d61de31d152a40c2835187dc0ca2c3718d5100bdf2fd4b603c338783568173ee42355d9fb5e5b13343dea28677c6c50df7b5c39ce91cd5a4b
+MISC ChangeLog 548 SHA256 b6cffe39b5dbd7689087acd4f4cef764e01471c7bfa6b34e66641c988bed7e9a SHA512 249cd8d6d9ee5f4489ce8ff730954319143ae032397c86fcce7394620d44c43614e5900dc0d8dfba205b999f837a15dfc58424a7236af04cc02ff833723f2d01 WHIRLPOOL 22d67cf3990fd12f02ad7d74099b7c7325d7702afc06b2e3bd81e58e583fe9ba26de184798e1573d09d0a14ddca1aa934c0203e98853012776ae4e0ee93af5fb
+MISC metadata.xml 497 SHA256 3ba778defe74a0a683099bd44b6f279b64bd6860c0c9ea53b5be8bb60c1b4340 SHA512 e8f4a2bd92a1a8f9997f43c9ddd3ad18bf56a0d0314514bac0f8e8a4439bf4a56fb33a80dd1cb910af74173a83d8abd80a390b510e90ede1b6ef8029f51d35cc WHIRLPOOL 15eeacfbccbba5a61a6ea1f853f0ed6b620b66a0b576cd4699ddc5c5d1afcb212dc24a28fde0ba73a5cf0b1a2d9d42af63cf6a6137fac878ac132a05cad1b955
diff --git a/sci-mathematics/pff/metadata.xml b/sci-mathematics/pff/metadata.xml
index 0a23bf26c..edab690a5 100644
--- a/sci-mathematics/pff/metadata.xml
+++ b/sci-mathematics/pff/metadata.xml
@@ -1,11 +1,14 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
<pkgmetadata>
-<herd>sci-mathematics</herd>
-<longdescription>
- PFF (Preuves Formelles sur les Flottants = Formal Proofs about Floats)
- is a repository of a Coq library about floating-point arithmetic. It
- contains both definitions and proofs of basic facts, old and new
- properties and algorithms.
-</longdescription>
+ <herd>sci</herd>
+ <longdescription>
+ PFF (Preuves Formelles sur les Flottants = Formal Proofs about Floats)
+ is a repository of a Coq library about floating-point arithmetic. It
+ contains both definitions and proofs of basic facts, old and new
+ properties and algorithms.
+ </longdescription>
+ <maintainer>
+ <email>sci@gentoo.org</email>
+ </maintainer>
</pkgmetadata>
diff --git a/sci-mathematics/pff/pff-8.4.ebuild b/sci-mathematics/pff/pff-8.4.ebuild
index 183dd611d..747366c36 100644
--- a/sci-mathematics/pff/pff-8.4.ebuild
+++ b/sci-mathematics/pff/pff-8.4.ebuild
@@ -1,8 +1,8 @@
-# Copyright 1999-2014 Gentoo Foundation
+# Copyright 1999-2013 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Header: $
-EAPI=5
+EAPI="2"
DESCRIPTION="Library for reasoning about floating point numbers in coq"
HOMEPAGE="http://lipforge.ens-lyon.fr/www/pff/"
@@ -19,12 +19,16 @@ RDEPEND="${DEPEND}"
S="${WORKDIR}/Float${PV}"
src_prepare() {
- sed \
- -e "s|\`\$(COQC) -where\`/user-contrib| \
- \$(DESTDIR)/\`\$(COQC) -where\`/user-contrib|g" \
- -i Makefile || die
+ sed -i Makefile \
+ -e "s|\`\$(COQC) -where\`/user-contrib|\$(DSTROOT)/\`\$(COQC) -where\`/user-contrib|g" \
+ -e "s|VOFILESINC=\$(filter \$(wildcard \./\*),\$(VOFILES))|VOFILESINC:=\$(filter-out ,\$(VOFILES))|g"
}
src_compile(){
- emake DESTDIR="/"
+ emake || die "emake failed"
}
+
+src_install(){
+ emake install DSTROOT="${D}" || die "emake install failed"
+}
+
diff --git a/sci-mathematics/why/ChangeLog b/sci-mathematics/why/ChangeLog
index 9a38faea6..f4b826ec9 100644
--- a/sci-mathematics/why/ChangeLog
+++ b/sci-mathematics/why/ChangeLog
@@ -1,19 +1,20 @@
# ChangeLog for sci-mathematics/why
-# Copyright 1999-2013 Gentoo Foundation; Distributed under the GPL v2
+# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2
# $Header: $
- 03 Mar 2013; Justin Lecher <jlec@gentoo.org> why-2.30.ebuild, metadata.xml:
- Drop ppc as deps are not keyworded; move to EAPI=5 and autotools-utils.eclass
+ 21 Jun 2014; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -why-2.30.ebuild, -files/why-2.30.patch, +why-2.34.ebuild, +why-flocq23.patch:
+ version bump
- 21 Dec 2011; J.-C. Demay <jcdemay@gmail.com>
- -why-2.29.ebuild, +why-2.30.ebuild, -files/why_jessie-carbon.patch, +files/why-2.30.patch:
+ 21 Dec 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ -why-2.29.ebuild, -files/why_jessie-carbon.patch, +why-2.30.ebuild, +files/why-2.30.patch:
version bump
- 06 May 2011; J.-C. Demay <jcdemay@gmail.com>
+ 06 May 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
-why-2.28.ebuild, +why-2.29.ebuild:
version bump
- 14 Feb 2011; J.-C. Demay <jcdemay@gmail.com>
+ 14 Feb 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
-why-2.26.ebuild, +why-2.28.ebuild, +files/why_jessie-carbon.patch:
version bump
@@ -21,11 +22,11 @@
why-2.26.ebuild:
Silenced repoman; dropped ~sparc since dependencies cannot be fulfilled.
- 08 Jul 2010; J.-C. Demay <jcdemay@gmail.com>
+ 08 Jul 2010; Jonathan-Christofer Demay <jcdemay@gmail.com>
-why-2.19.ebuild, +why-2.26.ebuild:
version Bump
- 08 Jul 2010; J.-C. Demay <jcdemay@gmail.com>
+ 08 Jul 2010; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ChangeLog, +metadata.xml:
QA fixes
diff --git a/sci-mathematics/why/Manifest b/sci-mathematics/why/Manifest
index 939ac0bbf..84a0f1c1e 100644
--- a/sci-mathematics/why/Manifest
+++ b/sci-mathematics/why/Manifest
@@ -1 +1,5 @@
-DIST why-2.30.tar.gz 3530934 SHA256 88e78f6ec684e5a2a89d4525159b6a622936614a3bd0fc1ad358e8b387a50d64
+AUX why-flocq23.patch 488 SHA256 3165cadaeeacd74f84f543d731f3823cf4d5b9c66235792754b38fca1dec57c2 SHA512 7cb3797b78cf7ed47953eead8bf0bca4ac202e5f1f060c74810fea7d72ebaf9d182400f88a8b1a6f4db813bd5d7c37315bb8596e210c91d6ac7c11f6126ec689 WHIRLPOOL 5a3bcbd255d46dc9c091c36c7dbfdf85e261d82da1d97db133af5c50c2c5c68b1fb46a19d49913573c5b35c8e1aefa05df5b2ed033a88f2c2b57308da7c1cc76
+DIST why-2.34.tar.gz 4019877 SHA256 4f861757c13cb7dd4ba8c0c640f04115be147d2d4ca8a55035048e9d305c658c SHA512 e4abf6573cff52fcfe5c6b867ec15f6f65a88c9892143681b74e3a35caa870acdf04fdda6fc67790af608975bb688c6ec14fc12f2e44b319abdd262ac59384a7 WHIRLPOOL 1d3383241647b5e676f4476898fb9c5580c27a3dbd43cd29b3e9ee4460b11610d9b321deb92c5921f4499fba325da17d8c329f3e58edf9389e93b03f2e83af98
+EBUILD why-2.34.ebuild 1491 SHA256 517f57178d7796f14fd551fe6bac57da78a142122852c658ef24affc345b12e0 SHA512 b6c126e2fc1ae1b6546b5d18f3b4fcdb67be483906e1904783b6e46970713d1a75b841d58b0873bb53527a85217ee6a3add47d7c789edb6445cf811906faa145 WHIRLPOOL 073087b8acf2454e159ee63a8865a1fc1ba35cda96765736f9bb3ae8a015704d6c05e6dbb4575dacc70058008b6674b8a7886de433aa6397b1a295c820a1283c
+MISC ChangeLog 1088 SHA256 ba7b9448e22cbdccf3c77497f8ad2edc4e09660093b6509c9ccf3a0ca33d40a7 SHA512 f1f236eff906c65b32e8dce51d34b124ec91036d16a30a92c8526c490cec4f27e2889ce1a68857099af9c47a1384b84841d1003004893ba5968dbdf879d45b1d WHIRLPOOL 6dabc8f18f30174e4a21206550046d88964e06dc71054f172c059447d704cbdedcfc831f08f9f320afb7e42f615ab318bf40c72bcd1cdb171dd87ebaa77b9755
+MISC metadata.xml 871 SHA256 039164bfd4f3369e6ef0ee6c5e934a7f5f119f5203bb3b0e995d8ad61594df5b SHA512 5f641c52001d1d2d1e82b6fc104bffb90913d561c680afc4d48890c29616c2e035471052ed77bb42cb0fb3ebdcbcea2fd69c07ee72e4f2787b1c07fba57b86a8 WHIRLPOOL 26b3b7ace4be726a20f4b8f78cf5dcb2b56a56af3838e3dc2a3aa9517df34dd5971649c5653e00ca38cc681e3a17894ff79942b2f3448dc8885cba1136521bfb
diff --git a/sci-mathematics/why/files/why-2.30.patch b/sci-mathematics/why/files/why-2.30.patch
deleted file mode 100644
index 2c8f48cf1..000000000
--- a/sci-mathematics/why/files/why-2.30.patch
+++ /dev/null
@@ -1,36 +0,0 @@
-diff -Naurp why-2.30-orig/jc/jc_annot_inference.ml why-2.30-save/jc/jc_annot_inference.ml
---- why-2.30-orig/jc/jc_annot_inference.ml 2011-10-24 15:21:06.000000000 +0000
-+++ why-2.30-save/jc/jc_annot_inference.ml 2011-12-21 18:08:50.920338014 +0000
-@@ -147,6 +147,7 @@ let rec destruct_pointer t =
- let offt = new term ~typ:integer_type tnode in
- Some(tptr,offt)
- end
-+ | JCTlet _
- | JCTvar _ | JCTderef _ | JCTapp _ | JCTold _ | JCTat _ | JCTif _
- | JCTrange _ | JCTmatch _ | JCTaddress _ | JCTbase_block _
- | JCTconst _ | JCTbinary _ | JCTunary _ | JCToffset _ | JCTinstanceof _
-@@ -491,7 +492,7 @@ let reg_annot ?id ?kind ?name ~pos ~anch
- in
- Format.fprintf Format.str_formatter "%a" Jc_output.assertion a;
- let formula = Format.flush_str_formatter () in
-- let lab = Output.reg_pos "G" ?id ?kind ?name ~formula loc in
-+ let lab = Output.old_reg_pos "G" ?id ?kind ?name ~formula (Loc.extract loc) in
- new assertion_with ~mark:lab a
-
-
-@@ -608,6 +609,7 @@ let rec atp_of_term t =
- Atp.Fn(atp_of_unop uop, [atp_of_term t1])
- | JCTvar _ | JCTderef _ | JCTapp _ | JCToffset _ ->
- Atp.Var (Vwp.variable_for_term t)
-+ | JCTlet _
- | JCTshift _ | JCTold _ | JCTat _ | JCTmatch _ | JCTinstanceof _
- | JCTcast _ | JCTrange_cast _ | JCTbitwise_cast _ | JCTreal_cast _
- | JCTaddress _ | JCTif _ | JCTrange _ | JCTunary _ | JCTbase_block _ ->
-@@ -1194,6 +1196,7 @@ let linearize t =
- (coeffs, minus_num cst1)
- | _ -> err ()
- end
-+ | JCTlet _
- | JCTvar _ | JCTderef _ | JCToffset _ | JCTapp _ | JCTbinary _
- | JCTunary _ | JCTshift _ | JCTinstanceof _ | JCTmatch _
- | JCTold _ | JCTat _ | JCTcast _ | JCTbitwise_cast _
diff --git a/sci-mathematics/why/files/why-flocq23.patch b/sci-mathematics/why/files/why-flocq23.patch
new file mode 100644
index 000000000..b54d85a38
--- /dev/null
+++ b/sci-mathematics/why/files/why-flocq23.patch
@@ -0,0 +1,11 @@
+--- lib/coq/WhyFloats.v.orig 2014-03-17 16:01:46.000000000 -0600
++++ lib/coq/WhyFloats.v 2014-04-21 15:39:55.680771647 -0600
+@@ -108,7 +108,7 @@
+ generalize (Zeq_bool_eq _ _ H1). clear.
+ rewrite Fcalc_digits.Z_of_nat_S_digits2_Pnat.
+ intros H.
+-apply (Fcalc_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
++apply (Fcore_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
+ revert H.
+ unfold FLT_exp.
+ generalize (Fcore_digits.Zdigits radix2 (Zpos m)).
diff --git a/sci-mathematics/why/metadata.xml b/sci-mathematics/why/metadata.xml
index 43f4d4f50..06bd0a5f2 100644
--- a/sci-mathematics/why/metadata.xml
+++ b/sci-mathematics/why/metadata.xml
@@ -1,19 +1,24 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
<pkgmetadata>
-<herd>sci-mathematics</herd>
-<longdescription>
- Why is a software verification platform. It contains a general-purpose
- verification condition generator (VCG) which is used as a back-end
- by other verification tools but it can also be used directly to verify
- programs. It also provides Krakatoa, a tool or the verification of Java
- programs and Caduceus, a tool for the verification of C programs.
-</longdescription>
-<use>
- <flag name="apron">Support for <pkg>sci-mathematics/apron</pkg></flag>
- <flag name="coq">Support for <pkg>sci-mathematics/coq</pkg></flag>
- <flag name="gappa">Support for <pkg>sci-mathematics/gappa</pkg></flag>
- <flag name="jessie">Support for <pkg>sci-mathematics/frama-c</pkg></flag>
- <flag name="pff">Support for <pkg>sci-mathematics/pff</pkg></flag>
- </use>
+ <herd>sci</herd>
+ <longdescription>
+ Why is a software verification platform. It contains a general-purpose
+ verification condition generator (VCG) which is used as a back-end
+ by other verification tools but it can also be used directly to verify
+ programs. It also provides Krakatoa, a tool or the verification of Java
+ programs and Caduceus, a tool for the verification of C programs.
+ </longdescription>
+ <maintainer>
+ <email>sci@gentoo.org</email>
+ </maintainer>
+ <use>
+ <flag name="apron">?apron?</flag>
+ <flag name="coq">?coq?</flag>
+ <flag name="gappa">?gappa?</flag>
+ <flag name="frama-c">?frama-c?</flag>
+ <flag name="gtk">?gtk?</flag>
+ <flag name="pff">?pff?</flag>
+ <flag name="why3">?why3?</flag>
+ </use>
</pkgmetadata>
diff --git a/sci-mathematics/why/why-2.30.ebuild b/sci-mathematics/why/why-2.30.ebuild
deleted file mode 100644
index 9b089bac0..000000000
--- a/sci-mathematics/why/why-2.30.ebuild
+++ /dev/null
@@ -1,73 +0,0 @@
-# Copyright 1999-2014 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-# $Header: $
-
-EAPI=5
-
-AUTOTOOLS_AUTORECONF=true
-
-inherit autotools-utils
-
-DESCRIPTION="Software verification platform"
-HOMEPAGE="http://why.lri.fr/"
-SRC_URI="http://why.lri.fr/download/${P}.tar.gz"
-
-LICENSE="GPL-2"
-SLOT="0"
-KEYWORDS="~amd64 ~x86"
-IUSE="apron coq doc examples gappa gtk jessie pff"
-
-DEPEND="
- >=dev-lang/ocaml-3.09
- >=dev-ml/ocamlgraph-1.2
- gtk? ( >=dev-ml/lablgtk-2.14 )
- apron? ( sci-mathematics/apron )
- coq? ( sci-mathematics/coq )
- gappa? ( sci-mathematics/gappalib-coq )
- pff? ( sci-mathematics/pff )
- jessie? ( >=sci-mathematics/frama-c-20100401 )"
-RDEPEND="${DEPEND}"
-
-PATCHES=( "${FILESDIR}"/${P}.patch )
-
-MAKEOPTS+=" -j1"
-AUTOTOOLS_IN_SOURCE_BUILD=1
-
-src_prepare() {
- sed \
- -e "s/DESTDIR =.*//g" \
- -e "s/@COQLIB@/\$(DESTDIR)\/@COQLIB@/g" \
- -i Makefile.in || die
-
- #to build with apron-0.9.10
- sed \
- -e "s/pvs/sri-pvs/g" \
- -e "s/oct_caml/octMPQ_caml/g" \
- -e "s/box_caml/boxMPQ_caml/g" \
- -e "s/polka_caml/polkaMPQ_caml/g" \
- -i configure.in
-
- autotools-utils_src_prepare
-}
-
-src_configure() {
- local myeconfargs=(
- $(use_enable apron)
- PATH="/usr/bin:$PATH"
- )
- autotools-utils_src_configure
-}
-
-src_compile(){
- autotools-utils_src_compile DESTDIR="/"
-}
-
-src_install(){
- use doc && DOCS=( doc/manual.ps )
- autotools-utils_src_install
-
- doman doc/why.1
-
- insinto /usr/share/doc/${PF}
- use examples && doins -r examples examples-c
-}
diff --git a/sci-mathematics/why/why-2.34.ebuild b/sci-mathematics/why/why-2.34.ebuild
new file mode 100644
index 000000000..c7eddfa66
--- /dev/null
+++ b/sci-mathematics/why/why-2.34.ebuild
@@ -0,0 +1,66 @@
+# Copyright 1999-2010 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: $
+
+EAPI="2"
+
+inherit autotools eutils
+
+DESCRIPTION="Why is a software verification platform"
+HOMEPAGE="http://why.lri.fr/"
+SRC_URI="http://why.lri.fr/download/${P}.tar.gz"
+
+LICENSE="GPL-2"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+IUSE="apron coq doc examples gappa frama-c gtk pff why3"
+
+DEPEND=">=dev-lang/ocaml-3.12.1
+ >=dev-ml/ocamlgraph-1.2
+ gtk? ( >=dev-ml/lablgtk-2.14 )
+ apron? ( sci-mathematics/apron )
+ coq? ( sci-mathematics/coq )
+ gappa? ( sci-mathematics/gappalib-coq )
+ pff? ( sci-mathematics/pff )
+ frama-c? ( >=sci-mathematics/frama-c-20140301 )
+ why3? ( sci-mathematics/why3 )"
+RDEPEND="${DEPEND}"
+
+src_prepare() {
+ sed -i Makefile.in \
+ -e "s/DESTDIR =.*//g" \
+ -e "s/@COQLIB@/\$(DESTDIR)\/@COQLIB@/g"
+
+ #to build with apron-0.9.10
+ sed -i configure.in \
+ -e "s/pvs/sri-pvs/g" \
+ -e "s/oct_caml/octMPQ_caml/g" \
+ -e "s/box_caml/boxMPQ_caml/g" \
+ -e "s/polka_caml/polkaMPQ_caml/g"
+
+ epatch "${FILESDIR}"/why-flocq23.patch
+ eautoreconf
+}
+
+src_configure() {
+ econf $(use_enable apron) PATH="/usr/bin:$PATH" || die "econf failed"
+}
+
+src_compile(){
+ DESTDIR="/" emake -j1 || die "emake failed"
+}
+
+src_install(){
+ DESTDIR="${D}" emake install || die "emake install failed"
+ dodoc CHANGES README Version
+ doman doc/why.1
+
+ if use doc; then
+ dodoc doc/manual.ps
+ fi
+
+ if use examples; then
+ insinto /usr/share/doc/${PF}
+ doins -r examples examples-c
+ fi
+}
diff --git a/sci-mathematics/why3/ChangeLog b/sci-mathematics/why3/ChangeLog
new file mode 100644
index 000000000..a91bee85b
--- /dev/null
+++ b/sci-mathematics/why3/ChangeLog
@@ -0,0 +1,7 @@
+# ChangeLog for sci-mathematics/why3
+# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2
+# $Header: $
+
+ 21 Jun 2014; Jonathan-Christofer Demay <jcdemay@gmail.com>
+ +ChangeLog, +metadata.xml, +why3-0.83.ebuild:
+ initial version
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
new file mode 100644
index 000000000..ec2faf65e
--- /dev/null
+++ b/sci-mathematics/why3/Manifest
@@ -0,0 +1,4 @@
+DIST why3-0.83.tar.gz 5347628 SHA256 cabf67e939e3422e491ef596f1a09ceaf1615642904182097cebde90e42e9ac9 SHA512 e1c4d462986835aa0e9a1ca117e4c3bbaf307b45b6de03da6ea8dd706770b8d9894031ea22ec732dfa7340d613b023ab499837203a132db5f138e51596e64177 WHIRLPOOL 4e1a6fb8462144ec5726f461a6548b5fdaeb2338557ec84cefa7a6eed5594c35908e7ccc337a93aaa704283f88874f5cb3ca1f9dbe2355266af163f27e81cf7e
+EBUILD why3-0.83.ebuild 1325 SHA256 c13afa35013186d12ffa7127e51815f20e3d52675d09d94b80df2f681ee84695 SHA512 1b73870850779d619e6103a7d7febe7a7fa2aee83e57da855460591590759d3fa00cdf4f85ff76a60e3dc36ddf764ec26abca983738a651e51c8dd7a32709a85 WHIRLPOOL ae8dbf7afaefb87470a4e5f6c2a30aec79fcb0236ace2d7e6609feb50a65ea794dbcfd163bbe7810edc6637d201b8a22f019248c4ee5e1866480f6ffb754deed
+MISC ChangeLog 248 SHA256 75e04e1c01a3bab95d3aea02729451bc72450b4a357e3cd7da5e250766dc4181 SHA512 59d5309b1fbc0e829ebe13318c221964cb97e6083ddb5c87acbcbe720882305911cd1f8187aa389b1394892edc0718370c4326cf889ed3144eb89e6d31259f24 WHIRLPOOL 743c17f5170e887142722dc269b465563ad496629dd35985870dfe25d94b41ecc18557d0a56ac55076b4c546c80e2fef3def54c9ce6f06fecda09bd03d37c89f
+MISC metadata.xml 1003 SHA256 5bb7fa100e8393607e63b9bdd5974184c86f51759da8f66e45a36fb4beca4aba SHA512 6ac8f7a9ffe33f930fd9522d28fb321bacb914fece132778e2184d552e4279ee583cbaf73a01437fd64ab3ea1fc3c7c94959fe36125e95e07c2a1bbf9c60a567 WHIRLPOOL 58fcab163ae5ebf598512f5ba2ab655ee4d0dd9d352882c38e8adf5beaada7e3dac4dab98412f79d305773f9290c214e06cc686cf596d2ab1e459ff4ac22998b
diff --git a/sci-mathematics/why3/metadata.xml b/sci-mathematics/why3/metadata.xml
new file mode 100644
index 000000000..361520dd3
--- /dev/null
+++ b/sci-mathematics/why3/metadata.xml
@@ -0,0 +1,23 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+<pkgmetadata>
+ <herd>sci</herd>
+ <longdescription>
+ Why3 is a platform for deductive program verification. It provides
+ a rich language for specification and programming, called WhyML,
+ and relies on external theorem provers, both automated and interactive,
+ to discharge verification conditions. Why3 comes with a standard
+ library of logical theories (integer and real arithmetic, Boolean
+ operations, sets and maps, etc.) and basic programming data structures
+ (arrays, queues, hash tables, etc.). A user can write WhyML programs
+ directly and get correct-by-construction OCaml programs through an
+ automated extraction mechanism. WhyML is also used as an intermediate
+ language for the verification of C, Java, or Ada programs.
+ </longdescription>
+ <maintainer>
+ <email>sci@gentoo.org</email>
+ </maintainer>
+ <use>
+ <flag name="frama-c">?frama-c?</flag>
+ </use>
+</pkgmetadata>
diff --git a/sci-mathematics/why3/why3-0.83.ebuild b/sci-mathematics/why3/why3-0.83.ebuild
new file mode 100644
index 000000000..55bc65684
--- /dev/null
+++ b/sci-mathematics/why3/why3-0.83.ebuild
@@ -0,0 +1,55 @@
+# Copyright 1999-2014 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: $
+
+EAPI="2"
+
+inherit autotools eutils
+
+DESCRIPTION=" Why3 is a platform for deductive program verification"
+HOMEPAGE="http://why3.lri.fr/"
+SRC_URI="https://gforge.inria.fr/frs/download.php/33490/${P}.tar.gz"
+
+LICENSE="LGPL-2"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+IUSE="frama-c doc examples"
+
+DEPEND=">=dev-lang/ocaml-3.12.1
+ dev-ml/zarith
+ sci-mathematics/coq
+ frama-c? ( >=sci-mathematics/frama-c-20140301 )
+ doc? ( dev-tex/rubber )"
+RDEPEND="${DEPEND}"
+
+src_prepare() {
+ mv doc/why.1 doc/why3.1
+ sed -i configure.in -e "s/\"pvs\"/\"sri-pvs\"/g"
+ sed -i configure -e "s/\"pvs\"/\"sri-pvs\"/g"
+ sed -i Makefile.in -e "s:DESTDIR =::g" \
+ -e "s:\$(RUBBER) --warn all --pdf manual.tex:makeindex manual.tex; \$(RUBBER) --warn all --pdf manual.tex; cd ..:g"
+}
+
+src_configure() {
+ econf $(use_enable frama-c) || die "econf failed"
+}
+
+src_compile() {
+ emake -j1 || die "emake failed"
+ if use doc; then
+ emake -j1 doc/manual.pdf || die "emake doc failed"
+ fi
+}
+
+src_install(){
+ DESTDIR="${D}" emake install || die "emake install failed"
+ dodoc CHANGES README Version
+ doman doc/why3.1
+ if use doc; then
+ dodoc doc/manual.pdf
+ fi
+ if use examples; then
+ insinto /usr/share/doc/${PF}
+ doins -r examples
+ fi
+ }