Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] export proof state to file

Email Gateway (Aug 22 2022 at 12:00):

From: Makarius <makarius@sketis.net>
On Fri, 4 Dec 2015, Sven Schneider wrote:

is it possible to export the entire current proof state (or how it is
actually called) to an external file?

It depends what you mean by "proof state". The goal statement as a term?
A pretty-printed version of it? Or the true internal state (which is
opaque and cannot easily be serialized)?

The canonical meta-question: What is the intended application?

I assume it is possible to insert some code like
ML {* exportProofState "/tmp/export.txt" *}
but I am not even convinced that ML code can be contained within a proof.

See the isar-ref manual about various ML commands. Looking around a bit
more, you will also see that Isabelle sources don't use camel case.

Makarius

Email Gateway (Aug 22 2022 at 12:06):

From: Sven Schneider <sven.schneider.pub@gmx.de>
Dear list,

is it possible to export the entire current proof state (or how it is
actually called) to an external file?
I assume it is possible to insert some code like
ML {* exportProofState "/tmp/export.txt" *}
but I am not even convinced that ML code can be contained within a proof.

Cheers
Sven

Last updated: Apr 23 2024 at 12:29 UTC