Paolo Giarrusso (Jul 06 2020 at 17:57): 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
RequireandImportto 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?
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.
Paolo Giarrusso (Jul 06 2020 at 20:53):Does it deserialize bodies, or only interfaces?
Gaëtan Gilbert (Jul 06 2020 at 21:36):Everything except Qed bodies gets deserialized IIRC
Paolo Giarrusso (Jul 06 2020 at 23:24):Right, that's what I should have said.
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.
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: Oct 01 2023 at 18:01 UTC