[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/files/
commit: 8a158de860dd20b8a4ac9f9b8adc6317ba8d738c Author: Alfredo Tupone gentoo org> AuthorDate: Mon Apr 3 06:20:30 2023 + Commit: Alfredo Tupone gentoo org> CommitDate: Mon Apr 3 06:21:06 2023 + URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=8a158de8 sci-mathematics/why3-for-spark: fix NOTPARALLEL Signed-off-by: Alfredo Tupone gentoo.org> sci-mathematics/why3-for-spark/files/why3-for-spark-2021-make.patch | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sci-mathematics/why3-for-spark/files/why3-for-spark-2021-make.patch b/sci-mathematics/why3-for-spark/files/why3-for-spark-2021-make.patch index 5eba27fd5d0e..fa23a1c32c5c 100644 --- a/sci-mathematics/why3-for-spark/files/why3-for-spark-2021-make.patch +++ b/sci-mathematics/why3-for-spark/files/why3-for-spark-2021-make.patch @@ -4,7 +4,7 @@ # # -+.NOTPARALLEL: notparallel ++.NOTPARALLEL: + VERBOSEMAKE ?= @enable_verbose_make@
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/files/, sci-mathematics/why3-for-spark/
commit: 8395f9bd24c6d239774bcc990eaaca63b9d77ef2 Author: Alfredo Tupone gentoo org> AuthorDate: Sun Apr 2 21:04:18 2023 + Commit: Alfredo Tupone gentoo org> CommitDate: Sun Apr 2 21:05:02 2023 + URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=8395f9bd sci-mathematics/why3-for-spark: disable shuffle Closes: https://bugs.gentoo.org/883167 Signed-off-by: Alfredo Tupone gentoo.org> .../why3-for-spark/files/why3-for-spark-2021-make.patch | 11 +++ sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild | 1 + 2 files changed, 12 insertions(+) diff --git a/sci-mathematics/why3-for-spark/files/why3-for-spark-2021-make.patch b/sci-mathematics/why3-for-spark/files/why3-for-spark-2021-make.patch new file mode 100644 index ..5eba27fd5d0e --- /dev/null +++ b/sci-mathematics/why3-for-spark/files/why3-for-spark-2021-make.patch @@ -0,0 +1,11 @@ +--- a/Makefile.in 2023-04-02 22:54:43.160504917 +0200 b/Makefile.in 2023-04-02 22:55:05.194152231 +0200 +@@ -9,6 +9,8 @@ + # # + + ++.NOTPARALLEL: notparallel ++ + VERBOSEMAKE ?= @enable_verbose_make@ + + ifeq ($(VERBOSEMAKE),yes) diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild index 10f8a95c8393..4204da3000b6 100644 --- a/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild +++ b/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild @@ -52,6 +52,7 @@ S="${WORKDIR}"/${MYP} PATCHES=( "${FILESDIR}"/${PN}-2020-gentoo.patch "${FILESDIR}"/${P}-flags.patch + "${FILESDIR}"/${P}-make.patch #Bug #883167 "${FILESDIR}"/${PN}-2020-bibtex.patch )
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/files/, sci-mathematics/why3-for-spark/
commit: aea65604ea143ed47ffbb54c9628113ec26908c9 Author: Alfredo Tupone gentoo org> AuthorDate: Sun Apr 2 14:22:42 2023 + Commit: Alfredo Tupone gentoo org> CommitDate: Sun Apr 2 14:22:57 2023 + URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=aea65604 sci-mathematics/why3-for-spark: drop 2020 Signed-off-by: Alfredo Tupone gentoo.org> sci-mathematics/why3-for-spark/Manifest| 1 - .../files/why3-for-spark-2020-flags.patch | 28 - .../why3-for-spark/why3-for-spark-2020.ebuild | 119 - 3 files changed, 148 deletions(-) diff --git a/sci-mathematics/why3-for-spark/Manifest b/sci-mathematics/why3-for-spark/Manifest index c3956f9e07e6..1653ff46cefc 100644 --- a/sci-mathematics/why3-for-spark/Manifest +++ b/sci-mathematics/why3-for-spark/Manifest @@ -1,2 +1 @@ -DIST 8bb5801e17b8b23453262da69c981c091959eec7?filename=why3-2020-20200429-199EF-src.tar.gz 9739066 BLAKE2B c7c11a92d4926f90be9ffa94d74e65ad78423953b53ee617565ccfcea4a5a60b251367b0712c30d170ab717d5868f7d95d62694f38c3d2f52805a28a6522ab8a SHA512 61cd5509957230ff81186d2507b9749b182cdc44698f6658337ce294d210742e57164d25d7c0eb3eb5ea0c53f5f46dea099e6a0769fadcb709a5a8557ed3cae3 DIST why3-2021-20210519-19ADF-src.tar.gz 10386938 BLAKE2B 93b6323c562126244f5cccef34088a521fe3dc1cec07c966e94472503ec8492707b20a641936449307f0439e711a82260d36679cbc69f53df8e7886a1d3673c3 SHA512 65e3c1430001962f2c7cce786f3e30f14b5295cff89c4087d95c1545e81743723319ba0309dbe15c4c46552110b25ff57addc3ee085dade02ea59a2273b127db diff --git a/sci-mathematics/why3-for-spark/files/why3-for-spark-2020-flags.patch b/sci-mathematics/why3-for-spark/files/why3-for-spark-2020-flags.patch deleted file mode 100644 index 2e5247ac3fa6.. --- a/sci-mathematics/why3-for-spark/files/why3-for-spark-2020-flags.patch +++ /dev/null @@ -1,28 +0,0 @@ a/Makefile.in 2020-06-12 21:03:33.375534124 +0200 -+++ b/Makefile.in 2020-06-12 21:03:48.623283408 +0200 -@@ -121,7 +121,7 @@ - - WARNINGS = A-4-9-41-44-45-50-52@5@8@48 - --FLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g $(INCLUDES) -+FLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g $(INCLUDES) -cclib "$(LDFLAGS)" -ccopt "$(CFLAGS)" - OFLAGS = $(FLAGS) - BFLAGS = $(FLAGS) - -@@ -664,13 +664,13 @@ - all: $(TOOLS) - - lib/why3server$(EXE): $(SERVER_O) -- $(CC) -Wall -o $@ $^ -+ $(CC) -Wall $(CFLAGS) -o $@ $^ $(LDFLAGS) - - lib/why3cpulimit$(EXE): $(CPULIM_O) -- $(CC) -Wall -o $@ $^ -+ $(CC) -Wall $(CFLAGS) -o $@ $^ $(LDFLAGS) - - %.o: %.c -- $(CC) -Wall -O -g -o $@ -c $< -+ $(CC) -Wall -O -g $(CFLAGS) -o $@ -c $< - - uninstall-bin:: - rm -f $(LIBDIR)/why3/why3server$(EXE) $(LIBDIR)/why3/why3cpulimit$(EXE) diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild deleted file mode 100644 index 201e90379c72.. --- a/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild +++ /dev/null @@ -1,119 +0,0 @@ -# Copyright 1999-2023 Gentoo Authors -# Distributed under the terms of the GNU General Public License v2 - -EAPI=7 - -inherit autotools - -MYP=why3-${PV}-20200429-199EF-src - -DESCRIPTION="Platform for deductive program verification" -HOMEPAGE="https://why3.lri.fr/"; -SRC_URI="https://community.download.adacore.com/v1/8bb5801e17b8b23453262da69c981c091959eec7?filename=${MYP}.tar.gz"; - -LICENSE="GPL-3" -SLOT="0" -KEYWORDS="amd64" -IUSE="doc emacs gtk html +ocamlopt zarith zip" -RESTRICT="strip" - -DEPEND=">=dev-lang/ocaml-4.09.0:=[ocamlopt=] - >=dev-ml/ocamlbuild-0.14.0 - dev-ml/menhir:= - =dev-ml/lablgtk-2.18.8:=[sourceview] ) - emacs? ( >=app-editors/emacs-23.1:* ) - html? ( dev-tex/hevea:= ) - zarith? ( dev-ml/zarith:= ) - zip? ( >=dev-ml/camlzip-1.07:= )" -RDEPEND="${DEPEND}" - -S="${WORKDIR}"/${MYP} - -PATCHES=( - "${FILESDIR}"/${P}-gentoo.patch - "${FILESDIR}"/${P}-flags.patch - "${FILESDIR}"/${P}-bibtex.patch -) - -QA_FLAGS_IGNORED=( - /usr/lib64/why3/commands/why3shell - /usr/lib64/why3/commands/why3extract - /usr/lib64/why3/commands/why3execute - /usr/lib64/why3/commands/why3prove - /usr/lib64/why3/commands/why3wc - /usr/lib64/why3/commands/why3doc - /usr/lib64/why3/commands/why3replay - /usr/lib64/why3/commands/why3webserver - /usr/lib64/why3/plugins/'.*'.cmxs - /usr/lib64/ocaml/why3/why3.cmxs - /usr/lib64/ocaml/why3/why3extract.cmxs - /usr/bin/why3 - /usr/bin/why3config - /usr/bin/why3session - /usr/bin/gnat_server - /usr/bin/gnatwhy3 - /usr/bin/why3realize -) - -REQUIRED_USE="html? ( doc )" - -src_prepare() { - find examples -name \*gz | xargs gunzip - default - eautoreconf -} - -src_configure() { - econf \ - --disable-pvs-libs \ - --disable-isabelle-l
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/files/, sci-mathematics/why3-for-spark/
commit: dd5f5eb5b4c7b6262816c4fcc5edee33abfd9261 Author: Alfredo Tupone gentoo org> AuthorDate: Sun Apr 2 12:48:09 2023 + Commit: Alfredo Tupone gentoo org> CommitDate: Sun Apr 2 12:48:09 2023 + URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=dd5f5eb5 sci-mathematics/why3-for-spark: drop 2019-r3 Signed-off-by: Alfredo Tupone gentoo.org> sci-mathematics/why3-for-spark/Manifest| 1 - .../files/why3-for-spark-2019-flags.patch | 28 - .../files/why3-for-spark-2019-gentoo.patch | 24 - .../why3-for-spark/why3-for-spark-2019-r3.ebuild | 117 - 4 files changed, 170 deletions(-) diff --git a/sci-mathematics/why3-for-spark/Manifest b/sci-mathematics/why3-for-spark/Manifest index afc57cb3d37d..c3956f9e07e6 100644 --- a/sci-mathematics/why3-for-spark/Manifest +++ b/sci-mathematics/why3-for-spark/Manifest @@ -1,3 +1,2 @@ DIST 8bb5801e17b8b23453262da69c981c091959eec7?filename=why3-2020-20200429-199EF-src.tar.gz 9739066 BLAKE2B c7c11a92d4926f90be9ffa94d74e65ad78423953b53ee617565ccfcea4a5a60b251367b0712c30d170ab717d5868f7d95d62694f38c3d2f52805a28a6522ab8a SHA512 61cd5509957230ff81186d2507b9749b182cdc44698f6658337ce294d210742e57164d25d7c0eb3eb5ea0c53f5f46dea099e6a0769fadcb709a5a8557ed3cae3 -DIST why3-2019-20190517-197BB-src.tar.gz 9439414 BLAKE2B 68072064e8ee9152528c90afc948047a1f4d58b960ac05b276761fdca5ba1204100c75f33db7bb0ea1a8a646b734e62892ed41bd875b954354f52b8f9d498d4a SHA512 9169a4ff9ee994a19f9f04b689d1b9c679f5340bcd631d7d49b4c55064f505bd5a6ca8149077e5d24d36f5365f0cab58587094e86f352a9105fc46f10c0746ba DIST why3-2021-20210519-19ADF-src.tar.gz 10386938 BLAKE2B 93b6323c562126244f5cccef34088a521fe3dc1cec07c966e94472503ec8492707b20a641936449307f0439e711a82260d36679cbc69f53df8e7886a1d3673c3 SHA512 65e3c1430001962f2c7cce786f3e30f14b5295cff89c4087d95c1545e81743723319ba0309dbe15c4c46552110b25ff57addc3ee085dade02ea59a2273b127db diff --git a/sci-mathematics/why3-for-spark/files/why3-for-spark-2019-flags.patch b/sci-mathematics/why3-for-spark/files/why3-for-spark-2019-flags.patch deleted file mode 100644 index b562bb02cd84.. --- a/sci-mathematics/why3-for-spark/files/why3-for-spark-2019-flags.patch +++ /dev/null @@ -1,28 +0,0 @@ a/Makefile.in 2020-06-12 21:03:33.375534124 +0200 -+++ b/Makefile.in 2020-06-12 21:03:48.623283408 +0200 -@@ -96,7 +96,7 @@ - - WARNINGS = A-4-9-41-44-45-50-52@5@8@48 - --OFLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g $(INCLUDES) -+OFLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g $(INCLUDES) -cclib "$(LDFLAGS)" -ccopt "$(CFLAGS)" - BFLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g $(INCLUDES) - - OLINKFLAGS = -linkall $(EXTCMXA) -@@ -664,13 +664,13 @@ - all: $(TOOLS) - - lib/why3server$(EXE): $(SERVER_O) -- $(CC) -Wall -o $@ $^ -+ $(CC) -Wall $(CFLAGS) -o $@ $^ $(LDFLAGS) - - lib/why3cpulimit$(EXE): $(CPULIM_O) -- $(CC) -Wall -o $@ $^ -+ $(CC) -Wall $(CFLAGS) -o $@ $^ $(LDFLAGS) - - %.o: %.c -- $(CC) -Wall -O -g -o $@ -c $< -+ $(CC) -Wall -O -g $(CFLAGS) -o $@ -c $< - - uninstall-bin:: - rm -f $(LIBDIR)/why3/why3server$(EXE) $(LIBDIR)/why3/why3cpulimit$(EXE) diff --git a/sci-mathematics/why3-for-spark/files/why3-for-spark-2019-gentoo.patch b/sci-mathematics/why3-for-spark/files/why3-for-spark-2019-gentoo.patch deleted file mode 100644 index 2dab12ddfbd3.. --- a/sci-mathematics/why3-for-spark/files/why3-for-spark-2019-gentoo.patch +++ /dev/null @@ -1,24 +0,0 @@ a/src/gnat/gnat_config.ml 2017-10-18 09:07:03.118919785 +0200 -+++ b/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 a/Makefile.in 2020-05-27 21:19:08.736241502 +0200 -+++ b/Makefile.in 2020-05-27 21:19:14.042156954 +0200 -@@ -50,7 +50,6 @@ - OCAMLINSTALLLIB = $(DESTDIR)@OCAMLINSTALLLIB@ - OCAMLBEST = @OCAMLBEST@ - OCAMLVERSION = @OCAMLVERSION@ --CC= gcc - COQC = @COQC@ - COQDEP= @COQDEP@ - FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@ diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r3.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r3.ebuild deleted file mode 100644 index 3747497af8a1.. --- a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r3.ebuild +++ /dev/null @@ -1,117 +0,0 @@ -# Copyright 1999-2023 Gentoo Authors -# Distributed under the terms of the GNU General Public License v2 - -EAPI=7 - -MYP=why3-${PV}-20190517-197BB-src - -DESCRIPTION="Platform for deductive program verification" -HOMEPAGE="https://why3.lri.fr/"; -SRC_URI="http://mirrors.cdn.adacore.com/art/5cdf91
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/files/
commit: d5e5640e5928b4e17ed5bdea1d1e0a999d36b0b9 Author: Michael Mair-Keimberger levelnine at> AuthorDate: Thu Feb 10 11:42:42 2022 + Commit: Alfredo Tupone gentoo org> CommitDate: Thu Feb 10 12:35:41 2022 + URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=d5e5640e sci-mathematics/why3-for-spark: remove unused patch Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Michael Mair-Keimberger gmail.com> Closes: https://github.com/gentoo/gentoo/pull/24147 Signed-off-by: Alfredo Tupone gentoo.org> .../files/why3-for-spark-2018-gentoo.patch | 25 -- 1 file changed, 25 deletions(-) diff --git a/sci-mathematics/why3-for-spark/files/why3-for-spark-2018-gentoo.patch b/sci-mathematics/why3-for-spark/files/why3-for-spark-2018-gentoo.patch deleted file mode 100644 index 9d7165cbed78.. --- a/sci-mathematics/why3-for-spark/files/why3-for-spark-2018-gentoo.patch +++ /dev/null @@ -1,25 +0,0 @@ why3-for-spark-gpl-2017-src/src/gnat/gnat_config.ml.old2017-10-18 09:07:03.118919785 +0200 -+++ why3-for-spark-gpl-2017-src/src/gnat/gnat_config.ml2017-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 why3-for-spark-gpl-2017-src/src/coq-tactic/why3tac.ml4.old 2017-10-26 22:25:55.289094778 +0200 -+++ why3-for-spark-gpl-2017-src/src/coq-tactic/why3tac.ml4 2017-10-26 22:26:10.719807270 +0200 -@@ -1352,7 +1352,7 @@ - let limit = - { Call_provers.empty_limit with Call_provers.limit_time = timelimit } in - let call = Driver.prove_task ~command ~limit drv !task in --wait_on_call call -+wait_on_call (ServerCall call) - with - | NotFO -> - if debug then Printexc.print_backtrace stderr; flush stderr;
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/files/, sci-mathematics/why3-for-spark/
commit: 5047348a53133478c69ec7994c0dc81390e03dd3 Author: Alfredo Tupone gentoo org> AuthorDate: Tue Jun 29 19:38:40 2021 + Commit: Alfredo Tupone gentoo org> CommitDate: Tue Jun 29 19:38:40 2021 + URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=5047348a sci-mathematics/why3-for-spark: enabled hypothesis-selection Package-Manager: Portage-3.0.20, Repoman-3.0.2 Signed-off-by: Alfredo Tupone gentoo.org> .../why3-for-spark/files/why3-for-spark-2021-flags.patch | 9 + sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild| 5 +++-- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/sci-mathematics/why3-for-spark/files/why3-for-spark-2021-flags.patch b/sci-mathematics/why3-for-spark/files/why3-for-spark-2021-flags.patch index 7f6dfd0f446..e12ec73318b 100644 --- a/sci-mathematics/why3-for-spark/files/why3-for-spark-2021-flags.patch +++ b/sci-mathematics/why3-for-spark/files/why3-for-spark-2021-flags.patch @@ -9,6 +9,15 @@ OFLAGS = $(FLAGS) BFLAGS = $(FLAGS) +@@ -572,7 +572,7 @@ + lib/plugins/hypothesis_selection.cmo: EXTOBJS += graph.cmo + ifeq (@enable_ocamlfind@,yes) + lib/plugins/hypothesis_selection.cmxs: FLAGS += -package ocamlgraph -dontlink "$(EXTPKGS)" -linkpkg +-lib/plugins/hypothesis_selection.cmo: FLAGS += -package ocamlgraph graph.cmo ++lib/plugins/hypothesis_selection.cmo: FLAGS += -package ocamlgraph + endif + endif + @@ -778,13 +778,13 @@ all: $(TOOLS) diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild index 06a68247055..b851107a4c4 100644 --- a/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild +++ b/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild @@ -16,7 +16,7 @@ SRC_URI="${ADAMIRROR}/${ID}?filename=${MYP}.tar.gz -> ${MYP}.tar.gz" LICENSE="GPL-3" SLOT="0" KEYWORDS="~amd64" -IUSE="coq doc emacs gtk html +ocamlopt zarith zip" +IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt zarith zip" RESTRICT="strip" DEPEND="dev-lang/ocaml:0/4.11[ocamlopt?] @@ -35,6 +35,7 @@ DEPEND="dev-lang/ocaml:0/4.11[ocamlopt?] gtk? ( dev-ml/lablgtk:=[sourceview] ) emacs? ( app-editors/emacs:* ) html? ( dev-tex/hevea:= ) + hypothesis-selection? ( dev-ml/ocamlgraph:= ) zarith? ( dev-ml/zarith:= ) zip? ( dev-ml/camlzip:= )" RDEPEND="${DEPEND}" @@ -80,12 +81,12 @@ src_configure() { --disable-pvs-libs \ --disable-isabelle-libs \ --enable-verbose-make \ - --disable-hypothesis-selection \ $(use_enable coq coq-libs) \ $(use_enable doc) \ $(use_enable emacs emacs-compilation) \ $(use_enable gtk ide) \ $(use_enable html html-pdf) \ + $(use_enable hypothesis-selection) \ $(use_enable ocamlopt native-code) \ $(use_enable zarith) \ $(use_enable zip)
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/files/, sci-mathematics/why3-for-spark/
commit: ea162b812cb64c737eba031c8fcb8bbef7a2084a Author: Alfredo Tupone gentoo org> AuthorDate: Fri Jun 12 21:24:23 2020 + Commit: Alfredo Tupone gentoo org> CommitDate: Fri Jun 12 21:24:23 2020 + URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ea162b81 sci-mathematics/why3-for-spark: fix flags and compression Closes: https://bugs.gentoo.org/728032 Closes: https://bugs.gentoo.org/728050 Package-Manager: Portage-2.3.99, Repoman-2.3.22 Signed-off-by: Alfredo Tupone gentoo.org> .../files/why3-for-spark-2019-flags.patch | 28 + .../why3-for-spark/why3-for-spark-2019-r2.ebuild | 116 + 2 files changed, 144 insertions(+) diff --git a/sci-mathematics/why3-for-spark/files/why3-for-spark-2019-flags.patch b/sci-mathematics/why3-for-spark/files/why3-for-spark-2019-flags.patch new file mode 100644 index 000..b562bb02cd8 --- /dev/null +++ b/sci-mathematics/why3-for-spark/files/why3-for-spark-2019-flags.patch @@ -0,0 +1,28 @@ +--- a/Makefile.in 2020-06-12 21:03:33.375534124 +0200 b/Makefile.in 2020-06-12 21:03:48.623283408 +0200 +@@ -96,7 +96,7 @@ + + WARNINGS = A-4-9-41-44-45-50-52@5@8@48 + +-OFLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g $(INCLUDES) ++OFLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g $(INCLUDES) -cclib "$(LDFLAGS)" -ccopt "$(CFLAGS)" + BFLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g $(INCLUDES) + + OLINKFLAGS = -linkall $(EXTCMXA) +@@ -664,13 +664,13 @@ + all: $(TOOLS) + + lib/why3server$(EXE): $(SERVER_O) +- $(CC) -Wall -o $@ $^ ++ $(CC) -Wall $(CFLAGS) -o $@ $^ $(LDFLAGS) + + lib/why3cpulimit$(EXE): $(CPULIM_O) +- $(CC) -Wall -o $@ $^ ++ $(CC) -Wall $(CFLAGS) -o $@ $^ $(LDFLAGS) + + %.o: %.c +- $(CC) -Wall -O -g -o $@ -c $< ++ $(CC) -Wall -O -g $(CFLAGS) -o $@ -c $< + + uninstall-bin:: + rm -f $(LIBDIR)/why3/why3server$(EXE) $(LIBDIR)/why3/why3cpulimit$(EXE) diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild new file mode 100644 index 000..e27b1427040 --- /dev/null +++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild @@ -0,0 +1,116 @@ +# Copyright 1999-2020 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=7 + +MYP=why3-${PV}-20190517-197BB-src + +DESCRIPTION="Platform for deductive program verification" +HOMEPAGE="http://why3.lri.fr/"; +SRC_URI="http://mirrors.cdn.adacore.com/art/5cdf915d31e87a8f1c967d54 + -> ${MYP}.tar.gz" + +LICENSE="GPL-3" +SLOT="0" +KEYWORDS="~amd64" +IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt zarith zip" +RESTRICT=strip + +DEPEND=">=dev-lang/ocaml-4.09.0[ocamlopt?] + >=dev-ml/ocamlbuild-0.14.0 + dev-ml/menhir + dev-ml/num + coq? ( >=sci-mathematics/coq-8.9.1 ) + doc? ( dev-tex/rubber ) + gtk? ( >=dev-ml/lablgtk-2.18.8[sourceview] ) + emacs? ( >=app-editors/emacs-23.1:* ) + html? ( dev-tex/hevea ) + hypothesis-selection? ( dev-ml/ocamlgraph ) + zarith? ( dev-ml/zarith ) + zip? ( >=dev-ml/camlzip-1.07 )" +RDEPEND="${DEPEND}" + +S="${WORKDIR}"/${MYP} + +PATCHES=( + "${FILESDIR}"/${P}-gentoo.patch + "${FILESDIR}"/${P}-flags.patch +) + +QA_FLAGS_IGNORED=( + /usr/lib64/why3/commands/why3shell + /usr/lib64/why3/commands/why3extract + /usr/lib64/why3/commands/why3execute + /usr/lib64/why3/commands/why3prove + /usr/lib64/why3/commands/why3wc + /usr/lib64/why3/commands/why3doc + /usr/lib64/why3/commands/why3replay + /usr/lib64/why3/commands/why3webserver + /usr/lib64/why3/plugins/python.cmxs + /usr/lib64/why3/plugins/hypothesis_selection.cmxs + /usr/lib64/why3/plugins/tptp.cmxs + /usr/lib64/why3/plugins/dimacs.cmxs + /usr/lib64/why3/plugins/genequlin.cmxs + /usr/lib64/ocaml/why3/why3.cmxs + /usr/lib64/ocaml/why3/why3extract.cmxs + /usr/bin/why3 + /usr/bin/why3config + /usr/bin/why3session + /usr/bin/gnat_server + /usr/bin/gnatwhy3 + /usr/bin/why3realize +) + +REQUIRED_USE="html? ( doc )" + +src_prepare() { + find examples -name \*gz | xargs gunzip + default +} + +src_configure() { + econf \ + --disable-pvs-libs \ + --disable-isabelle-libs \ + --enable-verbose-make \ + $(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 ocamlopt native-code) \ + $(use_enable zarith) \ + $(use_enable zip) +} + +src_compile() { + emake -j1 + if use ocamlopt; then +
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/files/
commit: 80264f6226c82b6ae16c92c98cd7835e71a53680 Author: Alfredo Tupone gentoo org> AuthorDate: Wed May 27 19:24:39 2020 + Commit: Alfredo Tupone gentoo org> CommitDate: Wed May 27 19:24:39 2020 + URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=80264f62 sci-mathematics/why3-for-spark: use CC Closes: https://bugs.gentoo.org/725598 Package-Manager: Portage-2.3.99, Repoman-2.3.22 Signed-off-by: Alfredo Tupone gentoo.org> .../why3-for-spark/files/why3-for-spark-2019-gentoo.patch | 10 ++ 1 file changed, 10 insertions(+) diff --git a/sci-mathematics/why3-for-spark/files/why3-for-spark-2019-gentoo.patch b/sci-mathematics/why3-for-spark/files/why3-for-spark-2019-gentoo.patch index f83a6256672..2dab12ddfbd 100644 --- a/sci-mathematics/why3-for-spark/files/why3-for-spark-2019-gentoo.patch +++ b/sci-mathematics/why3-for-spark/files/why3-for-spark-2019-gentoo.patch @@ -12,3 +12,13 @@ let rec file_concat l = match l with +--- a/Makefile.in 2020-05-27 21:19:08.736241502 +0200 b/Makefile.in 2020-05-27 21:19:14.042156954 +0200 +@@ -50,7 +50,6 @@ + OCAMLINSTALLLIB = $(DESTDIR)@OCAMLINSTALLLIB@ + OCAMLBEST = @OCAMLBEST@ + OCAMLVERSION = @OCAMLVERSION@ +-CC= gcc + COQC = @COQC@ + COQDEP= @COQDEP@ + FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/files/
commit: 1075f5c716518cebdef31cb080bceb6c2bb4f71b Author: Tupone Alfredo gentoo org> AuthorDate: Fri Mar 29 08:25:45 2019 + Commit: Alfredo Tupone gentoo org> CommitDate: Fri Mar 29 08:25:45 2019 + URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=1075f5c7 sci-mathematics/why3-for-spark: remove unused patch Closes: Closes: https://github.com/gentoo/gentoo/pull/11528 Signed-off-by: Alfredo Tupone gentoo.org> Package-Manager: Portage-2.3.62, Repoman-2.3.11 .../files/why3-for-spark-2017-gentoo.patch | 40 -- 1 file changed, 40 deletions(-) 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 deleted file mode 100644 index 225d081ca7f..000 --- a/sci-mathematics/why3-for-spark/files/why3-for-spark-2017-gentoo.patch +++ /dev/null @@ -1,40 +0,0 @@ why3-for-spark-gpl-2017-src/src/gnat/gnat_config.ml.old2017-10-18 09:07:03.118919785 +0200 -+++ why3-for-spark-gpl-2017-src/src/gnat/gnat_config.ml2017-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 why3-for-spark-gpl-2017-src/src/coq-tactic/why3tac.ml4.old 2017-10-26 22:25:55.289094778 +0200 -+++ why3-for-spark-gpl-2017-src/src/coq-tactic/why3tac.ml4 2017-10-26 22:26:10.719807270 +0200 -@@ -1352,7 +1352,7 @@ - let limit = - { Call_provers.empty_limit with Call_provers.limit_time = timelimit } in - let call = Driver.prove_task ~command ~limit drv !task in --wait_on_call call -+wait_on_call (ServerCall call) - with - | NotFO -> - if debug then Printexc.print_backtrace stderr; flush stderr; -@@ -1399,14 +1399,8 @@ - | StepLimitExceeded -> error "Step Limit Exceeded" - | HighFailure -> error ("Prover failure\n" ^ res.pr_output ^ "\n") - --IFDEF COQ84 THEN -- --ELSE -- - let why3tac ?timelimit s = Proofview.V82.tactic (why3tac ?timelimit s) - --END -- - end - - TACTIC EXTEND Why3
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/files/, sci-mathematics/why3-for-spark/
commit: f7767454e6ac2a9eb63c5fc48e3fe8d1fe0ff1dd Author: Tupone Alfredo gentoo org> AuthorDate: Wed Nov 1 20:28:03 2017 + Commit: Alfredo Tupone gentoo org> CommitDate: Wed Nov 1 20:30:29 2017 + URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=f7767454 sci-mathematics/why3-for-spark: Enable coq tactics Package-Manager: Portage-2.3.8, Repoman-2.3.3 .../files/why3-for-spark-2017-gentoo.patch | 26 ++ .../why3-for-spark/why3-for-spark-2017.ebuild | 2 +- 2 files changed, 27 insertions(+), 1 deletion(-) 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 index 502f394afa2..225d081ca7f 100644 --- 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 @@ -12,3 +12,29 @@ let rec file_concat l = match l with +--- why3-for-spark-gpl-2017-src/src/coq-tactic/why3tac.ml4.old 2017-10-26 22:25:55.289094778 +0200 why3-for-spark-gpl-2017-src/src/coq-tactic/why3tac.ml4 2017-10-26 22:26:10.719807270 +0200 +@@ -1352,7 +1352,7 @@ + let limit = + { Call_provers.empty_limit with Call_provers.limit_time = timelimit } in + let call = Driver.prove_task ~command ~limit drv !task in +-wait_on_call call ++wait_on_call (ServerCall call) + with + | NotFO -> + if debug then Printexc.print_backtrace stderr; flush stderr; +@@ -1399,14 +1399,8 @@ + | StepLimitExceeded -> error "Step Limit Exceeded" + | HighFailure -> error ("Prover failure\n" ^ res.pr_output ^ "\n") + +-IFDEF COQ84 THEN +- +-ELSE +- + let why3tac ?timelimit s = Proofview.V82.tactic (why3tac ?timelimit s) + +-END +- + end + + TACTIC EXTEND Why3 diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild index c143320a492..3fd44106514 100644 --- a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild +++ b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild @@ -46,10 +46,10 @@ src_prepare() { src_configure() { econf \ - --disable-coq-tactic \ --disable-pvs-libs \ --disable-isabelle-libs \ $(use_enable coq coq-libs) \ + $(use_enable coq coq-tactic) \ $(use_enable doc) \ $(use_enable emacs emacs-compilation) \ $(use_enable gtk ide) \
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/files/, sci-mathematics/why3-for-spark/
commit: eb5feee2d87d486910df3c8b3cb505f1eb0e47c3 Author: Tupone Alfredo gentoo org> AuthorDate: Thu Oct 19 19:43:39 2017 + Commit: Alfredo Tupone gentoo org> CommitDate: Thu Oct 19 19:43:39 2017 + 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 000..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 8f02f6c1744cd7c565117732935791b1ae7996a94314c40a66d125eae8a81f2257314246c94fd29d3cd16abcff6a50a152a1191a4aae39a2c8a8d7c3b9e1 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 000..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.old2017-10-18 09:07:03.118919785 +0200 why3-for-spark-gpl-2017-src/src/gnat/gnat_config.ml2017-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 000..6dbb21558b6 --- /dev/null +++ b/sci-mathematics/why3-for-spark/metadata.xml @@ -0,0 +1,27 @@ + +http://www.gentoo.org/dtd/metadata.dtd";> + + + sci-mathemat...@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/coq support + Build HTML documentation + Enable hypothesis selection + Enable profiling + Use dev-ml/zarith + + 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 000..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) \ + $(