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

[Brett Gilio <brettg@gnu.org>]

Julien Lepiller <julien@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@gnu.org> <brettg@posteo.net>