Re: [isabelle] usage of Isabelle as a simplifier in batch mode



On 11/10/2021 15:13, Sven Schneider wrote:
> 
> I would like to use Isabelle as an external tool to simplify terms.
> 
> Is there a way to execute Isabelle in batch mode to obtain that simplified term?

In principle you can use the Isabelle server, as documented in the "system"
manual chapter 4: you submit theory sources via a protocol message and get
results eventually (regular messages, warnings, errors etc.).

Often it is better to do it the other way round: assume a running Isabelle
application and invoke your tool from an existing theory context. There are
various possibilities to do this, e.g. as a Scala function from ML ("system
manual section 5.2), or as a TCP server from ML (like Isabelle/Naproche does).

All this works both in the Prover IDE (Isabelle/jEdit) and in batch mode
(isabelle build).


In contrast, invoking Isabelle as a whole in batch mode is going the be very
slow: it basically means to run a certain "isabelle build" process each time.


The remaining question: What is your tool? How is it used?


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.