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

Reply via email to