Arch Linux User Repository

"ocamlfind: Package `lablgtk2' not found" when a local ocamlfind along all $(opam env) stuff is in $PATH.

Thanks for the patch. I've just updated the package.

@maxammann quick hint: the bug is now resolved and your proverif_interact is also included in the patch.

Hi I've made a patch to update this package to 2.02pl1.

Please also consider adding me as a comaintainer. Thanks!

From 312974725cffa8cd22e33c67e1b20e3a9da2b24d Mon Sep 17 00:00:00 2001
From: DuckSoft <realducksoft@gmail.com>
Date: Sat, 10 Apr 2021 17:40:32 +0800
Subject: [PATCH] updpkg: 2.02pl1

---
 .SRCINFO | 10 ++++------
 PKGBUILD | 29 +++++++++++++++++++++--------
 2 files changed, 25 insertions(+), 14 deletions(-)

diff --git a/.SRCINFO b/.SRCINFO
index 4cfe732..8c8b2fe 100644
--- a/.SRCINFO
+++ b/.SRCINFO
@@ -1,8 +1,6 @@
-# Generated by mksrcinfo v8
-# Tue May 12 10:05:08 UTC 2020
 pkgbase = proverif
    pkgdesc = Cryptographic protocol verifier in the formal model
-   pkgver = 2.01
+   pkgver = 2.02pl1
    pkgrel = 1
    url = http://prosecco.gforge.inria.fr/personal/bblanche/proverif/
    arch = i686
@@ -13,9 +11,9 @@ pkgbase = proverif
    makedepends = lablgtk2
    depends = ocaml
    optdepends = graphviz: for displaying graphs of found attacks
-   source = http://prosecco.gforge.inria.fr/personal/bblanche/proverif/proverif2.01.tar.gz
-   sha1sums = b55a942a25f462013e575924baa0706b6b9c69ad
-   sha256sums = b1bf1496c5aebfa3c0f311317ca99626435faa5d08a6a49402ff1c1606299707
+   source = http://prosecco.gforge.inria.fr/personal/bblanche/proverif/proverif2.02pl1.tar.gz
+   sha1sums = d5421ac236a03a6c432417bf1b066d81cbc6b551
+   sha256sums = 5d4aa21eb05b9fe11d1fe448259b7dbda7adca1cd15c09f0acee3508fa75bfca

 pkgname = proverif

diff --git a/PKGBUILD b/PKGBUILD
index ff9d00e..ee078b0 100644
--- a/PKGBUILD
+++ b/PKGBUILD
@@ -1,6 +1,7 @@
 # Maintainer: Matej Grabovsky <matej.grabovsky at gmail>
+# Contributor: DuckSoft <realducksoft at gmail dot com>
 pkgname=proverif
-pkgver=2.01
+pkgver=2.02pl1
 pkgrel=1
 pkgdesc='Cryptographic protocol verifier in the formal model'
 arch=('i686' 'x86_64')
@@ -10,8 +11,8 @@ depends=('ocaml')
 makedepends=('ocamlbuild' 'ocaml-findlib' 'lablgtk2')
 optdepends=('graphviz: for displaying graphs of found attacks')
 source=("http://prosecco.gforge.inria.fr/personal/bblanche/proverif/proverif$pkgver.tar.gz")
-sha1sums=('b55a942a25f462013e575924baa0706b6b9c69ad')
-sha256sums=('b1bf1496c5aebfa3c0f311317ca99626435faa5d08a6a49402ff1c1606299707')
+sha1sums=('d5421ac236a03a6c432417bf1b066d81cbc6b551')
+sha256sums=('5d4aa21eb05b9fe11d1fe448259b7dbda7adca1cd15c09f0acee3508fa75bfca')

 build() {
   cd "$srcdir/proverif$pkgver"
@@ -19,15 +20,27 @@ build() {
 }

 check() {
+  # MODES and DATASETS are fetched from:
+  #     ./test --help
   cd "$srcdir/proverif$pkgver"
-  ./test all
-  ./test-type all
+  local MODES=(test test_add add update)
+  local DATASETS=(untyped typed)
+  parallel --tag --linebuffer -v ./test ::: ${MODES[@]} ::: ${DATASETS[@]}
 }

 package() {
   cd "$srcdir/proverif$pkgver"

-  install -Dm755 proverif "$pkgdir/usr/bin/proverif"
-  install -Dm755 proveriftotex "$pkgdir/usr/bin/proveriftotex"
-  install -Dm644 LICENSE "$pkgdir/usr/share/licenses/proverif/LICENSE"
+  msg2 "Copying binaries..."
+  install -Dm755 -vt "$pkgdir/usr/bin/" proverif{,totex,_interact}
+  
+  msg2 "Copying documentations..."
+  install -Dm644 -vt "$pkgdir/usr/share/doc/proverif" README CHANGES docs/*
+  
+  msg2 "Copying examples..."
+  mkdir -p "$pkgdir/usr/share/proverif/examples" 
+  cp --no-preserve=o -avt "$pkgdir/usr/share/proverif/examples" examples/*/
+  
+  # FIXME(ducksoft): I don't know how to package Emacs mode for proverif.el
+  # Patches are welcome.
 }
-- 
2.31.1

Can you add this line to the PKGBUILD?

install -Dm755 proverif_interact "$pkgdir/usr/bin/proverif_interact"

lablgtk2 has problems right now: https://bugs.archlinux.org/index.php?do=details&action=details.addvote&task_id=68503

Fix is to recompile it.

@mbloms the check does take a while, but it eventually terminates and installs successfully on my machine. Have you checked ps a | grep test, whether the tests are progressing?

The check function in the PKGBUILD just hangs on my machine. Program works great if I skip it.

@greyfox That's strange. gcc should not be necessary to build the native binary, the build process only invokes standard OCaml commands. (See the build script in the source distribution.)