commit: 9d31fe0253025c7f7c08e0828889c1f012977bd5 Author: Jonathan-Christofer Demay <jcdemay <AT> gmail <DOT> com> AuthorDate: Sun Jun 22 20:20:18 2014 +0000 Commit: Jonathan-Christofer Demay <jcdemay <AT> gmail <DOT> com> CommitDate: Sun Jun 22 20:20:18 2014 +0000 URL: http://git.overlays.gentoo.org/gitweb/?p=proj/sci.git;a=commit;h=9d31fe02
multiple move to EAPI=5 and regression fixes --- dev-libs/simclist/metadata.xml | 17 ++++---- dev-libs/simclist/simclist-1.6.ebuild | 4 +- dev-ml/mlgmpidl/metadata.xml | 23 +++++------ dev-ml/mlgmpidl/mlgmpidl-1.1.ebuild | 4 +- dev-ml/ocamlgraph/ChangeLog | 4 ++ dev-ml/ocamlgraph/metadata.xml | 47 +++++++++------------- dev-ml/ocamlgraph/ocamlgraph-1.8.5.ebuild | 2 +- dev-ml/zarith/ChangeLog | 15 +++++-- dev-ml/zarith/metadata.xml | 20 ++++----- sci-mathematics/alt-ergo/ChangeLog | 15 +++++-- sci-mathematics/alt-ergo/alt-ergo-0.95.2.ebuild | 12 +++--- sci-mathematics/alt-ergo/metadata.xml | 23 ++++------- sci-mathematics/apron/apron-0.9.10-r1.ebuild | 4 +- sci-mathematics/apron/apron-0.9.10.ebuild | 4 +- sci-mathematics/apron/metadata.xml | 28 +++++-------- sci-mathematics/flocq/ChangeLog | 4 ++ sci-mathematics/flocq/flocq-2.3.0.ebuild | 3 +- sci-mathematics/flocq/metadata.xml | 17 ++++---- sci-mathematics/frama-c/ChangeLog | 8 ++-- sci-mathematics/frama-c/frama-c-20140301.ebuild | 4 +- sci-mathematics/frama-c/metadata.xml | 28 +++++-------- sci-mathematics/gappa/ChangeLog | 6 ++- sci-mathematics/gappa/gappa-1.1.1.ebuild | 12 +++--- .../gappalib-coq/gappalib-coq-1.0.0.ebuild | 2 +- sci-mathematics/giac/ChangeLog | 3 ++ sci-mathematics/giac/metadata.xml | 26 +++++------- sci-mathematics/ltl2ba/ltl2ba-1.1.ebuild | 4 +- sci-mathematics/ltl2ba/metadata.xml | 3 -- sci-mathematics/pff/ChangeLog | 4 ++ sci-mathematics/pff/metadata.xml | 18 ++++----- sci-mathematics/pff/pff-8.4.ebuild | 4 +- sci-mathematics/why/ChangeLog | 4 ++ sci-mathematics/why/metadata.xml | 28 ++++--------- sci-mathematics/why/why-2.34.ebuild | 4 +- sci-mathematics/why3/metadata.xml | 32 ++++++--------- sci-mathematics/why3/why3-0.83.ebuild | 2 +- 36 files changed, 201 insertions(+), 237 deletions(-) diff --git a/dev-libs/simclist/metadata.xml b/dev-libs/simclist/metadata.xml index 49fb6b8..1da3891 100644 --- a/dev-libs/simclist/metadata.xml +++ b/dev-libs/simclist/metadata.xml @@ -1,14 +1,11 @@ <?xml version="1.0" encoding="UTF-8"?> <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd";> <pkgmetadata> - <herd>sci</herd> - <longdescription> - SimCList is a high quality C (C++ embeddable) library for handling - lists. It exploits several advanced techniques for improving - performance, including freelists, sentinels, automatic sort algorithm - selection, sort randomization, mid pointer and optional multithreading. - </longdescription> - <maintainer> - <email>s...@gentoo.org</email> - </maintainer> +<herd>sci</herd> +<longdescription> + SimCList is a high quality C (C++ embeddable) library for handling + lists. It exploits several advanced techniques for improving + performance, including freelists, sentinels, automatic sort algorithm + selection, sort randomization, mid pointer and optional multithreading. +</longdescription> </pkgmetadata> diff --git a/dev-libs/simclist/simclist-1.6.ebuild b/dev-libs/simclist/simclist-1.6.ebuild index 0df95c3..c79091d 100644 --- a/dev-libs/simclist/simclist-1.6.ebuild +++ b/dev-libs/simclist/simclist-1.6.ebuild @@ -1,8 +1,8 @@ -# Copyright 1999-2012 Gentoo Foundation +# Copyright 1999-2014 Gentoo Foundation # Distributed under the terms of the GNU General Public License v2 # $Header: $ -EAPI=3 +EAPI=5 inherit cmake-utils diff --git a/dev-ml/mlgmpidl/metadata.xml b/dev-ml/mlgmpidl/metadata.xml index c6107f8..a3fac81 100644 --- a/dev-ml/mlgmpidl/metadata.xml +++ b/dev-ml/mlgmpidl/metadata.xml @@ -1,17 +1,14 @@ <?xml version="1.0" encoding="UTF-8"?> <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd";> <pkgmetadata> - <herd>sci</herd> - <longdescription> - MLGMPIDL is a package offering an interface to the GMP and MPFR - libraries for OCaml version 3.07 or higher. The interface offers access - to almost all the functions of the library, and is decomposed into 7 - submodules. - </longdescription> - <maintainer> - <email>s...@gentoo.org</email> - </maintainer> - <use> - <flag name="mpfr">add support for mpfr, the library for multiple-precision floating-point computations with exact rounding</flag> - </use> +<herd>sci-mathematics</herd> +<longdescription> + MLGMPIDL is a package offering an interface to the GMP and MPFR + libraries for OCaml version 3.07 or higher. The interface offers access + to almost all the functions of the library, and is decomposed into 7 + submodules. +</longdescription> +<use> + <flag name="mpfr">Add support for <pkg>dev-libs/mpfr</pkg></flag> +</use> </pkgmetadata> diff --git a/dev-ml/mlgmpidl/mlgmpidl-1.1.ebuild b/dev-ml/mlgmpidl/mlgmpidl-1.1.ebuild index 6efca0c..3063fdf 100644 --- a/dev-ml/mlgmpidl/mlgmpidl-1.1.ebuild +++ b/dev-ml/mlgmpidl/mlgmpidl-1.1.ebuild @@ -1,8 +1,8 @@ -# Copyright 1999-2010 Gentoo Foundation +# Copyright 1999-2014 Gentoo Foundation # Distributed under the terms of the GNU General Public License v2 # $Header: $ -EAPI="2" +EAPI="5" inherit eutils toolchain-funcs diff --git a/dev-ml/ocamlgraph/ChangeLog b/dev-ml/ocamlgraph/ChangeLog index 42f0c5b..5e0ac6b 100644 --- a/dev-ml/ocamlgraph/ChangeLog +++ b/dev-ml/ocamlgraph/ChangeLog @@ -18,6 +18,10 @@ -ocamlgraph-1.7.ebuild, +ocamlgraph-1.8.1.ebuild: version bump + 24 Jun 2011; Justin Lecher <j...@gentoo.org> + ocamlgraph-1.7.ebuild: + Sort inherit and/or USE + 06 May 2011; Jonathan-Christofer Demay <jcde...@gmail.com> -ocamlgraph-1.6.ebuild, +ocamlgraph-1.7.ebuild: version bump diff --git a/dev-ml/ocamlgraph/metadata.xml b/dev-ml/ocamlgraph/metadata.xml index 763c1cd..87fc10d 100644 --- a/dev-ml/ocamlgraph/metadata.xml +++ b/dev-ml/ocamlgraph/metadata.xml @@ -1,32 +1,23 @@ <?xml version="1.0" encoding="UTF-8"?> <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd";> <pkgmetadata> - <herd>sci</herd> - <longdescription> - It provides an easy-to-use graph data structure together with several - operations and algorithms over graphs, in Graph.Pack. It is a reasonably - efficient imperative data structure for directed graphs with vertices - and edges labeled with integers. Several other graph implementations - are proposed for those not satisfied with the one above. Some are - persistent (imutable) and other imperative (mutable). Some are directed - and other are not. Some have labels for vertices, or labels for edges, - or both. Some have abstract types for vertices. etc. These - implementations are written as functors: you give the types of vertices - labels, edge labels, etc. and you get the data structure as a result. - it also provides several classic operations and algorithms over graphs. - They are also written as functors i.e. independently of the data - structure for graphs. One consequence is that you can define your own - data structure for graphs and yet re-use all the algorithms from this - library: you only need to provide a few operations such as iterating - over all vertices, over the successors of a vertex, etc. - </longdescription> - <maintainer> - <email>s...@gentoo.org</email> - </maintainer> - <use> - <flag name="doc">?doc?</flag> - <flag name="examples">?examples?</flag> - <flag name="gtk">?gtk?</flag> - <flag name="ocamlopt">?ocamlopt?</flag> - </use> +<herd>sci-mathematics</herd> +<longdescription> + It provides an easy-to-use graph data structure together with several + operations and algorithms over graphs, in Graph.Pack. It is a reasonably + efficient imperative data structure for directed graphs with vertices + and edges labeled with integers. Several other graph implementations + are proposed for those not satisfied with the one above. Some are + persistent (imutable) and other imperative (mutable). Some are directed + and other are not. Some have labels for vertices, or labels for edges, + or both. Some have abstract types for vertices. etc. These + implementations are written as functors: you give the types of vertices + labels, edge labels, etc. and you get the data structure as a result. + it also provides several classic operations and algorithms over graphs. + They are also written as functors i.e. independently of the data + structure for graphs. One consequence is that you can define your own + data structure for graphs and yet re-use all the algorithms from this + library: you only need to provide a few operations such as iterating + over all vertices, over the successors of a vertex, etc. +</longdescription> </pkgmetadata> diff --git a/dev-ml/ocamlgraph/ocamlgraph-1.8.5.ebuild b/dev-ml/ocamlgraph/ocamlgraph-1.8.5.ebuild index d950b6f..2a653f2 100644 --- a/dev-ml/ocamlgraph/ocamlgraph-1.8.5.ebuild +++ b/dev-ml/ocamlgraph/ocamlgraph-1.8.5.ebuild @@ -2,7 +2,7 @@ # Distributed under the terms of the GNU General Public License v2 # $Header: $ -EAPI="2" +EAPI="5" inherit eutils autotools diff --git a/dev-ml/zarith/ChangeLog b/dev-ml/zarith/ChangeLog index 2868b84..434b236 100644 --- a/dev-ml/zarith/ChangeLog +++ b/dev-ml/zarith/ChangeLog @@ -5,7 +5,7 @@ 22 Jun 2014; Jonathan-Christofer Demay <jcde...@gmail.com> zarith-1.2.1.ebuild: fix regression of pkg_setup - + 10 Jun 2014; Jonathan-Christofer Demay <jcde...@gmail.com> -zarith-1.1.ebuild, +zarith-1.2.1.ebuild: version bump @@ -14,7 +14,14 @@ zarith-1.1.ebuild, metadata.xml: Clean wrong space and blank lines; move EAPI=5 - 14 Jan 2013; Jonathan-Christofer Demay <jcde...@gmail.com> - +zarith-1.1.ebuild: - initial commit + 11 Aug 2012; Guillaume Horel <guillaume.ho...@gmail.com> + zarith-1.1.ebuild: + fix license and depend on multilib eclass + + 30 Mar 2012; Guillaume Horel <guillaume.ho...@gmail.com> + -zarith-1.0.ebuild, -files/zarith-1.0-bytecode.patch, -files/zarith-1.0-optnotrequired.patch, +zarith-1.1.ebuild: + version bump + 02 Mar 2012; Guillaume Horel <guillaume.ho...@gmail.com> +zarith-1.0.ebuild, + +files/zarith-1.0-bytecode.patch, +files/zarith-1.0-optnotrequired.patch, +metadata.xml: + initial import diff --git a/dev-ml/zarith/metadata.xml b/dev-ml/zarith/metadata.xml index d2e9691..1ff3218 100644 --- a/dev-ml/zarith/metadata.xml +++ b/dev-ml/zarith/metadata.xml @@ -1,17 +1,11 @@ <?xml version="1.0" encoding="UTF-8"?> <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd";> <pkgmetadata> - <herd>sci</herd> - <longdescription> - The Zarith library implements arithmetic and logical operations over - arbitrary-precision integers. It uses GMP to efficiently implement - arithmetic over big integers. Small integers are represented as Caml - unboxed integers, for speed and space economy. - </longdescription> - <maintainer> - <email>s...@gentoo.org</email> - </maintainer> - <use> - <flag name="ocamlopt">?ocamlopt?</flag> - </use> +<herd>sci-mathematics</herd> +<longdescription> + The Zarith library implements arithmetic and logical operations over + arbitrary-precision integers. It uses GMP to efficiently implement + arithmetic over big integers. Small integers are represented as Caml + unboxed integers, for speed and space economy. +</longdescription> </pkgmetadata> diff --git a/sci-mathematics/alt-ergo/ChangeLog b/sci-mathematics/alt-ergo/ChangeLog index e1becf1..ffdfbd7 100644 --- a/sci-mathematics/alt-ergo/ChangeLog +++ b/sci-mathematics/alt-ergo/ChangeLog @@ -2,9 +2,18 @@ # Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2 # $Header: $ - 10 Jan 2014; Jonathan-Christofer Demay <jcde...@gmail.com> - -alt-ergo-0.95.ebuild, +alt-ergo-0.95.2.ebuild: - version bump + 16 Jun 2014; Jauhien Piatlicki <jauh...@gentoo.org> + -alt-ergo-0.95.1.ebuild, +alt-ergo-0.95.2.ebuild: + version bump; fix bug #479994; move sources to my dev space + + 25 Aug 2013; Andrew Savchenko <birc...@gmail.com> + -alt-ergo-0.95.ebuild, +alt-ergo-0.95.1.ebuild, metadata.xml: + Version bump for a bugfix release. Cleanup metadata. + This also fixes bug 479994 (wrong manifest for alt-ergo-0.95). + + 03 Mar 2013; Justin Lecher <j...@gentoo.org> + alt-ergo-0.95.ebuild, metadata.xml: + Move to EAPI=5; clean quoting and ebuild syntax and indention 14 Jan 2013; Jonathan-Christofer Demay <jcde...@gmail.com> +alt-ergo-0.95.ebuild: 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 9bd6f6b..9fc811b 100644 --- a/sci-mathematics/alt-ergo/alt-ergo-0.95.2.ebuild +++ b/sci-mathematics/alt-ergo/alt-ergo-0.95.2.ebuild @@ -2,13 +2,13 @@ # Distributed under the terms of the GNU General Public License v2 # $Header: $ -EAPI=4 +EAPI=5 inherit eutils DESCRIPTION="Alt-Ergo is an automatic theorem prover" HOMEPAGE="http://alt-ergo.ocamlpro.com"; -SRC_URI="${HOMEPAGE}/download_manager.php?target=${P}.tar.gz" +SRC_URI="http://dev.gentoo.org/~jauhien/distfiles/${P}.tar.gz"; LICENSE="CeCILL-C" SLOT="0" @@ -17,20 +17,20 @@ IUSE="+ocamlopt gtk" DEPEND=">=dev-lang/ocaml-3.12.1[ocamlopt?] >=dev-ml/ocamlgraph-1.8.2[gtk?,ocamlopt?] + dev-ml/zarith gtk? ( >=x11-libs/gtksourceview-2.8 >=dev-ml/lablgtk-2.14[sourceview,ocamlopt?] )" RDEPEND="${DEPEND}" src_prepare(){ - sed -i ${S}/Makefile.in \ + sed \ -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 } src_compile(){ emake || die "emake failed" - if use gtk; then - emake gui || die "emake gui failed" - fi + use gtk && emake gui || die "emake gui failed" } src_install(){ diff --git a/sci-mathematics/alt-ergo/metadata.xml b/sci-mathematics/alt-ergo/metadata.xml index 4ac4fb5..70209e0 100644 --- a/sci-mathematics/alt-ergo/metadata.xml +++ b/sci-mathematics/alt-ergo/metadata.xml @@ -1,19 +1,12 @@ <?xml version="1.0" encoding="UTF-8"?> <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd";> <pkgmetadata> - <herd>sci</herd> - <longdescription> - Alt-Ergo is an open source automatic theorem prover dedicated to program verification. - It is an SMT solver based on CC(X): a congruence closure algorithm parameterized by an - equational theory X. Alt-Ergo is based on a home-made SAT-solver and implements an - instantiation mechanism for quantified formulas. Its architecture is summarized by the - the following picture. - </longdescription> - <maintainer> - <email>s...@gentoo.org</email> - </maintainer> - <use> - <flag name="gtk">?gtk?</flag> - <flag name="ocamlopt">?ocamlopt?</flag> - </use> +<herd>sci-mathematics</herd> +<longdescription> + Alt-Ergo is an open source automatic theorem prover dedicated to program verification. + It is an SMT solver based on CC(X): a congruence closure algorithm parameterized by an + equational theory X. Alt-Ergo is based on a home-made SAT-solver and implements an + instantiation mechanism for quantified formulas. Its architecture is summarized by the + the following picture. +</longdescription> </pkgmetadata> diff --git a/sci-mathematics/apron/apron-0.9.10-r1.ebuild b/sci-mathematics/apron/apron-0.9.10-r1.ebuild index 40791e2..94180af 100644 --- a/sci-mathematics/apron/apron-0.9.10-r1.ebuild +++ b/sci-mathematics/apron/apron-0.9.10-r1.ebuild @@ -1,8 +1,8 @@ -# Copyright 1999-2010 Gentoo Foundation +# Copyright 1999-2014 Gentoo Foundation # Distributed under the terms of the GNU General Public License v2 # $Header: $ -EAPI="2" +EAPI="5" inherit eutils toolchain-funcs diff --git a/sci-mathematics/apron/apron-0.9.10.ebuild b/sci-mathematics/apron/apron-0.9.10.ebuild index 2752070..f5bb5fc 100644 --- a/sci-mathematics/apron/apron-0.9.10.ebuild +++ b/sci-mathematics/apron/apron-0.9.10.ebuild @@ -1,8 +1,8 @@ -# Copyright 1999-2010 Gentoo Foundation +# Copyright 1999-2014 Gentoo Foundation # Distributed under the terms of the GNU General Public License v2 # $Header: $ -EAPI="2" +EAPI="5" inherit eutils toolchain-funcs diff --git a/sci-mathematics/apron/metadata.xml b/sci-mathematics/apron/metadata.xml index f87ceb9..f8c7d84 100644 --- a/sci-mathematics/apron/metadata.xml +++ b/sci-mathematics/apron/metadata.xml @@ -1,21 +1,15 @@ <?xml version="1.0" encoding="UTF-8"?> <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd";> <pkgmetadata> - <herd>sci</herd> - <longdescription> - The APRON library is dedicated to the static analysis of the numerical - variables of a program by Abstract Interpretation. The aim of such an - analysis is to infer invariants about these variables. The APRON library - is intended to be a common interface to various underlying - libraries/abstract domains and to provide additional services that can - be implemented independently from the underlying library/abstract - domain, as shown by the poster on the right (presented at the SAS 2007 - conference. - </longdescription> - <maintainer> - <email>s...@gentoo.org</email> - </maintainer> - <use> - <flag name="ocaml">?ocaml?</flag> - </use> +<herd>sci-mathematics</herd> +<longdescription> + The APRON library is dedicated to the static analysis of the numerical + variables of a program by Abstract Interpretation. The aim of such an + analysis is to infer invariants about these variables. The APRON library + is intended to be a common interface to various underlying + libraries/abstract domains and to provide additional services that can + be implemented independently from the underlying library/abstract + domain, as shown by the poster on the right (presented at the SAS 2007 + conference. +</longdescription> </pkgmetadata> diff --git a/sci-mathematics/flocq/ChangeLog b/sci-mathematics/flocq/ChangeLog index e3076b8..2f56c98 100644 --- a/sci-mathematics/flocq/ChangeLog +++ b/sci-mathematics/flocq/ChangeLog @@ -6,6 +6,10 @@ -flocq-2.1.0.ebuild, +flocq-2.3.0.ebuild: version bump + Mar 2013; Justin Lecher <j...@gentoo.org> + flocq-2.1.0.ebuild, metadata.xml: + Move to EAPI=5; assign RDEPEND explicitatly + 14 Jan 2013; Jonathan-Christofer Demay <jcde...@gmail.com> -flocq-1.4.0.ebuild, +flocq-2.1.0.ebuild: version bump diff --git a/sci-mathematics/flocq/flocq-2.3.0.ebuild b/sci-mathematics/flocq/flocq-2.3.0.ebuild index 6c32445..a26aad1 100644 --- a/sci-mathematics/flocq/flocq-2.3.0.ebuild +++ b/sci-mathematics/flocq/flocq-2.3.0.ebuild @@ -2,7 +2,7 @@ # Distributed under the terms of the GNU General Public License v2 # $Header: $ -EAPI="3" +EAPI="5" DESCRIPTION="A floating-point formalization for the Coq system" HOMEPAGE="http://flocq.gforge.inria.fr/"; @@ -14,6 +14,7 @@ KEYWORDS="~amd64 ~x86" IUSE="" DEPEND="sci-mathematics/coq" +RDEPEND="${DEPEND}" src_prepare() { sed -i Remakefile.in \ diff --git a/sci-mathematics/flocq/metadata.xml b/sci-mathematics/flocq/metadata.xml index c8feb0f..dad568b 100644 --- a/sci-mathematics/flocq/metadata.xml +++ b/sci-mathematics/flocq/metadata.xml @@ -1,14 +1,11 @@ <?xml version="1.0" encoding="UTF-8"?> <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd";> <pkgmetadata> - <herd>sci</herd> - <longdescription> - Flocq (Floats for Coq) is a floating-point formalization for the Coq - system. It provides a comprehensive library of theorems on a multi-radix - multi-precision arithmetic. It also supports efficient numerical - computations inside Coq. - </longdescription> - <maintainer> - <email>s...@gentoo.org</email> - </maintainer> +<herd>sci-mathematics</herd> +<longdescription> + Flocq (Floats for Coq) is a floating-point formalization for the Coq + system. It provides a comprehensive library of theorems on a multi-radix + multi-precision arithmetic. It also supports efficient numerical + computations inside Coq. +</longdescription> </pkgmetadata> diff --git a/sci-mathematics/frama-c/ChangeLog b/sci-mathematics/frama-c/ChangeLog index 3188d47..f57fb63 100644 --- a/sci-mathematics/frama-c/ChangeLog +++ b/sci-mathematics/frama-c/ChangeLog @@ -3,12 +3,12 @@ # $Header: $ 21 Jun 2014; Jonathan-Christofer Demay <jcde...@gmail.com> - -frama-c-20130601.ebuild, +frama-c-20140301.ebuild: + -frama-c-20130601.ebuild,-files/frama-c-ocaml-4.01.patch, -files/frama-c-make.patch, +frama-c-20140301.ebuild: version bump - 19 Jul 2013; Jonathan-Christofer Demay <jcde...@gmail.com> - -frama-c-20120901.ebuild, +frama-c-20130601.ebuild: - version bump + 24 Feb 2014; Andrew Savchenko <birc...@gmail.com> + +frama-c-20130601.ebuild, +files/frama-c-ocaml-4.01.patch, +files/frama-c-make.patch: + Version bump. Fix build with make >= 4.x, add ocaml-4.01 support. 14 Jan 2013; Jonathan-Christofer Demay <jcde...@gmail.com> -frama-c-20111001.ebuild, +frama-c-20120901.ebuild: diff --git a/sci-mathematics/frama-c/frama-c-20140301.ebuild b/sci-mathematics/frama-c/frama-c-20140301.ebuild index f93062c..02ad2c8 100644 --- a/sci-mathematics/frama-c/frama-c-20140301.ebuild +++ b/sci-mathematics/frama-c/frama-c-20140301.ebuild @@ -1,8 +1,8 @@ -# Copyright 1999-2013 Gentoo Foundation +# Copyright 1999-2015 Gentoo Foundation # Distributed under the terms of the GNU General Public License v2 # $Header: $ -EAPI="3" +EAPI="5" inherit autotools eutils diff --git a/sci-mathematics/frama-c/metadata.xml b/sci-mathematics/frama-c/metadata.xml index 59797bc..e429e61 100644 --- a/sci-mathematics/frama-c/metadata.xml +++ b/sci-mathematics/frama-c/metadata.xml @@ -1,22 +1,14 @@ <?xml version="1.0" encoding="UTF-8"?> <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd";> <pkgmetadata> - <herd>sci</herd> - <longdescription> - Frama-C is a suite of tools dedicated to the analysis of the source code - of software written in C. It gathers several static analysis techniques - in a single collaborative framework. The collaborative approach of - Frama-C allows static analyzers to build upon the results already - computed by other analyzers in the framework. Thanks to this approach, - Frama-C provides sophisticated tools, such as a slicer and dependency - analysis. - </longdescription> - <maintainer> - <email>s...@gentoo.org</email> - </maintainer> - <use> - <flag name="doc">?doc?</flag> - <flag name="gtk">?gtk?</flag> - <flag name="ocamlopt">?ocamlopt?</flag> - </use> +<herd>sci-mathematics</herd> +<longdescription> + Frama-C is a suite of tools dedicated to the analysis of the source code + of software written in C. It gathers several static analysis techniques + in a single collaborative framework. The collaborative approach of + Frama-C allows static analyzers to build upon the results already + computed by other analyzers in the framework. Thanks to this approach, + Frama-C provides sophisticated tools, such as a slicer and dependency + analysis. +</longdescription> </pkgmetadata> diff --git a/sci-mathematics/gappa/ChangeLog b/sci-mathematics/gappa/ChangeLog index cb7576d..f43aec5 100644 --- a/sci-mathematics/gappa/ChangeLog +++ b/sci-mathematics/gappa/ChangeLog @@ -3,9 +3,13 @@ # $Header: $ 21 Jun 2014; Jonathan-Christofer Demay <jcde...@gmail.com> - -gappa-0.16.6.ebuild, +gappa-1.1.1.ebuild: + -gappa-1.0.0.ebuild, +gappa-1.1.1.ebuild: version bump + 12 Aug 2013; Sebastien Fabbro <bicat...@gentoo.org> + -gappa-0.16.3.ebuild, +gappa-1.0.0.ebuild: + sci-mathematics/gappa: Version bump + 11 Dec 2013; Jonathan-Christofer Demay <jcde...@gmail.com> -gappa-0.16.3.ebuild, +gappa-0.16.6.ebuild: version bump diff --git a/sci-mathematics/gappa/gappa-1.1.1.ebuild b/sci-mathematics/gappa/gappa-1.1.1.ebuild index a817cbb..3da8e4b 100644 --- a/sci-mathematics/gappa/gappa-1.1.1.ebuild +++ b/sci-mathematics/gappa/gappa-1.1.1.ebuild @@ -2,7 +2,7 @@ # Distributed under the terms of the GNU General Public License v2 # $Header: $ -EAPI="3" +EAPI="5" DESCRIPTION="A tool to help verifying and proving properties on floating-point or fixed-point arithmetic" HOMEPAGE="http://gappa.gforge.inria.fr/"; @@ -21,12 +21,12 @@ DEPEND="${RDEPEND} 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" + -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" + ./remake -d ${MAKEOPTS} || die "emake failed" if use doc; then ./remake doc/html/index.html fi @@ -35,8 +35,6 @@ src_compile() { 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 + use doc && dohtml -A png -r doc/html/* } diff --git a/sci-mathematics/gappalib-coq/gappalib-coq-1.0.0.ebuild b/sci-mathematics/gappalib-coq/gappalib-coq-1.0.0.ebuild index 01d90ee..2be76ba 100644 --- a/sci-mathematics/gappalib-coq/gappalib-coq-1.0.0.ebuild +++ b/sci-mathematics/gappalib-coq/gappalib-coq-1.0.0.ebuild @@ -2,7 +2,7 @@ # Distributed under the terms of the GNU General Public License v2 # $Header: $ -EAPI="3" +EAPI="5" DESCRIPTION="Allows the certificates Gappa generates to be imported by the Coq" HOMEPAGE="http://gappa.gforge.inria.fr/"; diff --git a/sci-mathematics/giac/ChangeLog b/sci-mathematics/giac/ChangeLog index 0d8189d..5635167 100644 --- a/sci-mathematics/giac/ChangeLog +++ b/sci-mathematics/giac/ChangeLog @@ -6,6 +6,9 @@ -giac-1.0.0.ebuild, +giac-1.1.0.ebuild: version bump + 03 Mar 2013; Justin Lecher <j...@gentoo.org> giac-1.0.0.ebuild, metadata.xml: + Drop useless blank line + 14 Jan 2013; Jonathan-Christofer Demay <jcde...@gmail.com> -giac-0.9.2.ebuild, +giac-1.0.0.ebuild: version bump diff --git a/sci-mathematics/giac/metadata.xml b/sci-mathematics/giac/metadata.xml index 58559f4..e0b6115 100644 --- a/sci-mathematics/giac/metadata.xml +++ b/sci-mathematics/giac/metadata.xml @@ -1,20 +1,12 @@ <?xml version="1.0" encoding="UTF-8"?> <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd";> <pkgmetadata> - <herd>sci</herd> - <longdescription> - Giac is a free computer algebra system that can be used to perform - computer algebra, function graphs, interactive geometry (2-d and 3-d), - spreadsheet and statistics, programmation. It may be used as a replacement - for high end graphic calculators for example on netbooks (for about - the same price as a calculator but with much more performances). - </longdescription> - <maintainer> - <email>s...@gentoo.org</email> - </maintainer> - <use> - <flag name="doc">?doc?</flag> - <flag name="examples">?examples?</flag> - <flag name="fltk">?fltk?</flag> - </use> -</pkgmetadata> +<herd>sci-mathematics</herd> +<longdescription> + Giac is a free computer algebra system that can be used to perform + computer algebra, function graphs, interactive geometry (2-d and 3-d), + spreadsheet and statistics, programmation. It may be used as a replacement + for high end graphic calculators for example on netbooks (for about + the same price as a calculator but with much more performances). +</longdescription> +<pkgmetadata> diff --git a/sci-mathematics/ltl2ba/ltl2ba-1.1.ebuild b/sci-mathematics/ltl2ba/ltl2ba-1.1.ebuild index c0bf644..dc1288d 100644 --- a/sci-mathematics/ltl2ba/ltl2ba-1.1.ebuild +++ b/sci-mathematics/ltl2ba/ltl2ba-1.1.ebuild @@ -1,7 +1,9 @@ -# Copyright 1999-2010 Gentoo Foundation +# Copyright 1999-2015 Gentoo Foundation # Distributed under the terms of the GNU General Public License v2 # $Header: $ +EAPI="5" + DESCRIPTION="Fast LTL to Buechi Automata Translation" HOMEPAGE="http://www.lsv.ens-cachan.fr/~gastin/${PN}/"; SRC_URI="http://www.lsv.ens-cachan.fr/~gastin/${PN}/${P}.tar.gz"; diff --git a/sci-mathematics/ltl2ba/metadata.xml b/sci-mathematics/ltl2ba/metadata.xml index efb490d..b229aec 100644 --- a/sci-mathematics/ltl2ba/metadata.xml +++ b/sci-mathematics/ltl2ba/metadata.xml @@ -2,7 +2,4 @@ <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd";> <pkgmetadata> <herd>sci</herd> -<maintainer> - <email>s...@gentoo.org</email> -</maintainer> </pkgmetadata> diff --git a/sci-mathematics/pff/ChangeLog b/sci-mathematics/pff/ChangeLog index 1f0a01a..f4ba1e3 100644 --- a/sci-mathematics/pff/ChangeLog +++ b/sci-mathematics/pff/ChangeLog @@ -6,6 +6,10 @@ pff-8.4.ebuild: install fixes + Mar 2013; Justin Lecher <j...@gentoo.org> + pff-8.4.ebuild, metadata.xml: + Drop pcc and sparc keywords as deps are not keyworded; move to EAPI=5 + 14 Jan 2013; Jonathan-Christofer Demay <jcde...@gmail.com> -pff-8.3.ebuild, +pff-8.4.ebuild: version bump diff --git a/sci-mathematics/pff/metadata.xml b/sci-mathematics/pff/metadata.xml index edab690..af7c7b9 100644 --- a/sci-mathematics/pff/metadata.xml +++ b/sci-mathematics/pff/metadata.xml @@ -1,14 +1,12 @@ <?xml version="1.0" encoding="UTF-8"?> <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd";> <pkgmetadata> - <herd>sci</herd> - <longdescription> - PFF (Preuves Formelles sur les Flottants = Formal Proofs about Floats) - is a repository of a Coq library about floating-point arithmetic. It - contains both definitions and proofs of basic facts, old and new - properties and algorithms. - </longdescription> - <maintainer> - <email>s...@gentoo.org</email> - </maintainer> +<herd>sci-mathematics</herd> +<longdescription> + PFF (Preuves Formelles sur les Flottants = Formal Proofs about Floats) + is a repository of a Coq library about floating-point arithmetic. It + contains both definitions and proofs of basic facts, old and new + properties and algorithms. +</longdescription> + </pkgmetadata> diff --git a/sci-mathematics/pff/pff-8.4.ebuild b/sci-mathematics/pff/pff-8.4.ebuild index 747366c..5f0306d 100644 --- a/sci-mathematics/pff/pff-8.4.ebuild +++ b/sci-mathematics/pff/pff-8.4.ebuild @@ -1,8 +1,8 @@ -# Copyright 1999-2013 Gentoo Foundation +# Copyright 1999-2014 Gentoo Foundation # Distributed under the terms of the GNU General Public License v2 # $Header: $ -EAPI="2" +EAPI="5" DESCRIPTION="Library for reasoning about floating point numbers in coq" HOMEPAGE="http://lipforge.ens-lyon.fr/www/pff/"; diff --git a/sci-mathematics/why/ChangeLog b/sci-mathematics/why/ChangeLog index f4b826e..1fc178c 100644 --- a/sci-mathematics/why/ChangeLog +++ b/sci-mathematics/why/ChangeLog @@ -6,6 +6,10 @@ -why-2.30.ebuild, -files/why-2.30.patch, +why-2.34.ebuild, +why-flocq23.patch: version bump + 03 Mar 2013; Justin Lecher <j...@gentoo.org> + why-2.30.ebuild, metadata.xml: + Drop ppc as deps are not keyworded; move to EAPI=5 and autotools-utils.eclass + 21 Dec 2011; Jonathan-Christofer Demay <jcde...@gmail.com> -why-2.29.ebuild, -files/why_jessie-carbon.patch, +why-2.30.ebuild, +files/why-2.30.patch: version bump diff --git a/sci-mathematics/why/metadata.xml b/sci-mathematics/why/metadata.xml index 06bd0a5..a777c26 100644 --- a/sci-mathematics/why/metadata.xml +++ b/sci-mathematics/why/metadata.xml @@ -1,24 +1,12 @@ <?xml version="1.0" encoding="UTF-8"?> <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd";> <pkgmetadata> - <herd>sci</herd> - <longdescription> - Why is a software verification platform. It contains a general-purpose - verification condition generator (VCG) which is used as a back-end - by other verification tools but it can also be used directly to verify - programs. It also provides Krakatoa, a tool or the verification of Java - programs and Caduceus, a tool for the verification of C programs. - </longdescription> - <maintainer> - <email>s...@gentoo.org</email> - </maintainer> - <use> - <flag name="apron">?apron?</flag> - <flag name="coq">?coq?</flag> - <flag name="gappa">?gappa?</flag> - <flag name="frama-c">?frama-c?</flag> - <flag name="gtk">?gtk?</flag> - <flag name="pff">?pff?</flag> - <flag name="why3">?why3?</flag> - </use> +<herd>sci</herd> +<longdescription> + Why is a software verification platform. It contains a general-purpose + verification condition generator (VCG) which is used as a back-end + by other verification tools but it can also be used directly to verify + programs. It also provides Krakatoa, a tool or the verification of Java + programs and Caduceus, a tool for the verification of C programs. +</longdescription> </pkgmetadata> diff --git a/sci-mathematics/why/why-2.34.ebuild b/sci-mathematics/why/why-2.34.ebuild index c7eddfa..813aa20 100644 --- a/sci-mathematics/why/why-2.34.ebuild +++ b/sci-mathematics/why/why-2.34.ebuild @@ -1,8 +1,8 @@ -# Copyright 1999-2010 Gentoo Foundation +# Copyright 1999-2014 Gentoo Foundation # Distributed under the terms of the GNU General Public License v2 # $Header: $ -EAPI="2" +EAPI="5" inherit autotools eutils diff --git a/sci-mathematics/why3/metadata.xml b/sci-mathematics/why3/metadata.xml index 361520d..17c0a90 100644 --- a/sci-mathematics/why3/metadata.xml +++ b/sci-mathematics/why3/metadata.xml @@ -1,23 +1,17 @@ <?xml version="1.0" encoding="UTF-8"?> <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd";> <pkgmetadata> - <herd>sci</herd> - <longdescription> - Why3 is a platform for deductive program verification. It provides - a rich language for specification and programming, called WhyML, - and relies on external theorem provers, both automated and interactive, - to discharge verification conditions. Why3 comes with a standard - library of logical theories (integer and real arithmetic, Boolean - operations, sets and maps, etc.) and basic programming data structures - (arrays, queues, hash tables, etc.). A user can write WhyML programs - directly and get correct-by-construction OCaml programs through an - automated extraction mechanism. WhyML is also used as an intermediate - language for the verification of C, Java, or Ada programs. - </longdescription> - <maintainer> - <email>s...@gentoo.org</email> - </maintainer> - <use> - <flag name="frama-c">?frama-c?</flag> - </use> +<herd>sci-mathematics</herd> +<longdescription> + Why3 is a platform for deductive program verification. It provides + a rich language for specification and programming, called WhyML, + and relies on external theorem provers, both automated and interactive, + to discharge verification conditions. Why3 comes with a standard + library of logical theories (integer and real arithmetic, Boolean + operations, sets and maps, etc.) and basic programming data structures + (arrays, queues, hash tables, etc.). A user can write WhyML programs + directly and get correct-by-construction OCaml programs through an + automated extraction mechanism. WhyML is also used as an intermediate + language for the verification of C, Java, or Ada programs. +</longdescription> </pkgmetadata> diff --git a/sci-mathematics/why3/why3-0.83.ebuild b/sci-mathematics/why3/why3-0.83.ebuild index 55bc656..30615b5 100644 --- a/sci-mathematics/why3/why3-0.83.ebuild +++ b/sci-mathematics/why3/why3-0.83.ebuild @@ -2,7 +2,7 @@ # Distributed under the terms of the GNU General Public License v2 # $Header: $ -EAPI="2" +EAPI="5" inherit autotools eutils
