On Mon, 3 Sep 2012, Makarius wrote:
On Sat, 1 Sep 2012, Lars Noschinski wrote:
I found the rebuilding behaviour of "isabelle build" w.r.t. document output
a bit strange: When the session was recently built it skips the session,
even if the document_output directory does not even exist; so you always
need to force a clean build.
In some sense the document (and browser_info) aspect of the session is
still an unmanaged add-on. So the "-c" is likely to happen there more
often, but I've tried to make this work more smoothly than before.
This is a step backwards when compared to a correct Makefile, which
will always rebuild all needed files.
In all these years I have hardly ever seen a correct or complete
Makefile. For Isabelle "make" it is now an episode of the past -- we
have suffered from that long enough.
Another observation: many everyday applications are about quick document
generation from theories, not "build" of big sessions with lots of
dependencies.
So the solution to avoid both -c and the overhead to determine
dependencies is to run the session straight away, without any up-to-date
checks. This would accomodate the typical edit-run cycle of Isabelle
document preparation.
So another option like "isabelle build -r" might do the job, but it needs
some further rethinking.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
