Frama-C Bug Tracking System - Frama-C
View Issue Details
0002464Frama-COpampublic2019-07-11 01:142019-07-12 19:18
davidcok 
correnson 
highmajoralways
assignedopen 
MACOSX10.12.6 (SIERRA)
 
 
0002464: Potassium does not install on the given Mac version from opam
opam install frama-c
on Mac wants to downgrade alt-ergo to version 2.1.0 (instead of 2.3.0)
but 2.1.0 fails to build with the error

# Error: Unbound module Zip
# make: *** [lib/util/myZip.cmx] Error 2
opam install frama-c
No tags attached.
Issue History
2019-07-11 01:14davidcokNew Issue
2019-07-11 01:14davidcokStatusnew => assigned
2019-07-11 01:14davidcokAssigned To => maroneze
2019-07-11 01:15davidcokNote Added: 0006815
2019-07-11 08:47virgileSummaryPotassium does not install on the given Mac version from spam => Potassium does not install on the given Mac version from opam
2019-07-11 09:48virgileNote Added: 0006816
2019-07-12 10:17maronezeAssigned Tomaroneze => correnson
2019-07-12 10:40corrensonNote Added: 0006818
2019-07-12 19:18maronezeNote Added: 0006819

Notes
(0006815)
davidcok   
2019-07-11 01:15   
spam -> opam
(0006816)
virgile   
2019-07-11 09:48   
that's strange. camlzip is listed as a dependency of alt-ergo.2.1.0. Is it installed in your current opam switch? If not, you might try to install it by hand before trying to install Frama-C.
(0006818)
correnson   
2019-07-12 10:40   
For the purpose of testing Frama-C/WP with Potassium, I'm using OCaml v4.05 & alt-ergo 2.0.0
As far as I remember, we did not have any problem with alt-ergo 2.1.0, although there are some incompatibilities with more recent versions. But not for installing the prover !
(0006819)
maroneze   
2019-07-12 19:18   
It can be hard to debug opam dependencies sometimes.

- downgrading alt-ergo from 2.3.0 to 2.1.0: this is partially explained by the fact that frama-c.19.0 explicitly blacklists alt-ergo > 2.2.0. But it's not clear why opam downgraded it to 2.1.0, instead of 2.2.0. For instance, I tested installing 2.2.0, and it installed a new package (psmt2-frontend). Maybe opam's constraint solver tries to minimize the amount of installed packages? Anyway, both versions should work with Frama-C, and both require camlzip.

- I am unable to reproduce the error related to Zip. As virgile said, camlzip is a dependency of alt-ergo, so my opam installs it and then compiles alt-ergo.2.1.0 without issues. If I try to remove camlzip, opam removes alt-ergo as well.

I'm afraid your opam internal state may have reached some inconsistent configuration, or the solver got lost somehow. Trying to reinstall camlzip could help.

Otherwise, we'll need more details about the exact opam state (list of packages installed with `opam list`, for instance, plus `opam config list`) to try and reproduce it.

For information, I am able to install Frama-C 19.0 on a fresh macOS Mojave with Homebrew, without issues. Sierra should get the same results, since it is still supported by Homebrew.