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

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

Dmitriy