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.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.
Out of interest, I tried
}) 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