From 03917aeca50f3a5bfb3382205e973e7777a67570 Mon Sep 17 00:00:00 2001 From: Jonathan-Christofer Demay Date: Sun, 22 Jun 2014 16:29:25 +0200 Subject: multiple version bumps --- dev-libs/simclist/ChangeLog | 8 +- dev-libs/simclist/Manifest | 3 + dev-libs/simclist/metadata.xml | 17 +- dev-libs/simclist/simclist-1.6.ebuild | 6 +- dev-ml/mlgmpidl/ChangeLog | 2 +- dev-ml/mlgmpidl/Manifest | 4 + dev-ml/mlgmpidl/metadata.xml | 23 +- dev-ml/mlgmpidl/mlgmpidl-1.1.ebuild | 6 +- dev-ml/ocamlgraph/ChangeLog | 22 +- dev-ml/ocamlgraph/Manifest | 6 +- dev-ml/ocamlgraph/metadata.xml | 47 ++-- dev-ml/ocamlgraph/ocamlgraph-1.8.2.ebuild | 47 ---- dev-ml/ocamlgraph/ocamlgraph-1.8.5.ebuild | 51 +++++ dev-ml/zarith/ChangeLog | 9 +- dev-ml/zarith/Manifest | 5 +- dev-ml/zarith/metadata.xml | 20 +- dev-ml/zarith/zarith-1.1.ebuild | 41 ---- dev-ml/zarith/zarith-1.2.1.ebuild | 40 ++++ sci-mathematics/alt-ergo/ChangeLog | 21 +- sci-mathematics/alt-ergo/Manifest | 5 +- sci-mathematics/alt-ergo/alt-ergo-0.95.2.ebuild | 35 +-- sci-mathematics/alt-ergo/metadata.xml | 22 +- sci-mathematics/apron/ChangeLog | 14 +- sci-mathematics/apron/Manifest | 6 +- sci-mathematics/apron/apron-0.9.10-r1.ebuild | 79 +++++++ sci-mathematics/apron/apron-0.9.10.ebuild | 6 +- sci-mathematics/apron/metadata.xml | 31 +-- sci-mathematics/flocq/ChangeLog | 14 +- sci-mathematics/flocq/Manifest | 5 +- sci-mathematics/flocq/flocq-2.1.0.ebuild | 21 -- sci-mathematics/flocq/flocq-2.3.0.ebuild | 36 +++ sci-mathematics/flocq/metadata.xml | 17 +- sci-mathematics/frama-c/ChangeLog | 28 +-- sci-mathematics/frama-c/Manifest | 7 +- sci-mathematics/frama-c/files/frama-c-make.patch | 12 - .../frama-c/files/frama-c-ocaml-4.01.patch | 145 ------------ .../frama-c/files/ocamlgraph185_compat.patch | 254 +++++++++++++++++++++ sci-mathematics/frama-c/frama-c-20120901.ebuild | 63 ----- sci-mathematics/frama-c/frama-c-20130601.ebuild | 65 ------ sci-mathematics/frama-c/frama-c-20140301.ebuild | 68 ++++++ sci-mathematics/frama-c/metadata.xml | 28 ++- sci-mathematics/gappa/ChangeLog | 32 +-- sci-mathematics/gappa/Manifest | 5 +- sci-mathematics/gappa/gappa-1.0.0.ebuild | 37 --- sci-mathematics/gappa/gappa-1.1.1.ebuild | 42 ++++ sci-mathematics/gappalib-coq/ChangeLog | 30 +-- sci-mathematics/gappalib-coq/Manifest | 5 +- .../gappalib-coq/files/gappalib-coq-coq84.patch | 71 ------ .../gappalib-coq/gappalib-coq-0.18.0.ebuild | 35 --- .../gappalib-coq/gappalib-coq-1.0.0.ebuild | 35 +++ sci-mathematics/giac/ChangeLog | 15 +- sci-mathematics/giac/Manifest | 5 +- sci-mathematics/giac/giac-1.0.0.ebuild | 59 ----- sci-mathematics/giac/giac-1.1.0.ebuild | 58 +++++ sci-mathematics/giac/metadata.xml | 24 +- sci-mathematics/ltl2ba/Manifest | 3 + sci-mathematics/ltl2ba/ltl2ba-1.1.ebuild | 4 +- sci-mathematics/ltl2ba/metadata.xml | 3 + sci-mathematics/pff/ChangeLog | 17 +- sci-mathematics/pff/Manifest | 3 + sci-mathematics/pff/metadata.xml | 17 +- sci-mathematics/pff/pff-8.4.ebuild | 18 +- sci-mathematics/why/ChangeLog | 19 +- sci-mathematics/why/Manifest | 6 +- sci-mathematics/why/files/why-2.30.patch | 36 --- sci-mathematics/why/files/why-flocq23.patch | 11 + sci-mathematics/why/metadata.xml | 35 +-- sci-mathematics/why/why-2.30.ebuild | 73 ------ sci-mathematics/why/why-2.34.ebuild | 66 ++++++ sci-mathematics/why3/ChangeLog | 7 + sci-mathematics/why3/Manifest | 4 + sci-mathematics/why3/metadata.xml | 23 ++ sci-mathematics/why3/why3-0.83.ebuild | 55 +++++ 73 files changed, 1220 insertions(+), 972 deletions(-) delete mode 100644 dev-ml/ocamlgraph/ocamlgraph-1.8.2.ebuild create mode 100644 dev-ml/ocamlgraph/ocamlgraph-1.8.5.ebuild delete mode 100644 dev-ml/zarith/zarith-1.1.ebuild create mode 100644 dev-ml/zarith/zarith-1.2.1.ebuild create mode 100644 sci-mathematics/apron/apron-0.9.10-r1.ebuild delete mode 100644 sci-mathematics/flocq/flocq-2.1.0.ebuild create mode 100644 sci-mathematics/flocq/flocq-2.3.0.ebuild delete mode 100644 sci-mathematics/frama-c/files/frama-c-make.patch delete mode 100644 sci-mathematics/frama-c/files/frama-c-ocaml-4.01.patch create mode 100644 sci-mathematics/frama-c/files/ocamlgraph185_compat.patch delete mode 100644 sci-mathematics/frama-c/frama-c-20120901.ebuild delete mode 100644 sci-mathematics/frama-c/frama-c-20130601.ebuild create mode 100644 sci-mathematics/frama-c/frama-c-20140301.ebuild delete mode 100644 sci-mathematics/gappa/gappa-1.0.0.ebuild create mode 100644 sci-mathematics/gappa/gappa-1.1.1.ebuild delete mode 100644 sci-mathematics/gappalib-coq/files/gappalib-coq-coq84.patch delete mode 100644 sci-mathematics/gappalib-coq/gappalib-coq-0.18.0.ebuild create mode 100644 sci-mathematics/gappalib-coq/gappalib-coq-1.0.0.ebuild delete mode 100644 sci-mathematics/giac/giac-1.0.0.ebuild create mode 100644 sci-mathematics/giac/giac-1.1.0.ebuild delete mode 100644 sci-mathematics/why/files/why-2.30.patch create mode 100644 sci-mathematics/why/files/why-flocq23.patch delete mode 100644 sci-mathematics/why/why-2.30.ebuild create mode 100644 sci-mathematics/why/why-2.34.ebuild create mode 100644 sci-mathematics/why3/ChangeLog create mode 100644 sci-mathematics/why3/Manifest create mode 100644 sci-mathematics/why3/metadata.xml create mode 100644 sci-mathematics/why3/why3-0.83.ebuild 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 + 17 Mar 2012; Jonathan-Christofer Demay -simclist-1.5.ebuild, +simclist-1.6.ebuild: version bump - - 24 Nov 2010; J.-C. Demay + + 24 Nov 2010; Jonathan-Christofer Demay -simclist-1.4.4_rc4.ebuild, +simclist-1.5.ebuild: version bump - + 23 Jun 2010; Andreas K. Huettel (dilfridge) 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 @@ -sci - - 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. - + sci + + 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. + + + sci@gentoo.org + 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 + 03 Jul 2010; Jonathan-Christofer Demay 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 @@ -sci-mathematics - - 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. - - - Add support for dev-libs/mpfr - + sci + + 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. + + + sci@gentoo.org + + + add support for mpfr, the library for multiple-precision floating-point computations with exact rounding + 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 - +ocamlgraph-1.8.2.ebuild, +ocamlgraph-1.8.1.ebuild: + 21 Jun 2014; Jonathan-Christofer Demay + -ocamlgraph-1.8.3.ebuild, +ocamlgraph-1.8.5.ebuild: version bump - 21 Dec 2011; J.-C. Demay + 10 Jan 2014; Jonathan-Christofer Demay + -ocamlgraph-1.8.2.ebuild, +ocamlgraph-1.8.3.ebuild: + version bump + + 14 Jan 2013; Jonathan-Christofer Demay + -ocamlgraph-1.8.1.ebuild, +ocamlgraph-1.8.2.ebuild: + version bump + + 21 Dec 2011; Jonathan-Christofer Demay -ocamlgraph-1.7.ebuild, +ocamlgraph-1.8.1.ebuild: version bump - 06 May 2011; J.-C. Demay + 06 May 2011; Jonathan-Christofer Demay -ocamlgraph-1.6.ebuild, +ocamlgraph-1.7.ebuild: version bump - 13 Jul 2010; J.-C. Demay + 13 Jul 2010; Jonathan-Christofer Demay -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 + 04 Jul 2010; Jonathan-Christofer Demay -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 @@ -sci-mathematics - - 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. - + sci + + 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. + + + sci@gentoo.org + + + ?doc? + ?examples? + ?gtk? + ?ocamlopt? + diff --git a/dev-ml/ocamlgraph/ocamlgraph-1.8.2.ebuild b/dev-ml/ocamlgraph/ocamlgraph-1.8.2.ebuild deleted file mode 100644 index 1442073be..000000000 --- a/dev-ml/ocamlgraph/ocamlgraph-1.8.2.ebuild +++ /dev/null @@ -1,47 +0,0 @@ -# Copyright 1999-2014 Gentoo Foundation -# Distributed under the terms of the GNU General Public License v2 -# $Header: $ - -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" - -LICENSE="LGPL-2" -SLOT="0" -KEYWORDS="~amd64 ~ppc ~sparc ~x86" -IUSE="doc examples gtk +ocamlopt" - -DEPEND=">=dev-lang/ocaml-3.10.2[ocamlopt?] - gtk? ( >=dev-ml/lablgtk-2.12[gnomecanvas,ocamlopt?] )" -RDEPEND="${DEPEND}" - -src_prepare() { - epatch "${FILESDIR}/${PN}-makefile.patch" - eautoreconf -} - -src_compile() { - emake -j1 DESTDIR="/" || die "emake failed" - - if use doc; then - emake doc || die "emake doc failed" - fi -} - -src_install() { - emake install DESTDIR="${D}" || die "emake install failed" - dodoc CHANGES CREDITS FAQ README - - if use doc; then - dohtml doc/* - fi - - if use examples; then - insinto /usr/share/doc/${PF} - doins -r examples - fi -} diff --git a/dev-ml/ocamlgraph/ocamlgraph-1.8.5.ebuild b/dev-ml/ocamlgraph/ocamlgraph-1.8.5.ebuild new file mode 100644 index 000000000..d950b6f2d --- /dev/null +++ b/dev-ml/ocamlgraph/ocamlgraph-1.8.5.ebuild @@ -0,0 +1,51 @@ +# Copyright 1999-2014 Gentoo Foundation +# Distributed under the terms of the GNU General Public License v2 +# $Header: $ + +EAPI="2" + +inherit eutils autotools + +DESCRIPTION="A graph library for Objective Caml" +HOMEPAGE="http://ocamlgraph.lri.fr" +SRC_URI="${HOMEPAGE}/download/${P}.tar.gz" + +LICENSE="LGPL-2" +SLOT="0" +KEYWORDS="~amd64 ~x86" +IUSE="doc examples gtk +ocamlopt" + +DEPEND=">=dev-lang/ocaml-3.10.2[ocamlopt?] + gtk? ( >=dev-ml/lablgtk-2.12[gnomecanvas,ocamlopt?] )" +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() { + DESTDIR="/" emake -j1 || die "emake failed" + + if use doc; then + emake doc || die "emake doc failed" + fi +} + +src_install() { + DESTDIR="${D}" emake install || die "emake install failed" + dodoc CHANGES CREDITS FAQ README + + if use doc; then + dohtml doc/* + fi + + if use examples; then + insinto /usr/share/doc/${PF} + doins -r examples + fi +} 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 zarith-1.1.ebuild, metadata.xml: - Clean wrong space and blank lines; move EAPI=5 + 10 Jun 2014; Jonathan-Christofer Demay + -zarith-1.1.ebuild, +zarith-1.2.1.ebuild: + version bump - 14 Jan 2013; J.-C. Demay + 14 Jan 2013; Jonathan-Christofer Demay +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 @@ -sci-mathematics - - 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. - + sci + + 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. + + + sci@gentoo.org + + + ?ocamlopt? + 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 + -alt-ergo-0.95.ebuild, +alt-ergo-0.95.2.ebuild: + version bump - 16 Jun 2014; Jauhien Piatlicki -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 -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 alt-ergo-0.95.ebuild, - metadata.xml: - Move to EAPI=5; clean quoting and ebuild syntax and indention - - 14 Jan 2013; J.-C. Demay + 14 Jan 2013; Jonathan-Christofer Demay +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 @@ -sci-mathematics - - 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. - + sci + + 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. + + + sci@gentoo.org + + + ?gtk? + ?ocamlopt? + 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 + 21 Jun 2014; Jonathan-Christofer Demay + +apron-0.9.10-r1.ebuild: + dropping cxx and ppl support + + 13 Feb 2011; Jonathan-Christofer Demay 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) 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 + 04 Jul 2010; Jonathan-Christofer Demay -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 + 03 Jul 2010; Jonathan-Christofer Demay +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 @@ -sci-mathematics - - 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. - - - Enable optional interface to the Parma Polyhedra Library - + sci + + 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. + + + sci@gentoo.org + + + ?ocaml? + 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 flocq-2.1.0.ebuild, - metadata.xml: - Move to EAPI=5; assign RDEPEND explicitatly + 21 Jun 2014; Jonathan-Christofer Demay + -flocq-2.1.0.ebuild, +flocq-2.3.0.ebuild: + version bump - 14 Jan 2013; J.-C. Demay + 14 Jan 2013; Jonathan-Christofer Demay -flocq-1.4.0.ebuild, +flocq-2.1.0.ebuild: version bump - 06 May 2011; J.-C. Demay + 06 May 2011; Jonathan-Christofer Demay -flocq-1.2.ebuild, +flocq-1.4.0.ebuild: version bump - 13 Feb 2011; J.-C. Demay + 13 Feb 2011; Jonathan-Christofer Demay +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 @@ -sci-mathematics - - 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. - + sci + + 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. + + + sci@gentoo.org + 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 + -frama-c-20130601.ebuild, +frama-c-20140301.ebuild: + version bump - 24 Feb 2014; Andrew Savchenko +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 + -frama-c-20120901.ebuild, +frama-c-20130601.ebuild: + version bump - 14 Jan 2013; J.-C. Demay - +frama-c-20120901.ebuild, -frama-c-20111001.ebuild: + 14 Jan 2013; Jonathan-Christofer Demay + -frama-c-20111001.ebuild, +frama-c-20120901.ebuild: version bump - 21 Dec 2011; J.-C. Demay - +frama-c-20111001.ebuild, -frama-c-20110201.ebuild: + 21 Dec 2011; Jonathan-Christofer Demay + -frama-c-20110201.ebuild, +frama-c-20111001.ebuild: version bump - 06 may 2011; J.-C. Demay - +frama-c-20110201.ebuild, -frama-c-20101202_beta2.ebuild: + 06 may 2011; Jonathan-Christofer Demay + -frama-c-20101202_beta2.ebuild, +frama-c-20110201.ebuild: version bump - 14 Feb 2011; J.-C. Demay - +frama-c-20101202_beta2.ebuild, -frama-c-20100401.ebuild, -files/frama-c-20100401-plugin_install.patch: + 14 Feb 2011; Jonathan-Christofer Demay + -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) frama-c-20100401.ebuild: Dropped ~sparc since dependencies cannot be fulfilled. - 08 Jul 2010; J.-C. Demay + 08 Jul 2010; Jonathan-Christofer Demay +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 +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-20120901.ebuild b/sci-mathematics/frama-c/frama-c-20120901.ebuild deleted file mode 100644 index 2568ba4fc..000000000 --- a/sci-mathematics/frama-c/frama-c-20120901.ebuild +++ /dev/null @@ -1,63 +0,0 @@ -# Copyright 1999-2014 Gentoo Foundation -# Distributed under the terms of the GNU General Public License v2 -# $Header: $ - -EAPI="3" - -inherit autotools eutils - -DESCRIPTION="Framework for analysis of source codes written in C" -HOMEPAGE="http://frama-c.com" -NAME="Oxygen" -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 - - eautoreconf -} - -src_configure(){ - if use gtk; then - myconf="--enable-gui" - else - myconf="--disable-gui" - fi - - econf ${myconf} || die "econf failed" -} - -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" -} - -src_install(){ - emake install DESTDIR="${D}" || die "emake install failed" - dodoc Changelog doc/README - - if use doc; then - dodoc doc/manuals/*.pdf - fi -} 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-20140301.ebuild b/sci-mathematics/frama-c/frama-c-20140301.ebuild new file mode 100644 index 000000000..f93062cc5 --- /dev/null +++ b/sci-mathematics/frama-c/frama-c-20140301.ebuild @@ -0,0 +1,68 @@ +# Copyright 1999-2013 Gentoo Foundation +# Distributed under the terms of the GNU General Public License v2 +# $Header: $ + +EAPI="3" + +inherit autotools eutils + +DESCRIPTION="Framework for analysis of source codes written in C" +HOMEPAGE="http://frama-c.com" +NAME="Neon" +SRC_URI="http://frama-c.com/download/${PN/-c/-c-$NAME}-${PV/_/-}.tar.gz" + +LICENSE="LGPL-2" +SLOT="0" +KEYWORDS="~amd64 ~x86" +IUSE="doc gtk +ocamlopt" +RESTRICT="strip" + +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 + >=gnome-base/libgnomecanvas-2.26 + >=dev-ml/lablgtk-2.14[sourceview,gnomecanvas,ocamlopt?] )" +RDEPEND="${DEPEND}" + +S="${WORKDIR}/${PN/-c/-c-$NAME}-${PV/_/-}" + +src_prepare(){ + touch config_file + rm -f ocamlgraph.tar.gz + epatch "${FILESDIR}/ocamlgraph185_compat.patch" + eautoreconf +} + +src_configure(){ + if use gtk; then + myconf="--enable-gui" + else + myconf="--disable-gui" + fi + econf ${myconf} || die "econf failed" +} + +src_compile(){ + # dependencies can not be processed in parallel, + # this is the intended behavior. + emake -j1 depend || die "emake depend 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(){ + DESTDIR="${D}" emake install || die "emake install failed" + dodoc Changelog + + if use doc; then + 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 @@ -sci-mathematics - - 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. - + sci + + 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. + + + sci@gentoo.org + + + ?doc? + ?gtk? + ?ocamlopt? + 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 + -gappa-0.16.6.ebuild, +gappa-1.1.1.ebuild: + version bump - 12 Aug 2013; Sébastien Fabbro +gappa-1.0.0.ebuild, - -gappa-0.16.3.ebuild: - sci-mathematics/gappa: Version bump + 11 Dec 2013; Jonathan-Christofer Demay + -gappa-0.16.3.ebuild, +gappa-0.16.6.ebuild: + version bump - 14 Jan 2013; J.-C. Demay - +gappa-0.16.3.ebuild, -gappa-0.15.1.ebuild: + 14 Jan 2013; Jonathan-Christofer Demay + -gappa-0.15.1.ebuild, +gappa-0.16.3.ebuild: version bump - 21 Dec 2011; J.-C. Demay - +gappa-0.15.1.ebuild, -gappa-0.14.0.ebuild: + 21 Dec 2011; Jonathan-Christofer Demay + -gappa-0.14.0.ebuild, +gappa-0.15.1.ebuild: version bump - 13 Feb 2011; J.-C. Demay - +gappa-0.14.0.ebuild, -gappa-0.13.0.ebuild: + 13 Feb 2011; Jonathan-Christofer Demay + -gappa-0.13.0.ebuild, +gappa-0.14.0.ebuild: version bump 04 Jul 2010; Andreas K. Huettel (dilfridge) @@ -25,10 +27,10 @@ Silence repoman; improve license description; move doc generation dependencies to RDEPEND - 04 Jul 2010; J.-C. Demay - +gappa-0.13.0.ebuild, -gappa-0.12.1.ebuild: + 04 Jul 2010; Jonathan-Christofer Demay + -gappa-0.12.1.ebuild, +gappa-0.13.0.ebuild: version bump - - 04 Jul 2010; J.-C. Demay + + 04 Jul 2010; Jonathan-Christofer Demay +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 gappalib-coq-0.18.0.ebuild, - metadata.xml: + 21 Jun 2014; Jonathan-Christofer Demay + -gappalib-coq-0.18.0.ebuild, -files/gappalib-coq-coq84.patch, gappalib-coq-1.0.0.ebuild: + version bump + + 03 Mar 2013; Justin Lecher + 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 - +gappalib-coq-0.18.0.ebuild,+files/gappalib-coq-coq84.patch,-gappalib-coq-0.16.0.ebuild: + 14 Jan 2013; Jonathan-Christofer Demay + -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 - +gappalib-coq-0.16.0.ebuild, -gappalib-coq-0.14.1.ebuild: + 12 Dec 2011; Jonathan-Christofer Demay + -gappalib-coq-0.14.1.ebuild, -gappalib-coq-0.16.0.ebuild: version bump - 04 Jul 2010; J.-C. Demay - +gappalib-coq-0.14.1.ebuild, -gappalib-coq-0.13.ebuild: + 04 Jul 2010; Jonathan-Christofer Demay + -gappalib-coq-0.13.ebuild, +gappalib-coq-0.14.1.ebuild: version bump - 04 Jul 2010; J.-C. Demay - +gappalib-coq-0.13.ebuild, -gappalib-coq-0.12.ebuild: + 04 Jul 2010; Jonathan-Christofer Demay + -gappalib-coq-0.12.ebuild, +gappalib-coq-0.13.ebuild: version bump - - 04 Jul 2010; J.-C. Demay + + 04 Jul 2010; Jonathan-Christofer Demay +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 giac-1.0.0.ebuild, metadata.xml: - Drop useless blank line + 21 Jun 2014; Jonathan-Christofer Demay + -giac-1.0.0.ebuild, +giac-1.1.0.ebuild: + version bump - 14 Jan 2013; J.-C. Demay - +giac-1.0.0.ebuild, -giac-0.9.2.ebuild: + 14 Jan 2013; Jonathan-Christofer Demay + -giac-0.9.2.ebuild, +giac-1.0.0.ebuild: version bump - - 16 May 2011; J.-C. Demay + + 16 May 2011; Jonathan-Christofer Demay 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.0.0.ebuild deleted file mode 100644 index 95fe44fda..000000000 --- a/sci-mathematics/giac/giac-1.0.0.ebuild +++ /dev/null @@ -1,59 +0,0 @@ -# Copyright 1999-2014 Gentoo Foundation -# Distributed under the terms of the GNU General Public License v2 -# $Header: $ - -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" -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}" - -src_prepare(){ - sed -e "s:\$(prefix)/share:\$(DESTDIR)\$(prefix)/share:g" \ - -e "s:config.h \$(includedir)/giac:config.h \$(DESTDIR)\$(includedir)/giac:g" \ - -e "s:\$(DESTDIR)\$(DESTDIR):\$(DESTDIR):g" \ - -e "s:\$(DESTDIR)/\$(DESTDIR):\$(DESTDIR):g" \ - -i `find -name Makefile\*` - if use !fltk; then - sed -e "s: gl2ps\.[chlo]*::g" -i src/Makefile.* - fi -} - -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 - if use !fltk; then - rm "${D}"/usr/bin/x* - fi - if use !doc; then - 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 - else - 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 - fi -} diff --git a/sci-mathematics/giac/giac-1.1.0.ebuild b/sci-mathematics/giac/giac-1.1.0.ebuild new file mode 100644 index 000000000..d48ef0490 --- /dev/null +++ b/sci-mathematics/giac/giac-1.1.0.ebuild @@ -0,0 +1,58 @@ +# Copyright 1999-2014 Gentoo Foundation +# Distributed under the terms of the GNU General Public License v2 +# $Header: $ + +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/${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 + 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" \ + -e "s:config.h \$(includedir)/giac:config.h \$(DESTDIR)\$(includedir)/giac:g" \ + -e "s:\$(DESTDIR)\$(DESTDIR):\$(DESTDIR):g" \ + -e "s:\$(DESTDIR)/\$(DESTDIR):\$(DESTDIR):g" \ + -i `find -name Makefile\*` + if use !fltk; then + sed -e "s: gl2ps\.[chlo]*::g" -i src/Makefile.* + fi +} + +src_install() { + 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* + fi + if use !doc; then + 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 + else + 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 + 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 @@ -sci - - 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). - + sci + + 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). + + + sci@gentoo.org + + + ?doc? + ?examples? + ?fltk? + 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 @@ sci + + sci@gentoo.org + 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 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 + pff-8.4.ebuild: + install fixes - 14 Jan 2013; J.-C. Demay - +pff-8.4.ebuild, -pff-8.3.ebuild: + 14 Jan 2013; Jonathan-Christofer Demay + -pff-8.3.ebuild, +pff-8.4.ebuild: version bump - 21 Dec 2011; J.-C. Demay - +pff-8.3.ebuild, -pff-8.2.1.2.ebuild: + 21 Dec 2011; Jonathan-Christofer Demay + -pff-8.2.1.2.ebuild, +pff-8.3.ebuild: version bump - 04 Jul 2010; J.-C. Demay + 04 Jul 2010; Jonathan-Christofer Demay +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 @@ -sci-mathematics - - 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. - + sci + + 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. + + + sci@gentoo.org + 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 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 + -why-2.30.ebuild, -files/why-2.30.patch, +why-2.34.ebuild, +why-flocq23.patch: + version bump - 21 Dec 2011; J.-C. Demay - -why-2.29.ebuild, +why-2.30.ebuild, -files/why_jessie-carbon.patch, +files/why-2.30.patch: + 21 Dec 2011; Jonathan-Christofer Demay + -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 + 06 May 2011; Jonathan-Christofer Demay -why-2.28.ebuild, +why-2.29.ebuild: version bump - 14 Feb 2011; J.-C. Demay + 14 Feb 2011; Jonathan-Christofer Demay -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 + 08 Jul 2010; Jonathan-Christofer Demay -why-2.19.ebuild, +why-2.26.ebuild: version Bump - 08 Jul 2010; J.-C. Demay + 08 Jul 2010; Jonathan-Christofer Demay +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 @@ -sci-mathematics - - 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. - - - Support for sci-mathematics/apron - Support for sci-mathematics/coq - Support for sci-mathematics/gappa - Support for sci-mathematics/frama-c - Support for sci-mathematics/pff - + sci + + 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. + + + sci@gentoo.org + + + ?apron? + ?coq? + ?gappa? + ?frama-c? + ?gtk? + ?pff? + ?why3? + 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 + +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 @@ + + + + sci + + 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. + + + sci@gentoo.org + + + ?frama-c? + + 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 + } -- cgit v1.2.3