Email Gateway (Jan 07 2025 at 13:03): Email Gateway (Jan 07 2025 at 13:03):From: Tim Rieß <timriess@outlook.com>
Hi all,
is anyone aware of a way to call sledgehammer via the command line or how to retrieve the sledgehammer output from isabelle calls like "isabelle build"?
I'm currently developing python code that generates isabelle code and checks that code by calling "isabelle build" on the relevant .thy files and uses the command line error outputs to fix any mistakes in the theory.
It would be extremely useful to also get the output of sledgehammer, that the jEdit UI shows when you hover over the command, in the command line to further improve my ability to refine the theory.
Has anyone had the same or similar problem and knows of examples or resources that could help?
Thanks a lot in advance!
Best wishes
Tim
Last updated: Jan 30 2025 at 04:21 UTC