On 2020-06-18 19:31, Richard W.M. Jones 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 You seem to be running a rawhide system. Things with rawhide may be unstable. Is there any reason you can't use F32? Otherwise, you probably would get better assistance on the fedora-test list which is more geared towards rahide (aka F33 at the moment) > > I couldn't get any further. What I tried was: > > - Install both why3 and alt-ergo. Why aren't they deps of frama-c? > > - Run /usr/lib64/why3/commands/why3config by hand (why isn't it in > /usr/bin?), which creates $HOME/.why3.conf > > - stracing the program, it seems like it never attempts to > open or run anything to do with alt.*ergo > > ~/.why3.conf contains: > > ---------------------------------------------------------------------- > [detected_prover] > exec_name = "alt-ergo" > version = "2.0.0" > > [detected_prover] > exec_name = "coqtop" > version = "8.11.2" > > [main] > default_editor = "emacs -nw %f" > magic = 14 > memlimit = 1000 > running_provers_max = 2 > timelimit = 5 > ---------------------------------------------------------------------- > > $ rpm -q why3 frama-c alt-ergo coq > why3-1.3.1-10.fc33.x86_64 > frama-c-21.0-2.fc33.x86_64 > alt-ergo-2.0.0-15.fc33.x86_64 > coq-8.11.2-1.fc33.x86_64 > > Rich. > -- The key to getting good answers is to ask good questions. _______________________________________________ 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
