[isabelle-dev] Interrupt exception
ldixon at inf.ed.ac.uk
Wed Jul 15 12:46:09 CEST 2009
> On Wed, 15 Jul 2009, Lucas Dixon wrote:
>>>> apply (unfold Product_Type.pair_collapse[symmetric, of "al"])
>>> The equation Product_Type.pair_collapse[symmetric, of "al"] can be
>>> unfolded forever, so the method invocation does not terminate, leading
>>> to an unspecified behaviour of the system!
>> The point was just that unfold should probably be giving an error
>> message of some more readable sort.
> The interrupt exception is probably produced by the Poly/ML runtime
> system when it runs out of resources. The behaviour might have changed
> a bit in recent internal versions. Which one did you use?
Yes, I'm sure you are right; I'm using Isabelle (1d4d0b305f16: date:
Fri Jul 10 09:24:50 2009 +0200), and PolyML (svn 801, 2009-07-12)
The problem came up when I was writing a tactic and I wanted to unfold
all occurences within a goal but not do this recursively - I wanted any
introduced occurrences to be untouched. I was simulating this within a
tactic script as an experiment. But perhaps the idea of unfold all
current occurrences (modulo critical pairs) would be a sensible
semantics for unfold? It seems like a sensible semantics for something,
call it unfold or something else :)
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
More information about the isabelle-dev