0002377: Frama-C incompatible with Coq 8.8.0 - Frama-C Bug Tracking System

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
2018-07-11 15:33	signoles	Fixed in Version	Frama-C 17 Chlorine => Frama-C 16 Sulfur
2018-07-11 15:34	signoles	Status	resolved => closed
2018-07-11 15:34	signoles	Note Added: 0006575
2018-07-11 15:36	signoles	Note Edited: 0006575	View Revisions
2018-07-11 15:36	signoles	Note Deleted: 0006575
2018-07-11 15:36	signoles	Fixed in Version	Frama-C 16 Sulfur => Frama-C 17 Chlorine
2018-07-11 15:36	signoles	Status	closed => resolved
2018-07-11 15:39	signoles	Status	resolved => closed

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

Relationships