Sana I. (Mar 07 2025 at 17:18): Sana I. (Mar 07 2025 at 17:18):I’m working on automating some reasoning tasks in Isabelle and looking to efficiently run and verify multiple theory files without relying on the interactive GUI (Batch mode?). My goal is to streamline proof execution and analyze results at scale.
I’ve explored Isabelle’s batch mode using isabelle build -D and tested some small theory files, but I’m looking for best practices on:
I’d love to hear from anyone who has experience using batch mode for automation. Are there any recommended workflows, debugging strategies, or useful resources for setting up batch execution effectively?
Mathias Fleury (Mar 07 2025 at 18:44):Handling proof method failures that occur in batch mode but not in interactive mode.
That should not happen
Mathias Fleury (Mar 07 2025 at 18:47):Optimizing batch execution for larger sets of theory files.
You are limited by two things: the number of sessions you run in parallel (usually, the limit is given by your CPU/RAM) and the number of proofs you can run in parallel within your theory and the slowest proof path (usually the limit is given by your theory, but improving this is really really hard)
Sana I. (Mar 07 2025 at 21:04):Thanks, that makes sense. Where can I learn more about this?
irvin (Mar 08 2025 at 11:21):I would like to mention isabelle also supports distributed builds. Generally any paper by Makarius https://files.sketis.net/wenzel_bib.html about parallel/ asynchronous would probably be relevant.
Sana I. (Mar 09 2025 at 03:45):irvin said:
I would like to mention isabelle also supports distributed builds. Generally any paper by Makarius https://files.sketis.net/wenzel_bib.html about parallel/ asynchronous would probably be relevant.
Thank you, this is helpful.
Mathias Fleury (Mar 09 2025 at 06:21):Sana I. said:
Thanks, that makes sense. Where can I learn more about this?
mostly reading the documentation of isabelle build and trying stuff out
Last updated: Mar 09 2025 at 12:28 UTC