No Why3 libraries compiled for PVS
I have been using Why3 1.3.1 (through Frama-C 21.1/WP dev) to generate verification conditions in PVS.
Today I tried to install Why3 in a different computer (both are Macs) via Opam.
$ opam install why3
The following actions will be performed:
∗ install why3 1.3.1
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
[why3.1.3.1] downloaded from cache at https://opam.ocaml.org/cache
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
∗ installed why3.1.3.1
Done.
The installation goes smoothly but it seems that something is missing in order to be able to use PVS.
$ why3 config --detect
Found prover Alt-Ergo version 2.3.1, OK.
Found prover PVS version 6.0, but no Why3 libraries were compiled for it
1 prover(s) added
Save config to /Users/niauser/.why3.conf
When I try to use it, I get
$ frama-c test.c -wp -wp-prover pvs
[kernel] Parsing test.c (with preprocessing)
[wp] User Error: Prover 'pvs' not found in why3.conf
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.
I've also tried why3 config --full-config
with the same result.
$ why3 config --full-config
Found prover Alt-Ergo version 2.3.1, OK.
Found prover PVS version 6.0, but no Why3 libraries were compiled for it
1 prover(s) added
Generating strategies:
Prover Alt-Ergo 2.3.1 will be used in Auto level >= 1
Save config to /Users/niauser/.why3.conf
$ frama-c -wp-detect
[wp] Prover Alt-Ergo 2.3.1 [alt-ergo|altergo|Alt-Ergo:2.3.1]
$
I don’t remember performing any special step during the installation on my other Mac.
Is there something else I should do in order to be able to use Why3 with PVS?