public inbox for gentoo-commits@lists.gentoo.org
 help / color / mirror / Atom feed
From: "Andrew Ammerlaan" <andrewammerlaan@gentoo.org>
To: gentoo-commits@lists.gentoo.org
Subject: [gentoo-commits] proj/sci:master commit in: sci-mathematics/why3/
Date: Mon, 13 Dec 2021 10:57:58 +0000 (UTC)	[thread overview]
Message-ID: <1639393076.05665ef52991dd10e4c912a13b34656b3397fefc.andrewammerlaan@gentoo> (raw)

commit:     05665ef52991dd10e4c912a13b34656b3397fefc
Author:     Andrew Ammerlaan <andrewammerlaan <AT> gentoo <DOT> org>
AuthorDate: Mon Dec 13 10:57:12 2021 +0000
Commit:     Andrew Ammerlaan <andrewammerlaan <AT> gentoo <DOT> org>
CommitDate: Mon Dec 13 10:57:56 2021 +0000
URL:        https://gitweb.gentoo.org/proj/sci.git/commit/?id=05665ef5

sci-mathematics/why3: remove: ::guru version moved to ::gentoo

Signed-off-by: Andrew Ammerlaan <andrewammerlaan <AT> gentoo.org>

 sci-mathematics/why3/metadata.xml      | 24 -------------
 sci-mathematics/why3/why3-1.3.3.ebuild | 63 ----------------------------------
 2 files changed, 87 deletions(-)

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
-}


             reply	other threads:[~2021-12-13 10:58 UTC|newest]

Thread overview: 9+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2021-12-13 10:57 Andrew Ammerlaan [this message]
  -- strict thread matches above, loose matches on Subject: below --
2021-03-04 13:53 [gentoo-commits] proj/sci:master commit in: sci-mathematics/why3/ Andrew Ammerlaan
2021-03-04 13:07 Andrew Ammerlaan
2021-03-04 11:53 Andrew Ammerlaan
2021-03-04 11:53 Andrew Ammerlaan
2016-06-15 14:57 Marius Brehler
2015-02-08 21:07 Christoph Junghans
2014-09-16  4:07 Christoph Junghans
2014-09-02 21:19 Jauhien Piatlicki

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=1639393076.05665ef52991dd10e4c912a13b34656b3397fefc.andrewammerlaan@gentoo \
    --to=andrewammerlaan@gentoo.org \
    --cc=gentoo-commits@lists.gentoo.org \
    --cc=gentoo-dev@lists.gentoo.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body. 
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox