diff options
| -rw-r--r-- | sci-mathematics/why/ChangeLog | 12 | ||||
| -rw-r--r-- | sci-mathematics/why/Manifest | 8 | ||||
| -rw-r--r-- | sci-mathematics/why/files/why-2.19-jessie_lib.patch | 43 | ||||
| -rw-r--r-- | sci-mathematics/why/files/why-2.19-makefile_sandbox.patch | 75 | ||||
| -rw-r--r-- | sci-mathematics/why/metadata.xml | 23 | ||||
| -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 |