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

[Makarius]

On Thu, 13 Feb 2014, Makarius wrote:

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

I would like to thank Florian Haftmann for resolving this silently in 
Isabelle/b7f4da504b75.

Thus we are again one step closer to a situation where all of Isabelle + 
AFP can be loaded into a single Prover IDE session, without having to 
think about odd cases.  I have already some concrete ideas how to overcome 
the global theory naming problem, without too many upheaveals.


 	Makarius