[gentoo-commits] proj/sci:master commit in: sci-mathematics/why/files/, sci-mathematics/why/

[Jonathan-Christofer Demay]

commit:     2a68e26824aa72d512a85e1f79435f5353745f00
Author:     Jonathan-Christofer Demay <jcdemay <AT> gmail <DOT> com>
AuthorDate: Mon Feb  6 14:38:07 2012 +0000
Commit:     Jonathan-Christofer Demay <jcdemay <AT> gmail <DOT> com>
CommitDate: Mon Feb  6 14:38:07 2012 +0000
URL:        http://git.overlays.gentoo.org/gitweb/?p=proj/sci.git;a=commit;h=2a68e268

sci-mathematics/why: version bump

---
 sci-mathematics/why/ChangeLog                     |    5 +-
 sci-mathematics/why/files/why-2.30.patch          |   36 +++++++++++
 sci-mathematics/why/files/why_jessie-carbon.patch |   36 -----------
 sci-mathematics/why/metadata.xml                  |    2 +-
 sci-mathematics/why/why-2.29.ebuild               |   69 ---------------------
 sci-mathematics/why/why-2.30.ebuild               |   65 +++++++++++++++++++
 6 files changed, 105 insertions(+), 108 deletions(-)

diff --git a/sci-mathematics/why/ChangeLog b/sci-mathematics/why/ChangeLog
index 2a1bf9c..b7fb3e4 100644
--- a/sci-mathematics/why/ChangeLog
+++ b/sci-mathematics/why/ChangeLog
@@ -2,8 +2,9 @@
 # Copyright 1999-2011 Gentoo Foundation; Distributed under the GPL v2
 # $Header: $
 
-  24 Jun 2011; Justin Lecher <jlec@g.o> why-2.29.ebuild:
-  EAPI bump
+  21 Dec 2011; J.-C. Demay <jcdemay@×××××.com>
+  -why-2.29.ebuild, +why-2.30.ebuild, -files/why_jessie-carbon.patch, +files/why-2.30.patch:
+  version bump
 
   06 May 2011; J.-C. Demay <jcdemay@×××××.com>
   -why-2.28.ebuild, +why-2.29.ebuild:

diff --git a/sci-mathematics/why/files/why-2.30.patch b/sci-mathematics/why/files/why-2.30.patch
new file mode 100644
index 0000000..2c8f48c
--- /dev/null
+++ b/sci-mathematics/why/files/why-2.30.patch
@@ -0,0 +1,36 @@
+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_jessie-carbon.patch b/sci-mathematics/why/files/why_jessie-carbon.patch
deleted file mode 100644
index 0288bc7..0000000
--- a/sci-mathematics/why/files/why_jessie-carbon.patch
+++ /dev/null
@@ -1,36 +0,0 @@
-diff -Naurp why-2.28-orig/jc/jc_annot_inference.ml why-2.28/jc/jc_annot_inference.ml
---- why-2.28/jc/jc_annot_inference.ml	2010-12-17 20:06:44.000000000 +0000
-+++ why-2.28/jc/jc_annot_inference.ml	2011-02-14 11:34:21.000000000 +0000
-@@ -150,8 +150,8 @@ let rec destruct_pointer t =
-     | JCTvar _ | JCTderef _ | JCTapp _ | JCTold _ | JCTat _ | JCTif _ 
-     | JCTrange _ | JCTmatch _ | JCTaddress _ | JCTbase_block _
-     | JCTconst _ | JCTbinary _ | JCTunary _ | JCToffset _ | JCTinstanceof _ 
--    | JCTreal_cast _ | JCTrange_cast _ | JCTbitwise_cast _ | JCTcast _ ->
--	None
-+    | JCTreal_cast _ | JCTrange_cast _ | JCTbitwise_cast _ | JCTcast _
-+    | JCTlet (_, _, _) -> None
- 
- let equality_operator_of_type ty = `Beq, operator_of_type ty
- 
-@@ -610,8 +610,8 @@ let rec atp_of_term t =
- 	Atp.Var (Vwp.variable_for_term t)
-     | JCTshift _ | JCTold _ | JCTat _ | JCTmatch _ | JCTinstanceof _ 
-     | JCTcast _ | JCTrange_cast _ | JCTbitwise_cast _ | JCTreal_cast _ 
--    | JCTaddress _ | JCTif _ | JCTrange _ | JCTunary _ | JCTbase_block _ ->
--	err ()
-+    | JCTaddress _ | JCTif _ | JCTrange _ | JCTunary _ | JCTbase_block _
-+    | JCTlet (_, _, _) -> err ()
- 
- let rec term_of_atp tm =
-   try
-@@ -1198,8 +1198,8 @@ let linearize t =
-       | JCTunary _ | JCTshift _ | JCTinstanceof _ | JCTmatch _ 
-       | JCTold _ | JCTat _ | JCTcast _ | JCTbitwise_cast _ 
-       | JCTrange_cast _ | JCTreal_cast _ | JCTaddress _ | JCTbase_block _
--      | JCTrange _ | JCTif _ -> 
--	  err ()
-+      | JCTrange _ | JCTif _
-+      | JCTlet (_, _, _) -> err ()
-     with Failure "linearize" -> 
-       (TermMap.add t (Int 1) TermMap.empty, Int 0)
-   in aux t

diff --git a/sci-mathematics/why/metadata.xml b/sci-mathematics/why/metadata.xml
index 33676ea..8098c56 100644
--- a/sci-mathematics/why/metadata.xml
+++ b/sci-mathematics/why/metadata.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
 <pkgmetadata>
-	<herd>sci-mathematics</herd>
+	<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

diff --git a/sci-mathematics/why/why-2.29.ebuild b/sci-mathematics/why/why-2.29.ebuild
deleted file mode 100644
index c8cc38d..0000000
--- a/sci-mathematics/why/why-2.29.ebuild
+++ /dev/null
@@ -1,69 +0,0 @@
-# Copyright 1999-2011 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-# $Header: $
-
-EAPI=4
-
-inherit autotools eutils
-
-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 ~ppc ~x86"
-IUSE="apron coq doc examples gappa gtk jessie pff"
-
-DEPEND="
-	>=dev-lang/ocaml-3.09
-	>=dev-ml/ocamlgraph-1.2
-	apron? ( sci-mathematics/apron )
-	coq? ( sci-mathematics/coq )
-	gappa? ( sci-mathematics/gappalib-coq )
-	gtk? ( >=dev-ml/lablgtk-2.14 )
-	jessie? ( >=sci-mathematics/frama-c-20100401 )
-	pff? ( sci-mathematics/pff )"
-RDEPEND="${DEPEND}"
-
-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 || die
-
-	epatch "${FILESDIR}"/${PN}_jessie-carbon.patch
-	eautoreconf
-}
-
-src_configure() {
-	econf \
-		$(use_enable apron)
-}
-
-src_compile(){
-	emake -j1 DESTDIR="${EROOT}" || die "emake failed"
-}
-
-src_install(){
-	default
-
-	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/why/why-2.30.ebuild b/sci-mathematics/why/why-2.30.ebuild
new file mode 100644
index 0000000..79036b6
--- /dev/null
+++ b/sci-mathematics/why/why-2.30.ebuild
@@ -0,0 +1,65 @@
+# 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 ~ppc ~x86"
+IUSE="apron coq doc examples gappa jessie gtk 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}"
+
+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}"/${P}.patch
+	eautoreconf
+}
+
+src_configure() {
+	econf $(use_enable apron) PATH="/usr/bin:$PATH" || die "econf failed"
+}
+
+src_compile(){
+	emake -j1 DESTDIR="/" || 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
+}