--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on November 2019 ---
Hi Jens, > thank you very much for the hint with 'native:coq". > > By calling 'frama-c -wp-help' I have found out that '-wp-script' is now probably '-wp-coq-script'. > This is certainly a better name but this change should be better documented. Yes, you are absolutely right. > If why3 is now used at compile time, is it then still necessary to call "why3 config --detect" after the installation of provers? Definitively yes ! Frama-C is reading why3 configuration *at runtime* to find out prover configs, not at compile time. > I also received a couple of warning for various provers along the lines of > > Eprover 2.4: Failed > [Why3 Error] anomaly: Why3.Whyconf.StepsCommandNotSpecified("The solver is used with a step limit and the command for running the solver with a step limit is not specified.") > Coq 8.9.1: Failed > [Why3 Error] anomaly: Why3.Whyconf.StepsCommandNotSpecified("The solver is used with a step limit and the command for running the solver with a step limit is not specified.") Thanks for the report, we would look into it. Side remark : using coq _via_ why3 is about to fail, since we have no script available for running the proof. We probably should warn about this. L.