Gergely Buday (Sep 12 2023 at 15:41): Gergely Buday (Sep 12 2023 at 15:41):I have a theory file that does not much more than
imports Main "HOL-Probability.PMF_Impl"
only a definition and some comments and texts, but my Isabelle keeps using a lot of memory and reaches ML Cleanup every few seconds.
I restarted my Ubuntu, to the same effect. What this could be?
Wolfgang Jeltsch (Sep 12 2023 at 17:18):Your computer is not strong enough to withstand our tough Isabelle. :wink:
Wolfgang Jeltsch (Sep 12 2023 at 17:19):Seriously, perhaps HOL-Probability is resource-hungry. Your basing your work on HOL, I guess, for which you then use the pre-built heap, but HOL-Probability.PMF_Impl and everything outside HOL it depends on has to be processed in your current session.
Yong Kiam (Sep 13 2023 at 08:05):to elaborate on @Wolfgang Jeltsch 's answer, you might benefit from using a suitable heap here, e.g., starting Isabelle with:
isabelle jedit -l XXX foo.thy
where XXX is HOL-Probability or maybe something further down the line from the AFP
Gergely Buday (Sep 13 2023 at 09:46):Thanks, @Yong Kiam , this solved my problem. And indeed, HOL-Probability is a large development which calls the even larger HOL-Analysis library.
Wolfgang Jeltsch (Sep 13 2023 at 11:08):Gergely Buday said:
And indeed, HOL-Probability is a large development which calls the even larger HOL-Analysis library.
Well, then it’s clear: HOL-Analysis is a huge thing. When using it in one small development, I was always working with Isabelle/jEdit’s default heap set to HOL-Analysis instead of HOL.
Last updated: May 02 2024 at 01:06 UTC