From unknown Tue Jun 24 17:27:15 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#27874] add cubicle Resent-From: Julien Lepiller Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Jul 2017 08:45:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 27874 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: To: 27874@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.150140425710200 (code B ref -1); Sun, 30 Jul 2017 08:45:01 +0000 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 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-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 unknown Tue Jun 24 17:27:15 2025 MIME-Version: 1.0 X-Mailer: MIME-tools 5.505 (Entity 5.505) X-Loop: help-debbugs@gnu.org From: help-debbugs@gnu.org (GNU bug Tracking System) To: Julien Lepiller Subject: bug#27874: closed (Re: [bug#27874] add cubicle) Message-ID: References: <20170805101322.78d1a6ca@lepiller.eu> <20170730104312.759aa420@lepiller.eu> X-Gnu-PR-Message: they-closed 27874 X-Gnu-PR-Package: guix-patches Reply-To: 27874@debbugs.gnu.org Date: Sat, 05 Aug 2017 08:15:02 +0000 Content-Type: multipart/mixed; boundary="----------=_1501920902-15093-1" This is a multi-part message in MIME format... ------------=_1501920902-15093-1 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Your bug report #27874: add cubicle which was filed against the guix-patches package, has been closed. The explanation is attached below, along with your original report. If you require more details, please reply to 27874@debbugs.gnu.org. --=20 27874: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D27874 GNU Bug Tracking System Contact help-debbugs@gnu.org with problems ------------=_1501920902-15093-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit 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. ------------=_1501920902-15093-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit 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-- ------------=_1501920902-15093-1-- From unknown Tue Jun 24 17:27:15 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#27874] add cubicle Resent-From: ludo@gnu.org (Ludovic =?UTF-8?Q?Court=C3=A8s?=) Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 05 Aug 2017 21:25:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 27874 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: To: 27874@debbugs.gnu.org Cc: julien@lepiller.eu Received: via spool by 27874-submit@debbugs.gnu.org id=B27874.150196828719919 (code B ref 27874); Sat, 05 Aug 2017 21:25:02 +0000 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?=) 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-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.