|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002466||Frama-C||Opam||public||2019-07-25 01:52||2020-02-17 18:08|
|Product Version||Frama-C 18-Argon|
|Target Version||Fixed in Version||Frama-C 20-Calcium|
|Summary||0002466: Can't build from source using opam|
|Description||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).|
|Steps To Reproduce||When I try to install it using the prescribed method |
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
|Additional Information||If possible, I'd appreciate a patch I could do locally instead of waiting for the official fix. Thanks.|
|Tags||No tags attached.|
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.
Last edited: 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.
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 https://raw.githubusercontent.com/ocaml/opam-repository/1.2/packages/frama-c/frama-c.20181101/opam 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.
|Fixed in Frama-C 20.0 (Calcium).|
|2019-07-25 01:52||sshankar||New Issue|
|2019-07-25 01:52||sshankar||Status||new => assigned|
|2019-07-25 01:52||sshankar||Assigned To||=> maroneze|
|2019-07-25 09:12||maroneze||Note Added: 0006827|
|2019-07-27 01:01||sshankar||Note Added: 0006838|
|2019-07-27 01:02||sshankar||Note Edited: 0006838||View Revisions|
|2019-07-29 09:11||maroneze||Note Added: 0006839|
|2019-08-22 17:49||maroneze||Status||assigned => resolved|
|2019-08-22 17:49||maroneze||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: 0006942|