Search code examples
frama-copam

Error installing Frama-C with opam (Ubuntu 14.04 LTS)

Trying to install Frama-C with the recommended opam method gives the following error:

### stdout ###
# Cleaning     Installation directory
# Installing   WP shared files
### stderr ###
# /bin/sh: 1: src/plugins/wp/share/instwp: not found
# make: *** [src/plugins/wp/Makefile:355: install] Error 127

here are the commands used:

# install opam
$ wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin
# configure opam
$ eval `opam config env`
$ opam config setup -a
# install frama-c
$ opam install frama-c-base

Edit: here is the output of opam install -v frama-c-base: https://pastebin.com/eMH08ugA

Edit2: the system in question is running Linux Mint 17.3 (Ubuntu 14.04 LTS upstream); the Ubuntu package in the software repository is Make 3.81 (untested) although this had already been upgraded to Make 4.2 when this bug was encountered

Solution

  • I was able to reproduce the issue, and the culprit seems to be Make 4.2, due to this bug in particular:

    bug #44742: Double-dep with double-colon rule not built [in parallel builds]

    Several rules in Frama-C makefiles use double-colon, and by default the -j%{jobs}% is set in the opam Frama-C file to speed up the compilation.

    Unfortunately, it seems that the combination of these two results in the instwp file (among others) not being built, despite its rule being present in the WP makefile, when using that specific version of Make.

    I am using Make 4.2.1 by default and I do not have that issue (all files are produced as expected and make install succeeds). If I manually compile Frama-C without -j, I also do not have the issue.

    If you are unable to update your version of Make, you could try using opam install -j 1 frama-c, which should override the jobs variable and disable parallel compilation of Frama-C, thus avoiding the error.

    Still, my general recommendations would be:

    1. Install a newer OCaml (4.02.3 at least, it should be compatible will almost every package available in OCaml 4.02.1) to ensure the most recent release of Frama-C will be available (Frama-C Silicon is not available in OCaml 4.02.1);

    2. If you can, install frama-c itself, and not frama-c-base, since the only difference are the required packages, namely those for the GUI. You may want to do the following before running opam install frama-c:

      opam install depext
opam depext frama-c

      The first line will install depext, which is able to find external dependencies for your distribution, and the second line will apply depext to Frama-C, thus prompting you to install external dependencies available in your distribution.