Did anyone investigate why Require Import is so slow in byte? (my interest is that this makes js/wacoq slow, but also ocamldebug is affected)
What really takes time is the import according to my measurements
is it Require or Import which is slow?
My impressions is that running any other line is slower, but not that slower. Maybe it is just a wrong perception
On my setup Require Import all_ssreflect
takes 7 + 12 seconds, so both are slow
It is byte run via web assembly, I'm not complaining of the overall speed, it is just that these lines are visibly slow.
Yet it is quite a marvel one can do this at all in a web browser ...
on my machine
Time Require ZArith.
Time Import ZArith.
$ coqc foo.v
Finished transaction in 0.199 secs (0.146u,0.052s) (successful)
Finished transaction in 0.038 secs (0.034u,0.003s) (successful)
$ coqc.byte foo.v
Finished transaction in 0.861 secs (0.801u,0.06s) (successful)
Finished transaction in 0.261 secs (0.261u,0.s) (successful)
in ocamldebug:
(ocd) run
Loading program... done.
Finished transaction in 69.932 secs (8.23u,24.703s) (successful)
Finished transaction in 27.397 secs (2.664u,10.451s) (successful)
Time: 82663712
Program exit.
I could imagine that in ocamldebug the forking done to go back in time is quite slow for memory heavy operations. Afair this is on by default? But this should not affect normal bytecode runs.
So it seems Import
becomes more slower. Import is pure "ocaml" time, while require also loads files, maybe this is why.
with checkpoints off in ocamldebug
Finished transaction in 9.02 secs (5.602u,0.158s) (successful)
Finished transaction in 2.368 secs (1.77u,0.016s) (successful)
Last updated: Jun 04 2023 at 19:30 UTC