[isabelle-dev] Isabelle manuals as regular session documents
makarius at sketis.net
Mon Sep 3 17:16:54 CEST 2012
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
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
So another option like "isabelle build -r" might do the job, but it needs
some further rethinking.
More information about the isabelle-dev