On Wed, 21 Nov 2012, Tobias Nipkow wrote:
Most of the theories in there are loaded via Library.thy. But a few are
loaded via ROOT. What is the rational for this subdivision?
There is a longer history behind this, where I started some parts, and
others continued. So I don't know all the answers.
Historically, the idea of the universal Library.thy that includes
everything was to ensure that these theories are at least as compatible
with each other that they can be merged into one big theory. It might
also help users to import Library, like they would do for Main, but I am
unsure if this happens in practice. It is also useful for testing, to
have just one import to care about (with old-stype use_thy on the tty).
The latter aspect is gradually being superseded by the ROOT setup: it
tells which collection of theories (without merging) contribute to a
session. In the next round of the reforms the Prover IDE should be able
to import all of them in interactive mode, like build does in batch mode.
The theories that are not included in Library.thy are somehow in conflict
with other theories, or augment the context in ways that are better not
done by default (certain global syntax or type-class instantiations).
It looks like code generation is the difference, but why?
I can't say anything specific, only point to the 2-3 FIXMEs in
Isabelle/bc82d25af543 in this respect (in src/HOL/ROOT and
src/HOL/Library/Library.thy).
When there is a oddity, and a reason not to import things, just don't do
it and make a clear statement about it in the changelog. The history is
the place to explain why things are done in a certain way at that point,
not the source. Otherwise the source would become overcrowded by history
rather quickly, and nobody could read it anymore.
Think of it like an wikipedia article: the actual text and the discussion
leading to the text are clearly separated.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
