[isabelle] Running ML in a theory context from the command line



Dear list,

with the help of Makarius and Joe Hurd, OpenTheory can now be fully
loaded into Isabelle/Pure:

https://github.com/isabelle-prover/opentheory-component

Inside an interactive environment, e.g. Isabelle/jEdit, it is possible
to call the tool via "Open_Theory.main".

I am trying to figure out if this can also be done from the command
line, as an Isabelle tool. There's already precedent, e.g. the various
"tptp" tools from Jasmin.

In "tptp_sledgehammer", for example, a theory file is constructed that
imports some root theory and contains an ML snippet. It is then called
via "isabelle process". This of course works, but I was wondering
whether there's a more direct way, e.g. with "isabelle process -e". But
I'm not sure what the correct incantation is to make it evaluate the ML
snippet in the context of a theory, so that the "Open_Theory" structure
is available.

Cheers
Lars




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