Andrej Dudenhefner (Jul 23 2021 at 12:05): 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.
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: Jun 08 2023 at 04:01 UTC