Stream: Coq devs & plugin devs

Topic: Require Import in byte

Enrico Tassi (Nov 23 2022 at 15:14):

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)

Enrico Tassi (Nov 23 2022 at 15:15):

What really takes time is the import according to my measurements

Pierre-Marie Pédrot (Nov 23 2022 at 15:15):

is it Require or Import which is slow?

Enrico Tassi (Nov 23 2022 at 15:17):

My impressions is that running any other line is slower, but not that slower. Maybe it is just a wrong perception

Enrico Tassi (Nov 23 2022 at 15:19):

On my setup Require Import all_ssreflect takes 7 + 12 seconds, so both are slow

Enrico Tassi (Nov 23 2022 at 15:21):

It is byte run via web assembly, I'm not complaining of the overall speed, it is just that these lines are visibly slow.

Michael Soegtrop (Nov 23 2022 at 15:26):

Yet it is quite a marvel one can do this at all in a web browser ...

Gaëtan Gilbert (Nov 23 2022 at 15:31):

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.

Michael Soegtrop (Nov 23 2022 at 15:34):

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.

Enrico Tassi (Nov 23 2022 at 15:41):

So it seems Import becomes more slower. Import is pure "ocaml" time, while require also loads files, maybe this is why.

Gaëtan Gilbert (Nov 23 2022 at 15:48):

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: Dec 07 2023 at 04:02 UTC