Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002377Frama-COpampublic2018-05-30 23:042018-06-01 16:17
Reporterramsdell 
Assigned Tomaroneze 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
Platformi686OSFedoraOS Version28
Product VersionFrama-C 16 Sulfur 
Target VersionFixed in VersionFrama-C 17 Chlorine 
Summary0002377: Frama-C incompatible with Coq 8.8.0
DescriptionInstallation with opam worked well except that it deleted my modern version of Coq!
Steps To ReproduceInstall Coq and then install frama-c
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006553)
maroneze (developer)
2018-06-01 16:17
edited on: 2018-06-01 16:17

This is due to a necessary constraint blacklisting Coq >= 8.7 for Frama-C 16 Sulfur, otherwise Frama-C won't compile.

The way opam works is that, when it cannot solve a constraint, it will try in several ways, including downgrading existing packages, as in your case.

We have no direct control over the process. This Stack Overflow question has some suggestions, but they do not always work:

https://stackoverflow.com/questions/33351326 [^]

Anyway, with the just released Frama-C 17 Chlorine, the constraint is no longer there, so you should be able to install both Coq 8.8 and Frama-C:

opam update
opam install frama-c.20180501


- Issue History
Date Modified Username Field Change
2018-05-30 23:04 ramsdell New Issue
2018-05-30 23:04 ramsdell Status new => assigned
2018-05-30 23:04 ramsdell Assigned To => maroneze
2018-05-31 09:10 signoles Category Graphical User Interface => Opam
2018-06-01 16:17 maroneze Note Added: 0006553
2018-06-01 16:17 maroneze Status assigned => resolved
2018-06-01 16:17 maroneze Fixed in Version => Frama-C 17 Chlorine
2018-06-01 16:17 maroneze Resolution open => fixed
2018-06-01 16:17 maroneze Note Edited: 0006553 View Revisions


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker