--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on October 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] loading coq scripts in Frama-C



Hello,

Do you start Coq from the Frama-C GUI?
Which option did you use the start Frama-C?

In any case, I highly recommend using the most recent version of Frama-C (v21.1, Scandium).
You are using version 19 (Potassium).

Regards

Jens

> 
> 
> I am trying to load coq scripts in Frama-C, but I have been facing issues. I am using the WP plugin on the Frama-C potassium version with Coq 8.9.1.
> 
> Specifically, the problem arises when I try to prove the goal generated in the Coq template generated from Frama-C. I define lemmas outside the goal and import some standard Coq libraries to complete the proof. Even though I am able to prove the goal in Coq, closing the coq interface does not turn the yellow bubble to green in the WP goals. 
> 
> Does someone have any idea as to where I am going wrong? I would appreciate the suggestions.