Re: [isabelle] using Isabelle programmatically



On Fri, 10 Apr 2015, Viorel Preoteasa wrote:

After asking on the mailing list, the answer by Lars, was very helpful
(ML‹Simplifier.rewrite @{context} @{cterm "rev []"}›), but it was working
within an Isabelle theory only, and not as standalone Isabelle/ML program.

Isabelle/ML always runs in such a formal context, i.e. inside a theory or a more deeply nested context that is built up by other means. In such a situation the ML antiquotation @{context} provides the all-important context at compile time. When you implement your own tools, say a command or proof method, you get the context at runtime from the system infrastructure -- that is in fact the normal situation.

The final Isabelle/ML program which does what I need is the following:

use_thy "AutoSimp";
val thy = Thy_Info.get_theory "AutoSimp";
fun term_to_string ctxt t =
 let
   val ctxt' = Config.put show_markup false ctxt;
   in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;

val ctxt = Proof_Context.init_global thy;
val t = Syntax.read_term ctxt "rel (ExampleA0) (si_f) (d,so_f)";
val simp_term_a = Simplifier.rewrite ctxt (cterm_of thy t) |> Thm.rhs_of;
val simp_term_b = term_of simp_term_a;
val result = term_to_string ctxt simp_term_b;
writeln result;

This is not an Isabelle/ML program, but raw SML outside of the Isabelle environment. You won't get very far for non-trivial things. E.g. the whole Isabelle/HOL modules and tools are not accessible -- in fact the accessibility of Isabelle/Pure outside the normal Isabelle environment is merely an artifact of bootstrapping.

As the system manual points out, use_thy is the main thing you can do in this raw ML bootstrap environment, i.e. to get into some theory context to do the actual work.


It is not clear to me if it is better to use this program as such or embed
as ML{*...*} into a theory file. In the end I am only interested in the
string from the variable result.

ML {*...*} is always better, unless there is a very special situation. ML_file is the same and useful for bigger text files, also with more
support in the editor.


Scala can be a good solution, however Python is also a convenient language. Isabelle/ML can also be a solution, but the problem remains the same, figuring out the right functions for solving the problem.

Many years ago, I was considering Python as Isabelle system programming language, but it later became Scala. Today, you can do a fair amount of system programming both in Isabelle/Scala and Isabelle/ML, and it is initially hard to tell which side is better for an application. There are also applications on both sides, which requires some bilingual fluency. But the Isabelle/Scala and Isabelle/ML conventions and libraries are as close to each other as feasible.

E.g. there is Isabelle_System.bash to invoke an external process running a shell script both in Isabelle/ML and Isabelle/Scala.


Passing strings from one program to another does not seem such a big problem, and Python has a simple API for working with external programs.

By the way, how is the communication between Scala and Isabelle/ML done? I assume it is also by having the Isabelle/ML process running in the background, and by sending and receiving strings via pipes.

That is a very crude model, and the reality with something that actually works robustly and efficiently came out a bit different than I anticipated 7 or 8 years ago. My ITP 2014 paper has a small section on PIDE architecture and protocol layers: http://www4.in.tum.de/~wenzelm/papers/itp-pide.pdf -- another version of that aspect is explained here for Coq (!) http://arxiv.org/abs/1304.6626

So Isabelle/PIDE solves that prover connectivity problem. It just needs to be reused. The usual errors and mistakes don't have to be repeated.


	Makarius


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