Re: [isabelle] Fwd: Isabelle "Identity" Build Sessions



>In any case you should make sure that all add-on tex files are declared in
the 'files' section of the ROOT file -- this is not checked by the >system,
and thus reminiscent of the old IsaMakefiles.

I have not done that and this might have caused the problem. But the -c
option does the job nicely enough.

best!


On Wed, Nov 27, 2013 at 1:04 PM, Makarius <makarius at sketis.net> wrote:

> On Wed, 27 Nov 2013, Alfio Martini wrote:
>
>  Since my primitive solution mentioned bellow does not to seem to always to
>> work, I found the following
>> workaround: force cleaning before running the session again
>>
>> isabelle build -v -c -D Session
>>
>> Was this (cleaning) expected to be done (like in the old times of "make
>> clean" before rerunning the session?
>>
>
> Yes, build option -c is the standard way to enforce a clean build.
>
> In any case you should make sure that all add-on tex files are declared in
> the 'files' section of the ROOT file -- this is not checked by the system,
> and thus reminiscent of the old IsaMakefiles.
>
> The build system also takes changes of the ROOT specification and its
> options into account, but not changes of command line options. If you have
> run a session already without document or browser_info, but want it now
> with -o document=pdf -o browser_info you need to add -c to the command line
> to make double-sure.
>
>
> In some sense, the connection of batch builds with document preparation is
> just a historical accident.  I would like to see this eventually as part of
> the Prover IDE, without funny command line tools to be re-iterated all the
> time.
>
>
>         Makarius
>



-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
www.inf.pucrs.br/alfio
Lattes:  http://lattes.cnpq.br/4016080665372277
Associate Professor at Faculty of Informatics (PUCRS)
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.