Email Gateway (Aug 22 2022 at 17:32): Email Gateway (Aug 22 2022 at 17:32):From: Diego Marmsoler <diego.marmsoler@tum.de>
Dear Isabelle experts,
I have a question regarding the use of Isabelle in batch mode: Is there a way to invoke Isabelle in a way to check the proof of a single theorem in a given theory file?
So, assuming i have a theory containing proofs for several theorems and i want Isabelle to check the proof of one theorem only.
Many thanks and best regards!
Diego
Email Gateway (Aug 22 2022 at 17:32):From: Makarius <makarius@sketis.net>
Normally the purpose of batch mode is the check everything thoroughly.
It is possible to suppress whole theories via the "condition" option in
the session ROOT entry (see also the "system" manual, chapter 2.
It is also possible to use skip_proofs, although its meaning is not
clearly defined.
Can you give more context to the intended application?
Makarius
Email Gateway (Aug 22 2022 at 17:37):From: Makarius <makarius@sketis.net>
Just as a conclusion of the public thread: it looks to me like another
application of the new Isabelle server (for "headless PIDE"). See also
https://sketis.net/2018/the-isabelle-server-responsive-control-of-prover-sessions
I have given many demos and talks mentioning it recently, but it would
be nice if prospective users could start experimenting with it on time
before the Isabelle2018 becomes final, to make sure that it really works
as expected.
Makarius
Last updated: Apr 26 2024 at 12:28 UTC