Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
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 file icon 2019-07-26-frama-c-install-fail.txt [^] (90,442 bytes) 2019-07-26 16:16 [Show Content]
txt file icon 2019-07-26-retry-after-switch-4-06-1.txt [^] (13,056 bytes) 2019-07-26 17:47 [Show Content]
txt file icon 2019-07-26-retry-after-caveats.txt [^] (2,538 bytes) 2019-07-26 17:52 [Show Content]

- Relationships

-  Notes
Victor Sverdlin (reporter)
2019-07-26 16:19

Try: opam switch create 4.06.1 then opam install farma-c
maroneze (administrator)
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.
abutterfield (reporter)
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
abutterfield (reporter)
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
maroneze (administrator)
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.
maroneze (administrator)
2019-07-26 17:38
edited on: 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.
abutterfield (reporter)
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
abutterfield (reporter)
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
maroneze (administrator)
2019-07-26 18:05
edited on: 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.
abutterfield (reporter)
2019-07-26 19:13

Thanks very much for your prompt help - much appreciated!
maroneze (administrator)
2019-08-21 16:14

Updated to-be-released to include a few more details about Homebrew installation.
signoles (manager)
2020-02-17 18:08

Fixed in Frama-C 20.0 (Calcium).

- Issue History
Date Modified Username Field Change
2019-07-26 16:16 abutterfield New Issue
2019-07-26 16:16 abutterfield Status new => assigned
2019-07-26 16:16 abutterfield Assigned To => maroneze
2019-07-26 16:16 abutterfield File Added: 2019-07-26-frama-c-install-fail.txt
2019-07-26 16:19 Victor Sverdlin Note Added: 0006828
2019-07-26 16:25 maroneze Assigned To maroneze =>
2019-07-26 16:26 maroneze Assigned To => maroneze
2019-07-26 16:28 maroneze Note Added: 0006829
2019-07-26 16:31 abutterfield Note Added: 0006830
2019-07-26 16:39 abutterfield Note Added: 0006831
2019-07-26 17:31 maroneze Note Added: 0006832
2019-07-26 17:38 maroneze Note Added: 0006833
2019-07-26 17:39 maroneze Note Edited: 0006833 View Revisions
2019-07-26 17:39 maroneze Note Edited: 0006833 View Revisions
2019-07-26 17:47 abutterfield File Added: 2019-07-26-retry-after-switch-4-06-1.txt
2019-07-26 17:48 abutterfield Note Added: 0006834
2019-07-26 17:52 abutterfield Note Added: 0006835
2019-07-26 17:52 abutterfield File Added: 2019-07-26-retry-after-caveats.txt
2019-07-26 18:05 maroneze Note Added: 0006836
2019-07-26 18:15 maroneze Note Edited: 0006836 View Revisions
2019-07-26 19:13 abutterfield Note Added: 0006837
2019-08-21 16:14 maroneze Note Added: 0006844
2019-08-21 16:14 maroneze Status assigned => resolved
2019-08-21 16:14 maroneze Fixed in Version => Frama-C 20-Calcium
2019-08-21 16:14 maroneze Resolution open => fixed
2020-02-17 18:08 signoles Status resolved => closed
2020-02-17 18:08 signoles Note Added: 0006954

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker