[isabelle-dev] Extracting dependencies from theory headers

[Alexander Krauss]

Dear list, (and Makarius in particular :-) )

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.

How far is it to get this working from the present state?

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.

Alex