Sana I. (Apr 04 2025 at 23:33): Sana I. (Apr 04 2025 at 23:33):Hi everyone, I'm in a bit of a bind
So simply put, I’ve built a desktop app that allows users to check for some verification, the reasoning system is based in Isabelle, and I want it to call a script that runs proofs in batch mode (no GUI). My goal is to show users that certain named lemmas have been proved, sort of like auto-verifying a set of logical claims so there is no need for user interaction with isabelle.
I hit the following error when building in batch mode:
*** exception Fail raised (line 55 of "System/isabelle_system.ML"): Bad bash_process server address
*** At command "by" (line 1399 of "/Applications/Isabelle2024.app/src/HOL/Algebra/Group.thy")
It happens when I run
isabelle build -o -D TheoryA or basically any variant of this command. Everything works fine in jEdit. At first it would show errors wherever I used smt in my theories so I changed that because from what I’ve read, this seems related to smt or verit subprocesses on macOS being blocked in batch mode - not sure if that is accurate? Do I need to remove all smt usage? Or is there another solution like moving to Linux because I keep encountering issues in batch mode and sometimes even when there is no error in jEdit, I still come across this... I have checked the documentation but that has not helped much with this particular problem.
I also want to know how isabelle build and isabelle process command is different - for example if I use isabelle build -D .
or isabelle process -l HOL -e 'use_thy "theoryA";'
How do they work?
Any suggestions, tips, or "you’re totally doing this wrong" are very welcome.
Mathias Fleury (Apr 07 2025 at 07:22):This is strange
Mathias Fleury (Apr 07 2025 at 07:23):Especially since isabelle build is tested and everyone is using it (at least to build HOL)
Mathias Fleury (Apr 07 2025 at 07:24):Does it also happen if you limit the number of threads?
Mathias Fleury (Apr 07 2025 at 07:25):isabelle build -o "threads=4" -D TheoryA?
Fabian Huch (Apr 07 2025 at 08:06):Is this in the environment of your 'desktop app', or does this happen when running abuild through the command line?
Also (but probably unrelated) Isabelle2024 is outdated, we're at Isabelle2025.
Fabian Huch (Apr 07 2025 at 08:09):Sana I. said:
I also want to know how isabelle build and isabelle process command is different - for example if I use
isabelle build -D .
orisabelle process -l HOL -e 'use_thy "theoryA";'
How do they work?
Isabelle build manages everything around the build (heap images, session structure, concurrent processes, presentation, etc.). process runs a single raw ML process.
Sana I. (Apr 07 2025 at 09:46):It happens when running a build through the command line. Actually, I should mention that isabelle build -o "threads=4" -D TheoryA gives a successful build.
The output is
Running ...
Finished ... (0:00:14 elapsed time, 0:00:46 cpu time, factor 3.28)
0:00:19 elapsed time, 0:00:46 cpu time, factor 2.36
but since I want to load a single theory and see the proof output, I am using isabelle process -T use_thy and thats where I am running into issues with smt, encoding errors and this..
1.295s elapsed time, 1.709s cpu time, 0.351s GC time
exception Fail raised (line 55 of "System/isabelle_system.ML"): Bad bash_process server address
At command "by" (line 1399 of "/Applications/Isabelle2024.app/src/HOL/Algebra/Group.thy")
Does the error occur when running isabelle build -D TheoryA?
Sana I. (Apr 08 2025 at 00:05):Fabian Huch said:
Does the error occur when running
isabelle build -D TheoryA?
No, it does not occur when I use `isabelle build -D TheoryA. I am not sure what is causing it. I have used it without issues in other small projects. As I mentioned before, it is happening when I load a single thoery using isabelle process and I am trying to print proof output via command line.. I am at a loss
Fabian Huch (Apr 08 2025 at 07:25):Well a raw ML process is really only a raw ML process. Some (very restricted) theories might run only using the ML side, but other parts (printing, external solvers such as smt, file handling, export, database etc.) need the whole Isabelle system, which is not initialized by isabelle process. This is what Isabelle build/jEdit do. If you want to build your own special Isabelle application you'll have to do the same as well.
irvin (Apr 08 2025 at 07:27):Sana I. said:
Fabian Huch said:
Does the error occur when running
isabelle build -D TheoryA?No, it does not occur when I use `isabelle build -D TheoryA. I am not sure what is causing it. I have used it without issues in other small projects. As I mentioned before, it is happening when I load a single thoery using isabelle process and I am trying to print proof output via command line.. I am at a loss
If I recall correctly isabelle has a mechanism for sessions to produce build output. Just can't remember what it's called
Fabian Huch (Apr 08 2025 at 07:32):Do you mean the Export?
Fabian Huch (Apr 08 2025 at 07:33):That can be used to write results to the database, yes.
Sana I. (Apr 08 2025 at 15:35):Fabian Huch said:
Well a raw ML process is really only a raw ML process. Some (very restricted) theories might run only using the ML side, but other parts (printing, external solvers such as smt, file handling, export, database etc.) need the whole Isabelle system, which is not initialized by
isabelle process. This is what Isabelle build/jEdit do. If you want to build your own special Isabelle application you'll have to do the same as well.
Thank you so much, it makes more sense now and I feel quite stupid for not understanding the obvious. Thanks again
Fabian Huch (Apr 08 2025 at 15:37):No worries, these implementation details are certainly not obvious unless one is quite familiar with the code-base (at which point it is surprisingly self-explanatory).
Sana I. (Apr 11 2025 at 15:00):Although I am able to build successfully, I still have a follow up question.
I saw batch mode used like this in a paper and I was interested in finding out how we can use Isabelle like this..
Screenshot 2025-04-11 at 10.32.43 AM.png
Last updated: Apr 18 2025 at 20:21 UTC