Le 19/05/2021 à 08:40, Loïc Correnson a écrit :
Indeed, the new upcoming version of Frama-C will require why3 1.4.0 and will be
marked conflicting with why3 1.5*
However, from a user point of view, it is really annoying to let opam install
why3 and alt-ergo versions that are incompatible with
Indeed, the new upcoming version of Frama-C will require why3 1.4.0 and will be
marked conflicting with why3 1.5*
However, from a user point of view, it is really annoying to let opam install
why3 and alt-ergo versions that are incompatible with each others.
Do you really want us to (1) opam ins
Le 18/05/2021 à 21:33, David MENTRÉ a écrit :
In fact, frama-c 22 from opam explicitly requires Why3 1.3.3 version
only. And it also installs Alt-Ergo 2.4.0, probably because Why3 has no
requirement on Alt-Ergo version. That's why the situation occurred to me
I think.
Presumably, yes.
Maybe
Hello Guillaume,
Le 17/05/2021 à 07:17, Guillaume Melquiond a écrit :
You do not need to wait for the next release. Why3 1.4.0 already
supports Alt-Ergo 2.4.0.
Thank you.
In fact, frama-c 22 from opam explicitly requires Why3 1.3.3 version
only. And it also installs Alt-Ergo 2.4.0, probably
Le 16/05/2021 à 15:20, David MENTRÉ a écrit :
Thank you for the info. Looking forward for the next release.
You do not need to wait for the next release. Why3 1.4.0 already
supports Alt-Ergo 2.4.0.
Best regards,
Guillaume
___
Why3-club mailing lis
Hello Jean-Christophe,
Thank you for the info. Looking forward for the next release.
Best regards,
david
Le 14/05/2021 à 09:39, Jean-Christophe Filliatre a écrit :
Hi David,
Note that this is already fixed in the master version of Why3:
https://gitlab.inria.fr/why3/why3/-/commit/af70b6449eb6
Hi David,
Note that this is already fixed in the master version of Why3:
https://gitlab.inria.fr/why3/why3/-/commit/af70b6449eb66fdfc28a8d5e5c318f6155fe3df6
--
Jean-Christophe
On 05/13/2021 08:35 PM, David MENTRÉ wrote:
> Hello again,
>
> Le 13/05/2021 à 18:09, David MENTRÉ a écrit :
>> I have
Hello again,
Le 13/05/2021 à 18:09, David MENTRÉ a écrit :
I have a strange issue with Why3 1.3.3: it does not detect alt-ergo in
the PATH.
I do have alt-ergo installed and running:
david:~$ which alt-ergo
~/.opam/4.11.1/bin/alt-ergo
david:~$ alt-ergo --version
2.4.0
However it does not de
Hello,
I have a strange issue with Why3 1.3.3: it does not detect alt-ergo in
the PATH.
I do have alt-ergo installed and running:
david:~$ which alt-ergo
~/.opam/4.11.1/bin/alt-ergo
david:~$ alt-ergo --version
2.4.0
However it does not detect alt-ergo while it correctly finds other provers
