[isabelle-dev] HOL/Library/Code_Prolog.thy breakdown
makarius at sketis.net
Fri Feb 28 15:55:50 CET 2014
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
> 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
> 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
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.
More information about the isabelle-dev