[isabelle-dev] Extracting dependencies from theory headers

[Makarius]

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