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

David MENTRE dmentre at linux-france.org
Wed Nov 2 21:24:18 CET 2011

Hello François,

2011/11/2 François Bobot <bobot at lri.fr>:
> Patch applied (I just add a .depend for stats)

Thank you!

[ 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;
  finalize_stats stats;
  print_stats stats

I'll do some more detailed tests.

Best regards,

More information about the Why3-club mailing list