From unknown Mon Jun 23 13:15:25 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#38635] [WIP PATCH] Add why3 and frama-c Resent-From: Julien Lepiller Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 16 Dec 2019 11:47:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 38635 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38635@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.15764968151767 (code B ref -1); Mon, 16 Dec 2019 11:47:02 +0000 Received: (at submit) by debbugs.gnu.org; 16 Dec 2019 11:46:55 +0000 Received: from localhost ([127.0.0.1]:38021 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1igops-0000SK-I1 for submit@debbugs.gnu.org; Mon, 16 Dec 2019 06:46:55 -0500 Received: from lists.gnu.org ([209.51.188.17]:40216) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1igopo-0000S8-8b for submit@debbugs.gnu.org; Mon, 16 Dec 2019 06:46:47 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:38578) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1igopl-00074D-HF for guix-patches@gnu.org; Mon, 16 Dec 2019 06:46:43 -0500 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,URIBL_BLOCKED autolearn=disabled version=3.3.2 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1igopj-0005nV-DS for guix-patches@gnu.org; Mon, 16 Dec 2019 06:46:41 -0500 Received: from lepiller.eu ([2a00:5884:8208::1]:53012) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1igopi-0005NQ-NW for guix-patches@gnu.org; Mon, 16 Dec 2019 06:46:39 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 33b55185 for ; Mon, 16 Dec 2019 11:46:33 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=lepiller.eu; h=date:from :to:subject:message-id:mime-version:content-type; s=dkim; bh=ddC qRIHwitAK5b9ZvZVzjbVLBok=; b=A0myiVpuP6LjBaE5ouQb2+t8Lptf+cKZsO+ N8x4Okk14XwRlrB5RBclMBNcC8cQK2xOaPFMbtCz1w4bYqKb3azUbrGeAVhxweZE lfiM4SsIV4bpCSwsWdgn/oUsDr9e6UEYSWaufwob7lQHVRFSeUX2xDfirl2inzua vSCZQH+cbPT8Yom/wfGopkTJ+S/eA1DRIbeDXglbt5FYrv/WUA4tnaWNs7jVq/+4 xfX/P4q7XIF5QIFc3yq9rgCREjY+sW2LsYTZw+Asw6169ZnmF4xqD9dFG728f0GR ZJ9cH/cwbatM/jdwml2thC2ITbLqB6/1lTFmeHkmZmMOxSqgs/w== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id a163384c (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for ; Mon, 16 Dec 2019 11:46:33 +0000 (UTC) Date: Mon, 16 Dec 2019 12:46:26 +0100 From: Julien Lepiller Message-ID: <20191216124626.048f0e43@sybil.lepiller.eu> X-Mailer: Claws Mail 3.17.4 (GTK+ 2.24.32; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="MP_/u3+3XpCQJFzg+CVZkdv/T/7" X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 2a00:5884:8208::1 X-Spam-Score: -2.3 (--) 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: -1.0 (-) --MP_/u3+3XpCQJFzg+CVZkdv/T/7 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Disposition: inline Hi Guix! Since there was some interest very recently, I took another look at my incomplete why3 and frama-c packages. I updated them and polished them a little. I encourage formal-method guixers to test these patches, especially if you are a user of why3 or frama-c, because I'm not sure how these tools are supposed to be working. Note that I didn't include ide support in why3 because this adds ~1GiB to the closure of the program. A good thing could be to separate the why3 library (not required when using why3) from the main package, in a separate output. For some reason, frama-c doesn't work directly, it needs to be in an environment where its dependencies are present, hence the propagation. However, it's failing at runtime: $ guix environment --ad-hoc frama-c ocaml ocaml-findlib [env]$ frama-c --help [kernel] User Error: cannot load plug-in 'zip': cannot load module Details: error loading shared library: /gnu/store/hsjnvq5li28ak2wjnwlmqsfbg246skcg-profile/lib/ocaml/site-lib/zip/zip.cmxa: invalid ELF header [kernel] User Error: cannot load plug-in 'why3': cannot load module Details: error loading shared library: /gnu/store/hsjnvq5li28ak2wjnwlmqsfbg246skcg-profile/lib/ocaml/site-lib/why3/why3.cmxs: undefined symbol: camlGzip [kernel] User Error: cannot load plug-in 'frama-c-wp': cannot load module Details: error loading shared library: /gnu/store/daqn9vsc15j3slbalw2fag6amndv8x98-frama-c-20.0/lib/frama-c/plugins/top/Wp.cmxs: undefined symbol: camlWhy3__Theory [kernel] User Error: Deferred error message was emitted during execution. See above messages for more information. [kernel] Frama-C aborted: invalid user input. --MP_/u3+3XpCQJFzg+CVZkdv/T/7 Content-Type: text/x-patch Content-Transfer-Encoding: quoted-printable Content-Disposition: attachment; filename=0001-gnu-Add-why3.patch =46rom 9fc13943b29196763524ddbc247218398d889459 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Mon, 16 Dec 2019 12:09:16 +0100 Subject: [PATCH 1/2] gnu: Add why3. * gnu/packages/maths.scm (why3): New variable. --- gnu/packages/maths.scm | 67 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 66 insertions(+), 1 deletion(-) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 0ed61ad4a1..991f164737 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -28,7 +28,7 @@ ;;; Copyright =C2=A9 2018 Adam Massmann ;;; Copyright =C2=A9 2018 Marius Bakke ;;; Copyright =C2=A9 2018 Eric Brown -;;; Copyright =C2=A9 2018 Julien Lepiller +;;; Copyright =C2=A9 2018, 2019 Julien Lepiller ;;; Copyright =C2=A9 2018 Amin Bandali ;;; Copyright =C2=A9 2019 Nicolas Goaziou ;;; Copyright =C2=A9 2019 Steve Sprang @@ -61,6 +61,7 @@ #:use-module ((guix build utils) #:select (alist-replace)) #:use-module (guix build-system cmake) #:use-module (guix build-system gnu) + #:use-module (guix build-system ocaml) #:use-module (guix build-system python) #:use-module (guix build-system ruby) #:use-module (gnu packages algebra) @@ -72,10 +73,12 @@ #:use-module (gnu packages check) #:use-module (gnu packages cmake) #:use-module (gnu packages compression) + #:use-module (gnu packages coq) #:use-module (gnu packages curl) #:use-module (gnu packages cyrus-sasl) #:use-module (gnu packages documentation) #:use-module (gnu packages elf) + #:use-module (gnu packages emacs) #:use-module (gnu packages flex) #:use-module (gnu packages fltk) #:use-module (gnu packages fontutils) @@ -101,6 +104,7 @@ #:use-module (gnu packages mpi) #:use-module (gnu packages multiprecision) #:use-module (gnu packages netpbm) + #:use-module (gnu packages ocaml) #:use-module (gnu packages onc-rpc) #:use-module (gnu packages pcre) #:use-module (gnu packages popt) @@ -4182,6 +4186,67 @@ as equations, scalars, vectors, and matrices.") theories} (SMT) solver. It provides a C/C++ API, as well as Python bindin= gs.") (license license:expat))) =20 +(define-public why3 + (package + (name "why3") + (version "1.2.1") + (source (origin + (method url-fetch) + (uri (string-append "https://gforge.inria.fr/frs/download.ph= p/file" + "/38185/why3-" version ".tar.gz")) + (sha256 + (base32 + "014gkwisjp05x3342zxkryb729p02ngx1hcjjsrplpa53jzgz647")))) + (build-system ocaml-build-system) + (native-inputs + `(("coq" ,coq) + ("ocaml" ,ocaml) + ("which" ,which))) + (propagated-inputs + `(("camlzip" ,camlzip) + ("ocaml-graph" ,ocaml-graph) + ("ocaml-menhir" ,ocaml-menhir) + ("ocaml-num" ,ocaml-num) + ("ocaml-zarith" ,ocaml-zarith))) + (inputs + `(("coq-flocq" ,coq-flocq) + ("emacs-minimal" ,emacs-minimal) + ("zlib" ,zlib))) + (arguments + `(#:phases + (modify-phases %standard-phases + (add-before 'configure 'fix-configure + (lambda _ + (setenv "CONFIG_SHELL" (which "sh")) + (substitute* "configure" + ;; find ocaml-num in the correct directory + (("\\$DIR/nums.cma") "$DIR/../nums.cma") + (("\\$DIR/num.cmi") "$DIR/../num.cmi")) + #t)) + (add-after 'configure 'fix-makefile + (lambda _ + (substitute* "Makefile" + ;; find ocaml-num in the correct directory + (("site-lib/num") "site-lib")) + #t)) + (add-after 'install 'install-lib + (lambda _ + (invoke "make" "byte") + (invoke "make" "install-lib") + #t))))) + (home-page "http://why3.lri.fr") + (synopsis "Deductive program verification") + (description "Why3 provides a language for specification and programmi= ng, +called WhyML, and relies on external theorem provers, both automated and +interactive, to discharge verification conditions. Why3 comes with a stan= dard +library of logical theories (integer and real arithmetic, Boolean operatio= ns, +sets and maps, etc.) and basic programming data structures (arrays, queues, +hash tables, etc.). A user can write WhyML programs directly and get +correct-by-construction OCaml programs through an automated extraction +mechanism. WhyML is also used as an intermediate language for the verific= ation +of C, Java, or Ada programs.") + (license license:lgpl2.1))) + (define-public elpa (package (name "elpa") --=20 2.24.0 --MP_/u3+3XpCQJFzg+CVZkdv/T/7 Content-Type: text/x-patch Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=0002-gnu-Add-frama-c.patch >From f9501f1cc5725d49c69c948f6f7cc70c13f1dbdc Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Mon, 16 Dec 2019 12:40:18 +0100 Subject: [PATCH 2/2] gnu: Add frama-c. * gnu/packages/maths.scm (frama-c): New variable. --- gnu/packages/maths.scm | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 991f164737..d4e3e74c98 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -4247,6 +4247,44 @@ mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.") (license license:lgpl2.1))) +(define-public frama-c + (package + (name "frama-c") + (version "20.0") + (source (origin + (method url-fetch) + (uri (string-append "http://frama-c.com/download/frama-c-" + version "-Calcium.tar.gz")) + (sha256 + (base32 + "03dvn162djylj2skmk6vv75gh87mm4s5cspkzcrlm5x0rlla2yqn")))) + (build-system ocaml-build-system) + (arguments + `(#:tests? #f; no test target in Makefile + #:phases + (modify-phases %standard-phases + (add-before 'configure 'export-shell + (lambda* (#:key inputs #:allow-other-keys) + (setenv "CONFIG_SHELL" (string-append (assoc-ref inputs "bash") + "/bin/sh")) + #t))))) + (inputs + `(("gmp" ,gmp))) + (propagated-inputs + `(("ocaml-biniou" ,ocaml-biniou) + ("ocaml-easy-format" ,ocaml-easy-format) + ("ocaml-graph" ,ocaml-graph) + ("ocaml-yojson" ,ocaml-yojson) + ("ocaml-zarith" ,ocaml-zarith) + ("why3" ,why3))) + (home-page "http://frama-c.com") + (synopsis "C source code analysis platform") + (description "Frama-C is an extensible and collaborative platform dedicated +to source-code analysis of C software. The Frama-C analyzers assist you in +various source-code-related activities, from the navigation through unfamiliar +projects up to the certification of critical software.") + (license license:lgpl2.1+))) + (define-public elpa (package (name "elpa") -- 2.24.0 --MP_/u3+3XpCQJFzg+CVZkdv/T/7-- From unknown Mon Jun 23 13:15:25 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#38635] [WIP PATCH] Add why3 and frama-c Resent-From: Brett Gilio Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Wed, 25 Dec 2019 07:02:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38635 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Julien Lepiller Cc: bandali@gnu.org, 38635@debbugs.gnu.org Received: via spool by 38635-submit@debbugs.gnu.org id=B38635.157725731818285 (code B ref 38635); Wed, 25 Dec 2019 07:02:02 +0000 Received: (at 38635) by debbugs.gnu.org; 25 Dec 2019 07:01:58 +0000 Received: from localhost ([127.0.0.1]:53236 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ik0g9-0004kr-Ty for submit@debbugs.gnu.org; Wed, 25 Dec 2019 02:01:58 -0500 Received: from eggs.gnu.org ([209.51.188.92]:48601) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ik0g7-0004kc-Mq for 38635@debbugs.gnu.org; Wed, 25 Dec 2019 02:01:56 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:56441) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ik0g2-0007JU-1K; Wed, 25 Dec 2019 02:01:50 -0500 Received: from [2605:6000:1a0d:6320::6a8] (port=39516 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ik0fz-0004qA-Ic; Wed, 25 Dec 2019 02:01:48 -0500 From: Brett Gilio References: <20191216124626.048f0e43@sybil.lepiller.eu> Date: Wed, 25 Dec 2019 01:01:56 -0600 In-Reply-To: <20191216124626.048f0e43@sybil.lepiller.eu> (Julien Lepiller's message of "Mon, 16 Dec 2019 12:46:26 +0100") Message-ID: <878sn0zy57.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Spam-Score: -2.3 (--) 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.3 (---) Julien Lepiller writes: > Hi Guix! > > Since there was some interest very recently, I took another look at my > incomplete why3 and frama-c packages. I updated them and polished them > a little. I encourage formal-method guixers to test these patches, > especially if you are a user of why3 or frama-c, because I'm not sure > how these tools are supposed to be working. > > Note that I didn't include ide support in why3 because this adds ~1GiB > to the closure of the program. A good thing could be to separate the > why3 library (not required when using why3) from the main package, in a > separate output. > > For some reason, frama-c doesn't work directly, it needs to be in an > environment where its dependencies are present, hence the propagation. > However, it's failing at runtime: > > $ guix environment --ad-hoc frama-c ocaml ocaml-findlib > [env]$ frama-c --help > > [kernel] User Error: cannot load plug-in 'zip': cannot load > module Details: error loading shared library: > /gnu/store/hsjnvq5li28ak2wjnwlmqsfbg246skcg-profile/lib/ocaml/site-lib/zip/zip.cmxa: > invalid ELF header [kernel] User Error: cannot load plug-in 'why3': > cannot load module Details: error loading shared library: > /gnu/store/hsjnvq5li28ak2wjnwlmqsfbg246skcg-profile/lib/ocaml/site-lib/why3/why3.cmxs: > undefined symbol: camlGzip [kernel] User Error: cannot load plug-in > 'frama-c-wp': cannot load module Details: error loading shared library: > /gnu/store/daqn9vsc15j3slbalw2fag6amndv8x98-frama-c-20.0/lib/frama-c/plugins/top/Wp.cmxs: > undefined symbol: camlWhy3__Theory [kernel] User Error: Deferred error > message was emitted during execution. See above messages for more > information. [kernel] Frama-C aborted: invalid user input. > > > Hey Julien, Sorry for the delay. I got your patches the day you sent them, but have been rather busy and have inadvertently put them off and forget they existed. Woops! My apologies. I have Cc'ed Amin Bandali as we are both co-proposers for the formal methods working group. These type checking and safety systems are obviously very important to the formal methods community and software developers unaware of the nice guarantees offered by them. So i'd like to see this get added and in shape regardless of if the Guix maintainers "approve" our working group proposal. Thank you for sharing this. I will take another look at it soon and let you know what I find. :) -- Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE] From unknown Mon Jun 23 13:15:25 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#38635] [WIP PATCH v2] Add why3 and frama-c References: <20191216124626.048f0e43@sybil.lepiller.eu> In-Reply-To: <20191216124626.048f0e43@sybil.lepiller.eu> Resent-From: Julien Lepiller Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Wed, 02 Sep 2020 13:06:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38635 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38635@debbugs.gnu.org Received: via spool by 38635-submit@debbugs.gnu.org id=B38635.159905194922710 (code B ref 38635); Wed, 02 Sep 2020 13:06:02 +0000 Received: (at 38635) by debbugs.gnu.org; 2 Sep 2020 13:05:49 +0000 Received: from localhost ([127.0.0.1]:58646 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kDSSM-0005u7-MW for submit@debbugs.gnu.org; Wed, 02 Sep 2020 09:05:49 -0400 Received: from lepiller.eu ([89.234.186.109]:49738) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kDSSJ-0005tx-IX for 38635@debbugs.gnu.org; Wed, 02 Sep 2020 09:05:42 -0400 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id b667dbfb for <38635@debbugs.gnu.org>; Wed, 2 Sep 2020 13:05:37 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from :to:subject:message-id:mime-version:content-type; s=dkim; bh=xRd A5Ofu3qUS7cBm8Y5/jVuzUOLQY8zEwvMJt7q14HM=; b=bFXQetr1CMxstF0w3WP 1sJaak3W6L9g3KQ1tseIOXFIv389kX+7waMzsao5eZYR3vnwopeB6ULVqa44Dk/1 E5E4duKQIOd/Q9fc9ARTcO/3AWzbWlllx0IlAROm2jqT6oB3aoLl31cH1gWHuzRE 4VjREIa1nV/otp9qUGsfWzIw+3/hWONwItsOIPbQiymVyjrE/T5+tJQ0ZgVHRi1y JROxCisd+uBDLyRgHlMGXT4dIFNg8q/kVlUgt/mgAjRYAIgZbczSSyLAempp1scF XhvTrwV7dvOuV61peg3Q+t4fmI1X5JeAgI4uHJl/ed1sqa5c3FpGPbY4OyrrVVWA rhQ== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 61c742bd (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for <38635@debbugs.gnu.org>; Wed, 2 Sep 2020 13:05:37 +0000 (UTC) Date: Wed, 2 Sep 2020 15:05:30 +0200 From: Julien Lepiller Message-ID: <20200902150508.5c4a45e8@tachikoma.lepiller.eu> X-Mailer: Claws Mail 3.17.6 (GTK+ 2.24.32; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="MP_/j7X1Bwt=V/zaysvKe+hHAY3" X-Spam-Score: 0.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: -1.0 (-) --MP_/j7X1Bwt=V/zaysvKe+hHAY3 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Disposition: inline Hi Guix! I've updated my patches to the newest versions of why3 and frama-c. The issue is still present as before: $ frama-c --help [kernel] User Error: cannot load plug-in 'zip': cannot load module Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/gnu/store/jrbkl0ls1vqnr1w7gcbg8jlxcd1jp71m-profile/lib/ocaml/site-lib/zip/zip.cmxa: invalid ELF header\")") [kernel] User Error: cannot load plug-in 'why3': cannot load module Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/gnu/store/jrbkl0ls1vqnr1w7gcbg8jlxcd1jp71m-profile/lib/ocaml/site-lib/why3/why3.cmxs: undefined symbol: camlGzip\")") [kernel] User Error: cannot load plug-in 'frama-c-wp': cannot load module Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/gnu/store/bicyz7li6bvrxh4kh2h1dc5398bx5xsm-frama-c-21.1/lib/frama-c/plugins/top/Wp.cmxs: undefined symbol: camlWhy3__Theory\")") [kernel] User Error: Deferred error message was emitted during execution. See above messages for more information. [kernel] Frama-C aborted: invalid user input. --MP_/j7X1Bwt=V/zaysvKe+hHAY3 Content-Type: text/x-patch Content-Transfer-Encoding: quoted-printable Content-Disposition: attachment; filename=0001-gnu-Add-why3.patch =46rom 45254e8c70eb186a587c49295555e6c3096d67ab Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Mon, 16 Dec 2019 12:09:16 +0100 Subject: [PATCH 1/2] gnu: Add why3. * gnu/packages/maths.scm (why3): New variable. --- gnu/packages/maths.scm | 67 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 66 insertions(+), 1 deletion(-) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 97f57ddd24..aa3d0da77c 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -28,7 +28,7 @@ ;;; Copyright =C2=A9 2018 Adam Massmann ;;; Copyright =C2=A9 2018, 2020 Marius Bakke ;;; Copyright =C2=A9 2018 Eric Brown -;;; Copyright =C2=A9 2018 Julien Lepiller +;;; Copyright =C2=A9 2018-2020 Julien Lepiller ;;; Copyright =C2=A9 2018 Amin Bandali ;;; Copyright =C2=A9 2019 Nicolas Goaziou ;;; Copyright =C2=A9 2019 Steve Sprang @@ -69,6 +69,7 @@ #:use-module (guix build-system cmake) #:use-module (guix build-system glib-or-gtk) #:use-module (guix build-system gnu) + #:use-module (guix build-system ocaml) #:use-module (guix build-system python) #:use-module (guix build-system ruby) #:use-module (gnu packages algebra) @@ -80,11 +81,13 @@ #:use-module (gnu packages check) #:use-module (gnu packages cmake) #:use-module (gnu packages compression) + #:use-module (gnu packages coq) #:use-module (gnu packages curl) #:use-module (gnu packages cyrus-sasl) #:use-module (gnu packages dbm) #:use-module (gnu packages documentation) #:use-module (gnu packages elf) + #:use-module (gnu packages emacs) #:use-module (gnu packages file) #:use-module (gnu packages flex) #:use-module (gnu packages fltk) @@ -113,6 +116,7 @@ #:use-module (gnu packages mpi) #:use-module (gnu packages multiprecision) #:use-module (gnu packages netpbm) + #:use-module (gnu packages ocaml) #:use-module (gnu packages onc-rpc) #:use-module (gnu packages pcre) #:use-module (gnu packages popt) @@ -5970,3 +5974,64 @@ and conversions, physical constants, symbolic calcul= ations (including integrals and equations), arbitrary precision, uncertainty propagation, interval arithmetic, plotting.") (license license:gpl2+))) + +(define-public why3 + (package + (name "why3") + (version "1.3.1") + (source (origin + (method url-fetch) + (uri (string-append "https://gforge.inria.fr/frs/download.ph= p/file" + "/38291/why3-" version ".tar.gz")) + (sha256 + (base32 + "16zcrc60zz2j3gd3ww93z2z9x2jkxb3kr57y8i5rcgmacy7mw3bv")))) + (build-system ocaml-build-system) + (native-inputs + `(("coq" ,coq) + ("ocaml" ,ocaml) + ("which" ,which))) + (propagated-inputs + `(("camlzip" ,camlzip) + ("ocaml-graph" ,ocaml-graph) + ("ocaml-menhir" ,ocaml-menhir) + ("ocaml-num" ,ocaml-num) + ("ocaml-zarith" ,ocaml-zarith))) + (inputs + `(("coq-flocq" ,coq-flocq) + ("emacs-minimal" ,emacs-minimal) + ("zlib" ,zlib))) + (arguments + `(#:phases + (modify-phases %standard-phases + (add-before 'configure 'fix-configure + (lambda _ + (setenv "CONFIG_SHELL" (which "sh")) + (substitute* "configure" + ;; find ocaml-num in the correct directory + (("\\$DIR/nums.cma") "$DIR/../nums.cma") + (("\\$DIR/num.cmi") "$DIR/../num.cmi")) + #t)) + (add-after 'configure 'fix-makefile + (lambda _ + (substitute* "Makefile" + ;; find ocaml-num in the correct directory + (("site-lib/num") "site-lib")) + #t)) + (add-after 'install 'install-lib + (lambda _ + (invoke "make" "byte") + (invoke "make" "install-lib") + #t))))) + (home-page "http://why3.lri.fr") + (synopsis "Deductive program verification") + (description "Why3 provides a language for specification and programmi= ng, +called WhyML, and relies on external theorem provers, both automated and +interactive, to discharge verification conditions. Why3 comes with a stan= dard +library of logical theories (integer and real arithmetic, Boolean operatio= ns, +sets and maps, etc.) and basic programming data structures (arrays, queues, +hash tables, etc.). A user can write WhyML programs directly and get +correct-by-construction OCaml programs through an automated extraction +mechanism. WhyML is also used as an intermediate language for the verific= ation +of C, Java, or Ada programs.") + (license license:lgpl2.1))) --=20 2.28.0 --MP_/j7X1Bwt=V/zaysvKe+hHAY3 Content-Type: text/x-patch Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=0002-gnu-Add-frama-c.patch >From 408f2a6feffc8d86d0e3ff31b891614b160ed142 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Mon, 16 Dec 2019 12:40:18 +0100 Subject: [PATCH 2/2] gnu: Add frama-c. * gnu/packages/maths.scm (frama-c): New variable. --- gnu/packages/maths.scm | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index aa3d0da77c..a18d35504c 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -6035,3 +6035,41 @@ correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.") (license license:lgpl2.1))) + +(define-public frama-c + (package + (name "frama-c") + (version "21.1") + (source (origin + (method url-fetch) + (uri (string-append "http://frama-c.com/download/frama-c-" + version "-Scandium.tar.gz")) + (sha256 + (base32 + "0qq0d08dzr0dmdjysiimdqmwlzgnn932vp5kf8lfn3nl45ai09dy")))) + (build-system ocaml-build-system) + (arguments + `(#:tests? #f; no test target in Makefile + #:phases + (modify-phases %standard-phases + (add-before 'configure 'export-shell + (lambda* (#:key inputs #:allow-other-keys) + (setenv "CONFIG_SHELL" (string-append (assoc-ref inputs "bash") + "/bin/sh")) + #t))))) + (inputs + `(("gmp" ,gmp))) + (propagated-inputs + `(("ocaml-biniou" ,ocaml-biniou) + ("ocaml-easy-format" ,ocaml-easy-format) + ("ocaml-graph" ,ocaml-graph) + ("ocaml-yojson" ,ocaml-yojson) + ("ocaml-zarith" ,ocaml-zarith) + ("why3" ,why3))) + (home-page "http://frama-c.com") + (synopsis "C source code analysis platform") + (description "Frama-C is an extensible and collaborative platform dedicated +to source-code analysis of C software. The Frama-C analyzers assist you in +various source-code-related activities, from the navigation through unfamiliar +projects up to the certification of critical software.") + (license license:lgpl2.1+))) -- 2.28.0 --MP_/j7X1Bwt=V/zaysvKe+hHAY3-- From unknown Mon Jun 23 13:15:25 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#38635] [PATCH v3] Add why3 and frama-c Resent-From: Julien Lepiller Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Thu, 29 Apr 2021 20:40:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38635 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38635@debbugs.gnu.org Received: via spool by 38635-submit@debbugs.gnu.org id=B38635.16197287804245 (code B ref 38635); Thu, 29 Apr 2021 20:40:02 +0000 Received: (at 38635) by debbugs.gnu.org; 29 Apr 2021 20:39:40 +0000 Received: from localhost ([127.0.0.1]:56882 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lcDRd-00016J-1V for submit@debbugs.gnu.org; Thu, 29 Apr 2021 16:39:39 -0400 Received: from lepiller.eu ([89.234.186.109]:35752) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lcDRY-000165-DA for 38635@debbugs.gnu.org; Thu, 29 Apr 2021 16:39:31 -0400 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 34fb140d for <38635@debbugs.gnu.org>; Thu, 29 Apr 2021 20:39:24 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from :to:subject:message-id:in-reply-to:references:mime-version :content-type; s=dkim; bh=OvNYrtOaDDmQr2u8jmftkLpr8J9qEzzvJJZzGm pnU4g=; b=OcAu0brMsQj/3SMXCCQbQdCltCY3STEYjNAIH7EyrjNM6pwpEfQE/g 0s6a0fyqYiTzqfLOrm7R5wBgg/jk5VwSt3DbuujuQ7DinCA6tKfmek31TpmQ91fR r8nhih1M9BH5FPI1sFoiCzZ3V9K7g7cSYlvVxD73SL4JukKdh4dVvuFyvTU9fOmS nRa/skx26vZbOJsLtoZ6rzdSMQVnKuE96UPCTTao5emvSat1E0s7/BaRMwjXjY3H hgNp7eQiMG5W9rF8XD50DKXj8ZwZbMO7wg7vnLzzYn6/bYQSQzWOMU/W1lqsupgp KBsvTu64xWDBrRolQG/GzZRTg/SNUyNg== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 947ea0ef (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for <38635@debbugs.gnu.org>; Thu, 29 Apr 2021 20:39:24 +0000 (UTC) Date: Thu, 29 Apr 2021 22:39:18 +0200 From: Julien Lepiller Message-ID: <20210429223850.7659957a@tachikoma.lepiller.eu> In-Reply-To: <20200902150508.5c4a45e8@tachikoma.lepiller.eu> References: <20191216124626.048f0e43@sybil.lepiller.eu> <20200902150508.5c4a45e8@tachikoma.lepiller.eu> X-Mailer: Claws Mail 3.17.8 (GTK+ 2.24.32; x86_64-pc-linux-gnu) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="MP_/QzT+U_b0luleQBdJJK+jriZ" X-Spam-Score: -0.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: -1.0 (-) --MP_/QzT+U_b0luleQBdJJK+jriZ Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Disposition: inline Hi Guix! I updated my patches to the latest version of frama-c, and the issue is gone now! Frama-c is working, as long as ocaml is in the environment (because it's calling ocaml-findlib that needs an environment variable defined by the ocaml package). --MP_/QzT+U_b0luleQBdJJK+jriZ Content-Type: text/x-patch Content-Transfer-Encoding: quoted-printable Content-Disposition: attachment; filename=0001-gnu-Add-why3.patch =46rom 103afc0730fda2b27a103bc66f1ff283b7883e8b Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Mon, 16 Dec 2019 12:09:16 +0100 Subject: [PATCH 1/2] gnu: Add why3. * gnu/packages/maths.scm (why3): New variable. --- gnu/packages/maths.scm | 66 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 65 insertions(+), 1 deletion(-) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index a79e128955..a214b5d780 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -28,7 +28,7 @@ ;;; Copyright =C2=A9 2018 Adam Massmann ;;; Copyright =C2=A9 2018, 2020 Marius Bakke ;;; Copyright =C2=A9 2018 Eric Brown -;;; Copyright =C2=A9 2018 Julien Lepiller +;;; Copyright =C2=A9 2018, 2021 Julien Lepiller ;;; Copyright =C2=A9 2018 Amin Bandali ;;; Copyright =C2=A9 2019, 2021 Nicolas Goaziou ;;; Copyright =C2=A9 2019 Steve Sprang @@ -74,6 +74,7 @@ #:use-module (guix build-system cmake) #:use-module (guix build-system glib-or-gtk) #:use-module (guix build-system gnu) + #:use-module (guix build-system ocaml) #:use-module (guix build-system python) #:use-module (guix build-system ruby) #:use-module (gnu packages algebra) @@ -85,11 +86,13 @@ #:use-module (gnu packages check) #:use-module (gnu packages cmake) #:use-module (gnu packages compression) + #:use-module (gnu packages coq) #:use-module (gnu packages curl) #:use-module (gnu packages cyrus-sasl) #:use-module (gnu packages dbm) #:use-module (gnu packages documentation) #:use-module (gnu packages elf) + #:use-module (gnu packages emacs) #:use-module (gnu packages file) #:use-module (gnu packages flex) #:use-module (gnu packages fltk) @@ -6190,3 +6193,64 @@ and conversions, physical constants, symbolic calcul= ations (including integrals and equations), arbitrary precision, uncertainty propagation, interval arithmetic, plotting.") (license license:gpl2+))) + +(define-public why3 + (package + (name "why3") + (version "1.3.1") + (source (origin + (method url-fetch) + (uri (string-append "https://gforge.inria.fr/frs/download.ph= p/file" + "/38291/why3-" version ".tar.gz")) + (sha256 + (base32 + "16zcrc60zz2j3gd3ww93z2z9x2jkxb3kr57y8i5rcgmacy7mw3bv")))) + (build-system ocaml-build-system) + (native-inputs + `(("coq" ,coq) + ("ocaml" ,ocaml) + ("which" ,which))) + (propagated-inputs + `(("camlzip" ,camlzip) + ("ocaml-graph" ,ocaml-graph) + ("ocaml-menhir" ,ocaml-menhir) + ("ocaml-num" ,ocaml-num) + ("ocaml-zarith" ,ocaml-zarith))) + (inputs + `(("coq-flocq" ,coq-flocq) + ("emacs-minimal" ,emacs-minimal) + ("zlib" ,zlib))) + (arguments + `(#:phases + (modify-phases %standard-phases + (add-before 'configure 'fix-configure + (lambda _ + (setenv "CONFIG_SHELL" (which "sh")) + (substitute* "configure" + ;; find ocaml-num in the correct directory + (("\\$DIR/nums.cma") "$DIR/../nums.cma") + (("\\$DIR/num.cmi") "$DIR/../num.cmi")) + #t)) + (add-after 'configure 'fix-makefile + (lambda _ + (substitute* "Makefile" + ;; find ocaml-num in the correct directory + (("site-lib/num") "site-lib")) + #t)) + (add-after 'install 'install-lib + (lambda _ + (invoke "make" "byte") + (invoke "make" "install-lib") + #t))))) + (home-page "http://why3.lri.fr") + (synopsis "Deductive program verification") + (description "Why3 provides a language for specification and programmi= ng, +called WhyML, and relies on external theorem provers, both automated and +interactive, to discharge verification conditions. Why3 comes with a stan= dard +library of logical theories (integer and real arithmetic, Boolean operatio= ns, +sets and maps, etc.) and basic programming data structures (arrays, queues, +hash tables, etc.). A user can write WhyML programs directly and get +correct-by-construction OCaml programs through an automated extraction +mechanism. WhyML is also used as an intermediate language for the verific= ation +of C, Java, or Ada programs.") + (license license:lgpl2.1))) --=20 2.26.3 --MP_/QzT+U_b0luleQBdJJK+jriZ Content-Type: text/x-patch Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=0002-gnu-Add-frama-c.patch >From 431dc3f0212c53b60f075e4e2719531f2ad4d84a Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Mon, 16 Dec 2019 12:40:18 +0100 Subject: [PATCH 2/2] gnu: Add frama-c. * gnu/packages/maths.scm (frama-c): New variable. --- gnu/packages/maths.scm | 47 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index a214b5d780..49a3fd3904 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -6254,3 +6254,50 @@ correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.") (license license:lgpl2.1))) + +(define-public frama-c + (package + (name "frama-c") + (version "22.0") + (source (origin + (method url-fetch) + (uri (string-append "http://frama-c.com/download/frama-c-" + version "-Titanium.tar.gz")) + (sha256 + (base32 + "1mq1fijka95ydrla486yr4w6wdl9l7vmp512s1q00b0p6lmfwmkh")))) + (build-system ocaml-build-system) + (arguments + `(#:tests? #f; no test target in Makefile + #:phases + (modify-phases %standard-phases + (add-before 'configure 'export-shell + (lambda* (#:key inputs #:allow-other-keys) + (setenv "CONFIG_SHELL" (string-append (assoc-ref inputs "bash") + "/bin/sh")) + #t))))) + (inputs + `(("gmp" ,gmp))) + (propagated-inputs + `(("ocaml-biniou" ,ocaml-biniou) + ("ocaml-easy-format" ,ocaml-easy-format) + ("ocaml-graph" ,ocaml-graph) + ("ocaml-yojson" ,ocaml-yojson) + ("ocaml-zarith" ,ocaml-zarith) + ("why3" ,why3))) + (native-search-paths + (list (search-path-specification + (variable "FRAMAC_SHARE") + (files '("share/frama-c")) + (separator #f)) + (search-path-specification + (variable "FRAMAC_LIB") + (files '("lib/frama-c")) + (separator #f)))) + (home-page "http://frama-c.com") + (synopsis "C source code analysis platform") + (description "Frama-C is an extensible and collaborative platform dedicated +to source-code analysis of C software. The Frama-C analyzers assist you in +various source-code-related activities, from the navigation through unfamiliar +projects up to the certification of critical software.") + (license license:lgpl2.1+))) -- 2.26.3 --MP_/QzT+U_b0luleQBdJJK+jriZ-- From unknown Mon Jun 23 13:15:25 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#38635: closed (Re: [bug#38635] [PATCH v3] Add why3 and frama-c) Message-ID: References: <20210602031145.17815d14@tachikoma.lepiller.eu> <20191216124626.048f0e43@sybil.lepiller.eu> X-Gnu-PR-Message: they-closed 38635 X-Gnu-PR-Package: guix-patches X-Gnu-PR-Keywords: patch Reply-To: 38635@debbugs.gnu.org Date: Wed, 02 Jun 2021 01:12:02 +0000 Content-Type: multipart/mixed; boundary="----------=_1622596322-29893-1" This is a multi-part message in MIME format... ------------=_1622596322-29893-1 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Your bug report #38635: [WIP PATCH] Add why3 and frama-c 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 38635@debbugs.gnu.org. --=20 38635: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D38635 GNU Bug Tracking System Contact help-debbugs@gnu.org with problems ------------=_1622596322-29893-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at 38635-done) by debbugs.gnu.org; 2 Jun 2021 01:11:58 +0000 Received: from localhost ([127.0.0.1]:38218 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1loFQM-0007ls-4o for submit@debbugs.gnu.org; Tue, 01 Jun 2021 21:11:58 -0400 Received: from lepiller.eu ([89.234.186.109]:39082) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1loFQJ-0007lf-J1 for 38635-done@debbugs.gnu.org; Tue, 01 Jun 2021 21:11:56 -0400 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id e3ed5f5e for <38635-done@debbugs.gnu.org>; Wed, 2 Jun 2021 01:11:53 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from :to:subject:message-id:in-reply-to:references:mime-version :content-type:content-transfer-encoding; s=dkim; bh=47wKTgR4avHp cTlA3y2HSWLhhFvZFnnOkeRlA7DHJpM=; b=E1SR7GVRJWEIP0nccHtuwdGo3/C3 18KDXQttQ/QCYDbkaUErmmHyD1fow+Xwrq8d+wxeGZ474UWwagTRPQg4lMQqucnO c+rHho0wrSkyK3/z2bXoM9l8E7rltdk5xdUGO1Zz/OOl6z9QWc4Mqli2WwiVgn3S dLCOA2swyONb9DyaMeO1j0gr05aBC1WYPYjyrD2fMlKF4bkSaU/szHAuVoRts27G ad1JJmufpcBzWYt+2pBk8M1kZk09IRBlvEzAn4wSIlaTXamzMUdRXe/UPZQ9oBu0 12fnkdz4NZHXI0N+4wbbA2FA13WF/d1zZYzkCtNG4jyhXgQZGFwSpkasgA== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 686f1441 (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for <38635-done@debbugs.gnu.org>; Wed, 2 Jun 2021 01:11:53 +0000 (UTC) Date: Wed, 2 Jun 2021 03:11:45 +0200 From: Julien Lepiller To: 38635-done@debbugs.gnu.org Subject: Re: [bug#38635] [PATCH v3] Add why3 and frama-c Message-ID: <20210602031145.17815d14@tachikoma.lepiller.eu> In-Reply-To: <20210429223850.7659957a@tachikoma.lepiller.eu> References: <20191216124626.048f0e43@sybil.lepiller.eu> <20200902150508.5c4a45e8@tachikoma.lepiller.eu> <20210429223850.7659957a@tachikoma.lepiller.eu> X-Mailer: Claws Mail 3.17.8 (GTK+ 2.24.32; x86_64-pc-linux-gnu) MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 38635-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: -1.0 (-) After more than a month without a reply, I pushed to master as c9b3627d566bde6b60841185f147589df45e65eb and b94bc3ea30a9451f9019cca66ac20f585870eecd. Thanks! ------------=_1622596322-29893-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at submit) by debbugs.gnu.org; 16 Dec 2019 11:46:55 +0000 Received: from localhost ([127.0.0.1]:38021 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1igops-0000SK-I1 for submit@debbugs.gnu.org; Mon, 16 Dec 2019 06:46:55 -0500 Received: from lists.gnu.org ([209.51.188.17]:40216) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1igopo-0000S8-8b for submit@debbugs.gnu.org; Mon, 16 Dec 2019 06:46:47 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:38578) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1igopl-00074D-HF for guix-patches@gnu.org; Mon, 16 Dec 2019 06:46:43 -0500 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,URIBL_BLOCKED autolearn=disabled version=3.3.2 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1igopj-0005nV-DS for guix-patches@gnu.org; Mon, 16 Dec 2019 06:46:41 -0500 Received: from lepiller.eu ([2a00:5884:8208::1]:53012) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1igopi-0005NQ-NW for guix-patches@gnu.org; Mon, 16 Dec 2019 06:46:39 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 33b55185 for ; Mon, 16 Dec 2019 11:46:33 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=lepiller.eu; h=date:from :to:subject:message-id:mime-version:content-type; s=dkim; bh=ddC qRIHwitAK5b9ZvZVzjbVLBok=; b=A0myiVpuP6LjBaE5ouQb2+t8Lptf+cKZsO+ N8x4Okk14XwRlrB5RBclMBNcC8cQK2xOaPFMbtCz1w4bYqKb3azUbrGeAVhxweZE lfiM4SsIV4bpCSwsWdgn/oUsDr9e6UEYSWaufwob7lQHVRFSeUX2xDfirl2inzua vSCZQH+cbPT8Yom/wfGopkTJ+S/eA1DRIbeDXglbt5FYrv/WUA4tnaWNs7jVq/+4 xfX/P4q7XIF5QIFc3yq9rgCREjY+sW2LsYTZw+Asw6169ZnmF4xqD9dFG728f0GR ZJ9cH/cwbatM/jdwml2thC2ITbLqB6/1lTFmeHkmZmMOxSqgs/w== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id a163384c (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for ; Mon, 16 Dec 2019 11:46:33 +0000 (UTC) Date: Mon, 16 Dec 2019 12:46:26 +0100 From: Julien Lepiller To: guix-patches@gnu.org Subject: [WIP PATCH] Add why3 and frama-c Message-ID: <20191216124626.048f0e43@sybil.lepiller.eu> X-Mailer: Claws Mail 3.17.4 (GTK+ 2.24.32; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="MP_/u3+3XpCQJFzg+CVZkdv/T/7" X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 2a00:5884:8208::1 X-Spam-Score: -2.3 (--) 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: -1.0 (-) --MP_/u3+3XpCQJFzg+CVZkdv/T/7 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Disposition: inline Hi Guix! Since there was some interest very recently, I took another look at my incomplete why3 and frama-c packages. I updated them and polished them a little. I encourage formal-method guixers to test these patches, especially if you are a user of why3 or frama-c, because I'm not sure how these tools are supposed to be working. Note that I didn't include ide support in why3 because this adds ~1GiB to the closure of the program. A good thing could be to separate the why3 library (not required when using why3) from the main package, in a separate output. For some reason, frama-c doesn't work directly, it needs to be in an environment where its dependencies are present, hence the propagation. However, it's failing at runtime: $ guix environment --ad-hoc frama-c ocaml ocaml-findlib [env]$ frama-c --help [kernel] User Error: cannot load plug-in 'zip': cannot load module Details: error loading shared library: /gnu/store/hsjnvq5li28ak2wjnwlmqsfbg246skcg-profile/lib/ocaml/site-lib/zip/zip.cmxa: invalid ELF header [kernel] User Error: cannot load plug-in 'why3': cannot load module Details: error loading shared library: /gnu/store/hsjnvq5li28ak2wjnwlmqsfbg246skcg-profile/lib/ocaml/site-lib/why3/why3.cmxs: undefined symbol: camlGzip [kernel] User Error: cannot load plug-in 'frama-c-wp': cannot load module Details: error loading shared library: /gnu/store/daqn9vsc15j3slbalw2fag6amndv8x98-frama-c-20.0/lib/frama-c/plugins/top/Wp.cmxs: undefined symbol: camlWhy3__Theory [kernel] User Error: Deferred error message was emitted during execution. See above messages for more information. [kernel] Frama-C aborted: invalid user input. --MP_/u3+3XpCQJFzg+CVZkdv/T/7 Content-Type: text/x-patch Content-Transfer-Encoding: quoted-printable Content-Disposition: attachment; filename=0001-gnu-Add-why3.patch =46rom 9fc13943b29196763524ddbc247218398d889459 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Mon, 16 Dec 2019 12:09:16 +0100 Subject: [PATCH 1/2] gnu: Add why3. * gnu/packages/maths.scm (why3): New variable. --- gnu/packages/maths.scm | 67 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 66 insertions(+), 1 deletion(-) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 0ed61ad4a1..991f164737 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -28,7 +28,7 @@ ;;; Copyright =C2=A9 2018 Adam Massmann ;;; Copyright =C2=A9 2018 Marius Bakke ;;; Copyright =C2=A9 2018 Eric Brown -;;; Copyright =C2=A9 2018 Julien Lepiller +;;; Copyright =C2=A9 2018, 2019 Julien Lepiller ;;; Copyright =C2=A9 2018 Amin Bandali ;;; Copyright =C2=A9 2019 Nicolas Goaziou ;;; Copyright =C2=A9 2019 Steve Sprang @@ -61,6 +61,7 @@ #:use-module ((guix build utils) #:select (alist-replace)) #:use-module (guix build-system cmake) #:use-module (guix build-system gnu) + #:use-module (guix build-system ocaml) #:use-module (guix build-system python) #:use-module (guix build-system ruby) #:use-module (gnu packages algebra) @@ -72,10 +73,12 @@ #:use-module (gnu packages check) #:use-module (gnu packages cmake) #:use-module (gnu packages compression) + #:use-module (gnu packages coq) #:use-module (gnu packages curl) #:use-module (gnu packages cyrus-sasl) #:use-module (gnu packages documentation) #:use-module (gnu packages elf) + #:use-module (gnu packages emacs) #:use-module (gnu packages flex) #:use-module (gnu packages fltk) #:use-module (gnu packages fontutils) @@ -101,6 +104,7 @@ #:use-module (gnu packages mpi) #:use-module (gnu packages multiprecision) #:use-module (gnu packages netpbm) + #:use-module (gnu packages ocaml) #:use-module (gnu packages onc-rpc) #:use-module (gnu packages pcre) #:use-module (gnu packages popt) @@ -4182,6 +4186,67 @@ as equations, scalars, vectors, and matrices.") theories} (SMT) solver. It provides a C/C++ API, as well as Python bindin= gs.") (license license:expat))) =20 +(define-public why3 + (package + (name "why3") + (version "1.2.1") + (source (origin + (method url-fetch) + (uri (string-append "https://gforge.inria.fr/frs/download.ph= p/file" + "/38185/why3-" version ".tar.gz")) + (sha256 + (base32 + "014gkwisjp05x3342zxkryb729p02ngx1hcjjsrplpa53jzgz647")))) + (build-system ocaml-build-system) + (native-inputs + `(("coq" ,coq) + ("ocaml" ,ocaml) + ("which" ,which))) + (propagated-inputs + `(("camlzip" ,camlzip) + ("ocaml-graph" ,ocaml-graph) + ("ocaml-menhir" ,ocaml-menhir) + ("ocaml-num" ,ocaml-num) + ("ocaml-zarith" ,ocaml-zarith))) + (inputs + `(("coq-flocq" ,coq-flocq) + ("emacs-minimal" ,emacs-minimal) + ("zlib" ,zlib))) + (arguments + `(#:phases + (modify-phases %standard-phases + (add-before 'configure 'fix-configure + (lambda _ + (setenv "CONFIG_SHELL" (which "sh")) + (substitute* "configure" + ;; find ocaml-num in the correct directory + (("\\$DIR/nums.cma") "$DIR/../nums.cma") + (("\\$DIR/num.cmi") "$DIR/../num.cmi")) + #t)) + (add-after 'configure 'fix-makefile + (lambda _ + (substitute* "Makefile" + ;; find ocaml-num in the correct directory + (("site-lib/num") "site-lib")) + #t)) + (add-after 'install 'install-lib + (lambda _ + (invoke "make" "byte") + (invoke "make" "install-lib") + #t))))) + (home-page "http://why3.lri.fr") + (synopsis "Deductive program verification") + (description "Why3 provides a language for specification and programmi= ng, +called WhyML, and relies on external theorem provers, both automated and +interactive, to discharge verification conditions. Why3 comes with a stan= dard +library of logical theories (integer and real arithmetic, Boolean operatio= ns, +sets and maps, etc.) and basic programming data structures (arrays, queues, +hash tables, etc.). A user can write WhyML programs directly and get +correct-by-construction OCaml programs through an automated extraction +mechanism. WhyML is also used as an intermediate language for the verific= ation +of C, Java, or Ada programs.") + (license license:lgpl2.1))) + (define-public elpa (package (name "elpa") --=20 2.24.0 --MP_/u3+3XpCQJFzg+CVZkdv/T/7 Content-Type: text/x-patch Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=0002-gnu-Add-frama-c.patch >From f9501f1cc5725d49c69c948f6f7cc70c13f1dbdc Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Mon, 16 Dec 2019 12:40:18 +0100 Subject: [PATCH 2/2] gnu: Add frama-c. * gnu/packages/maths.scm (frama-c): New variable. --- gnu/packages/maths.scm | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 991f164737..d4e3e74c98 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -4247,6 +4247,44 @@ mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.") (license license:lgpl2.1))) +(define-public frama-c + (package + (name "frama-c") + (version "20.0") + (source (origin + (method url-fetch) + (uri (string-append "http://frama-c.com/download/frama-c-" + version "-Calcium.tar.gz")) + (sha256 + (base32 + "03dvn162djylj2skmk6vv75gh87mm4s5cspkzcrlm5x0rlla2yqn")))) + (build-system ocaml-build-system) + (arguments + `(#:tests? #f; no test target in Makefile + #:phases + (modify-phases %standard-phases + (add-before 'configure 'export-shell + (lambda* (#:key inputs #:allow-other-keys) + (setenv "CONFIG_SHELL" (string-append (assoc-ref inputs "bash") + "/bin/sh")) + #t))))) + (inputs + `(("gmp" ,gmp))) + (propagated-inputs + `(("ocaml-biniou" ,ocaml-biniou) + ("ocaml-easy-format" ,ocaml-easy-format) + ("ocaml-graph" ,ocaml-graph) + ("ocaml-yojson" ,ocaml-yojson) + ("ocaml-zarith" ,ocaml-zarith) + ("why3" ,why3))) + (home-page "http://frama-c.com") + (synopsis "C source code analysis platform") + (description "Frama-C is an extensible and collaborative platform dedicated +to source-code analysis of C software. The Frama-C analyzers assist you in +various source-code-related activities, from the navigation through unfamiliar +projects up to the certification of critical software.") + (license license:lgpl2.1+))) + (define-public elpa (package (name "elpa") -- 2.24.0 --MP_/u3+3XpCQJFzg+CVZkdv/T/7-- ------------=_1622596322-29893-1--