[isabelle-dev] AODV

[Gerwin Klein]

Only the “everything” session should ever be run in a normal test, the other sessions are for convenience while developing only.

This is why AODV is in group “AFP” and the others are not. There are other entries that have similar setup, i.e. “build -a” will usually do too much. The best way to test the afp is to use the afp_build tool (in afp/tools), e.g.

isabelle afp_build -A

This will also select the right latex setup etc (the AFP needs to be set up as a component for this to work).

If the everything session times out for you consistently, we should probably increase the time limit.

Cheers,
Gerwin

> On 7 Dec 2014, at 2:18 am, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
>
> I noticed that the ROOT of AODV contains one big session for everything
> as well as separate sessions for the different variants.
>
> In my current setup, this is a little bit unfortunate.  When running
> tests I usually do
>
>       build -a -d "${AFP}"
>
> i.e. test distribution and AFP simultaneously, particularly to have the
> voluminous sessions like JinjaThreads started as early as possible.
>
> With the current setup, this effectively runs the AODV matter twice – or
> at least attempts so, since the »everything«-session times out.
>
> Maybe it would be better using ISABELLE_FULL_TEST rather than session
> groups to separate the two kinds of AODV sessions.  Any ideas or
> suggestions?
>
> Thanks a lot,
>       Florian
>
> --
>
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.