2021-03-03 03:17 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002466Frama-COpampublic2020-02-17 18:08
Assigned Tomaroneze 
PlatformOSUbuntu OS Version18.04
Product VersionFrama-C 18-Argon 
Target VersionFixed in VersionFrama-C 20-Calcium 
Summary0002466: Can't build from source using opam
DescriptionArgon 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 ReproduceWhen 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
Additional InformationIf possible, I'd appreciate a patch I could do locally instead of waiting for the official fix. Thanks.
TagsNo tags attached.
Attached Files




maroneze (administrator)

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.


sshankar (reporter)

Last edited: 2019-07-27 01:02

View 2 revisions

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.


maroneze (administrator)

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.


signoles (manager)

Fixed in Frama-C 20.0 (Calcium).

-Issue History
Date Modified Username Field Change
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
+Issue History