aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndrew Ammerlaan <andrewammerlaan@gentoo.org>2021-12-13 11:57:12 +0100
committerAndrew Ammerlaan <andrewammerlaan@gentoo.org>2021-12-13 11:57:56 +0100
commit05665ef52991dd10e4c912a13b34656b3397fefc (patch)
treee9b2250e2440aea61b6d204262d4fec6f28902cb
parentsci-libs/geom: remove masked package (diff)
downloadsci-05665ef52991dd10e4c912a13b34656b3397fefc.tar.gz
sci-05665ef52991dd10e4c912a13b34656b3397fefc.tar.bz2
sci-05665ef52991dd10e4c912a13b34656b3397fefc.zip
sci-mathematics/why3: remove: ::guru version moved to ::gentoo
Signed-off-by: Andrew Ammerlaan <andrewammerlaan@gentoo.org>
-rw-r--r--sci-mathematics/why3/Manifest1
-rw-r--r--sci-mathematics/why3/metadata.xml24
-rw-r--r--sci-mathematics/why3/why3-1.3.3.ebuild63
3 files changed, 0 insertions, 88 deletions
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
deleted file mode 100644
index 20a390e40..000000000
--- a/sci-mathematics/why3/Manifest
+++ /dev/null
@@ -1 +0,0 @@
-DIST why3-1.3.3.tar.gz 5807572 BLAKE2B b1a04e78010f841e217b9a81c096cadfa0cddabadbe81ef55c310a104668feb1e46cd50576a965a58c74658903d6d08f9fd348bd2064a79ac3b176548927bcbe SHA512 a2dc95691cea29bbd20843a05add3985f777085086b654b53566ecdb752ba892366da703e232c85d5e0237d0e59564527aed55f6ccae9118d49e5f2cf93a53ce
diff --git a/sci-mathematics/why3/metadata.xml b/sci-mathematics/why3/metadata.xml
deleted file mode 100644
index 5f92771c1..000000000
--- a/sci-mathematics/why3/metadata.xml
+++ /dev/null
@@ -1,24 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
-<pkgmetadata>
- <maintainer type="project">
- <email>sci-mathematics@gentoo.org</email>
- <name>Gentoo Mathematics Project</name>
- </maintainer>
- <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>
- <use>
- <flag name="float">Add <pkg>sci-mathematics/flocq</pkg> support</flag>
- <flag name="frama-c">Enable Frama-C plugin</flag>
- </use>
-</pkgmetadata>
diff --git a/sci-mathematics/why3/why3-1.3.3.ebuild b/sci-mathematics/why3/why3-1.3.3.ebuild
deleted file mode 100644
index 62706c32f..000000000
--- a/sci-mathematics/why3/why3-1.3.3.ebuild
+++ /dev/null
@@ -1,63 +0,0 @@
-# Copyright 1999-2021 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=7
-
-PYTHON_COMPAT=( python3_{7,8,9} )
-DOCS_BUILDER="sphinx"
-DOCS_DIR="doc"
-DOCS_DEPEND="
- dev-python/sphinxcontrib-bibtex
- dev-python/graphviz
-"
-
-inherit python-any-r1 docs
-
-DESCRIPTION="Why3 is a platform for deductive program verification"
-HOMEPAGE="http://why3.lri.fr/"
-SRC_URI="https://gforge.inria.fr/frs/download.php/file/38367/${P}.tar.gz"
-
-LICENSE="LGPL-2"
-SLOT="0"
-KEYWORDS="~amd64"
-
-IUSE="float frama-c examples"
-
-DEPEND="
- >=dev-lang/ocaml-3.12.1
- dev-ml/zarith
- dev-ml/menhir
- dev-ml/num
- sci-mathematics/coq
- frama-c? ( >=sci-mathematics/frama-c-22 )
- float? ( sci-mathematics/flocq )
-"
-RDEPEND="${DEPEND}"
-
-src_prepare() {
- default
- mv doc/why.1 doc/why3.1 || die
- sed -i configure.in -e "s/\"pvs\"/\"sri-pvs\"/g" || die
- sed -i configure -e "s/\"pvs\"/\"sri-pvs\"/g" || die
- # fix dev-ml/num path
- sed -i configure.in -e "s/nums.cma/num.cma/g" -e "s/num.cmi/core\/num.cmi/g" || die
- sed -i configure -e "s/nums.cma/num.cma/g" -e "s/num.cmi/core\/num.cmi/g" || die
- sed -i Makefile.in -e "s:DESTDIR =::g" \
- -e "s:\$(RUBBER) --warn all --pdf manual.tex:makeindex manual.tex; \$(RUBBER) --warn all --pdf manual.tex; cd ..:g" || die
- # add autodoc to sphinx
- sed -i -e "/^extensions = \[/a \ \ \ \ \'sphinx.ext.autodoc\'," doc/conf.py || die
-}
-
-src_configure() {
- econf $(use_enable frama-c)
-}
-
-src_compile() {
- docs_compile
- default
-}
-
-src_install(){
- default
- use examples && dodoc -r examples
-}