From debbugs-submit-bounces@debbugs.gnu.org Wed Dec 25 02:01:58 2019 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 To: Julien Lepiller Subject: Re: [bug#38635] [WIP PATCH] Add why3 and frama-c 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-Debbugs-Envelope-To: 38635 Cc: bandali@gnu.org, 38635@debbugs.gnu.org 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]