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

David MENTRE dmentre at linux-france.org
Tue Nov 1 17:58:11 CET 2011

Hello François,

2011/10/30 François Bobot <bobot at lri.fr>:
> If we don't want to have a "why3session latex" "why3session stats" which
> behave like the subcommand of cvs ,svn, git, and others; we should use
> different commands : why3latex, why3stats. So at the end I think that your
> idea, David, was the good one and we should incorporate your patch for
> why3stats as it is and extract from why3replayer a program why3latex, and
> perhaps write a why3html.

Regarding why3stats vs. "why3session -stats" or "why3session stats", I
don't have a strong opinion. My only remark as a programmer would be
to avoid copy/pasted code between why3replayer and why3stats (which is
currently the case). But as you suggested, we can first make those
tools and then, in a second step, refactor the code to put duplicated
code somewhere in a library.

> 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?

For me, a close_session function would be more useful.

Best regards,

More information about the Why3-club mailing list