Stream: Beginner Questions

Topic: Is it me or does isabelle slows do after running fo a while?

view this post on Zulip 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 :/

view this post on Zulip Kevin Kappelmann (Feb 03 2025 at 10:00):

I have the same problem :'/

view this post on Zulip 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.

Last updated: Mar 09 2025 at 12:28 UTC