all messages for Guix-related lists mirrored at yhetil.org
 help / color / mirror / code / Atom feed
* [bug#27874] add cubicle
@ 2017-07-30  8:43 Julien Lepiller
  2017-08-05  8:13 ` bug#27874: " Julien Lepiller
  0 siblings, 1 reply; 3+ messages in thread
From: Julien Lepiller @ 2017-07-30  8:43 UTC (permalink / raw)
  To: 27874

[-- Attachment #1: Type: text/plain, Size: 52 bytes --]

Hi, here is a patch to add cubicle, a model checker.

[-- Attachment #2: 0001-gnu-Add-cubicle.patch --]
[-- Type: text/x-patch, Size: 2371 bytes --]

From efd5bd9b677d55954b3af856c7657f0aae8ab63a Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Sun, 30 Jul 2017 10:23:08 +0200
Subject: [PATCH] gnu: Add cubicle.

* gnu/packages/maths.scm (cubicle): New variable.
---
 gnu/packages/maths.scm | 43 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 6566d750b..9cd9a1dcc 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -3196,3 +3196,46 @@ as equations, scalars, vectors, and matrices.")
 theories} (SMT) solver.  It provides a C/C++ API.")
     (home-page "https://github.com/Z3Prover/z3")
     (license license:expat)))
+
+(define-public cubicle
+  (package
+    (name "cubicle")
+    (version "1.1.1")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "http://cubicle.lri.fr/cubicle-"
+                                  version ".tar.gz"))
+              (sha256
+               (base32
+                "1sny9c4fm14k014pk62ibpwbrjjirkx8xmhs9jg7q1hk7y7x3q2h"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("ocaml" ,ocaml)
+       ("which" ,which)))
+    (propagated-inputs
+     `(("z3" ,z3)))
+    (arguments
+     `(#:configure-flags (list "--with-z3")
+       #:tests? #f
+       #:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'configure-for-release
+           (lambda _
+             (substitute* "Makefile.in"
+               (("SVNREV=") "#SVNREV="))))
+         (add-before 'configure 'fix-/bin/sh
+           (lambda _
+             (substitute* "configure"
+               (("/bin/sh") (which "sh")))))
+         (add-before 'configure 'fix-smt-z3wrapper.ml
+           (lambda _
+             (substitute* "Makefile.in"
+               (("\\\\n") "")))))))
+    (home-page "http://cubicle.lri.fr/")
+    (synopsis "Model checker for array-based systems")
+    (description "Cubicle is an open source model checker for verifying safety
+properties of array-based systems.  This is a syntactically restricted class of
+parametrized transition systems with states represented as arrays indexed by an
+arbitrary number of processes.  Cache coherence protocols and mutual exclusion
+algorithms are typical examples of such systems.")
+    (license license:asl2.0)))
-- 
2.13.3


^ permalink raw reply related	[flat|nested] 3+ messages in thread

* bug#27874: add cubicle
  2017-07-30  8:43 [bug#27874] add cubicle Julien Lepiller
@ 2017-08-05  8:13 ` Julien Lepiller
  2017-08-05 21:24   ` [bug#27874] " Ludovic Courtès
  0 siblings, 1 reply; 3+ messages in thread
From: Julien Lepiller @ 2017-08-05  8:13 UTC (permalink / raw)
  To: 27874-done

Le Sun, 30 Jul 2017 10:43:12 +0200,
Julien Lepiller <julien@lepiller.eu> a écrit :

> Hi, here is a patch to add cubicle, a model checker.

Pushed as 3d5d87a3ae4a3320bb909265ac4d2739e206dfdd.

^ permalink raw reply	[flat|nested] 3+ messages in thread

* [bug#27874] add cubicle
  2017-08-05  8:13 ` bug#27874: " Julien Lepiller
@ 2017-08-05 21:24   ` Ludovic Courtès
  0 siblings, 0 replies; 3+ messages in thread
From: Ludovic Courtès @ 2017-08-05 21:24 UTC (permalink / raw)
  To: 27874

Julien Lepiller <julien@lepiller.eu> skribis:

> Le Sun, 30 Jul 2017 10:43:12 +0200,
> Julien Lepiller <julien@lepiller.eu> a écrit :
>
>> Hi, here is a patch to add cubicle, a model checker.
>
> Pushed as 3d5d87a3ae4a3320bb909265ac4d2739e206dfdd.

Please remove “open source” from the description.  :-)

Thanks for this patch!

Ludo’.

^ permalink raw reply	[flat|nested] 3+ messages in thread

end of thread, other threads:[~2017-08-05 21:25 UTC | newest]

Thread overview: 3+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2017-07-30  8:43 [bug#27874] add cubicle Julien Lepiller
2017-08-05  8:13 ` bug#27874: " Julien Lepiller
2017-08-05 21:24   ` [bug#27874] " Ludovic Courtès

Code repositories for project(s) associated with this external index

	https://git.savannah.gnu.org/cgit/guix.git

This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.