On Thu, Jun 18, 2020 at 5:31 AM Richard W.M. Jones <rjones@xxxxxxxxxx> wrote: > I was trying to run through the tutorial here: > > https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf > > The first example on page 15 & 16 fails with: > > [wp] Running WP plugin... > [wp] User Error: Prover 'alt-ergo' not found in why3.conf > > I couldn't get any further. What I tried was: > > - Install both why3 and alt-ergo. Why aren't they deps of frama-c? Historically, they were not required for frama-c to do something useful. The WP plugin needs them, but frama-c can be used in other ways. However, I see that frama-c's opam file lists both of them as non-optional "depends", so I will make them Requires for the next frama-c build. (Note that alt-ergo is a Suggests already.) > - Run /usr/lib64/why3/commands/why3config by hand (why isn't it in > /usr/bin?), which creates $HOME/.why3.conf I see you figured this one out already. > - stracing the program, it seems like it never attempts to > open or run anything to do with alt.*ergo I see this in the log: [wp] User Error: Prover 'alt-ergo' not found in why3.conf which is a lie. Prover alt-ergo is most definitely listed in why3.conf. I'll debug this. Stand by. -- Jerry James http://www.jamezone.org/ _______________________________________________ users mailing list -- users@xxxxxxxxxxxxxxxxxxxxxxx To unsubscribe send an email to users-leave@xxxxxxxxxxxxxxxxxxxxxxx Fedora Code of Conduct: https://docs.fedoraproject.org/en-US/project/code-of-conduct/ List Guidelines: https://fedoraproject.org/wiki/Mailing_list_guidelines List Archives: https://lists.fedoraproject.org/archives/list/users@xxxxxxxxxxxxxxxxxxxxxxx
