Alex Sanchez-Stern (Apr 21 2023 at 22:40): Alex Sanchez-Stern (Apr 21 2023 at 22:40):Hey folks
What state inside of sertop is the "Reset Initial" command supposed to reset? I've been using it to run the same few proofs in a file over and over again (for some reinforcement learning experiments), but I've noticed that the memory usage of sertop is increasing every time, and that increase survives through the resets. Eventually (in my case 120-240 proofs in) it gets oom killed. Should I just be killing sertop and restarting it every once in a while to contain the memory usage, or are there tricks with Resetting that can get my same coq instance to flush whatever is taking up that memory?
Pierre Roux (Apr 22 2023 at 06:09):Have you tried Optimize Heap. to run the GC?
Alex Sanchez-Stern (Apr 23 2023 at 00:40):Ah that did the trick. Out of curiosity, does the GC never run on it's own? Or is there just some trigger I'm not hitting?
Last updated: Apr 19 2024 at 12:02 UTC