On Thu, Jun 18, 2020 at 12:31:44PM +0100, Richard W.M. Jones wrote: > - Run /usr/lib64/why3/commands/why3config by hand (why isn't it in > /usr/bin?), which creates $HOME/.why3.conf So the reason it's not in /usr/bin is because you have to run it like this: $ why3 config --detect Found prover Alt-Ergo version 2.0.0, OK. Prover Coq version 8.11.2 is not known to be supported. Known versions for this prover: 8.6, 8.6.1, ^8\.7\.[0-2]$, ^8\.8\.[0-2]$, ^8\.9\.[0-1]$, ^8\.10\.[0-2]$, ^8\.11\.0$. Known old versions for this prover: 8.5, ^8\.5pl[1-3]$. 2 prover(s) added (including 1 prover(s) with an unrecognized version) Save config to /home/rjones/.why3.conf Although it still doesn't work. It's possible to omit the -wp parameter and get frama-c to start up, but it doesn't appear to be working correctly. In particular I couldn't get it to prove anything about the example code. Rich. -- Richard Jones, Virtualization Group, Red Hat http://people.redhat.com/~rjones Read my programming and virtualization blog: http://rwmj.wordpress.com virt-df lists disk usage of guests without needing to install any software inside the virtual machine. Supports Linux and Windows. http://people.redhat.com/~rjones/virt-df/ _______________________________________________ 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
