Stream: Coq devs & plugin devs

Topic: Require Import in byte


view this post on Zulip 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)

view this post on Zulip Enrico Tassi (Nov 23 2022 at 15:15):

What really takes time is the import according to my measurements

view this post on Zulip Pierre-Marie Pédrot (Nov 23 2022 at 15:15):

is it Require or Import which is slow?

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 23 2022 at 15:19):

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

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Nov 23 2022 at 15:26):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Feb 05 2023 at 20:03 UTC