[isabelle-dev] HOL/Library/Code_Prolog.thy breakdown

[Dmitriy Traytel]

Am 13.02.2014 13:08, schrieb Dmitriy Traytel:
> Am 13.02.2014 12:48, schrieb Makarius:
>> Today isatest has reported a breakdown of HOL/Library/Code_Prolog.thy.
>>
>> This was undetected in a more regular test due to this change that 
>> removed it from the normal HOL-Library session:
>>
>> changeset:   38504:76965c356d2a
>> user:        haftmann
>> date:        Wed Aug 18 09:46:59 2010 +0200
>> files:       src/HOL/Library/ROOT.ML 
>> src/HOL/Tools/Predicate_Compile/code_prolog.ML
>> description:
>> removed Code_Prolog: modifies global environment setup 
>> non-conservatively
>>
>>
>> The mysterious modification of the global environment above was a 
>> redefined outer syntax command "values", with slightly different 
>> behaviour than the normal one.  Such a "poke" into the outer syntax 
>> affects the whole prover process, it escapes the context of the 
>> loaded theory and provokes erratic behaviour.
>>
>> The ability to redefine outer syntax commands is merely an accidental 
>> left-over from the distant past.  It is required in interactive mode, 
>> to allow repeated processing of the (one!) command definition, but 
>> even that restricted scheme is apt to surprises as everybody knows.
>>
>>
>> So apart from some repairs of 
>> src/HOL/Tools/Predicate_Compile/code_prolog.ML in a76c679c0218, the 
>> changeset e42a3fc18458 makes more clear (in batch mode) that 
>> redefining outer syntax commands is not supposed to happen. This 
>> provides a window of opportunity to remove spurious redefinitions 
>> elsewhere, until the coming release.
> If nobody stops me, I will take care of 
> "~~/src/HOL/ex/Interpretations_with_Defs". It's redefinition of the 
> interpretation command disturbed me already for a while.
For the record: I have been stopped.

Dmitriy