[Why3-club] [PATCH] New tool proposal: why3stats
dmentre at linux-france.org
Wed Nov 2 21:24:18 CET 2011
2011/11/2 François Bobot <bobot at lri.fr>:
> Patch applied (I just add a .depend for stats)
[ About list of provers ]
> I added the needed
> machinery in session and now session_ro gives the list of provers registered
> in the session.
Thanks, this was the intent of my code.
> Furthermore, stats can now handle transformations and it can accept other
> configuration file with -C like why3.
> I'll appreciate if you can check my changes in your code.
I've reviewed the patches and done some basic tests: everything seems
fine to me. I've seen that you have done some refactoring and
The only part that I will probably change is that you are gathering
stats per Why3 file when several files are given on the command line.
In that case, I would prefer to gather the statistics for all the
files, i.e. something like:
let () =
let stats = new_proof_stats () in
Queue.iter (fun fname ->
ignore(extract_stats_from_file stats fname)) files;
I'll do some more detailed tests.
More information about the Why3-club