Re: [isabelle] Initialisation of session and nodes: What's changed?



On Thu, 31 Jan 2013, Avi Knoll wrote:

I have been writing a tool that interfaces with the Isabelle/Scala API, and have previously (with Isabelle 2012) been using the example at https://bitbucket.org/pide/pide_examples/src/5ac145e991f9/ex.scala?at=default to load theories and run the prover, so that I can collect output and process theory semantic information as needed.

As the instance method Session.edit_node no longer exists, may I ask what the current method for loading nodes and running the prover is, please?

I am answering this on isabelle-users, because you merely want to know how to use public Isabelle/Scala programming interfaces of in a public release (Isabelle2013), and not argue about the ongoing development process between the releases.

BTW, this is a continuation of the
thread https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-February/msg00067.html


Back to your question. https://bitbucket.org/pide/pide_examples version 212919b16b3a is now updated to Isabelle2013. It was interesting to see myself, how certain functions to manage Isabelle sessions have evolved since Isabelle2012.

Session.update is now the main operation to feed edits into the prover, but there were more changes concerning Thy_Load etc.


What is notable is the isabelle.Build module of Isabelle/Scala to manage Isabelle sessions "offline", without starting a prover process yet; e.g. you can get hold of the all-important outer syntax that is required for editing operations. The internal protocols for this have changed substantially, but they were never public in the first place.

The "isabelle build" shell wrapper is merely some old-fashioned bash access to the rich functionality of isabelle.Build. Both are equal in being user-space tools to work with Isabelle systematically -- it does not make sense to say bash is user-space and Scala not. (Bash is actually quite far removed for Isabelle users on Windows, so it will gradually be de-emphasized in favour of Isabelle/Scala, also with some GUI wrappers.)


	Makarius





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