[isabelle-dev] Extracting dependencies from theory headers

[Alexander Krauss]

Makarius wrote:
> Here are some examples for the "isabelle scala" toplevel:
[...]

Thanks, these are good pointers.

Unfortunately, this is (once again) harder than I thought. Here are the
issues/questions:

- Relative paths are not resolved by the current simple parser. I
remember that there used to be some oddities in PG related to relative
paths. I am not sure what the situation is now. What is the meaning of a
relative path in an "imports" or "uses" declaration?

- Related to the above: Dynamic load path modifications via "add_path"
(as e.g. in HOL/Plain.thy) are a show-stopper, since they make it
impossible to see what an Import refers to just by looking at headers.
These would have to be replaced by something static, possibly a property
of the session. Question: What are typical uses of add_path, other than 
the two instances in the current distribution (which set the library 
path, once for HOL and once for HOLCF)?

> After our very brief 
> excursion into "distributed make and queue management" last year, the 
> main new aspect from this year was http://hudson-ci.org/
> 
> Did anybody take a look at that?  At least the website looks nice and 
> simple.  It is all JVM-based and seems to support Mercurial projects, too.

I looked at it, but I found the design fairly inflexible. Its Mercurial 
support is limited to testing the tipmost revision when it comes in. 
Aggregation is nice (weather icons etc.), but all data seems to be 
time-indexed and not revision-indexed. It could be a replacement for the 
current isatest if somebody manages to set it up properly. But it will 
not do any of the following:
- developer-initiated tests of unpublished changes
- automatic bisects
- multi-repository compatibility tracking (Isabelle vs. AFP)

Florian recently spent some time with our own testing tool, which is now 
in a better state. I still hope that this becomes reality in the 
not-too-distant future. But this is another story.

Alex