Re: [isabelle] How to use Isabelle/Isar as a compiler?

> Date: Mon, 4 Apr 2011 22:32:07 -0400
> From: Anh Le <anhlevn at>
> Subject: [isabelle] How to use Isabelle/Isar as a compiler?
> To: cl-isabelle-users at
> Message-ID: <BANLkTinv-3S3pAgyKbFmYEfM_2EPk34M3w at>
> Content-Type: text/plain; charset=ISO-8859-1
> Hi everyone,
> Is there any way that we can use Isabelle/Isar as a compiler?
> For example, how do we run a command like:
> $ ./isabelle MyTheory.thy
> And then isabelle will do as the Proof General processes the whole buffer,
> and will return the first found error if it exists.
> Hi,

Recently I wrote a small expect script to do the same, it is attached along
with this mail. It uses the Isabelle tty tool. You should copy (don't link)
it to your isabelle_home/bin directory where the 'isabelle' script resides.

The script needs 'expect' tool to be present in /usr/bin/
You can use this tool by passing your theory file as an argument. If
successful it returns 0 else 1.
Ex: bin/thm-validator test.thy

Sree Harsha Totakura
Technische Universität München

Attachment: thm-validator
Description: Binary data

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