--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on October 2020 ---
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.