[isabelle-dev] Naming context of ROOT.ML and similar.

[Thomas Sewell]

It would appear that with Isabelle-2009-1, the ROOT.ML or similar ML 
file called by isabelle usedir isn't allowed to do anything. Or at 
least, it's not allowed to know about any useful structures.

The clearest example we have is if I put the following in CKERNEL.ML (a 
ROOT.ML-like file in our repository).

use_thy "~/path-to-repository/lib/Crunch";

Crunch.crunch;

If I now run isabelle usedir -f CKERNEL.ML ., the log will conclude with 
these lines:

Loading theory "Crunch"
structure Crunch :
(contents of structure)
val it = () : unit
Error: Structure (Crunch) has not been declared
Crunch.crunch
At (line 3 of "CKERNEL.ML")
Exception- Fail "Static Errors" raised
*** ML error

I take it that all structures are somehow being purged from the context 
of the ML files called by usedir. Why? Do I need to have ROOT.ML and 
similar use_thy a Root.thy file just so it can use a ACTUAL_ROOT.ML file 
in order to get any work done? I suppose I only really need two files, 
since I could fold ACTUAL_ROOT.ML into an ML {* *} block in Root.thy. 
Still seems silly.

All I wanted was to enable Record.timing so the log would keep better 
track of progress while the image builds ...

Yours,
    Thomas.