[Why3-club] getting error during installation of the why3 latest version

Jean-Christophe Filliâtre Jean-Christophe.Filliatre at lri.fr
Mon Mar 17 07:51:43 CET 2014


A possible explanation: Why3 and Coq are not compiled with the same
version of OCaml.

-- 
Jean-Christophe


Le 15/03/2014 21:56, Dragan a écrit :
> Hi all,
> I am getting an error during installation of the latest why3 version from :
> https://gforge.inria.fr/git/why3/why3.git
> 
> File "src/coq-tactic/g_why3tac.ml <http://g_why3tac.ml>", line 1,
> characters 0-1:
> Error: The files src/coq-tactic/why3tac.cmi
>        and /usr/local/lib/coq/lib/genarg.cmi make inconsistent assumptions
>        over interface Genarg
> make: *** [src/coq-tactic/g_why3tac.cmx]
> 
> installed provers are :
> Z3 version 4.3.1
> Coq version 8.4pl3
> PVS version 6.0
> 
> Any advice ?
> 
> Regards 
> -- 
> Dragan Stosic
> Senior developer at IBM
> phone: 085-773-1050
> e-mail: dragan.stosic at gmail.com <mailto:dragan.stosic at gmail.com>
> e-mail:DRAGANST at ie.ibm.com <mailto:e-mail%3ADRAGANST at ie.ibm.com>
> IBM Technology Campus
> Damastown Industrial Estate
> Mulhuddart
> Dublin 15
> Ireland
> 
> 
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
> 





More information about the Why3-club mailing list