GNU logs - #73236, boring messages

Message sent to guix-patches@HIDDEN:

Subject: [bug#73236] [PATCH 0/2] gnu: Add coq-actris.
Resent-From: Antero Mejr <mail@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Fri, 13 Sep 2024 20:49:01 +0000
Resent-Message-ID: <handler.73236.B.172626053231570 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
To: 73236 <at> debbugs.gnu.org
From: Antero Mejr <mail@HIDDEN>
Date: Fri, 13 Sep 2024 20:48:33 +0000
Message-ID: <87ed5n2sbi.fsf@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13)
MIME-Version: 1.0
Content-Type: text/plain
Received-SPF: pass client-ip=149.28.215.223;
 envelope-from=SRS0=0bc9=QM=antr.me=mail@HIDDEN;
 helo=smtp.forwardemail.net
X-Spam_score_int: -20
X-Spam_score: -2.1
X-Spam_bar: --
X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
 DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, SPF_HELO_PASS=-0.001,
 SPF_PASS=-0.001 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-Spam-Score: -1.4 (-)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -2.4 (--)

This patchset adds the Coq verification library Actris, and its
dependency coq-iris.

Message sent:

Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable
MIME-Version: 1.0
X-Mailer: MIME-tools 5.505 (Entity 5.505)
Content-Type: text/plain; charset=utf-8
X-Loop: help-debbugs@HIDDEN
From: help-debbugs@HIDDEN (GNU bug Tracking System)
To: Antero Mejr <mail@HIDDEN>
Subject: bug#73236: Acknowledgement ([PATCH 0/2] gnu: Add coq-actris.)
Message-ID: <handler.73236.B.172626053231570.ack <at> debbugs.gnu.org>
References: <87ed5n2sbi.fsf@HIDDEN>
X-Gnu-PR-Message: ack 73236
X-Gnu-PR-Package: guix-patches
X-Gnu-PR-Keywords: patch
Reply-To: 73236 <at> debbugs.gnu.org
Date: Fri, 13 Sep 2024 20:49:02 +0000

Thank you for filing a new bug report with debbugs.gnu.org.

This is an automatically generated reply to let you know your message
has been received.

Your message is being forwarded to the package maintainers and other
interested parties for their attention; they will reply in due course.

Your message has been sent to the package maintainer(s):
 guix-patches@HIDDEN

If you wish to submit further information on this problem, please
send it to 73236 <at> debbugs.gnu.org.

Please do not send mail to help-debbugs@HIDDEN unless you wish
to report a problem with the Bug-tracking system.

--=20
73236: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D73236
GNU Bug Tracking System
Contact help-debbugs@HIDDEN with problems

Message sent to guix-patches@HIDDEN:

