Chengsong Tan (Aug 31 2024 at 19:46): Chengsong Tan (Aug 31 2024 at 19:46):Hi,
I was encountering the exception "Interrupt_Breakdown" while calling some heavy-duty command (my super_sketch tool actually). This seems like some exception that is raised when some resources have been exhausted or some function timed out. Any ideas why this exception and how to get over this?
To reproduce the exception, use the following files:
Interrupt_Breakdown_example.zip
Open the file linux_I_SIA_conjunct.thy and scroll to the lines containing "super_sketch3" to activate the command causing the exception.
Best wishes,
Chengsong
Mathias Fleury (Sep 01 2024 at 12:19):As far as I know it is a polyml error and you cannot recover from it
Mathias Fleury (Sep 01 2024 at 12:19):You could try to use the 64-bit version which can use more memory than the 32 bit version
Mathias Fleury (Sep 01 2024 at 12:20):(in the Isabelle settings from Isabelle/jEdit, there is a 64 bit setting)
Mathias Fleury (Sep 01 2024 at 12:21):the major drawback is that polyml is incredibly stupid with memory. I have it using 500GB of RAM on a 2TB machine (for absolutely no reason). And the more memory it uses, the slower GC is becoming, to the point that restarting can be more efficient.
Mathias Fleury (Sep 01 2024 at 12:21):(you can set the max-heap to avoid tha behavior)
Chengsong Tan (Sep 01 2024 at 20:47):Mathias Fleury said:
You could try to use the 64-bit version which can use more memory than the 32 bit version
Wait, so all users of Isabelle are set to use 32-bit version by default?
Chengsong Tan (Sep 01 2024 at 20:52):Mathias Fleury said:
You could try to use the 64-bit version which can use more memory than the 32 bit version
Is that set by Plugin Options -> Isabelle -> General -> ML 64? That's the closest I can find.
Mathias Fleury (Sep 02 2024 at 04:54):Chengsong Tan said:
Mathias Fleury said:
You could try to use the 64-bit version which can use more memory than the 32 bit version
Is that set by Plugin Options -> Isabelle -> General -> ML 64? That's the closest I can find.
Yeah exactly (requires an Isabelle restart)
Mathias Fleury (Sep 02 2024 at 04:56):Chengsong Tan said:
Mathias Fleury said:
You could try to use the 64-bit version which can use more memory than the 32 bit version
Wait, so all users of Isabelle are set to use 32-bit version by default?
For polyml yes, as most people do not need that much memory. java and Isabelle/jEdit is independent.
Mathias Fleury (Sep 02 2024 at 04:59):There is also the 64_32 intermediate version that allows up to 30GB heap
Chengsong Tan (Sep 03 2024 at 10:49):Mathias Fleury said:
Chengsong Tan said:
Mathias Fleury said:
You could try to use the 64-bit version which can use more memory than the 32 bit version
Wait, so all users of Isabelle are set to use 32-bit version by default?
For polyml yes, as most people do not need that much memory. java and Isabelle/jEdit is independent.
I see, so this ML setting should not impact the performance of the Prover IDE, I presume? (e.g. provers/sledgehammer performance)
Last updated: Dec 30 2024 at 16:22 UTC