Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002466Frama-COpampublic2019-07-25 01:522020-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 sync.
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

- Relationships

-  Notes
maroneze (administrator)
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.
sshankar (reporter)
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.
maroneze (administrator)
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.
signoles (manager)
2020-02-17 18:08

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

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker