Stream: Coq users

Topic: Performance of Require Import


view this post on Zulip Paolo Giarrusso (Jul 06 2020 at 17:57):

Gregory Malecha said:

Maxime Dénès said:

Regarding 5., it could be interesting to split the Require and Import to measure which one is slow.

Thanks. I'll take a look at that.

In very unscientific timings, using Require on iris easily takes 1-2 second. The cost of Import is negligible in comparison (tho it is sometimes measurable). What is the cost proportional to?

view this post on Zulip Pierre-Marie Pédrot (Jul 06 2020 at 20:37):

It's probably loading a lot of stuff in memory. In my profiling the top cause of require slowness is merely OCaml deserialization.

view this post on Zulip Paolo Giarrusso (Jul 06 2020 at 20:53):

Does it deserialize bodies, or only interfaces?

view this post on Zulip Gaëtan Gilbert (Jul 06 2020 at 21:36):

Everything except Qed bodies gets deserialized IIRC

view this post on Zulip Paolo Giarrusso (Jul 06 2020 at 23:24):

Right, that's what I should have said.

view this post on Zulip Pierre-Marie Pédrot (Jul 07 2020 at 10:18):

FTR, I my TODO list regarding memory consumption of Coq there is the careful scrutiny of the kind of stuff we store in the vo.

view this post on Zulip Pierre-Marie Pédrot (Jul 07 2020 at 10:18):

I think we could save quite a bit by using the same strategy as opaque proofs for VM bytecode for instance.


Last updated: Feb 08 2023 at 23:03 UTC