Subject: [bug#73236] [PATCH 1/2] gnu: Add coq-iris.
Resent-From: Antero Mejr <mail@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Fri, 13 Sep 2024 20:52:01 +0000
Resent-Message-ID: <handler.73236.B73236.172626071132422 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
To: 73236 <at> debbugs.gnu.org
Cc: pukkamustard@HIDDEN, julien@HIDDEN
From: Antero Mejr <mail@HIDDEN>
In-Reply-To: <handler.73236.B.172626053231570.ack <at> debbugs.gnu.org> (GNU bug
 Tracking System's message of "Fri, 13 Sep 2024 20:49:02 +0000")
References: <87ed5n2sbi.fsf@HIDDEN>
 <handler.73236.B.172626053231570.ack <at> debbugs.gnu.org>
Date: Fri, 13 Sep 2024 20:51:26 +0000
Message-ID: <87a5gb2s6p.fsf_-_@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13)
MIME-Version: 1.0
Content-Type: text/plain
Precedence: list
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>


* gnu/packages/coq.scm (coq-iris): New variable.

Change-Id: I3841ab402fe82149996e1413f9ab3a475f4859d9
---
 gnu/packages/coq.scm | 94 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 94 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 31d1e8d51d..bd80cc4a34 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -42,6 +42,7 @@ (define-module (gnu packages coq)
   #:use-module (gnu packages perl)
   #:use-module (gnu packages python)
   #:use-module (gnu packages rsync)
+  #:use-module (gnu packages tex)
   #:use-module (gnu packages texinfo)
   #:use-module (guix build-system dune)
   #:use-module (guix build-system gnu)
@@ -777,3 +778,96 @@ (define-public coq-mathcomp-bigenough
 purposes as @code{bigenough} will be subsumed by the near tactics.  The
 formalization is based on the Mathematical Components library.")
     (license license:cecill-b)))
+
+(define-public coq-iris
+  (package
+    (name "coq-iris")
+    (version "4.2.0")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://gitlab.mpi-sws.org/iris/iris.git/")
+                    (commit (string-append "iris-" version))))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "1wr1jigzgl4fajl5jv4lanmb8nk4k6wdakakmxhfp5drxwhqgs0y"))))
+    (build-system gnu-build-system)
+    (arguments
+     (list #:parallel-build? #f ; non-deterministic failures
+           #:tests? #f ; 3 proof failures, appears formatting-related
+           #:test-target "test"
+           #:make-flags #~(list (string-append "COQLIBINSTALL=" #$output
+                                               "/lib/coq/user-contrib")
+                                ;; Coq interleaves tests into the build.
+                                ;; Work around this in the check phase.
+                                "NO_TEST=1"
+                                ;; Load mappings from _CoqProject into coqtop
+                                ;; TODO: can this be automated?
+                                "COQTOP=coqtop -Q iris/prelude iris.prelude \
+-Q iris/algebra iris.algebra \
+-Q iris/si_logic iris.si_logic \
+-Q iris/bi iris.bi \
+-Q iris/proofmode iris.proofmode \
+-Q iris/base_logic iris.base_logic \
+-Q iris/program_logic iris.program_logic \
+-Q iris_heap_lang iris.heap_lang \
+-Q iris_unstable iris.unstable \
+-Q iris_deprecated iris.deprecated")
+           #:phases #~(modify-phases %standard-phases
+                        (delete 'configure)
+                        (add-after 'build 'build-doc
+                          (lambda _
+                            (with-directory-excursion "tex"
+                              (invoke "make"))))
+                        (replace 'check
+                          (lambda* (#:key tests? test-target parallel-build?
+                                    make-flags #:allow-other-keys)
+                            (when tests?
+                              (apply invoke "make" "-f" "Makefile.coq.local"
+                                     "-j" (number->string
+                                           (if parallel-build?
+                                               (parallel-job-count)
+                                               1))
+                                     test-target make-flags))))
+                        (add-after 'install 'install-doc
+                          (lambda _
+                            (install-file
+                             "tex/iris.pdf"
+                             (string-append #$output
+                                            "/share/doc/iris/iris.pdf")))))))
+    (native-inputs (list (texlive-updmap.cfg
+                          (list texlive-amsfonts
+                                texlive-amsmath
+                                texlive-babel
+                                texlive-biber
+                                texlive-biblatex
+                                texlive-csquotes
+                                texlive-dashbox
+                                texlive-enumitem
+                                texlive-faktor
+                                texlive-geometry
+                                texlive-hyperref
+                                texlive-ifmtarg
+                                texlive-latexmk
+                                texlive-marvosym
+                                texlive-mathpartir
+                                texlive-mathtools
+                                texlive-microtype
+                                texlive-pgf
+                                texlive-scalerel
+                                texlive-semantic
+                                texlive-stmaryrd
+                                texlive-tabbing
+                                texlive-tensor
+                                texlive-xcolor
+                                texlive-xifthen))))
+    (propagated-inputs (list coq coq-stdpp))
+    (home-page "https://iris-project.org/")
+    (synopsis "Concurrent separation logic library for Coq")
+    (description
+     "This package provides a higher-order concurrent separation logic
+library, implemented and verified in the Coq proof assistant.  It is used for
+reasoning about safety of concurrent programs, as the logic in logical
+relations, and to reason about type-systems, data-abstraction, etc.")
+    (license license:bsd-3)))

