aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJonathan-Christofer Demay <jcdemay@gmail.com>2010-07-08 19:43:02 +0000
committerJonathan-Christofer Demay <jcdemay@gmail.com>2010-07-08 19:43:02 +0000
commit0676029c15ace58b89520cf2828c0672c81bb8d2 (patch)
treedce7034bb91730310e4fdb5bde18fb0920814fa6
parentsci-mathematics/frama-c: Version bump (diff)
downloadsci-0676029c15ace58b89520cf2828c0672c81bb8d2.tar.gz
sci-0676029c15ace58b89520cf2828c0672c81bb8d2.tar.bz2
sci-0676029c15ace58b89520cf2828c0672c81bb8d2.zip
sci-mathematics/why: Version bump
-rw-r--r--sci-mathematics/why/ChangeLog12
-rw-r--r--sci-mathematics/why/Manifest8
-rw-r--r--sci-mathematics/why/files/why-2.19-jessie_lib.patch43
-rw-r--r--sci-mathematics/why/files/why-2.19-makefile_sandbox.patch75
-rw-r--r--sci-mathematics/why/metadata.xml23
-rw-r--r--sci-mathematics/why/why-2.26.ebuild (renamed from sci-mathematics/why/why-2.19.ebuild)20
6 files changed, 48 insertions, 133 deletions
diff --git a/sci-mathematics/why/ChangeLog b/sci-mathematics/why/ChangeLog
new file mode 100644
index 000000000..07ace3a5d
--- /dev/null
+++ b/sci-mathematics/why/ChangeLog
@@ -0,0 +1,12 @@
+# ChangeLog for sci-mathematics/why
+# Copyright 1999-2010 Gentoo Foundation; Distributed under the GPL v2
+# $Header: $
+
+ 08 Jul 2010; J.-C. Demay <jcdemay@gmail.com>
+ -why-2.19.ebuild, +why-2.26.ebuild:
+ Version Bump
+
+ 08 Jul 2010; J.-C. Demay <jcdemay@gmail.com>
+ +ChangeLog, +metadata.xml:
+ QA fixes
+
diff --git a/sci-mathematics/why/Manifest b/sci-mathematics/why/Manifest
index 6fda3e99b..0924a92ae 100644
--- a/sci-mathematics/why/Manifest
+++ b/sci-mathematics/why/Manifest
@@ -1,4 +1,4 @@
-AUX why-2.19-jessie_lib.patch 1631 RMD160 b3975a252f539a04b079b6e973332136fde464cb SHA1 2ba2c2956354c896904d0c9a2e1d6079fbb56027 SHA256 aaff9f7648438d54eec0b1e9f0ff4828aaa26558ee7d847190d7a3d6e0c4abbc
-AUX why-2.19-makefile_sandbox.patch 3025 RMD160 b8b1b178b09a7b6eda9c8aeac7f5013650fb6c84 SHA1 6bd5e80aa79a6a36d89a114696da716b92aa60df SHA256 121b67a2b46139b93be9af293615a6a04e06a00323096e8b2317a7116bbf5d84
-DIST why-2.19.tar.gz 2622629 RMD160 d1e3a099226a42b039672161ada63270e6274b46 SHA1 6139699168c6aab76d42e02029ba4c51cf2a8130 SHA256 f5eef288c25744f1c7725c1c733b3129a74cde6cf08eaa57b9705115d75499a3
-EBUILD why-2.19.ebuild 1473 RMD160 432f46e94b8a118fd04ef94863b784b4783fa910 SHA1 03b322c41488f3f55edd4ab8483ac76f5ff4473c SHA256 ff96a7de9ee0372f823912f2fd748846554e5894ee7c0c9877b8d954d8889828
+DIST why-2.26.tar.gz 2681455 RMD160 f4a2e758d3ede4d2c682e2b8ea307f02d1c6c944 SHA1 f6958a7af8a5e12bb4cb669880b161ca171d06b7 SHA256 c74c2181da9ffbd1c122bb34becafa7c520427bc1a72008c0a286a7a1fe38246
+EBUILD why-2.26.ebuild 1431 RMD160 45c7d11c1b76cce6aa8b6fbc40f889e3aeca1e9b SHA1 05d03badd33de6fd5b725c275f473e53e0106671 SHA256 22a841e9338d7b4ead8bacf9054de88ac3bab8e79cf7cc74a553b2c8a61ba4f1
+MISC ChangeLog 309 RMD160 2542a421513d2cfeffed91638e95bd55c1cb3921 SHA1 87cd70c37fa0536a31bf02a22d96461ed45ca71a SHA256 f59cbcefe55addc566be53beb26096370219abb81b16a52805003723ce497d1a
+MISC metadata.xml 835 RMD160 38717707edcc9cd836d5f13bbfd38ae7a26114e2 SHA1 c7eb904790b811b3e9393a40440dc24c917f8b39 SHA256 fe7c99c8ec56d17c9fe627e4e2b7edbb2b97a81b33d27fcf2d64a7254d3fe8de
diff --git a/sci-mathematics/why/files/why-2.19-jessie_lib.patch b/sci-mathematics/why/files/why-2.19-jessie_lib.patch
deleted file mode 100644
index 5a312a4ff..000000000
--- a/sci-mathematics/why/files/why-2.19-jessie_lib.patch
+++ /dev/null
@@ -1,43 +0,0 @@
-diff -Naur why-2.19-orig/Makefile.in why-2.19-ptch/Makefile.in
---- why-2.19-orig/Makefile.in 2009-06-23 12:09:43.000000000 +0000
-+++ why-2.19-ptch/Makefile.in 2009-09-04 16:11:28.000000000 +0000
-@@ -147,8 +147,10 @@
-
- ifeq ($(OCAMLBEST),opt)
- JCLIB=jc/jc.cmo jc/jc.cmx
-+JCLD=jc/jc.cmi jc/jc.o
- else
- JCLIB=jc/jc.cmo
-+JCLD=jc/jc.cmi
- endif
-
- all: $(BINARY) $(WHYCONFIG) check $(CADUCEUS) $(JESSIE) $(KRAKATOA) coq-@COQ@ pvs-@PVS@ $(TOOLS) gwhy-@LABLGTK2@ $(JCLIB) $(REGTEST)
-@@ -276,15 +278,15 @@
-
- # jessie
- JCCML_EXPORT = src/lib.ml src/rc.ml src/loc.ml src/pp.ml src/option_misc.ml \
-- jc/jc_type_var.ml jc/output.ml \
-+ jc/jc_type_var.ml jc/jc_env.ml jc/output.ml \
- jc/jc_common_options.ml jc/jc_stdlib.ml \
-- jc/jc_envset.ml jc/jc_region.ml jc/jc_fenv.ml \
-+ jc/jc_envset.ml jc/jc_region.ml jc/jc_ast.ml jc/jc_fenv.ml \
- jc/jc_constructors.ml \
- jc/jc_pervasives.ml jc/jc_iterators.ml \
- jc/jc_output_misc.ml jc/jc_poutput.ml jc/jc_output.ml jc/jc_noutput.ml
- JCCMO_EXPORT = $(JCCML_EXPORT:.ml=.cmo)
- JCCMX_EXPORT = $(JCCML_EXPORT:.ml=.cmx)
--JCCMI_EXPORT = jc/jc_ast.cmi jc/jc_env.cmi $(JCCML_EXPORT:.ml=.cmi)
-+JCCMI_EXPORT = $(JCCML_EXPORT:.ml=.cmi)
-
- JCCMO = src/version.cmo \
- @ATPCMO@ $(JCCMO_EXPORT) \
-@@ -744,7 +746,8 @@
- mkdir -p $(LIBDIR)/why/why
- cp -f $(PRELUDE) $(LIBDIR)/why/why
- mkdir -p $(LIBDIR)/caduceus/why
--# ??? cp -f $(JCLIB) $(JCCMI_EXPORT) $(LIBDIR)
-+ mkdir -p $(LIBDIR)/ocaml/jessie
-+ cp -f $(JCLIB) $(JCLD) $(JCCMI_EXPORT) $(LIBDIR)/ocaml/jessie
- cp -f lib/why/caduceus.why $(LIBDIR)/caduceus/why
- cp -f lib/why/caduceus_arith.why $(LIBDIR)/caduceus/why
- mkdir -p $(LIBDIR)/caduceus/coq
diff --git a/sci-mathematics/why/files/why-2.19-makefile_sandbox.patch b/sci-mathematics/why/files/why-2.19-makefile_sandbox.patch
deleted file mode 100644
index 3ec92830a..000000000
--- a/sci-mathematics/why/files/why-2.19-makefile_sandbox.patch
+++ /dev/null
@@ -1,75 +0,0 @@
-diff -Naur why-2.19-orig/Makefile.in why-2.19-ptch/Makefile.in
---- why-2.19-orig/Makefile.in 2009-06-23 12:09:43.000000000 +0000
-+++ why-2.19-ptch/Makefile.in 2009-09-04 14:43:22.000000000 +0000
-@@ -777,9 +777,9 @@
- cp -f $(VO7) $(LIBDIR)/why/coq7
- install-coq-v8:
- if test -w $(COQLIB) ; then \
-- mkdir -p $(COQLIB)/user-contrib ; \
-- cp -f $(V8FILES) $(COQLIB)/user-contrib ; \
-- cp -f $(VO8) $(COQLIB)/user-contrib ; \
-+ mkdir -p $(DESTDIR)/$(COQLIB)/user-contrib ; \
-+ cp -f $(V8FILES) $(DESTDIR)/$(COQLIB)/user-contrib ; \
-+ cp -f $(VO8) $(DESTDIR)/$(COQLIB)/user-contrib ; \
- else \
- echo "Cannot copy to Coq standard library. Add $(LIBDIR)/why/coq to Coq include path." ;\
- mkdir -p $(LIBDIR)/why/coq ;\
-@@ -788,18 +788,18 @@
-
- install-pvs-no:
- install-pvs-yes: $(PVSFILES)
-- mkdir -p $(PVSLIB)/why
-- cp $(PVSFILES) $(PVSFILES:.pvs=.prf) $(PVSLIB)/why
-- cp lib/pvs/top.pvs lib/pvs/pvscontext.el $(PVSLIB)/why
-+ mkdir -p $(DESTDIR)/$(PVSLIB)/why
-+ cp $(PVSFILES) $(PVSFILES:.pvs=.prf) $(DESTDIR)/$(PVSLIB)/why
-+ cp lib/pvs/top.pvs lib/pvs/pvscontext.el $(DESTDIR)/$(PVSLIB)/why
- @echo "====== Compiling PVS theories, this may take some time ======"
-- (cd $(PVSLIB)/why ; @PVSC@ -batch -l pvscontext.el -q -v 2 > top.out)
-+ (cd $(DESTDIR)/$(PVSLIB)/why ; @PVSC@ -batch -l pvscontext.el -q -v 2 > top.out)
- @echo "====== Done compiling PVS theories ======"
-
- install-mizar-no:
- install-mizar-yes:
-- mkdir -p @MIZARLIB@/mml/dict
-- cp lib/mizar/why.miz @MIZARLIB@/mml
-- cp lib/mizar/dict/why.voc @MIZARLIB@/mml/dict
-+ mkdir -p $(DESTDIR)/@MIZARLIB@/mml/dict
-+ cp lib/mizar/why.miz $(DESTDIR)/@MIZARLIB@/mml
-+ cp lib/mizar/dict/why.voc $(DESTDIR)/@MIZARLIB@/mml/dict
-
- local-install: $(BINARY) $(WHYCONFIG) $(CADUCEUS) $(JESSIE) bin/gwhy.$(OCAMLBEST) byte bin/gwhy.byte
- cp $(BINARY) $$HOME/bin/why
-@@ -817,15 +817,15 @@
- # cp -f $(WHY2HTML) $$HOME/bin/$$OSTYPE/why2html
- # cp -f $(DP) $$HOME/bin/$$OSTYPE/dp
- # cp -f $(RVMERGE) $$HOME/bin/$$OSTYPE/rv_merge
--# # mkdir -p $(COQLIB)/contrib7/why
--# # cp -f $(VO7) $(VFILES) $(COQLIB)/contrib7/why
--# # mkdir -p $(COQLIB)/contrib/why
--# # cp -f $(VO8) $(VFILES) $(COQLIB)/contrib/why
--# mkdir -p $(PVSLIB)/why
--# cp $(PVSFILES) $(PVSLIB)/why
--# mkdir -p $(MIZFILES)/mml/dict
--# cp lib/mizar/why.miz $(MIZFILES)/mml
--# cp lib/mizar/dict/why.voc $(MIZFILES)/mml/dict
-+# # mkdir -p $(DESTDIR)/$(COQLIB)/contrib7/why
-+# # cp -f $(VO7) $(VFILES) $(DESTDIR)/$(COQLIB)/contrib7/why
-+# # mkdir -p $(DESTDIR)/$(COQLIB)/contrib/why
-+# # cp -f $(VO8) $(VFILES) $(DESTDIR)/$(COQLIB)/contrib/why
-+# mkdir -p $(DESTDIR)/$(PVSLIB)/why
-+# cp $(PVSFILES) $(DESTDIR)/$(PVSLIB)/why
-+# mkdir -p $(DESTDIR)/$(MIZFILES)/mml/dict
-+# cp lib/mizar/why.miz $(DESTDIR)/$(MIZFILES)/mml
-+# cp lib/mizar/dict/why.voc $(DESTDIR)/$(MIZFILES)/mml/dict
- # mkdir -p $$HOME/man/man1
- # cp -f doc/*.1 $$HOME/man/man1
-
-@@ -1119,7 +1119,6 @@
- rm -f $(GENERATED)
- make -C atp clean
- make -C doc clean
-- make -C examples-v7 clean
- make -C examples clean
-
- dist-clean:: clean
diff --git a/sci-mathematics/why/metadata.xml b/sci-mathematics/why/metadata.xml
new file mode 100644
index 000000000..8098c5667
--- /dev/null
+++ b/sci-mathematics/why/metadata.xml
@@ -0,0 +1,23 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+<pkgmetadata>
+ <herd>sci</herd>
+ <longdescription>
+ 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="jessie">?jessie?</flag>
+ <flag name="gtk">?gtk?</flag>
+ <flag name="pff">?pff?</flag>
+ </use>
+</pkgmetadata>
diff --git a/sci-mathematics/why/why-2.19.ebuild b/sci-mathematics/why/why-2.26.ebuild
index 46af70f51..a8c1ffac0 100644
--- a/sci-mathematics/why/why-2.19.ebuild
+++ b/sci-mathematics/why/why-2.26.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2009 Gentoo Foundation
+# Copyright 1999-2010 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Header: $
@@ -13,24 +13,22 @@ SRC_URI="http://why.lri.fr/download/${P}.tar.gz"
LICENSE="GPL-2"
SLOT="0"
KEYWORDS="~amd64 ~ppc ~sparc ~x86"
-IUSE="apron coq doc examples gappa gtk pff pvs"
+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.12 )
+ gtk? ( >=dev-ml/lablgtk-2.14 )
apron? ( sci-mathematics/apron )
coq? ( sci-mathematics/coq )
gappa? ( sci-mathematics/gappalib-coq )
pff? ( sci-mathematics/pff )
- pvs? ( sci-mathematics/pvs )"
+ jessie? ( >=sci-mathematics/frama-c-20100401 )"
RDEPEND="${DEPEND}"
src_prepare() {
- epatch "${FILESDIR}/${P}-makefile_sandbox.patch"
-
- mv jc/jc_ast.mli jc/jc_ast.ml
- mv jc/jc_env.mli jc/jc_env.ml
- epatch "${FILESDIR}/${P}-jessie_lib.patch"
+ 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 \
@@ -47,11 +45,11 @@ src_configure() {
}
src_compile(){
- emake DESTDIR="/" || die "emake failed"
+ emake -j1 DESTDIR="/" || die "emake failed"
}
src_install(){
- emake install DESTDIR="${D}" || die "emake install failed"
+ DESTDIR="${D}" emake install || die "emake install failed"
dodoc CHANGES COPYING README Version
doman doc/why.1