Why3 parsing slow
This is an issue that we discovered together with @sdailler. I added the attached patch to why3 to mesure CPU time spent in some parts of the code (here: driver loading).timing.patch With this patch I was able to determine that on some file (I don't think it matters which), if I ask why3 to load e.g. the cvc4 driver:
why3 prove -P CVC4 <somefile>
loading the driver takes roughly 0.1 seconds. With @sdailler we found that it isn't actually loading drivers that is slow, but the reading of the why3 libs referenced from the driver.
In SPARK we have switched to a mode where we run why3 much more often than before (possibly hundreds of times on large projects) so while 0.1 seconds seems tiny, it does add up to dozens of seconds on such projects. Also, the above 0.1s measures only parts of the why3 library, while in SPARK we also have some support files which are parsed on every invocation of why3, so for us the time is closer to 0.2 or even 0.4s.
I checked the file sizes of the entire why3 stdlib, and of drivers, and everything is very small, so I'm surprised that any measurable time is spent parsing these files. Can this be improved?