I tried to print in the IDE the MLW file with Mlw_printer.pp_mlw_file
in the IDE instead of the raw sexp file to see if it changes something in term of performance, but I didn't notice any speed-up.
Anyway, it would be better if it the mlw code was printed instead of the raw sexp in the IDE.
Loading a session in the IDE that contains sexp files takes a long time. Our sexp files are printed in a single line.
The problem does not exist when the session is replayed with why3 replay
. Then it's more likely that the problem comes from the highlighting or the rendering of the sexp file in the IDE.
If needed, I can provide a reproducer. I'm working with Why3 version based on 7a94aceb.
Shouldn't you remove the oracles CVC5,1.0.0
? So that it's also easier to see if there are improvements/regressions between cvc5 1.0.0 and 1.0.5.
Guillaume Cluzel (d6b17a89) at 10 Jul 13:33
The script can now be run from any location.
Guillaume Cluzel (d6b17a89) at 10 Jul 12:00
Make the script check-ce-bench a bit more robust
But maybe you cannot access the Vc
module in core
...
Strings.has_prefix (Vc.eid_attr ^ ":") a.attr_string
let prefix = Vc.eid_attr ^ ":" in
let print_expr_id = Format.pp_print_int
I think that you should define "vc:eid"
at top level and reuse the variable when you need it since you use it at multiple locations in the code (and even in multiple files). So that there are less risk to forget one occurrence if someone decides to rename the attribute.
I'm not sure whether it's an improvement or a regression. @marche can you enlighten me?
Guillaume Cluzel (d4c054d0) at 12 Jun 18:52
Update check-ce-bench
Guillaume Cluzel (125888b0) at 12 Jun 18:51
Update check-ce-bench
My bad. I'll take care of this. Sorry
Guillaume Cluzel (e15bb976) at 12 Jun 18:44
Update check-ce-bench
Guillaume Cluzel (b0a9b4f5) at 23 May 14:31
Indeed it works. Maybe that a paragraph could be added to CONTRIBUTING.md to explain the procedure to newcomers, no?