[isabelle-dev] Isabelle manuals as regular session documents

[Makarius]

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