Frama-C Bug Tracking System - Frama-C
View Issue Details
0002468Frama-COpampublic2019-07-26 16:162020-02-17 18:08
Assigned Tomaroneze 
PlatformMacbook ProOSOS X MojaveOS Version10.14.5
Product VersionFrama-C 19-Potassium 
Target VersionFixed in VersionFrama-C 20-Calcium 
Summary0002468: opam fails to install frama-c
Description ~> opam install frama-c
The following dependencies couldn't be met:
  - frama-c → frama-c-base → ocaml < 4.06
      base of this switch (use `--unlock-base' to force)
  - frama-c → ocaml < 4.08.0
      base of this switch (use `--unlock-base' to force)

No solution found, exiting
Steps To ReproduceFollowed instructions on
after doing update/upgraders for both brew and opam - opam and Ocaml already installed.

Attached file shows complete OS X Terminal transcript
TagsNo tags attached.
Attached Filestxt 2019-07-26-frama-c-install-fail.txt (90,442) 2019-07-26 16:16
txt 2019-07-26-retry-after-switch-4-06-1.txt (13,056) 2019-07-26 17:47
txt 2019-07-26-retry-after-caveats.txt (2,538) 2019-07-26 17:52

Victor Sverdlin   
2019-07-26 16:19   
opam switch create 4.06.1
opam install farma-c
2019-07-26 16:28   
I'll try reproducing the issue on my Macbook, but opam constraints are sometimes fiddly. Could you please provide the versions of opam and ocaml that you have (`opam --version` and `ocaml --version`)? Either they do not appear in your log, or I missed them.
2019-07-26 16:31   
I am trying the switch suggestion to 4.06.1 at present,
so ocaml is currently not available.

opam is version 2.0.4
2019-07-26 16:39   
I ran 'opam install frame-c' after the switch, and 'eval $(whatever)' with OCaml 4.06.1
Things are better, but its seems I need to install gtksourceview, libgnomecanvas, and libxml2

I tried this with brew, but it says they are already installed!

So I did brew reinstall - I get warnings about libxml2 being "keg only" because it interacts badly with the OS X version.

I then tried to re-install frama-c - it fails
2019-07-26 17:31   
The keg-only issue with libxml2 should not be an issue, I also have this warning and it works for me.

gtksourceview and libgnomecanvas are necessary for the graphical interface, but indeed, once installed with brew, after switching the OCaml version, opam only needs to install `conf-*` packages, which check that the underlying C packages are installed. These are automatically installed as dependencies when running `opam install frama-c`, so that shouldn't be a problem.

Do you know which Frama-C plug-ins you intend to use? For instance, Coq is used by WP but not Eva, so depending on your interests, you could try skipping the installation of coq (if it is causing issues) and doing `opam install frama-c` directly.

Now, I just tried installing 4.06.1 and then frama-c, and I got this error:

# Package 'libffi', required by 'gobject-2.0', not found

Is it the same one that you are having? This prevents conf-gtksourceview from being installed.

Apparently the libffi issue is somewhat recurrent on macOS (I found several github mentions), I will see if I can find a solution. In any case, if you have a different error message, please post it so we can further investigate it.
2019-07-26 17:38   
(Last edited: 2019-07-26 17:39)
Ok, so I had actually missed the message about libffi, which is necessary for conf-gtksourceview:

==> Caveats
libffi is keg-only, which means it was not symlinked into /usr/local,
because some formulae require a newer version of libffi.

For compilers to find libffi you may need to set:
  export LDFLAGS="-L/usr/local/opt/libffi/lib"

For pkg-config to find libffi you may need to set:
  export PKG_CONFIG_PATH="/usr/local/opt/libffi/lib/pkgconfig"

After adding these lines, running `opam install conf-gtksourceview` (or `opam install frama-c` directly) works.

The way I found out was by looking at the error message of opam, as mentioned before, then reinstalling libffi (`brew reinstall libffi`). It was already installed, but the reinstallation displayed the caveat, so I did as indicated and it worked.

If this was your error, please try it and report back, or post the error message you are having.

We will consider updating the installation instructions, however these dependent package issues change often and it's hard to keep track of them all.

2019-07-26 17:48   
just loaded the log of the failure after the switch to 4.06.1
Currently trying your most recent suggestion
2019-07-26 17:52   
That worked - both frama-c and frama-c-gui are running - I'll upload the log of this build in case it is helpful to you
2019-07-26 18:05   
(Last edited: 2019-07-26 18:15)
Good to know!

I don't think the log will be necessary, it seems to be very similar to what I got in my machine.

The first issue you had was due to the OCaml version, either you had a too recent OCaml (4.08), or a too old one (< 4.05), and in both cases opam does not report a very intuitive error message.

The second issue was due to libffi, which did not happen at the time the instructions were written, at least with OCaml 4.05.0.

In both cases, I hope Google will index this issue so other people will find it if they have the same problem. We'll update the installation instructions to provide more details about it.

2019-07-26 19:13   
Thanks very much for your prompt help - much appreciated!
2019-08-21 16:14   
Updated to-be-released to include a few more details about Homebrew installation.
2020-02-17 18:08   
Fixed in Frama-C 20.0 (Calcium).

Issue History
2019-07-26 16:16abutterfieldNew Issue
2019-07-26 16:16abutterfieldStatusnew => assigned
2019-07-26 16:16abutterfieldAssigned To => maroneze
2019-07-26 16:16abutterfieldFile Added: 2019-07-26-frama-c-install-fail.txt
2019-07-26 16:19Victor SverdlinNote Added: 0006828
2019-07-26 16:25maronezeAssigned Tomaroneze =>
2019-07-26 16:26maronezeAssigned To => maroneze
2019-07-26 16:28maronezeNote Added: 0006829
2019-07-26 16:31abutterfieldNote Added: 0006830
2019-07-26 16:39abutterfieldNote Added: 0006831
2019-07-26 17:31maronezeNote Added: 0006832
2019-07-26 17:38maronezeNote Added: 0006833
2019-07-26 17:39maronezeNote Edited: 0006833bug_revision_view_page.php?bugnote_id=6833#r407
2019-07-26 17:39maronezeNote Edited: 0006833bug_revision_view_page.php?bugnote_id=6833#r408
2019-07-26 17:47abutterfieldFile Added: 2019-07-26-retry-after-switch-4-06-1.txt
2019-07-26 17:48abutterfieldNote Added: 0006834
2019-07-26 17:52abutterfieldNote Added: 0006835
2019-07-26 17:52abutterfieldFile Added: 2019-07-26-retry-after-caveats.txt
2019-07-26 18:05maronezeNote Added: 0006836
2019-07-26 18:15maronezeNote Edited: 0006836bug_revision_view_page.php?bugnote_id=6836#r410
2019-07-26 19:13abutterfieldNote Added: 0006837
2019-08-21 16:14maronezeNote Added: 0006844
2019-08-21 16:14maronezeStatusassigned => resolved
2019-08-21 16:14maronezeFixed in Version => Frama-C 20-Calcium
2019-08-21 16:14maronezeResolutionopen => fixed
2020-02-17 18:08signolesStatusresolved => closed
2020-02-17 18:08signolesNote Added: 0006954