Le 23/10/2017 à 13:59, Pierre-Yves Strub a écrit : > Hi again, > > If found Call_prover.forward_results in the git repository and this is > definitively what I need. This new API is great as it will allow > EasyCrypt to run multiple provers in parallel under Windows > (currently, we are running provers one by one under win32) & will > allow me to remove all this fork/waitpid stuffs in our code base. I > have a few questions/requests : > > - when do you plan to release Why3 with "forward_results" available > --- if I'm right, it is not present in Why3 0.88.0?
Ouch, sorry, I though it was already there in Why3 0.88.0 The current master branch of the git contains a lot of diffs with 0.88, regarding the structure of sessions, and the GTK interface. Since you are not using them, then master branch could be suitable for you. However, I guess you would like to rely on a Why3 release, available e.g. in OPAM ? Then indeed, we might need to make a 0.88.1 release soon. We'll try to do our best to make one. > - I need to create search trees or hash tables using job IDs as key, > i.e. using prover_call as key. Currently, breaking the abstraction, I > can see that using the polymorphic comparison/hash functions, all will > be fine... but having explicit eq/compare/hash functions for the > prover_call type would allow me not to rely on breaking the Why3 API > abstraction. Good point, we should add them in the API. - Claude -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Île-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
