Re: [isabelle] using Isabelle programmatically




On 04/09/2015 11:17 PM, Makarius wrote:
> On Thu, 9 Apr 2015, Viorel Preoteasa wrote:
>
>> How can this be done programmatically? Should I use
>> "isabelle_process" or "isabelle console"?
>
> For me a console is a device where a human is sitting to connect to
> the computer.  A tty is something similar, but from the Unix world
> (actually a brand name of a particular device).
Here, I just meant the option "console" available for the bin/isabelle
command. Ideally I would need an API
available in Python which does what I need: Simplifies a term based on a
specific theory. I understand
now that this API is available for Scala, and of course for SML, so in
the future I may use Scala.

On the other hand, even if using SML, getting started with it does not
seem easy. I tried to find the right
functions for this job before posting the question to the mailing list.


>
>
> "Programmatically" probably refers to batch mode, so the raw
> isabelle_process is the most elementary way to do it.
You are right, maybe batch mode is more appropriate term.

Thank you,

Viorel




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