commit: 2fff060ebb4023f54b11fe044c1f9ea517a2ba06
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sun Aug 13 12:22:31 2023 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sun Aug 13 19:26:08 2023 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=2fff060e
sci-mathematics/proverif: new package; add 2.04
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/proverif/Manifest | 1 +
.../proverif/files/50proverif-gentoo.el | 13 +++++
sci-mathematics/proverif/metadata.xml | 33 ++++++++++++
sci-mathematics/proverif/proverif-2.04.ebuild | 63 ++++++++++++++++++++++
sci-mathematics/proverif/proverif-9999.ebuild | 63 ++++++++++++++++++++++
5 files changed, 173 insertions(+)
diff --git a/sci-mathematics/proverif/Manifest
b/sci-mathematics/proverif/Manifest
new file mode 100644
index 000000000000..7c7ae0993907
--- /dev/null
+++ b/sci-mathematics/proverif/Manifest
@@ -0,0 +1 @@
+DIST proverif-v2.04.tar.bz2 61001112 BLAKE2B
03364d315bfa3d6cc8dfb68819be6b92301f554cf7ae4db0c4b9d8190a7d7576b79295dd536bf1356e12679028c100e6040d8c4e4299cf137c15114caf0216d2
SHA512
dbfafa62f4df72044b05563e10219b034ad49dd972598bf72eba616f2a88ff1cb85c3ee7bb9235050d0f35dbde750bffddbc93897b9ca2101dc6d153d3ea5575
diff --git a/sci-mathematics/proverif/files/50proverif-gentoo.el
b/sci-mathematics/proverif/files/50proverif-gentoo.el
new file mode 100644
index 000000000000..2e2da4d3b3bf
--- /dev/null
+++ b/sci-mathematics/proverif/files/50proverif-gentoo.el
@@ -0,0 +1,13 @@
+(add-to-list 'load-path "@SITELISP@")
+(autoload 'proverif-horn-mode "proverif"
+ "Major mode for editing ProVerif code." t)
+(autoload 'proverif-horntype-mode "proverif"
+ "Major mode for editing ProVerif code." t)
+(autoload 'proverif-pi-mode "proverif"
+ "Major mode for editing ProVerif code." t)
+(autoload 'proverif-pv-mode "proverif"
+ "Major mode for editing ProVerif code." t)
+(add-to-list 'auto-mode-alist '("\\.horn$" . proverif-horn-mode))
+(add-to-list 'auto-mode-alist '("\\.horntype$" . proverif-horntype-mode))
+(add-to-list 'auto-mode-alist '("\\.pi$" . proverif-pi-mode))
+(add-to-list 'auto-mode-alist '("\\.pv[l]?$" . proverif-pv-mode))
diff --git a/sci-mathematics/proverif/metadata.xml
b/sci-mathematics/proverif/metadata.xml
new file mode 100644
index 000000000000..e388e8201c2b
--- /dev/null
+++ b/sci-mathematics/proverif/metadata.xml
@@ -0,0 +1,33 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd";>
+
+<pkgmetadata>
+ <maintainer type="project">
+ <email>[email protected]</email>
+ <name>ML</name>
+ </maintainer>
+ <maintainer type="project">
+ <email>[email protected]</email>
+ <name>Gentoo Mathematics Project</name>
+ </maintainer>
+ <longdescription>
+ ProVerif is an automatic cryptographic protocol verifier, in the formal
+ model (so called Dolev-Yao model). This protocol verifier is based on a
+ representation of the protocol by Horn clauses. Its main features are: 1)
+ It can handle many different cryptographic primitives, including shared-
+ and public-key cryptography (encryption and signatures), hash functions,
+ and Diffie-Hellman key agreements, specified both as rewrite rules or as
+ equations. 2) It can handle an unbounded number of sessions of the protocol
+ (even in parallel) and an unbounded message space. This result has been
+ obtained thanks to some well-chosen approximations. This means that the
+ verifier can give false attacks, but if it claims that the protocol
+ satisfies some property, then the property is actually satisfied. The
+ considered resolution algorithm terminates on a large class of protocols
+ (the so-called "tagged" protocols). When the tool cannot prove a property,
+ it tries to reconstruct an attack, that is, an execution trace of the
+ protocol that falsifies the desired property.
+ </longdescription>
+ <upstream>
+ <bugs-to>https://gitlab.inria.fr/bblanche/proverif/-/issues/</bugs-to>
+ </upstream>
+</pkgmetadata>
diff --git a/sci-mathematics/proverif/proverif-2.04.ebuild
b/sci-mathematics/proverif/proverif-2.04.ebuild
new file mode 100644
index 000000000000..248a70edb9d2
--- /dev/null
+++ b/sci-mathematics/proverif/proverif-2.04.ebuild
@@ -0,0 +1,63 @@
+# Copyright 1999-2023 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+inherit edo elisp-common findlib
+
+DESCRIPTION="Cryptographic protocol verifier in the formal model"
+HOMEPAGE="https://bblanche.gitlabpages.inria.fr/proverif/
+ https://gitlab.inria.fr/bblanche/proverif/";
+
+if [[ ${PV} == *9999* ]] ; then
+ inherit git-r3
+ EGIT_REPO_URI="https://gitlab.inria.fr/bblanche/${PN}.git";
+ S="${WORKDIR}/${P}/${PN}"
+else
+
SRC_URI="https://gitlab.inria.fr/bblanche/${PN}/-/archive/v${PV}/${PN}-v${PV}.tar.bz2";
+ KEYWORDS="~amd64 ~x86"
+ S="${WORKDIR}/${PN}-v${PV}/${PN}"
+fi
+
+LICENSE="GPL-2+"
+SLOT="0"
+IUSE="emacs"
+
+RDEPEND="
+ emacs? ( >=app-editors/emacs-25:* )
+"
+BDEPEND="
+ ${RDEPEND}
+"
+
+DOCS=( CHANGES README docs/dev docs/manual )
+SITEFILE="50${PN}-gentoo.el"
+
+src_compile() {
+ edob sh ./build -nointeract
+
+ if use emacs ; then
+ cd "${S}/emacs" || die
+
+ elisp-compile *.el
+ fi
+}
+
+src_test() {
+ edob sh ./test
+}
+
+src_install() {
+ findlib_src_preinst
+
+ exeinto /usr/bin
+ doexe proverif
+ doexe proveriftotex
+
+ if use emacs ; then
+ elisp-install "${PN}" "${S}/emacs"/*.el{,c}
+ elisp-site-file-install "${FILESDIR}/${SITEFILE}"
+ fi
+
+ einstalldocs
+}
diff --git a/sci-mathematics/proverif/proverif-9999.ebuild
b/sci-mathematics/proverif/proverif-9999.ebuild
new file mode 100644
index 000000000000..248a70edb9d2
--- /dev/null
+++ b/sci-mathematics/proverif/proverif-9999.ebuild
@@ -0,0 +1,63 @@
+# Copyright 1999-2023 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+inherit edo elisp-common findlib
+
+DESCRIPTION="Cryptographic protocol verifier in the formal model"
+HOMEPAGE="https://bblanche.gitlabpages.inria.fr/proverif/
+ https://gitlab.inria.fr/bblanche/proverif/";
+
+if [[ ${PV} == *9999* ]] ; then
+ inherit git-r3
+ EGIT_REPO_URI="https://gitlab.inria.fr/bblanche/${PN}.git";
+ S="${WORKDIR}/${P}/${PN}"
+else
+
SRC_URI="https://gitlab.inria.fr/bblanche/${PN}/-/archive/v${PV}/${PN}-v${PV}.tar.bz2";
+ KEYWORDS="~amd64 ~x86"
+ S="${WORKDIR}/${PN}-v${PV}/${PN}"
+fi
+
+LICENSE="GPL-2+"
+SLOT="0"
+IUSE="emacs"
+
+RDEPEND="
+ emacs? ( >=app-editors/emacs-25:* )
+"
+BDEPEND="
+ ${RDEPEND}
+"
+
+DOCS=( CHANGES README docs/dev docs/manual )
+SITEFILE="50${PN}-gentoo.el"
+
+src_compile() {
+ edob sh ./build -nointeract
+
+ if use emacs ; then
+ cd "${S}/emacs" || die
+
+ elisp-compile *.el
+ fi
+}
+
+src_test() {
+ edob sh ./test
+}
+
+src_install() {
+ findlib_src_preinst
+
+ exeinto /usr/bin
+ doexe proverif
+ doexe proveriftotex
+
+ if use emacs ; then
+ elisp-install "${PN}" "${S}/emacs"/*.el{,c}
+ elisp-site-file-install "${FILESDIR}/${SITEFILE}"
+ fi
+
+ einstalldocs
+}