base-commit: 0e0d9bc91f20ac6dda439ab09330f0163eb9bf42
-- 
2.46.0

Message sent to guix-patches@HIDDEN:

Subject: [bug#73236] [PATCH 2/2] gnu: Add coq-actris.
Resent-From: Antero Mejr <mail@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Fri, 13 Sep 2024 20:54:02 +0000
Resent-Message-ID: <handler.73236.B73236.172626078732579 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
To: 73236 <at> debbugs.gnu.org
Cc: pukkamustard@HIDDEN, julien@HIDDEN
From: Antero Mejr <mail@HIDDEN>
In-Reply-To: <handler.73236.B.172626053231570.ack <at> debbugs.gnu.org> (GNU bug
 Tracking System's message of "Fri, 13 Sep 2024 20:49:02 +0000")
References: <87ed5n2sbi.fsf@HIDDEN>
 <handler.73236.B.172626053231570.ack <at> debbugs.gnu.org>
Date: Fri, 13 Sep 2024 20:52:44 +0000
Message-ID: <874j6j2s4j.fsf_-_@HIDDEN>
MIME-Version: 1.0
Content-Type: text/plain
Precedence: list
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>


* gnu/packages/coq.scm (coq-actris): New variable.

Change-Id: Ied7bff06ee88271400e145844139ded2f3c80108
---
 gnu/packages/coq.scm | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index bd80cc4a34..1640e68b03 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -871,3 +871,40 @@ (define-public coq-iris
 reasoning about safety of concurrent programs, as the logic in logical
 relations, and to reason about type-systems, data-abstraction, etc.")
     (license license:bsd-3)))
+
+(define-public coq-actris
+  (let ((commit "18f784adb884ac14edd3eb19610d0b3fd62f4985") ;no tags
+        (revision "0"))
+    (package
+      (name "coq-actris")
+      (version (git-version "2.0" revision commit)) ;2.0 has subprotocols
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url "https://gitlab.mpi-sws.org/iris/actris.git/")
+                      (commit commit)))
+                (file-name (git-file-name name version))
+                (sha256
+                 (base32
+                  "0d6xjccnk6jw530mzvs8gya3q3cck9jc8a9mb267d1dhypvdxc40"))))
+      (build-system gnu-build-system)
+      (arguments
+       (list #:parallel-build? #f ; non-deterministic failures
+             #:tests? #f ; no tests
+             #:make-flags #~(list (string-append "COQLIBINSTALL=" #$output
+                                                 "/lib/coq/user-contrib")
+                                  "NO_TEST=1"
+                                  "COQTOP=coqtop -Q theories actris")
+             #:phases #~(modify-phases %standard-phases
+                          (delete 'configure)
+                          (replace 'install
+                            (lambda* (#:key make-flags #:allow-other-keys)
+                              (apply invoke "make" "-f" "Makefile.coq"
+                                     "install" make-flags))))))
+      (propagated-inputs (list coq coq-iris))
+      (home-page "https://gitlab.mpi-sws.org/iris/actris")
+      (synopsis "Coq library for session types in separation logic")
+      (description
+       "This package provides a Coq library for proving functional correctness
+of programs that use message-passing concurrency.")
+      (license license:bsd-3))))
-- 
2.46.0

Message sent to guix-patches@HIDDEN:

