On Mon, 15 Nov 2010, Alexander Krauss wrote:
I remember some offline discussions last year about having an Isabelle
tool that extracts file dependencies from theory sources (probably
starting from some special "session" file, which specifies the "root
theories") and outputs it in a simple textual format. I also remember
that Makarius already had the important ingredients for such a tool.
That was the state last winter: relatively robust parsing of headers
(which is surprisingly difficult to get right due to strange 16bit chars
on the JVM) and some rudiments of "session management".
Here are some examples for the "isabelle scala" toplevel:
import isabelle._
val system = new Isabelle_System
val header = new isabelle.Thy_Header(system.symbols)
header.read(system.platform_file("~~/src/HOL/HOL.thy"))
val manager = new Session_Manager(system)
manager.component_sessions()
The enumeration of component sessions depends on "session.root" files
sprinkled in the relevant directories. Right now "touch session.root"
will do the trick, because the content is not processed at all.
I am asking because Lars, Florian and I had this discussion again today.
If we had such a tool, we would actually be willing to spend some time
trying to replace the user-written (rather: copied) IsaMakefiles in the
AFP with a single generated one. (Lars seems to be a "make" expert, and
he had some realistic ideas on simplifying the whole setup). In
particular, this would allow parallel builds of the AFP using make -j.
Last winter my plan was to generate make files and let some of the many
variants of make do the job, not just GNU make -j also some of these
distributed make systems around.
In the meantime, I have mentally moved away from make more and more: it
comes with a huge legacy (compatibility issues, inherent limitations like
lack of support for spaces or unicode in file names, absence of make on
most end-user systems etc.) These problems are not relevant for
administrative tasks for AFP, of course.
Presently my main concern is to get the interactive session management for
Isabelle/Scala right, by a fully internalized process management. I have
already reworked the basic process wrapper several times, and merely need
to add existing parallel processing facilities on top (using threads or
actors as usual).
I wanted to have that in "fall", but it is probably going to be around
Christmas again. The lack of interactive session management is one of the
main showstoppers for realistic applications of Isabelle/jEdit right now.
Ultimately, the division of batch mode vs. interaction should disappear
altogether, but this could take quite some time. So reworking batch mode
independently could make some sense. 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.
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
