[isabelle-dev] Extracting dependencies from theory headers

[Makarius]

On Fri, 19 Nov 2010, Alexander Krauss wrote:

> - 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)?

In principle the relatively recent "master path" concept should solve all 
that, but its needs to be done right once and for all in the Scala layer. 
The add_path stuff should disappear at some point, with the usual delay in 
deleting old features.


>> 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)

OK, it sounds like Hudson is one of these SVN-based tools that have been 
superficially adapted for the current genration of version control.


 	Makarius