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

Makarius wrote:
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)
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.


The "old" ML Goal command was introduced in October 1998!! It was said to _improve_ upon the old "goal" command, which _did_ require a context. Incidentally, the prove_goal command - which was purely functional, and the "goal" command, which required specifying the context, were left unchanged, even though the developers then thought that non purely functional code was preferable. Those users who preferred purely functional ML code were given the option to continue using it. They were not compelled to go to the inconvenience of changing all their code just because the developers then had a different preference. If few contemporary Isabelle users will remember that the Goal command existed, that means that, of those who used Isabelle when the Goal command was in common use, most are no longer Isabelle users. This may well be true, I wouldn't be surprised. But if few people can survive using Isabelle for more than a few years, that is not a great recommendation for it.

And what of the proofs those users did using Isabelle? Pen and paper proofs, once published, will still be in libraries for a hundred years. An Isabelle proof, using "Goal", will, in approach reflected in your email and other, have had a useful life of only a few years.

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.

Does this mean that all the functions involving an implicit context will disappear?
eg, Simp_tac, simpset, etc ?  My code is full of these.

I notice that the_context() has disappeared from Isabelle2008.

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.

Thanks. Incidentally, I notice that the_context() has disappeared from Isabelle2008. Once one has created the context by entering Isar and exiting it again, how does one get hold of it?




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