[isabelle-dev] Extracting dependencies from theory headers
krauss at in.tum.de
Fri Nov 19 00:37:16 CET 2010
> 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
- 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.
More information about the isabelle-dev