1
$\begingroup$

I'm running Isabelle2024 on Windows 10. When using sledgehammer, some eprover processes do not exit after sledgehammer is completed. Each of these processes can consume gigabytes of memory (which grows even after sledgehammer exits) and stall my system eventually. This only happens when my theory is "complex" enough somehow.

The process tree of such eprover process looks like

enter image description here

Other ATP processes exit correctly, including the eprover called by zipperposition.

enter image description here

I can provide a process log if needed.

Improve this question
$\endgroup$
2
  • $\begingroup$ I have similar experiences with Isabelle 2024 on Debian/Linux. I had to deactivate e for sledgehammer because it tended to eat up my RAM. $\endgroup$
    – Benjamin Bisping
    Commented Oct 4 at 16:34
  • $\begingroup$ @BenjaminBisping That's interesting because this does not happen to my Ubuntu.. And actually in Isabelle2023 on Windows 10 some other ATPs also do not get cleaned up by sledgehammer. I thought the issue's gone after the update until my current work's complexity grew beyond some extent recently. $\endgroup$
    – K. Ritsuka
    Commented Oct 4 at 22:22

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.