On 10/11/2017 09:32, Frédéric Blanqui wrote: > Hello. FYI, when doing an opam update this morning, I got the following > error: > « src/coq-tactic/.why3-vo-byte » a échouée
Which version of Coq is installed in your system? If it is 8.7, the failure is kind of expected, as the opam package for Coq 8.7 no longer installs some of the files needed to compile the why3 tactic. The configure script for the next release of Why3 will try to detect that situation (assuming we haven't dropped support for the tactic in the meantime). But for now, I don't have any workaround to suggest, short of manually editing the opam file of why3-base to pass the --disable-coq-tactic option at configuration time. Best regards, Guillaume _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
