[isabelle-dev] AODV

Tobias Nipkow nipkow at in.tum.de
Wed Dec 10 08:32:15 CET 2014

On 09/12/2014 21:50, Makarius wrote:
> On Wed, 10 Dec 2014, Gerwin Klein wrote:
>> “build -a” is still going to miss document preparation errors in the AFP,
>> though, so it’s still not really the right command to run for testing it.
> We've had that discussion occasionally.  Nowadays I usually do full "build -a -d
> '$AFP'" quite aggresively, but rarely -o document=pdf.  It is just a matter to
> get the most relevant information out of the test.

For the AFP test we don't want to most relevant or most of the information but 
all of it. It is as simple as that.


> Document preparation adds
> very little, and quite often it is just a problem of the LaTeX installation anyway.
> This canonical "build -a" will eventually become a certain mode of using PIDE,
> but without any add-on features such as -g AFP.
>      Makarius
> ----------------------------------------------------------------------------
>                  https://stop-ttip.org/signatures-member-states
> ----------------------------------------------------------------------------
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5059 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141210/9a6ccd36/attachment.bin>

More information about the isabelle-dev mailing list