[Why3-club] [PATCH] New tool proposal: why3stats
bobot at lri.fr
Wed Nov 2 11:15:07 CET 2011
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 ;).
More information about the Why3-club