X-Loop: help-debbugs@HIDDEN
Subject: [bug#73236] [PATCH 0/2] gnu: Add coq-actris.
Resent-From: Arnaud Daby-Seesaram <ds-ac@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Wed, 09 Oct 2024 12:20:02 +0000
Resent-Message-ID: <handler.73236.B73236.172847635414694 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: followup 73236
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: 73236 <at> debbugs.gnu.org
Cc: Antero Mejr <mail@HIDDEN>, pukkamustard@HIDDEN, julien@HIDDEN
Received: via spool by 73236-submit <at> debbugs.gnu.org id=B73236.172847635414694
          (code B ref 73236); Wed, 09 Oct 2024 12:20:02 +0000
Received: (at 73236) by debbugs.gnu.org; 9 Oct 2024 12:19:14 +0000
Received: from localhost ([127.0.0.1]:55897 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1syVer-0003ow-So
	for submit <at> debbugs.gnu.org; Wed, 09 Oct 2024 08:19:14 -0400
Received: from nanein.fr ([185.230.78.41]:42784)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <ds-ac@HIDDEN>) id 1syVeo-0003oe-Ls
 for 73236 <at> debbugs.gnu.org; Wed, 09 Oct 2024 08:19:11 -0400
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=nanein.fr; s=mail;
 t=1728476334; bh=qm/hH/ol/rwWHfzEXzqfDYmorfODcj3w1DqVTmxJIb8=;
 h=From:To:Cc:Subject:In-Reply-To:References:Date:From;
 b=m35eGemNS2+oS/T47oKRZ3vpnFbYun/iBf5F7WnJs6VBwP8Ki0102IhDBPh8/Fmhk
 IQ/Gdj75b60j3Wy0sqDbSGYRr1a5fcTd9xGngk9ig4sYi9DVDQwODymGlbho1OBUK2
 ukmXh6m/Yr7/oRn33wJeR6PZzg+wavMNReo98Uym0dd7vtbqgLR9pM1XhkWHsFAmsr
 3YNeCvJQACy60QKZbhAZpeo7GOqTaSAMtEb9JuTZX9micoo4bo4cYJ1Rm3sB+HVgJM
 6+AQ30El/1C94h9glRpZnUHrdtcnC9BjNjYKSbFTafaAm5LRWB18L5l2sNLj++T9Py
 6K60SZHwBe7Jfq2bHC4eX8vCj9qpOJl5rPbGl7B6zUuM3X+Q8Fjj8gJ95OKFSOHgWf
 kyRK5tVFNqAlRy+xQTAdoD/L7LRE14NctwFcXbvaXXL/8neubu6oNxLRxbQ1Oplb+g
 L8S8MHdAo9S7FNSud9ch3buXlB2NETBDuB+gx0xnXb0MXzBkEPhauvsN7NDYJhbTTa
 omMpZAZ8Sg0OCzdqXlmXbDaHCYstt1YNLPtQPyt1aqXsW70uWLazs9wM4nJ3WdrQBh
 Fk/ubZAZmHl4hUffScOlY7jNm80r5Ui3hRqVLaKp0tmrLdDMGo+6z/PVIQ+dJ55Jju
 4VUenSeRuEDloZSVZB1qZdlE=
Received: from cochea (eduroam09.au.dk [185.45.22.146])
 (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)
 key-exchange ECDHE (prime256v1) server-signature ECDSA (prime256v1)
 server-digest SHA256) (No client certificate requested)
 by nanein.fr (Postfix) with ESMTPSA id 11841140215;
 Wed,  9 Oct 2024 14:18:54 +0200 (CEST)
From: Arnaud Daby-Seesaram <ds-ac@HIDDEN>
In-Reply-To: <87ed5n2sbi.fsf@HIDDEN> (Antero Mejr via Guix-patches via's
 message of "Fri, 13 Sep 2024 20:48:33 +0000")
References: <87ed5n2sbi.fsf@HIDDEN>
Date: Wed, 09 Oct 2024 14:18:42 +0200
Message-ID: <87ldyxzcyl.fsf@HIDDEN>
MIME-Version: 1.0
Content-Type: multipart/signed; boundary="=-=-=";
 micalg=pgp-sha512; protocol="application/pgp-signature"
X-Spam-Score: 0.0 (/)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

--=-=-=
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable

Hi Antero,

Thank you for your patches; I apologise for the response delay.

You will find a quick review below.

