--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on October 2020 ---
I start Coq from the Frama-C GUI. I click on the yellow bubble to load the Coq script in the Coq IDE and prove the goal there. On Mon, Oct 5, 2020 at 10:41 AM Mohit Tekriwal <tmohit at umich.edu> wrote: > Hello, > > 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. > > Thanking you, > > Mohit Tekriwal > > -- > Mohit Tekriwal, > PhD Candidate, > Department of Aerospace Engineering, > University of Michigan. > -- Mohit Tekriwal, PhD Candidate, Department of Aerospace Engineering, University of Michigan. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20201005/c3b25a5f/attachment-0001.html>