Stream: General

Topic: Run out of store errors when building sessions

Chengsong Tan (Nov 09 2024 at 08:57):

I got this when building a session:

Run out of store - interrupting threads

How do I resolve this? I tried following the error message's suggestion of doing a

$ isabelle build_log -H Error MySession

But got

*** java.lang.StringIndexOutOfBoundsException: Range [-736, 3) out of bounds for length 3

Yutaka Nagashima (Nov 09 2024 at 10:54):

Have you set your own timeout in ROOT?

Chengsong Tan (Nov 09 2024 at 14:17):

Yutaka Nagashima said:

Have you set your own timeout in ROOT?

Nope, no timeout set. Maybe good to mention: this is a root file with about 70 files, and most of them having 3000-ish lines of code. But surely Isabelle/HOL itself has much larger session right?

Yutaka Nagashima (Nov 09 2024 at 15:55):

Ah… it’s probably not due to a timeout.

I encountered similar messages while extracting features for PaMpeR. :grimacing:

You might want to check which line in which Isabelle file is causing the issue.

Chengsong Tan (Nov 10 2024 at 08:45):

Thank you! I have built separate folders and sessions for each file to isolate the errors. Indeed, some files I believed correct are wrong.

Chengsong Tan (Nov 10 2024 at 16:18):

For future reference: one of the causes of "run out of store" is a non-terminating line in the theory, for instance a looping metis/smt one-liner proof.

Last updated: Dec 21 2024 at 12:33 UTC