[isabelle-dev] HOL/Library/Code_Prolog.thy breakdown
traytel at in.tum.de
Thu Feb 13 13:51:45 CET 2014
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
>> removed Code_Prolog: modifies global environment setup
>> 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.
More information about the isabelle-dev