Frama-C Bug Tracking System - Frama-C
View Issue Details
0002466Frama-COpampublic2019-07-25 01:522019-07-29 09:11
sshankar 
maroneze 
normalblockalways
assignedopen 
Ubuntu 18.04
Frama-C 18-Argon 
 
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: 0006838bug_revision_view_page.php?bugnote_id=6838#r412
2019-07-29 09:11maronezeNote Added: 0006839

Notes
(0006827)
maroneze   
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.
(0006838)
sshankar   
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.

(0006839)
maroneze   
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 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.