[Why3-club] Problem with type definition

Andrei Paskevich andrei at tertium.org
Fri Feb 10 15:21:48 CET 2012


On Fri, Feb 10, 2012 at 09:27, Benjamin Gregoire
<Benjamin.Gregoire at inria.fr> wrote:
>   This bug is very blocking for us (we use why3 to develop EasyCrypt).

Fixed in 0c56437.

>    And I have some other problem:
>    I have patched why3 in such way that we can kill provers
>    (I think it is the patch you suggested to me).
>    The modification of the ML code was trivial, but we should also
>    call the provers, using  why3-cpulimit with the option -h else it
>    does not work.
>    I think that the problem is that with the -s option, a new process
>    is created using fork (for the prover), and kill will kill process
>    waiting for the prover and not the prover itself.

You can make why3-cpulimit the leader of its process group (by calling
setpgid(0,0) before fork/exec) and then send the kill signal to the
whole group (by using -pid_of_cpulimit as the first argument of
Unix.kill).

>    So my question is: do you think it is a good idea to work with the trunk
>    branch (once you will correct the bug) and to patch it as we do for the 0.71?
>   Do you see another solution?

As long as your patch is easy to maintain (and we are willing to help
to update it
if necessary), the best solution IMO is to keep it in sync with Why3,
either with the
trunk or with the releases, as you prefer.

Best,
Andrei



More information about the Why3-club mailing list