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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
