|Anonymous | Login | Signup for a new account||2019-08-25 21:13 CEST|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002464||Frama-C||Opam||public||2019-07-11 01:14||2019-07-12 19:18|
|Platform||MAC||OS||OSX||OS Version||10.12.6 (SIERRA)|
|Target Version||Fixed in Version|
|Summary||0002464: Potassium does not install on the given Mac version from opam|
|Description||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
|Steps To Reproduce||opam install frama-c|
|Tags||No tags attached.|
|spam -> opam|
|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.|
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 !
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.
|2019-07-11 01:14||davidcok||New Issue|
|2019-07-11 01:14||davidcok||Status||new => assigned|
|2019-07-11 01:14||davidcok||Assigned To||=> maroneze|
|2019-07-11 01:15||davidcok||Note Added: 0006815|
|2019-07-11 08:47||virgile||Summary||Potassium 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:48||virgile||Note Added: 0006816|
|2019-07-12 10:17||maroneze||Assigned To||maroneze => correnson|
|2019-07-12 10:40||correnson||Note Added: 0006818|
|2019-07-12 19:18||maroneze||Note Added: 0006819|
|Copyright © 2000 - 2019 MantisBT Team|