[isabelle-dev] Extracting dependencies from theory headers
krauss at in.tum.de
Mon Nov 15 15:40:29 CET 2010
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.
More information about the isabelle-dev