* [gentoo-commits] proj/sci:master commit in: sci-mathematics/giac/, dev-ml/zarith/, dev-ml/mlgmpidl/, sci-mathematics/pff/, ...
@ 2014-06-22 20:23 Jonathan-Christofer Demay
0 siblings, 0 replies; only message in thread
From: Jonathan-Christofer Demay @ 2014-06-22 20:23 UTC (permalink / raw
To: gentoo-commits
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>sci@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>sci@gentoo.org</email>
- </maintainer>
- <use>
- <flag name="mpfr">add support for mpfr, the library for multiple-precision floating-point computations with exact rounding</flag>
- </use>
+<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 <jlec@gentoo.org>
+ ocamlgraph-1.7.ebuild:
+ Sort inherit and/or USE
+
06 May 2011; Jonathan-Christofer Demay <jcdemay@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>sci@gentoo.org</email>
- </maintainer>
- <use>
- <flag name="doc">?doc?</flag>
- <flag name="examples">?examples?</flag>
- <flag name="gtk">?gtk?</flag>
- <flag name="ocamlopt">?ocamlopt?</flag>
- </use>
+<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 <jcdemay@gmail.com>
zarith-1.2.1.ebuild:
fix regression of pkg_setup
-
+
10 Jun 2014; Jonathan-Christofer Demay <jcdemay@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 <jcdemay@gmail.com>
- +zarith-1.1.ebuild:
- initial commit
+ 11 Aug 2012; Guillaume Horel <guillaume.horel@gmail.com>
+ zarith-1.1.ebuild:
+ fix license and depend on multilib eclass
+
+ 30 Mar 2012; Guillaume Horel <guillaume.horel@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.horel@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>sci@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 <jcdemay@gmail.com>
- -alt-ergo-0.95.ebuild, +alt-ergo-0.95.2.ebuild:
- version bump
+ 16 Jun 2014; Jauhien Piatlicki <jauhien@gentoo.org>
+ -alt-ergo-0.95.1.ebuild, +alt-ergo-0.95.2.ebuild:
+ version bump; fix bug #479994; move sources to my dev space
+
+ 25 Aug 2013; Andrew Savchenko <bircoph@gmail.com>
+ -alt-ergo-0.95.ebuild, +alt-ergo-0.95.1.ebuild, metadata.xml:
+ Version bump for a bugfix release. Cleanup metadata.
+ This also fixes bug 479994 (wrong manifest for alt-ergo-0.95).
+
+ 03 Mar 2013; Justin Lecher <jlec@gentoo.org>
+ alt-ergo-0.95.ebuild, metadata.xml:
+ Move to EAPI=5; clean quoting and ebuild syntax and indention
14 Jan 2013; Jonathan-Christofer Demay <jcdemay@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>sci@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>sci@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 <jlec@gentoo.org>
+ flocq-2.1.0.ebuild, metadata.xml:
+ Move to EAPI=5; assign RDEPEND explicitatly
+
14 Jan 2013; Jonathan-Christofer Demay <jcdemay@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>sci@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 <jcdemay@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 <jcdemay@gmail.com>
- -frama-c-20120901.ebuild, +frama-c-20130601.ebuild:
- version bump
+ 24 Feb 2014; Andrew Savchenko <bircoph@gmail.com>
+ +frama-c-20130601.ebuild, +files/frama-c-ocaml-4.01.patch, +files/frama-c-make.patch:
+ Version bump. Fix build with make >= 4.x, add ocaml-4.01 support.
14 Jan 2013; Jonathan-Christofer Demay <jcdemay@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>sci@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 <jcdemay@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 <bicatali@gentoo.org>
+ -gappa-0.16.3.ebuild, +gappa-1.0.0.ebuild:
+ sci-mathematics/gappa: Version bump
+
11 Dec 2013; Jonathan-Christofer Demay <jcdemay@gmail.com>
-gappa-0.16.3.ebuild, +gappa-0.16.6.ebuild:
version bump
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 <jlec@gentoo.org> giac-1.0.0.ebuild, metadata.xml:
+ Drop useless blank line
+
14 Jan 2013; Jonathan-Christofer Demay <jcdemay@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>sci@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>sci@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 <jlec@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 <jcdemay@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>sci@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 <jlec@gentoo.org>
+ why-2.30.ebuild, metadata.xml:
+ Drop ppc as deps are not keyworded; move to EAPI=5 and autotools-utils.eclass
+
21 Dec 2011; Jonathan-Christofer Demay <jcdemay@gmail.com>
-why-2.29.ebuild, -files/why_jessie-carbon.patch, +why-2.30.ebuild, +files/why-2.30.patch:
version bump
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>sci@gentoo.org</email>
- </maintainer>
- <use>
- <flag name="apron">?apron?</flag>
- <flag name="coq">?coq?</flag>
- <flag name="gappa">?gappa?</flag>
- <flag name="frama-c">?frama-c?</flag>
- <flag name="gtk">?gtk?</flag>
- <flag name="pff">?pff?</flag>
- <flag name="why3">?why3?</flag>
- </use>
+<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>sci@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
^ permalink raw reply related [flat|nested] only message in thread
only message in thread, other threads:[~2014-06-22 20:23 UTC | newest]
Thread overview: (only message) (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2014-06-22 20:23 [gentoo-commits] proj/sci:master commit in: sci-mathematics/giac/, dev-ml/zarith/, dev-ml/mlgmpidl/, sci-mathematics/pff/, Jonathan-Christofer Demay
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox