From: "Alfredo Tupone" <tupone@gentoo.org>
To: gentoo-commits@lists.gentoo.org
Subject: [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/files/, sci-mathematics/why3-for-spark/
Date: Thu, 19 Oct 2017 19:44:03 +0000 (UTC) [thread overview]
Message-ID: <1508442219.eb5feee2d87d486910df3c8b3cb505f1eb0e47c3.tupone@gentoo> (raw)
commit: eb5feee2d87d486910df3c8b3cb505f1eb0e47c3
Author: Tupone Alfredo <tupone <AT> gentoo <DOT> org>
AuthorDate: Thu Oct 19 19:43:39 2017 +0000
Commit: Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Thu Oct 19 19:43:39 2017 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=eb5feee2
sci-mathematics/why3-for-spark: Adding why3 for spark
Package-Manager: Portage-2.3.8, Repoman-2.3.3
sci-mathematics/why3-for-spark/Manifest | 1 +
.../files/why3-for-spark-2017-gentoo.patch | 14 ++++
sci-mathematics/why3-for-spark/metadata.xml | 27 ++++++++
.../why3-for-spark/why3-for-spark-2017.ebuild | 74 ++++++++++++++++++++++
4 files changed, 116 insertions(+)
diff --git a/sci-mathematics/why3-for-spark/Manifest b/sci-mathematics/why3-for-spark/Manifest
new file mode 100644
index 00000000000..4aba92a50d6
--- /dev/null
+++ b/sci-mathematics/why3-for-spark/Manifest
@@ -0,0 +1 @@
+DIST why3-for-spark-gpl-2017-src.tar.gz 9248235 SHA256 7e7aee3912421847c416bc1f066ac342e811601c29d7b69e98e789a59a724d8e SHA512 8f444402f6c1744cd7c565117732935791b1ae7996a94314c40a66d125eae8a81f2257314246c94fd29d3cd16abcff6a50a152a1191a4aae39a2c8a8d7c3b9e1 WHIRLPOOL 256648567b3a220f762c7e30d0f90265fd10af21b66c3607b9072e81444b0a33dc971126232e11f3edc64eac2598fbd3ad428d063f2c9db8d247be2abe5be904
diff --git a/sci-mathematics/why3-for-spark/files/why3-for-spark-2017-gentoo.patch b/sci-mathematics/why3-for-spark/files/why3-for-spark-2017-gentoo.patch
new file mode 100644
index 00000000000..502f394afa2
--- /dev/null
+++ b/sci-mathematics/why3-for-spark/files/why3-for-spark-2017-gentoo.patch
@@ -0,0 +1,14 @@
+--- why3-for-spark-gpl-2017-src/src/gnat/gnat_config.ml.old 2017-10-18 09:07:03.118919785 +0200
++++ why3-for-spark-gpl-2017-src/src/gnat/gnat_config.ml 2017-10-18 09:07:45.198216939 +0200
+@@ -12,10 +12,7 @@
+ | Limit_Check of Gnat_expl.check
+ | Limit_Line of Gnat_loc.loc
+
+-let spark_prefix =
+- (Filename.dirname
+- (Filename.dirname (Filename.dirname
+- (Filename.dirname Sys.executable_name))))
++let spark_prefix = "/usr"
+
+ let rec file_concat l =
+ match l with
diff --git a/sci-mathematics/why3-for-spark/metadata.xml b/sci-mathematics/why3-for-spark/metadata.xml
new file mode 100644
index 00000000000..6dbb21558b6
--- /dev/null
+++ b/sci-mathematics/why3-for-spark/metadata.xml
@@ -0,0 +1,27 @@
+<?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="coq">Add <pkg>sci-mathematics/coq</pkg> support</flag>
+ <flag name="html">Build HTML documentation</flag>
+ <flag name="hypothesis-selection">Enable hypothesis selection</flag>
+ <flag name="profiling">Enable profiling</flag>
+ <flag name="zarith">Use <pkg>dev-ml/zarith</pkg></flag>
+</use>
+</pkgmetadata>
diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
new file mode 100644
index 00000000000..b69b22e506f
--- /dev/null
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
@@ -0,0 +1,74 @@
+# Copyright 1999-2017 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=6
+
+inherit autotools
+
+MYP=${PN}-gpl-${PV}-src
+
+DESCRIPTION="Platform for deductive program verification"
+HOMEPAGE="http://why3.lri.fr/"
+SRC_URI="https//mirrors.cdn.adacore.com/art/591c45e2c7a447af2deed055
+ -> ${MYP}.tar.gz"
+
+LICENSE="GPL-3"
+SLOT="0"
+KEYWORDS="~amd64"
+IUSE="coq doc emacs gtk html hypothesis-selection profiling zarith"
+
+DEPEND=">=dev-lang/ocaml-4.02.3
+ dev-ml/menhir
+ coq? ( sci-mathematics/coq )
+ doc? ( dev-tex/rubber )
+ gtk? ( dev-ml/lablgtk[sourceview] )
+ emacs? ( app-editors/emacs:* )
+ html? ( dev-tex/hevea )
+ hypothesis-selection? ( dev-ml/ocamlgraph )
+ zarith? ( dev-ml/zarith )"
+RDEPEND="${DEPEND}"
+
+S="${WORKDIR}"/${MYP}
+
+PATCHES=( "${FILESDIR}"/${P}-gentoo.patch )
+
+REQUIRED_USE="html? ( doc )"
+
+src_prepare() {
+ mv configure.{in,ac} || die
+ sed -i \
+ -e "s:configure.in:configure.ac:g" \
+ Makefile.in
+ default
+ eautoreconf
+}
+
+src_configure() {
+ econf \
+ --disable-coq-tactic \
+ --disable-pvs-libs \
+ --disable-isabelle-libs \
+ --disable-zip \
+ $(use_enable coq coq-libs) \
+ $(use_enable doc) \
+ $(use_enable emacs emacs-compilation) \
+ $(use_enable gtk ide) \
+ $(use_enable html html-doc) \
+ $(use_enable hypothesis-selection) \
+ $(use_enable profiling) \
+ $(use_enable zarith)
+}
+
+src_compile() {
+ default
+ use doc && emake doc
+}
+
+src_install() {
+ default
+ emake DESTDIR="${D}" install_spark2014_dev
+ if use doc; then
+ dodoc doc/manual.pdf
+ use html && dodoc -r doc/html
+ fi
+}
next reply other threads:[~2017-10-19 19:44 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-10-19 19:44 Alfredo Tupone [this message]
-- strict thread matches above, loose matches on Subject: below --
2017-11-01 20:31 [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/files/, sci-mathematics/why3-for-spark/ Alfredo Tupone
2020-06-12 21:24 Alfredo Tupone
2021-06-29 19:38 Alfredo Tupone
2023-04-02 12:48 Alfredo Tupone
2023-04-02 14:24 Alfredo Tupone
2023-04-02 21:05 Alfredo Tupone
2025-02-07 20:56 Alfredo Tupone
2025-02-11 17:09 Alfredo Tupone
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=1508442219.eb5feee2d87d486910df3c8b3cb505f1eb0e47c3.tupone@gentoo \
--to=tupone@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