From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:470:142:3::10]:38887) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1igoq8-0007Qb-BK for guix-patches@gnu.org; Mon, 16 Dec 2019 06:47:06 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1igoq6-0007Ty-Ff for guix-patches@gnu.org; Mon, 16 Dec 2019 06:47:04 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:60281) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1igoq6-0007SV-BJ for guix-patches@gnu.org; Mon, 16 Dec 2019 06:47:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1igoq6-0000Sn-8X for guix-patches@gnu.org; Mon, 16 Dec 2019 06:47:02 -0500 Subject: [bug#38635] [WIP PATCH] Add why3 and frama-c Resent-Message-ID: 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 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) 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> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="MP_/u3+3XpCQJFzg+CVZkdv/T/7" List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: 38635@debbugs.gnu.org --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--