[isabelle] Interfacing Isabelle



On 11.06.2014 19:35, Eddy Westbrook wrote:
> Lars,
>
> Just saw your note about the low-level ways to interact with Isabelle;
> thanks for the pointer, btw.
>
> Is there any way you could point me to any documentation of /
> introduction to these features? I found some of Makarius Wenzel’s
> papers and talks about asynchronous proof processing, which discuss
> the concepts at a high level, but I haven’t been able to find anything
> yet to help me figure out the low-level details of how to actually
> talk directly to Isabelle.
Unfortunately, I do not have any experience in this area. It might be
worth skimming through Makarius' postings. He dropped some hints about
Scala/ML interaction over the time.

For terms in YXML format: As far as I understand, the standard
Isabelle(/ML) functions for parsing terms accept the "normal"
representation as well as the YXML representation; so one could just
generate theory files with the latter instead of the former (at expense
of human readability). There is this bit about it in the NEWS file:

    * The inner syntax of sort/type/term/prop supports inlined YXML
    representations within quoted string tokens.  By encoding logical
    entities via Term_XML (in ML or Scala) concrete syntax can be
    bypassed, which is particularly useful for producing bits of text
    under external program control.


So have a look at files at src/Pure/term_xml.{ML,scala} -- they describe
the XML representation of terms. YXML is just a (binary) representation
of (a subset of) XML. It should be described in either the
implementation or the system manual.

  -- Lars



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