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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
