GNU bug report logs - #38635
[WIP PATCH] Add why3 and frama-c

Previous Next

Package: guix-patches;

Reported by: Julien Lepiller <julien <at> lepiller.eu>

Date: Mon, 16 Dec 2019 11:47:02 UTC

Severity: normal

Tags: patch

Done: Julien Lepiller <julien <at> lepiller.eu>

Bug is archived. No further changes may be made.

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 38635 in the body.
You can then email your comments to 38635 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

View this report as an mbox folder, status mbox, maintainer mbox


Report forwarded to guix-patches <at> gnu.org:
bug#38635; Package guix-patches. (Mon, 16 Dec 2019 11:47:02 GMT) Full text and rfc822 format available.

Acknowledgement sent to Julien Lepiller <julien <at> lepiller.eu>:
New bug report received and forwarded. Copy sent to guix-patches <at> gnu.org. (Mon, 16 Dec 2019 11:47:02 GMT) Full text and rfc822 format available.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: guix-patches <at> gnu.org
Subject: [WIP PATCH] Add why3 and frama-c
Date: Mon, 16 Dec 2019 12:46:26 +0100
[Message part 1 (text/plain, 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.
[0001-gnu-Add-why3.patch (text/x-patch, attachment)]
[0002-gnu-Add-frama-c.patch (text/x-patch, attachment)]

Information forwarded to guix-patches <at> gnu.org:
bug#38635; Package guix-patches. (Wed, 25 Dec 2019 07:02:02 GMT) Full text and rfc822 format available.

Message #8 received at 38635 <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: bandali <at> gnu.org, 38635 <at> debbugs.gnu.org
Subject: Re: [bug#38635] [WIP PATCH] Add why3 and frama-c
Date: Wed, 25 Dec 2019 01:01:56 -0600
Julien Lepiller <julien <at> lepiller.eu> 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]
<brettg <at> gnu.org> <brettg <at> posteo.net>




Information forwarded to guix-patches <at> gnu.org:
bug#38635; Package guix-patches. (Wed, 02 Sep 2020 13:06:02 GMT) Full text and rfc822 format available.

Message #11 received at 38635 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: 38635 <at> debbugs.gnu.org
Subject: [WIP PATCH v2] Add why3 and frama-c
Date: Wed, 2 Sep 2020 15:05:30 +0200
[Message part 1 (text/plain, 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.
[0001-gnu-Add-why3.patch (text/x-patch, attachment)]
[0002-gnu-Add-frama-c.patch (text/x-patch, attachment)]

Information forwarded to guix-patches <at> gnu.org:
bug#38635; Package guix-patches. (Thu, 29 Apr 2021 20:40:02 GMT) Full text and rfc822 format available.

Message #14 received at 38635 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: 38635 <at> debbugs.gnu.org
Subject: Re: [bug#38635] [PATCH v3] Add why3 and frama-c
Date: Thu, 29 Apr 2021 22:39:18 +0200
[Message part 1 (text/plain, 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).
[0001-gnu-Add-why3.patch (text/x-patch, attachment)]
[0002-gnu-Add-frama-c.patch (text/x-patch, attachment)]

Reply sent to Julien Lepiller <julien <at> lepiller.eu>:
You have taken responsibility. (Wed, 02 Jun 2021 01:12:01 GMT) Full text and rfc822 format available.

Notification sent to Julien Lepiller <julien <at> lepiller.eu>:
bug acknowledged by developer. (Wed, 02 Jun 2021 01:12:02 GMT) Full text and rfc822 format available.

Message #19 received at 38635-done <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: 38635-done <at> debbugs.gnu.org
Subject: Re: [bug#38635] [PATCH v3] Add why3 and frama-c
Date: Wed, 2 Jun 2021 03:11:45 +0200
After more than a month without a reply, I pushed to master as
c9b3627d566bde6b60841185f147589df45e65eb and
b94bc3ea30a9451f9019cca66ac20f585870eecd. Thanks!




bug archived. Request was from Debbugs Internal Request <help-debbugs <at> gnu.org> to internal_control <at> debbugs.gnu.org. (Wed, 30 Jun 2021 11:24:05 GMT) Full text and rfc822 format available.

This bug report was last modified 2 years and 272 days ago.

Previous Next


GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.