View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002466 | Frama-C | Opam | public | 2019-07-25 01:52 | 2020-02-17 18:08 | ||||
Reporter | sshankar | ||||||||
Assigned To | maroneze | ||||||||
Priority | normal | Severity | block | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | OS | Ubuntu | OS Version | 18.04 | |||||
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 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 Information | If possible, I'd appreciate a patch I could do locally instead of waiting for the official fix. Thanks. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
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 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. |
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 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) 2020-02-17 18:08 |
Fixed in Frama-C 20.0 (Calcium). |
![]() |
|||
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 |