[Why3-club] [PATCH] New tool proposal: why3stats

David MENTRE dmentre at linux-france.org
Wed Nov 2 15:25:27 CET 2011


Hello François,

2011/11/2 François Bobot <bobot at lri.fr>:
> I think Session_ro, that is now in the trunk, can be seen as the needed
> factorization. It add some interesting simplification that can't be done in
> Session :
> - You can read different sessions at the same time. In fact a session is
> read once and a big immutable tree is constructed.
> - It uses Map instead of Hashtbl. Since we add many functions to Map.S. I
> think its easier to use.
> - The paths of the edited files are relatives to the current working
> directory and not to the session directory.
> - Running/Waiting status are removed.

Please find attached a new patch that implements why3stats using your
new Session_ro module.

The only missing function in Session_ro is Session.Make.get_provers to
get the detailed information on used provers.

Best regards,
david
-------------- next part --------------
A non-text attachment was scrubbed...
Name: why3stats.patch
Type: text/x-patch
Size: 9052 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20111102/cc946d67/attachment.bin>


More information about the Why3-club mailing list