=2D Build: using your patch, both coq-iris and coq-actris can be
  successfully built (I only tried on a x86-64 machine with --rounds=3D3
  at the moment).

  However, I have a few questions:

  + I do not understand why COQTOP has to be specified in the
    #:make-flags.

  + Tests indeed fail if I switch #:tests? to #t.

    However, when I let the main build phase run the tests, they all
    seem to pass.  Do you experience the same result?
    If so, it could be worth it to (at least temporarily) allow tests in
    the main build phase (as is done in stdpp for example) and better
    understand where the issues come from.

  + Open question: would it be appropriate to split coq-iris across
    several outputs (main output for Iris, heap-lang, deprecated and
    unstable)?

  NB: I have not had the time to look at why there is a need to replace
      the install phase in coq-actris yet.

=2D Licenses: the licenses are correct.

=2D Home pages:
  + Iris: Ok.
  + Actris: you used a link to the GitLab repository.
    https://iris-project.org/actris/ might be more appropriate.

=2D Description fields:
  Descriptions are are usually phrased as "X is ...", where "X" is the
  name of the project.  Could you please rephrase the description in
  this style?

  Note: the Opam file of Iris reads "Iris is ..." too if you need a
  reference text.

=2D Documentation:
  It is very nice that you build and install iris.pdf.

  Do you think that adding a `native-search-paths' field to `coq-iris'
  (for variables "GUIX_TEXMF" and "BIBINPUTS") would be interesting?
  This way, `tex/iris.sty' and `tex/bib.bib' (maybe renamed into
  iris.bib) would be made available to TeX installations?


Sorry if writing my review as a list reads a bit cold (this is not my
intention); I=C2=A0just wanted to be as organised as possible.

Overall, thank you for you patches.  It would be nice to see
Iris-related stuff in Guix (and more generally more movement in the
OCaml/Coq worlds) :).

Best regards,

=2D-=20
Arnaud

--=-=-=
Content-Type: application/pgp-signature; name="signature.asc"

-----BEGIN PGP SIGNATURE-----

iQJEBAEBCgAuFiEEMgqfJ4U0fby1t860ojLKXoMTiAwFAmcGdKMQHGRzLWFjQG5h
bmVpbi5mcgAKCRCiMspegxOIDDulD/9kyPD8eewzWm4Y3bR1Pv6IVPSI78D7CqkN
MvVa2fV+Vp50+ICK5q66iqpvDnaHjxOUEs8NYY8wxDs5bo1ypbmTqCBE6kusiTAT
09MasEQjb3G4Cy6s/hC48+4V5yAhbkOjUGsY3oGgbOXMkPdXlaaTqSZ9bbacVorV
Io31GziAb7GCo4iXKYIHIV3q+lbcvrRXGfeYPiWeEQ6vYFkrblw5UoQU2y46fGjW
SXfTBPVNaeXjgR1xKcZ99XGez98PFeJh8jENAI9pUlnQE9RgzCFW+A6STPwfSkwY
SiDomUCN852h/7pLsYZ+8ghIOFLsKaqlOK5rQA2ZaJ9sARd0DuVIqZIeKllGlO+T
bYoRJxFBKA6oGX7ronXTHwSN2Gtl7AarcR+cIG+i8DhWLJ1gI3i3xdFq3dNOHASF
n5ktJ5y7O4AUSFALWZvBHl8p4461s8ODVQ1yluhy/Esk1Dwu0jLTIGBtMP4syc//
z9raZFl9PdxMe+3S0ok6QEkKwQool9qbN04NteuXb47wCiOiCpFtV99nHXJP5IQM
q7tBZPOOXCI5kR7cZ/NvWj4l/8ybocVutsqucETqr5hSHJ+K2sVKFVACKXtbaOjw
YxUhZDlELZSWPODrOsm49rNq/tT/2xodTtq+Z0xnJXTPB28+ROo6rV/qTw5m7SRd
YqQhtsDWaw==
=J9Av
-----END PGP SIGNATURE-----
--=-=-=--

Last modified: Sun, 12 Jan 2025 05:45:02 UTC

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997 nCipher Corporation Ltd, 1994-97 Ian Jackson.