Sana I. (Feb 20 2025 at 17:13): Sana I. (Feb 20 2025 at 17:13):Isabelle Keeps Rebuilding HOL and Fails with "Prover Process Terminated with Error Code 127"
I recently ran an '.ML' file in interactive mode, and since then, every time I start Isabelle/jEdit, it rebuilds HOL from scratch, which takes a long time. After a while, the build fails with the error:
Prover process terminated with error code 127
Prover is failed
What I Tried:
I ran isabelle getenv ISABELLE_HOME_USER, and it pointed to a normal location.
I ran isabelle build -b HOL, but it still rebuilds every time I start Isabelle.
My file contains basic ML commands like 'use "myfile.ML";' but nothing that should modify HOL.
did not explicitly call 'OS.Process.exit' or 'use_thy "HOL"'.
I deleted ~/.isabelle/IsabelleYYYY/heaps and rebuilt HOL, but the problem persists.
Before this happened, I also noticed that whenever I build my project using the terminal, it somehow resets Isabelle/jEdit to rebuild the prover each time I open it.
My questions are :
Why does Isabelle keep rebuilding HOL every time I start jEdit?
What causes error 127 in the prover process, and how can I fix it?
Is there a way to prevent HOL from rebuilding unnecessarily?
Could running an .ML file in interactive mode have caused this, and how do I recover?
I am using Isabelle 2024 on Mac.
Yutaka Nagashima (Feb 26 2025 at 01:26):Have you found a solution?
Sana I. (Feb 26 2025 at 01:32):I have not, unfortunately. I had to reinstall Isabelle and that fixed it for the time being but I have not tried to use my ML code or build it batch mode. I am sure the issue will persist and it would be nice to understand why this happens or if I am doing something wrong here.
irvin (Feb 26 2025 at 12:43):Can you share the .ML that caused this?
Last updated: Mar 09 2025 at 12:28 UTC