From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from lists.gentoo.org (pigeon.gentoo.org [208.92.234.80]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits)) (No client certificate requested) by finch.gentoo.org (Postfix) with ESMTPS id 3DA6E158086 for ; Mon, 13 Dec 2021 10:58:08 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id 201E02BC00D; Mon, 13 Dec 2021 10:58:06 +0000 (UTC) Received: from smtp.gentoo.org (woodpecker.gentoo.org [140.211.166.183]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (No client certificate requested) by pigeon.gentoo.org (Postfix) with ESMTPS id 78D582BC00D for ; Mon, 13 Dec 2021 10:58:03 +0000 (UTC) Received: from oystercatcher.gentoo.org (unknown [IPv6:2a01:4f8:202:4333:225:90ff:fed9:fc84]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (No client certificate requested) by smtp.gentoo.org (Postfix) with ESMTPS id 2606F343238 for ; Mon, 13 Dec 2021 10:58:00 +0000 (UTC) Received: from localhost.localdomain (localhost [IPv6:::1]) by oystercatcher.gentoo.org (Postfix) with ESMTP id 73CF61BF for ; Mon, 13 Dec 2021 10:57:58 +0000 (UTC) From: "Andrew Ammerlaan" To: gentoo-commits@lists.gentoo.org Content-Transfer-Encoding: 8bit Content-type: text/plain; charset=UTF-8 Reply-To: gentoo-dev@lists.gentoo.org, "Andrew Ammerlaan" Message-ID: <1639393076.05665ef52991dd10e4c912a13b34656b3397fefc.andrewammerlaan@gentoo> Subject: [gentoo-commits] proj/sci:master commit in: sci-mathematics/why3/ X-VCS-Repository: proj/sci X-VCS-Files: sci-mathematics/why3/metadata.xml sci-mathematics/why3/why3-1.3.3.ebuild X-VCS-Directories: sci-mathematics/why3/ X-VCS-Committer: andrewammerlaan X-VCS-Committer-Name: Andrew Ammerlaan X-VCS-Revision: 05665ef52991dd10e4c912a13b34656b3397fefc X-VCS-Branch: master Date: Mon, 13 Dec 2021 10:57:58 +0000 (UTC) Precedence: bulk List-Post: List-Help: List-Unsubscribe: List-Subscribe: List-Id: Gentoo Linux mail X-BeenThere: gentoo-commits@lists.gentoo.org X-Auto-Response-Suppress: DR, RN, NRN, OOF, AutoReply X-Archives-Salt: c30f5657-4a89-4e0b-9a5e-c74fcbfe55c7 X-Archives-Hash: 47d125775e62c03b951784a2d430eb0c commit: 05665ef52991dd10e4c912a13b34656b3397fefc Author: Andrew Ammerlaan gentoo org> AuthorDate: Mon Dec 13 10:57:12 2021 +0000 Commit: Andrew Ammerlaan gentoo 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 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 @@ - - - - - sci-mathematics@gentoo.org - Gentoo Mathematics Project - - -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. - - - Add sci-mathematics/flocq support - Enable Frama-C plugin - - 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 -}