From unknown Tue Jun 24 17:23:51 2025 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.509 (Entity 5.509) Content-Type: text/plain; charset=utf-8 From: bug#27874 <27874@debbugs.gnu.org> To: bug#27874 <27874@debbugs.gnu.org> Subject: Status: add cubicle Reply-To: bug#27874 <27874@debbugs.gnu.org> Date: Wed, 25 Jun 2025 00:23:51 +0000 retitle 27874 add cubicle reassign 27874 guix-patches submitter 27874 Julien Lepiller severity 27874 normal thanks From debbugs-submit-bounces@debbugs.gnu.org Sun Jul 30 04:44:17 2017 Received: (at submit) by debbugs.gnu.org; 30 Jul 2017 08:44:17 +0000 Received: from localhost ([127.0.0.1]:33566 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dbjpd-0002eP-H6 for submit@debbugs.gnu.org; Sun, 30 Jul 2017 04:44:17 -0400 Received: from eggs.gnu.org ([208.118.235.92]:37837) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dbjpb-0002eB-5b for submit@debbugs.gnu.org; Sun, 30 Jul 2017 04:44:11 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dbjpV-0003lV-24 for submit@debbugs.gnu.org; Sun, 30 Jul 2017 04:44:05 -0400 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=0.8 required=5.0 tests=BAYES_50 autolearn=disabled version=3.3.2 Received: from lists.gnu.org ([2001:4830:134:3::11]:47314) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1dbjpU-0003lR-UQ for submit@debbugs.gnu.org; Sun, 30 Jul 2017 04:44:04 -0400 Received: from eggs.gnu.org ([2001:4830:134:3::10]:57033) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dbjpT-0000AU-Jd for guix-patches@gnu.org; Sun, 30 Jul 2017 04:44:04 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dbjpP-0003ig-QT for guix-patches@gnu.org; Sun, 30 Jul 2017 04:44:03 -0400 Received: from static-176-182-42-79.ncc.abo.bbox.fr ([176.182.42.79]:42000 helo=metebelis3) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1dbjpP-0003g4-CB for guix-patches@gnu.org; Sun, 30 Jul 2017 04:43:59 -0400 Received: from localhost (bbox.lan [192.168.1.254]); by metebelis3 (OpenSMTPD) with ESMTPSA id d57c08f7; TLS version=TLSv1/SSLv3 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO; for ; Sun, 30 Jul 2017 08:43:52 +0000 (UTC) Date: Sun, 30 Jul 2017 10:43:12 +0200 From: Julien Lepiller To: guix-patches@gnu.org Subject: add cubicle Message-ID: <20170730104312.759aa420@lepiller.eu> X-Mailer: Claws Mail 3.15.0-dirty (GTK+ 2.24.31; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="MP_/smDkFaGbp20sAEa0zMl4hio" X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-Received-From: 2001:4830:134:3::11 X-Spam-Score: -4.0 (----) X-Debbugs-Envelope-To: submit X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -4.0 (----) --MP_/smDkFaGbp20sAEa0zMl4hio Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Disposition: inline Hi, here is a patch to add cubicle, a model checker. --MP_/smDkFaGbp20sAEa0zMl4hio Content-Type: text/x-patch Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=0001-gnu-Add-cubicle.patch >From efd5bd9b677d55954b3af856c7657f0aae8ab63a Mon Sep 17 00:00:00 2001 From: Julien Lepiller 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 --MP_/smDkFaGbp20sAEa0zMl4hio-- From debbugs-submit-bounces@debbugs.gnu.org Sat Aug 05 04:14:10 2017 Received: (at 27874-done) by debbugs.gnu.org; 5 Aug 2017 08:14:10 +0000 Received: from localhost ([127.0.0.1]:42426 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dduDq-0003u7-6e for submit@debbugs.gnu.org; Sat, 05 Aug 2017 04:14:10 -0400 Received: from static-176-182-42-79.ncc.abo.bbox.fr ([176.182.42.79]:59054 helo=metebelis3) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dduDo-0003tw-9T for 27874-done@debbugs.gnu.org; Sat, 05 Aug 2017 04:14:08 -0400 Received: from localhost (bbox.lan [192.168.1.254]) by metebelis3 (OpenSMTPD) with ESMTPSA id 0fb791f4 (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for <27874-done@debbugs.gnu.org>; Sat, 5 Aug 2017 08:14:02 +0000 (UTC) Date: Sat, 5 Aug 2017 10:13:22 +0200 From: Julien Lepiller To: 27874-done@debbugs.gnu.org Subject: Re: [bug#27874] add cubicle Message-ID: <20170805101322.78d1a6ca@lepiller.eu> In-Reply-To: <20170730104312.759aa420@lepiller.eu> References: <20170730104312.759aa420@lepiller.eu> X-Mailer: Claws Mail 3.15.0-dirty (GTK+ 2.24.31; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: 3.6 (+++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: Le Sun, 30 Jul 2017 10:43:12 +0200, Julien Lepiller a écrit : > Hi, here is a patch to add cubicle, a model checker. Pushed as 3d5d87a3ae4a3320bb909265ac4d2739e206dfdd. [...] Content analysis details: (3.6 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 3.6 RCVD_IN_PBL RBL: Received via a relay in Spamhaus PBL [176.182.42.79 listed in zen.spamhaus.org] 0.0 FSL_HELO_NON_FQDN_1 No description available. -0.0 SPF_PASS SPF: sender matches SPF record X-Debbugs-Envelope-To: 27874-done X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 3.6 (+++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: Le Sun, 30 Jul 2017 10:43:12 +0200, Julien Lepiller a écrit : > Hi, here is a patch to add cubicle, a model checker. Pushed as 3d5d87a3ae4a3320bb909265ac4d2739e206dfdd. [...] Content analysis details: (3.6 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 3.6 RCVD_IN_PBL RBL: Received via a relay in Spamhaus PBL [176.182.42.79 listed in zen.spamhaus.org] 0.0 FSL_HELO_NON_FQDN_1 No description available. -0.0 SPF_PASS SPF: sender matches SPF record Le Sun, 30 Jul 2017 10:43:12 +0200, Julien Lepiller a =C3=A9crit : > Hi, here is a patch to add cubicle, a model checker. Pushed as 3d5d87a3ae4a3320bb909265ac4d2739e206dfdd. From debbugs-submit-bounces@debbugs.gnu.org Sat Aug 05 17:24:47 2017 Received: (at 27874) by debbugs.gnu.org; 5 Aug 2017 21:24:47 +0000 Received: from localhost ([127.0.0.1]:43793 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1de6Yx-0005BC-0P for submit@debbugs.gnu.org; Sat, 05 Aug 2017 17:24:47 -0400 Received: from eggs.gnu.org ([208.118.235.92]:52376) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1de6Yv-0005B0-Oo for 27874@debbugs.gnu.org; Sat, 05 Aug 2017 17:24:46 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1de6Yp-0003tl-L9 for 27874@debbugs.gnu.org; Sat, 05 Aug 2017 17:24:40 -0400 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,RP_MATCHES_RCVD autolearn=disabled version=3.3.2 Received: from fencepost.gnu.org ([2001:4830:134:3::e]:57536) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1de6Yh-0003nt-Nt; Sat, 05 Aug 2017 17:24:31 -0400 Received: from reverse-83.fdn.fr ([80.67.176.83]:50806 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1de6Yh-0002T7-86; Sat, 05 Aug 2017 17:24:31 -0400 From: ludo@gnu.org (Ludovic =?utf-8?Q?Court=C3=A8s?=) To: 27874@debbugs.gnu.org Subject: Re: bug#27874: add cubicle References: <20170730104312.759aa420@lepiller.eu> <20170805101322.78d1a6ca@lepiller.eu> X-URL: http://www.fdn.fr/~lcourtes/ X-Revolutionary-Date: 18 Thermidor an 225 de la =?utf-8?Q?R=C3=A9volution?= X-PGP-Key-ID: 0x090B11993D9AEBB5 X-PGP-Key: http://www.fdn.fr/~lcourtes/ludovic.asc X-PGP-Fingerprint: 3CE4 6455 8A84 FDC6 9DB4 0CFB 090B 1199 3D9A EBB5 X-OS: x86_64-unknown-linux-gnu Date: Sat, 05 Aug 2017 23:24:29 +0200 In-Reply-To: <20170805101322.78d1a6ca@lepiller.eu> (Julien Lepiller's message of "Sat, 5 Aug 2017 10:13:22 +0200") Message-ID: <87shh5k8s2.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 2001:4830:134:3::e X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: 27874 Cc: julien@lepiller.eu X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -5.0 (-----) Julien Lepiller skribis: > Le Sun, 30 Jul 2017 10:43:12 +0200, > Julien Lepiller a =C3=A9crit : > >> Hi, here is a patch to add cubicle, a model checker. > > Pushed as 3d5d87a3ae4a3320bb909265ac4d2739e206dfdd. Please remove =E2=80=9Copen source=E2=80=9D from the description. :-) Thanks for this patch! Ludo=E2=80=99. From unknown Tue Jun 24 17:23:51 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Sun, 03 Sep 2017 11:24:05 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator