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.


	Makarius





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