From 28fa4c56bba04fe751e45cff07af6e2285bca741 Mon Sep 17 00:00:00 2001 From: Maciej Barć Date: Sat, 23 Jul 2022 00:23:52 +0200 Subject: sci-mathematics/why3: remove unnecessary seq dependency MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Maciej Barć --- sci-mathematics/why3/why3-1.4.0-r2.ebuild | 98 ---------------------------- sci-mathematics/why3/why3-1.4.0-r3.ebuild | 98 ++++++++++++++++++++++++++++ sci-mathematics/why3/why3-1.4.1-r1.ebuild | 98 ++++++++++++++++++++++++++++ sci-mathematics/why3/why3-1.4.1.ebuild | 98 ---------------------------- sci-mathematics/why3/why3-1.5.0-r1.ebuild | 103 ++++++++++++++++++++++++++++++ sci-mathematics/why3/why3-1.5.0.ebuild | 103 ------------------------------ 6 files changed, 299 insertions(+), 299 deletions(-) delete mode 100644 sci-mathematics/why3/why3-1.4.0-r2.ebuild create mode 100644 sci-mathematics/why3/why3-1.4.0-r3.ebuild create mode 100644 sci-mathematics/why3/why3-1.4.1-r1.ebuild delete mode 100644 sci-mathematics/why3/why3-1.4.1.ebuild create mode 100644 sci-mathematics/why3/why3-1.5.0-r1.ebuild delete mode 100644 sci-mathematics/why3/why3-1.5.0.ebuild diff --git a/sci-mathematics/why3/why3-1.4.0-r2.ebuild b/sci-mathematics/why3/why3-1.4.0-r2.ebuild deleted file mode 100644 index efe23fa3bbde..000000000000 --- a/sci-mathematics/why3/why3-1.4.0-r2.ebuild +++ /dev/null @@ -1,98 +0,0 @@ -# Copyright 1999-2022 Gentoo Authors -# Distributed under the terms of the GNU General Public License v2 - -EAPI=7 - -inherit autotools findlib - -DESCRIPTION="Platform for deductive program verification" -HOMEPAGE="http://why3.lri.fr/" -SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz" - -LICENSE="LGPL-2" -SLOT="0/${PV}" -KEYWORDS="~amd64" -IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip" - -RDEPEND=" - !sci-mathematics/why3-for-spark - >=dev-lang/ocaml-4.05.0:=[ocamlopt?] - >=dev-ml/menhir-20170418:= - dev-ml/num:= - coq? ( >=sci-mathematics/coq-8.6 ) - emacs? ( app-editors/emacs:* ) - gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] ) - re? ( dev-ml/re:= dev-ml/seq:= ) - sexp? ( - dev-ml/ppx_deriving:=[ocamlopt?] - dev-ml/ppx_sexp_conv:=[ocamlopt?] - dev-ml/sexplib:=[ocamlopt?] - ) - zarith? ( dev-ml/zarith:= ) - zip? ( dev-ml/camlzip:= ) -" -DEPEND="${RDEPEND}" -BDEPEND=" - doc? ( - dev-python/sphinx - dev-python/sphinxcontrib-bibtex - media-gfx/graphviz - dev-texlive/texlive-latex - dev-texlive/texlive-fontsrecommended - dev-texlive/texlive-latexextra - ) -" - -DOCS=( CHANGES.md README.md ) - -src_prepare() { - mv configure.in configure.ac || die - sed -i 's/configure\.in/configure.ac/g' Makefile.in || die - sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \ - -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \ - -e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \ - -i Makefile.in || die - - eautoreconf - default -} - -src_configure() { - local myconf=( - --disable-hypothesis-selection - --disable-pvs-libs - --disable-isabelle-libs - --disable-frama-c - --disable-infer - --disable-web-ide - $(use_enable coq coq-libs) - $(use_enable doc) - $(use_enable emacs emacs-compilation) - $(use_enable gtk ide) - $(use_enable ocamlopt native-code) - $(use_enable re) - $(use_enable sexp pp-sexp) - $(use_enable zarith) - $(use_enable zip) - ) - econf "${myconf[@]}" -} - -src_compile() { - emake - emake plugins - use doc && emake doc -} - -src_install(){ - findlib_src_preinst - emake install install-lib DESTDIR="${ED}" - - einstalldocs - docompress -x /usr/share/doc/${PF}/examples - dodoc -r examples - if use doc; then - dodoc doc/latex/manual.pdf - dodoc -r doc/html - fi -} diff --git a/sci-mathematics/why3/why3-1.4.0-r3.ebuild b/sci-mathematics/why3/why3-1.4.0-r3.ebuild new file mode 100644 index 000000000000..e57cc66c0237 --- /dev/null +++ b/sci-mathematics/why3/why3-1.4.0-r3.ebuild @@ -0,0 +1,98 @@ +# Copyright 1999-2022 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=7 + +inherit autotools findlib + +DESCRIPTION="Platform for deductive program verification" +HOMEPAGE="http://why3.lri.fr/" +SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz" + +LICENSE="LGPL-2" +SLOT="0/${PV}" +KEYWORDS="~amd64" +IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip" + +RDEPEND=" + !sci-mathematics/why3-for-spark + >=dev-lang/ocaml-4.05.0:=[ocamlopt?] + >=dev-ml/menhir-20170418:= + dev-ml/num:= + coq? ( >=sci-mathematics/coq-8.6 ) + emacs? ( app-editors/emacs:* ) + gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] ) + re? ( dev-ml/re:= ) + sexp? ( + dev-ml/ppx_deriving:=[ocamlopt?] + dev-ml/ppx_sexp_conv:=[ocamlopt?] + dev-ml/sexplib:=[ocamlopt?] + ) + zarith? ( dev-ml/zarith:= ) + zip? ( dev-ml/camlzip:= ) +" +DEPEND="${RDEPEND}" +BDEPEND=" + doc? ( + dev-python/sphinx + dev-python/sphinxcontrib-bibtex + media-gfx/graphviz + dev-texlive/texlive-latex + dev-texlive/texlive-fontsrecommended + dev-texlive/texlive-latexextra + ) +" + +DOCS=( CHANGES.md README.md ) + +src_prepare() { + mv configure.in configure.ac || die + sed -i 's/configure\.in/configure.ac/g' Makefile.in || die + sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \ + -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \ + -e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \ + -i Makefile.in || die + + eautoreconf + default +} + +src_configure() { + local myconf=( + --disable-hypothesis-selection + --disable-pvs-libs + --disable-isabelle-libs + --disable-frama-c + --disable-infer + --disable-web-ide + $(use_enable coq coq-libs) + $(use_enable doc) + $(use_enable emacs emacs-compilation) + $(use_enable gtk ide) + $(use_enable ocamlopt native-code) + $(use_enable re) + $(use_enable sexp pp-sexp) + $(use_enable zarith) + $(use_enable zip) + ) + econf "${myconf[@]}" +} + +src_compile() { + emake + emake plugins + use doc && emake doc +} + +src_install(){ + findlib_src_preinst + emake install install-lib DESTDIR="${ED}" + + einstalldocs + docompress -x /usr/share/doc/${PF}/examples + dodoc -r examples + if use doc; then + dodoc doc/latex/manual.pdf + dodoc -r doc/html + fi +} diff --git a/sci-mathematics/why3/why3-1.4.1-r1.ebuild b/sci-mathematics/why3/why3-1.4.1-r1.ebuild new file mode 100644 index 000000000000..e57cc66c0237 --- /dev/null +++ b/sci-mathematics/why3/why3-1.4.1-r1.ebuild @@ -0,0 +1,98 @@ +# Copyright 1999-2022 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=7 + +inherit autotools findlib + +DESCRIPTION="Platform for deductive program verification" +HOMEPAGE="http://why3.lri.fr/" +SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz" + +LICENSE="LGPL-2" +SLOT="0/${PV}" +KEYWORDS="~amd64" +IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip" + +RDEPEND=" + !sci-mathematics/why3-for-spark + >=dev-lang/ocaml-4.05.0:=[ocamlopt?] + >=dev-ml/menhir-20170418:= + dev-ml/num:= + coq? ( >=sci-mathematics/coq-8.6 ) + emacs? ( app-editors/emacs:* ) + gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] ) + re? ( dev-ml/re:= ) + sexp? ( + dev-ml/ppx_deriving:=[ocamlopt?] + dev-ml/ppx_sexp_conv:=[ocamlopt?] + dev-ml/sexplib:=[ocamlopt?] + ) + zarith? ( dev-ml/zarith:= ) + zip? ( dev-ml/camlzip:= ) +" +DEPEND="${RDEPEND}" +BDEPEND=" + doc? ( + dev-python/sphinx + dev-python/sphinxcontrib-bibtex + media-gfx/graphviz + dev-texlive/texlive-latex + dev-texlive/texlive-fontsrecommended + dev-texlive/texlive-latexextra + ) +" + +DOCS=( CHANGES.md README.md ) + +src_prepare() { + mv configure.in configure.ac || die + sed -i 's/configure\.in/configure.ac/g' Makefile.in || die + sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \ + -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \ + -e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \ + -i Makefile.in || die + + eautoreconf + default +} + +src_configure() { + local myconf=( + --disable-hypothesis-selection + --disable-pvs-libs + --disable-isabelle-libs + --disable-frama-c + --disable-infer + --disable-web-ide + $(use_enable coq coq-libs) + $(use_enable doc) + $(use_enable emacs emacs-compilation) + $(use_enable gtk ide) + $(use_enable ocamlopt native-code) + $(use_enable re) + $(use_enable sexp pp-sexp) + $(use_enable zarith) + $(use_enable zip) + ) + econf "${myconf[@]}" +} + +src_compile() { + emake + emake plugins + use doc && emake doc +} + +src_install(){ + findlib_src_preinst + emake install install-lib DESTDIR="${ED}" + + einstalldocs + docompress -x /usr/share/doc/${PF}/examples + dodoc -r examples + if use doc; then + dodoc doc/latex/manual.pdf + dodoc -r doc/html + fi +} diff --git a/sci-mathematics/why3/why3-1.4.1.ebuild b/sci-mathematics/why3/why3-1.4.1.ebuild deleted file mode 100644 index efe23fa3bbde..000000000000 --- a/sci-mathematics/why3/why3-1.4.1.ebuild +++ /dev/null @@ -1,98 +0,0 @@ -# Copyright 1999-2022 Gentoo Authors -# Distributed under the terms of the GNU General Public License v2 - -EAPI=7 - -inherit autotools findlib - -DESCRIPTION="Platform for deductive program verification" -HOMEPAGE="http://why3.lri.fr/" -SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz" - -LICENSE="LGPL-2" -SLOT="0/${PV}" -KEYWORDS="~amd64" -IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip" - -RDEPEND=" - !sci-mathematics/why3-for-spark - >=dev-lang/ocaml-4.05.0:=[ocamlopt?] - >=dev-ml/menhir-20170418:= - dev-ml/num:= - coq? ( >=sci-mathematics/coq-8.6 ) - emacs? ( app-editors/emacs:* ) - gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] ) - re? ( dev-ml/re:= dev-ml/seq:= ) - sexp? ( - dev-ml/ppx_deriving:=[ocamlopt?] - dev-ml/ppx_sexp_conv:=[ocamlopt?] - dev-ml/sexplib:=[ocamlopt?] - ) - zarith? ( dev-ml/zarith:= ) - zip? ( dev-ml/camlzip:= ) -" -DEPEND="${RDEPEND}" -BDEPEND=" - doc? ( - dev-python/sphinx - dev-python/sphinxcontrib-bibtex - media-gfx/graphviz - dev-texlive/texlive-latex - dev-texlive/texlive-fontsrecommended - dev-texlive/texlive-latexextra - ) -" - -DOCS=( CHANGES.md README.md ) - -src_prepare() { - mv configure.in configure.ac || die - sed -i 's/configure\.in/configure.ac/g' Makefile.in || die - sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \ - -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \ - -e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \ - -i Makefile.in || die - - eautoreconf - default -} - -src_configure() { - local myconf=( - --disable-hypothesis-selection - --disable-pvs-libs - --disable-isabelle-libs - --disable-frama-c - --disable-infer - --disable-web-ide - $(use_enable coq coq-libs) - $(use_enable doc) - $(use_enable emacs emacs-compilation) - $(use_enable gtk ide) - $(use_enable ocamlopt native-code) - $(use_enable re) - $(use_enable sexp pp-sexp) - $(use_enable zarith) - $(use_enable zip) - ) - econf "${myconf[@]}" -} - -src_compile() { - emake - emake plugins - use doc && emake doc -} - -src_install(){ - findlib_src_preinst - emake install install-lib DESTDIR="${ED}" - - einstalldocs - docompress -x /usr/share/doc/${PF}/examples - dodoc -r examples - if use doc; then - dodoc doc/latex/manual.pdf - dodoc -r doc/html - fi -} diff --git a/sci-mathematics/why3/why3-1.5.0-r1.ebuild b/sci-mathematics/why3/why3-1.5.0-r1.ebuild new file mode 100644 index 000000000000..5f542a4b9e57 --- /dev/null +++ b/sci-mathematics/why3/why3-1.5.0-r1.ebuild @@ -0,0 +1,103 @@ +# Copyright 1999-2022 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=7 + +inherit autotools findlib + +DESCRIPTION="Platform for deductive program verification" +HOMEPAGE="http://why3.lri.fr/" +SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz" + +LICENSE="LGPL-2" +SLOT="0/${PV}" +KEYWORDS="~amd64" +IUSE="coq doc emacs gtk +ocamlopt re sexp stackify +zarith zip" + +RDEPEND=" + !sci-mathematics/why3-for-spark + >=dev-lang/ocaml-4.05.0:=[ocamlopt?] + >=dev-ml/menhir-20170418:= + dev-ml/num:= + coq? ( >=sci-mathematics/coq-8.7 ) + emacs? ( app-editors/emacs:* ) + gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] ) + re? ( dev-ml/re:= ) + sexp? ( + dev-ml/ppx_deriving:=[ocamlopt?] + dev-ml/ppx_sexp_conv:=[ocamlopt?] + dev-ml/sexplib:=[ocamlopt?] + ) + stackify? ( dev-ml/ocamlgraph:=[ocamlopt?] ) + zarith? ( dev-ml/zarith:= ) + zip? ( dev-ml/camlzip:= ) +" +DEPEND="${RDEPEND}" +BDEPEND=" + doc? ( + dev-python/sphinx + dev-python/sphinxcontrib-bibtex + media-gfx/graphviz + dev-texlive/texlive-latex + dev-texlive/texlive-fontsrecommended + dev-texlive/texlive-latexextra + ) +" + +DOCS=( CHANGES.md README.md ) + +src_prepare() { + mv configure.in configure.ac || die + sed -i 's/configure\.in/configure.ac/g' Makefile.in || die + sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \ + -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \ + -e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \ + -i Makefile.in || die + + # remove QA warning about duplicated compressed file: + rm examples/mlcfg/basic/why3shapes.gz || die + + eautoreconf + default +} + +src_configure() { + local myconf=( + --disable-hypothesis-selection + --disable-pvs-libs + --disable-isabelle-libs + --disable-frama-c + --disable-infer + --disable-web-ide + $(use_enable coq coq-libs) + $(use_enable doc) + $(use_enable emacs emacs-compilation) + $(use_enable gtk ide) + $(use_enable ocamlopt native-code) + $(use_enable re) + $(use_enable sexp pp-sexp) + $(use_enable stackify) + $(use_enable zarith) + $(use_enable zip) + ) + econf "${myconf[@]}" +} + +src_compile() { + emake + emake plugins + use doc && emake doc +} + +src_install(){ + findlib_src_preinst + emake install install-lib DESTDIR="${ED}" + + einstalldocs + docompress -x /usr/share/doc/${PF}/examples + dodoc -r examples + if use doc; then + dodoc doc/latex/manual.pdf + dodoc -r doc/html + fi +} diff --git a/sci-mathematics/why3/why3-1.5.0.ebuild b/sci-mathematics/why3/why3-1.5.0.ebuild deleted file mode 100644 index 9c250c09c3d0..000000000000 --- a/sci-mathematics/why3/why3-1.5.0.ebuild +++ /dev/null @@ -1,103 +0,0 @@ -# Copyright 1999-2022 Gentoo Authors -# Distributed under the terms of the GNU General Public License v2 - -EAPI=7 - -inherit autotools findlib - -DESCRIPTION="Platform for deductive program verification" -HOMEPAGE="http://why3.lri.fr/" -SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz" - -LICENSE="LGPL-2" -SLOT="0/${PV}" -KEYWORDS="~amd64" -IUSE="coq doc emacs gtk +ocamlopt re sexp stackify +zarith zip" - -RDEPEND=" - !sci-mathematics/why3-for-spark - >=dev-lang/ocaml-4.05.0:=[ocamlopt?] - >=dev-ml/menhir-20170418:= - dev-ml/num:= - coq? ( >=sci-mathematics/coq-8.7 ) - emacs? ( app-editors/emacs:* ) - gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] ) - re? ( dev-ml/re:= dev-ml/seq:= ) - sexp? ( - dev-ml/ppx_deriving:=[ocamlopt?] - dev-ml/ppx_sexp_conv:=[ocamlopt?] - dev-ml/sexplib:=[ocamlopt?] - ) - stackify? ( dev-ml/ocamlgraph:=[ocamlopt?] ) - zarith? ( dev-ml/zarith:= ) - zip? ( dev-ml/camlzip:= ) -" -DEPEND="${RDEPEND}" -BDEPEND=" - doc? ( - dev-python/sphinx - dev-python/sphinxcontrib-bibtex - media-gfx/graphviz - dev-texlive/texlive-latex - dev-texlive/texlive-fontsrecommended - dev-texlive/texlive-latexextra - ) -" - -DOCS=( CHANGES.md README.md ) - -src_prepare() { - mv configure.in configure.ac || die - sed -i 's/configure\.in/configure.ac/g' Makefile.in || die - sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \ - -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \ - -e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \ - -i Makefile.in || die - - # remove QA warning about duplicated compressed file: - rm examples/mlcfg/basic/why3shapes.gz || die - - eautoreconf - default -} - -src_configure() { - local myconf=( - --disable-hypothesis-selection - --disable-pvs-libs - --disable-isabelle-libs - --disable-frama-c - --disable-infer - --disable-web-ide - $(use_enable coq coq-libs) - $(use_enable doc) - $(use_enable emacs emacs-compilation) - $(use_enable gtk ide) - $(use_enable ocamlopt native-code) - $(use_enable re) - $(use_enable sexp pp-sexp) - $(use_enable stackify) - $(use_enable zarith) - $(use_enable zip) - ) - econf "${myconf[@]}" -} - -src_compile() { - emake - emake plugins - use doc && emake doc -} - -src_install(){ - findlib_src_preinst - emake install install-lib DESTDIR="${ED}" - - einstalldocs - docompress -x /usr/share/doc/${PF}/examples - dodoc -r examples - if use doc; then - dodoc doc/latex/manual.pdf - dodoc -r doc/html - fi -} -- cgit v1.2.3-65-gdbad