why3 config for provers with compile-time support
To use a prover such as Coq, the detected version needs to match the one used to compile the .vo
(assuming they were even compiled). If this is not the case, the prover is discarded. This is the expected behavior, but why3 config
's message is quite confusing for the user:
$ why3 config --detect
Found prover Alt-Ergo version 2.0.0, OK.
Found prover Coq version 8.7.2, but Why3 wasn't compiled with support for it
Found prover Coq version 8.7.2, but Why3 wasn't compiled with support for it
Found prover Coq version 8.7.2, but Why3 wasn't compiled with support for it
1 provers detected and 0 provers detected with unsupported version
First, the check should be made only once. Second, the final summary should reflect the result of the check.