Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)

On Wed, 8 Oct 2008, Jeremy Dawson wrote:

> In attempting to run Isabelle 2008, I get
> >  Goal "X";
> Exception- ERROR "Unknown context" raised

> In Isabelle 2007 (and prior) this works fine
> > Goal "X";
> ### Legacy feature: old goal command
> Level 0 (1 subgoal)
> X
> 1. X
> val it = [] : Thm.thm list
> What has happened here?

Even in Isabelle2007 it clearly says that the old ML Goal command is a 
legacy feature -- few contemporary Isabelle users will remember that it 

Legacy features just disappear at some point.  In Isabelle2008 the ML 
function still happens to be around, but does not work without a proper 
context -- almost everything in Isabelle needs one.

In the forthcoming Isabelle release even plain ML bindings already require 
a context -- we will have a purely functional ML toplevel that works 
seamlessly with undo and multithreading.

There are two ways to issue ML stuff *with* a context:

  * Either: use the 'ML' command within the Isar toplevel, usually within 
    Proof General.  This is the regular, preferred way.

  * Or: startup a raw tty Isar loop, e.g. using "isatool tty", enter a 
    theory, exit, poke around in ML, re-enter Isar:

      $ isatool tty -l HOL
      > theory A imports Maib begin
      > exit
      ML> ...
      ML> Isar.loop ()

    This scheme is useful for debugging in rare situations, e.g. when 
    there are problems in conjunction with the Isar toplevel itself.


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