Re: [isabelle] using Isabelle programmatically
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).
"Programmatically" probably refers to batch mode, so the raw
isabelle_process is the most elementary way to do it.
The examples so far on this thread where using the cold and naked toplevel
of the underlying ML system -- working there is possible, but might become
a bit awkward. Isabelle/ML normally runs within the Isabelle environment,
e.g. with a theory that is loaded via use_thy from outside.
Much more possibilities of "programmatic" use of Isabelle are thinkable,
e.g. taling to Isabelle/Scala as already explained by Lars Hupel. In may
applications one might even want to talk directly within the PIDE to the
Isabelle process, depending on user interaction result.
There are many possiblities beyond 1970-TTY-mode. It all depends on the
application what is the best way.
This archive was generated by a fusion of
Pipermail (Mailman edition) and