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

François Bobot bobot at lri.fr
Wed Nov 2 11:15:07 CET 2011

Hello David,

Le 01/11/2011 17:58, David MENTRE a écrit :
> 2011/10/30 François Bobot<bobot at lri.fr>:
>> Perhaps we can also add an intermediate API for
>> working read only with sessions. It seems that your patch is cluttered with
>> complication that can be removed if you can see a sessions just like an
>> immutable tree-like algebraic datatypes. What do you think?
> Once again, no strong opinion. :-) I can live with the current API.
> Are you sure maintaining several API (doc, tests, etc.) can be
> sustained on the long term?

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.

I'm not sure that many people need to modify sessions in multiple ways. 
Why3ide is a great tool for that. On the contrary presenting nicely 
results and choosing which results to present is a matter of taste. So I 
think a simpler API for reading sessions is a good evil, even if that 
can add some maintenance costs.

> For me, a close_session function would be more useful.

In Session_ro there is no open ;).

Best regards,


More information about the Why3-club mailing list