Frama-C Bug Tracking System - Frama-C
View Issue Details
0002466Frama-COpampublic2019-07-25 01:522020-02-17 18:08
Ubuntu 18.04
Frama-C 18-Argon 
Frama-C 20-Calcium 
0002466: Can't build from source using opam
Argon doesn't build, presumably due to config related bugs in opam/opam. I am guessing its due to inconsistency with opam semantics of "|" (used under conflicts in $FRAMAC/opam/opam).
When I try to install it using the prescribed method opam init eval `opam config env` opam install depext opam depext frama-c opam install --deps-only frama-c cd ~/src (where argon is) opam pin add --kind=path frama-c frama-c-18.0-Argon/ I get the following error (and no frama-c): frama-c needs to be installed. [ERROR] why3-base (< 0.88 | >= 1.0.0) & coq < 8.4.6 & lablgtk < 2.18.2 & frama-c-e-acsl & frama-c-base is not a valid conjunction [NOTE] Pinning command successful, but your installed packages may be out of sync.
If possible, I'd appreciate a patch I could do locally instead of waiting for the official fix. Thanks.
No tags attached.
Issue History
2019-07-25 01:52sshankarNew Issue
2019-07-25 01:52sshankarStatusnew => assigned
2019-07-25 01:52sshankarAssigned To => maroneze
2019-07-25 09:12maronezeNote Added: 0006827
2019-07-27 01:01sshankarNote Added: 0006838
2019-07-27 01:02sshankarNote Edited: 0006838View Revisions
2019-07-29 09:11maronezeNote Added: 0006839
2019-08-22 17:49maronezeStatusassigned => resolved
2019-08-22 17:49maronezeResolutionopen => fixed
2020-02-17 18:06signolesFixed in Version => Frama-C 20-Calcium
2020-02-17 18:08signolesStatusresolved => closed
2020-02-17 18:08signolesNote Added: 0006942

2019-07-25 09:12   
Could you please provide the opam version you are using (opam --version)? Also, is there a specific reason you need Frama-C Argon, or could you use Frama-C 19.0 (Potassium) instead? By default, Ubuntu 18.04 contains version 1.2 of package opam, and Argon was the last release on it. Since Frama-C 19, we had to migrate to opam 2, so if you are still using opam 1.2, upgrading it (via `opam install opam-devel`) could help. Also, if you have the sources, in the worst case you can try compiling them directly, skipping the opam constraints. After `opam install --deps-only frama-c`, you can simply go inside the directory containing the sources and run `./configure && make -j && make install`. On my opam 2 I am not able to reproduce the issue, so if you are using 1.2 and cannot upgrade, I'll try downgrading to see if I can get the same errors as you do.
2019-07-27 01:01   
(edited on: 2019-07-27 01:02)
As you suspected I am running opam 1.2.2. Upgrading to opam-devel caused some other (unrelated) problems that I did not explore any further for now. But your suggestion to build from source did the job, so I will stick with that. Thanks very much! Also, the reason for using Argon is that we are trying to use an Argon plugin.
2019-07-29 09:11   
Ok, so the issue is that, in the Argon .tar.gz, the opam constraints use the syntax from opam 2, since opam switched its main repository to that version prior to the Frama-C release. This has been patched post-release in the opam file within the opam 1.2 repository (removing the "|" from the why3-base constraint) to ensure backwards compatibility, but it only works when installing directly from opam. When doing `opam pin`, it uses the file `opam/opam` from the .tar.gz archive, which results in the error. So, if opam 2 is being a problem, you can try keeping 1.2, by downloading the opam file from and replacing `opam/opam` with it. Then, when doing the `opam pin` again, it should read the new opam file and, hopefully, parse it correctly. I'd still recommend upgrading to opam 2 if possible (despite the name of the upgrade package, `opam-devel`, it is not a "development version" but the stable release), for future proofing if nothing else, but it can indeed be hard to upgrade due to dependencies.
2020-02-17 18:08   
Fixed in Frama-C 20.0 (Calcium).