Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 03:02 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002464Frama-COpampublic2020-02-17 18:08
Assigned Tocorrenson 
PlatformMACOSOSXOS Version10.12.6 (SIERRA)
Product Version 
Target VersionFixed in VersionFrama-C 20-Calcium 
Summary0002464: Potassium does not install on the given Mac version from opam
Descriptionopam 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 Reproduceopam install frama-c
TagsNo tags attached.
Attached Files




davidcok (reporter)

spam -> opam


virgile (developer)

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.


correnson (manager)

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 !


maroneze (administrator)

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.


correnson (manager)

Switch to :
 - opam 2.0
 - ocaml > 4.05
 - why3 1.2.0
 - alt-ergo 2.0+


correnson (manager)

Switch to :
 - opam 2.0
 - ocaml > 4.05
 - why3 1.2.0
 - alt-ergo 2.0+

New opam OK in upcoming 20.0 Calcium release


signoles (manager)

Fixed in Frama-C 20.0 (Calcium).

-Issue History
Date Modified Username Field Change
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
2019-10-17 14:50 correnson Note Added: 0006887
2019-10-17 14:50 correnson Note Added: 0006888
2019-10-17 14:50 correnson Status assigned => resolved
2019-10-17 14:50 correnson Resolution open => fixed
2020-02-17 18:06 signoles Fixed in Version => Frama-C 20-Calcium
2020-02-17 18:08 signoles Status resolved => closed
2020-02-17 18:08 signoles Note Added: 0006943
+Issue History