Re: [isabelle] using Isabelle programmatically
On Fri, 10 Apr 2015, Viorel Preoteasa wrote:
Ideally I would need an API available in Python which does what I need:
Simplifies a term based on a specific theory. I understand now that this
API is available for Scala, and of course for SML, so in the future I
may use Scala.
On the other hand, even if using SML, getting started with it does not
seem easy. I tried to find the right functions for this job before
posting the question to the mailing list.
Do you mean SML as a language, or Isabelle/ML as a language + library?
Getting started with Standard ML should be easy, using resources on the
web or text books.
Getting started with Isabelle/ML should be easy as well, since the
Isabelle Prover IDE allows to explore whatever you see, down to its actual
definition. Tools are defined in Isabelle/ML, so the standard PIDE
control-hover-click over Isar commands, methods, attributes etc. will show
the relevant ML definitions.
Reading and understanding that needs some practice and some guidance,
though. The "implementation" provides many explanations of many things,
but it is not a quick-and-dirty HOWTO guide.
Depending on what you ultimately want to achieve, some decent Isabelle/ML
could work out easier and more robust than tinkering with scripting
languages, processes, generated sources etc.
This archive was generated by a fusion of
Pipermail (Mailman edition) and