Poscat (Feb 03 2025 at 09:54): Poscat (Feb 03 2025 at 09:54):So after interactively editing a theory for a while in vscode, the proof checking becomes much slower. After restarting vscode though the problem disappeared. I've also observed that the polyml program memory usage goes down quite a bit after restarting (1.5G vs 8G before). Is this to be expected?
I'm running isabelle 2024, using vscode and has 64bit polyml enabled (it was running out of RAM with 32bit version).
edit: slows down... can't edit the title ugh :/
Kevin Kappelmann (Feb 03 2025 at 10:00):I have the same problem :'/
Fabian Huch (Feb 03 2025 at 10:10):My observation is that PolyML works much better with 64_32 bit mode and max. 16G heap. Maybe you can build a heap image to decrease memory requirements -- 16GB works for everything in the AFP at least.
Maximilian Vollath (Mar 26 2025 at 10:40):If your problem appears after using "try" or "sledgehammer" multiple times, it might be due to eprover.exe not properly exiting.
My workaround is to have a script pinned to the taskbar that kills eprover.exe and I run after every time I use "try". So far, it hasn't negatively impacted Isabelle.
irvin (Mar 26 2025 at 11:44):Note that if you're running polyml on machines with alot of ram there's a patch here. https://www.mail-archive.com/polyml@inf.ed.ac.uk/msg01908.html that's meant to improve things.
Fabian Huch (Mar 26 2025 at 15:58):I wonder why that was never adopted?
irvin (Mar 27 2025 at 14:57):I don't know. I do know that it's applied on the regression machine for CakeML at UNSW(1 TB memory size).
irvin (Mar 27 2025 at 14:58):It might be the fact that it's a mitigation.
Last updated: Apr 18 2025 at 20:21 UTC