On Wed, 10 Oct 2012, Makarius wrote:
After some detours I am now back on Isabelle/28e37eab4e6f.
So with the "ch-strict" changeset applied to the critical spot of local
notes, the namespace policy enforces the concentual locale scopes.
Applying this in practice leads to many surprises about situations found in
existing theory libraries, though. Some of the changsets leading up to
Isabelle/28e37eab4e6f already sort this out. Some other ad-hoc changes are
attached as ch-test here.
With Isabelle/28e37eab4e6f + ch-strict + ch-test and AFP/77f79b2076f1
the following sessions fail:
BDD, Dijkstra_Shortest_Path, Free-Groups, Group-Ring-Module, HOL-Algebra,
HOL-Number_Theory, HOL-ex, JinjaThreads, KBPs, Markov_Models, Ordinal,
Ordinary_Differential_Equations, Pi_Calculus, Presburger-Automata,
PseudoHoops, Psi_Calculi, Refine_Monadic, Simpl, Slicing, Topology,
Transitive-Closure-II, Valuation
So the question if ch-strict can be activated soon is mainly a matter of
library space. It is up to emerging volunteers to sort it out further.
What is the situation with this fine point of authentic local notes? The
general plan is to make Local_Theory.define/note more uniform in the name
space treatment, which is conceptually part of the game already, but was
not yet pushed through for various historical reasons.
Johannes has updated his sessions, but very little happened elsewhere.
Concerning accidental/unintended name clashes, the half-open question for
me is, how to name sublocale ranges more systematically. There might be
some conventions known by locale experts that are worth sharing here.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
