Email Gateway (Jan 07 2025 at 15:03): Email Gateway (Jan 07 2025 at 15:03):From: Makarius <makarius@sketis.net>
On 06/01/2025 10:08, Tim Rieß wrote:
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"?
Maybe you want to take a look at the existing Isabelle command-line tool
"isabelle mirabelle", with its sources in
Isabelle2024/src/HOL/Tools/Mirabelle/. The general approach to Isabelle
command-line tools is demonstrated in Isabelle2024/src/Tools/Demo/.
This is really for batch-mode systems tools, interaction works differently:
e.g. see the Isabelle server that is explained in the "system" manual (chapter
4). The Server also has more direct access in Isabelle/Scala via the Headless
module. It might also turn out that it is better to stay within the regular
Isabelle/PIDE setup of one Isabelle/Scala process connected to one Isabelle/ML
process.
There are many possibilities. Can you describe your project and requirements a
bit?
Generally note that Isabelle is a very complex system, and it deviates from
what is usually done elsewhere quite often. Sometimes people try to apply
force to put Isabelle into a form of their liking, but this will not work out
well in the end. Applications better work with the Isabelle system platform,
rather than against it.
Makarius
Last updated: Jan 30 2025 at 04:21 UTC