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 
existed.

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.


	Makarius





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