Email Gateway (Aug 18 2022 at 12:28): Email Gateway (Aug 18 2022 at 12:28):From: Alexander Krauss <krauss@in.tum.de>
Dear Jeremy,
All the worries you describe are definitely serious problems, and most
people on this list have probably experienced this in one or the other
way. Different releases of Isabelle are hardly compatible on the ML
level and even the theory level requires a fair amount of changes from
one release to the next. This is especially true for the transition
2005->2007, due to the many accumulated changes.
These issues seem to be capable of causing massive and unnecessary
difficulties.
However, I cannot agree that these difficulties were unnecessary. How
could they be avoided? Not making any incompatible changes to Isabelle
anymore would essentially stop history and carve the current state of
the art into stone.
The alternative - maintaining various compatibility layers that
implement all interfaces and functionality present in some old versions
So the only realistic chance is that users keep up with the development
and update their theories. Sticking to some old version may seem
convenient for some time but, as you describe, it locks you into a
closed world, where you cannot use other people's work and do not profit
from new developments. Updating your theories is an investment that pays
off finally. I agree that the 2005->2007 transition is undesirably
painful but we are trying to make releases frequent enough to avoid this
in the future. 2007->2008 is in fact not such a big deal (even with the
somewhat radical removal of sets as a separate type).
Embrace change!
Alex
PS. Anyway, what aspects of the documentation are actually tested?
The (old) Isabelle Reference Manual and the various "Logics"
descriptions are still plain latex documents and hence cannot be tested.
Everything else is generated from theories.
Email Gateway (Aug 18 2022 at 12:28):From: Makarius <makarius@sketis.net>
This is also my experience. Even though ML interfaces often change
substantially, it is usually reasonable easy to port old code (thanks to
static type-checking in ML).
Proofs are much more fragile, notably unstructured ones. One way around
this is to submit theory libraries and applications to
http://afp.sourceforge.net/ where they get updated to latest Isabelle
automagically.
Makarius
Email Gateway (Aug 18 2022 at 12:29):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
In attempting to run Isabelle 2008, I get
jeremy@stiletto:~/isabelle/2008/gen$ isabelle
Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters (h=204800K,ib=40960K,ip=100%,mb=45056K,mp=20%)
Mapping
/home/users/jeremy/isabelle/heaps/Isabelle2008/polyml-4.1.4_x86-linux/HOL
Mapping /home/users/jeremy/Isabelle2008/../polyml/x86-linux/ML_dbase
Poly/ML 4.2.0 Release
Goal "X";
Exception- ERROR "Unknown context" raised
In Isabelle 2007 (and prior) this works fine
jeremy@stiletto:~/isabelle/2007$ is07
Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters
(h=512000K,ib=102400K,ip=100%,mb=106496K,mp=20%)
Mapping /home/users/jeremy/Isabelle2007/heaps/polyml-4.1.4_x86-linux/HOL
Mapping /home/users/jeremy/Isabelle2007/../polyml/x86-linux/ML_dbase
Poly/ML 4.2.0 Release
Goal ;
val it = fn : string -> Thm.thm list
Goal "X";
Level 0 (1 subgoal)
X
What has happened here?
Jeremy
Email Gateway (Aug 18 2022 at 12:29):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 12:29):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
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)
X
1. X
val it = [] : Thm.thm listWhat 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.Makarius,
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?
Regards,
Jeremy
Makarius
Email Gateway (Aug 18 2022 at 12:30):From: Makarius <makarius@sketis.net>
Simp_tac and simpset: unit -> simpset are indeed legacy features, too,
although not explicitly marked as such. When embedding ML into Isar proof
text, say via the method called "tactic", you can refer to the simpset
from the context via the @{simpset} antiquotation.
Makarius
Email Gateway (Aug 18 2022 at 12:30):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Makarius wrote:
Makarius,
Well, this is all very well, but I have dozens of emails showing that I
tried to understand what these antiquotations do and why I should use
them.
When I failed to achieve any such understanding, I tried using them
anyway, because you and others in Munich were so adamant that I should,
saying that using the alternative calls would lead to errors.
The result of this was that introducing antiquotations into my code
_caused_ errors, which were fixed when I reverted to not using them.
Regards,
Jeremy
Last updated: May 03 2024 at 12:27 UTC