[isabelle-dev] HOL/Library

[Makarius]

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