Stream: Coq devs & plugin devs

Topic: Memory consumption


view this post on Zulip Andrej Dudenhefner (Jul 23 2021 at 12:05):

Looking at ci failure due to memory consmuption of FlatToRiscvFunctions.v I wonder:
is there a tactically good spot to place a garbage collection trigger (such as Gc.minor / Gc.major / ...) so that memory consumption is lowered without sacrificing too much performance?
Suggestions: after internal refine with check, or on closing current subgoal (e.g. with } or an end of a bullet point. On Qed would not solve the bedrock2 problem.

view this post on Zulip Andrej Dudenhefner (Jul 23 2021 at 13:36):

Out of interest, I tried Gc.full_major on vernac_end_subproof (closing }) my results:

no Gc: FlatToRiscvFunctions.vo (real: 895.18, user: 893.47, sys: 1.44, mem: 3158784 ko)
Gc: FlatToRiscvFunctions.vo (real: 969.93, user: 968.96, sys: 0.75, mem: 2335772 ko)

Possibly not worth it. @Samuel Gruetter Instead optimize_heap should be used to get ci going without altering the proof structure.


Last updated: Oct 16 2021 at 02:03 UTC