[isabelle-dev] HOL/Library/Code_Prolog.thy breakdown
traytel at in.tum.de
Thu Feb 13 13:08:18 CET 2014
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
> 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.
More information about the isabelle-dev