Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002464Frama-COpampublic2019-07-11 01:142019-07-12 19:18
Reporterdavidcok 
Assigned Tocorrenson 
PriorityhighSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
PlatformMACOSOSXOS Version10.12.6 (SIERRA)
Product Version 
Target VersionFixed in Version 
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

- Relationships

-  Notes
(0006815)
davidcok (reporter)
2019-07-11 01:15

spam -> opam
(0006816)
virgile (developer)
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 (manager)
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 (developer)
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.

- 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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker