[isabelle-dev] AODV

[Gerwin Klein]

> Back to afp_build: I merely made that in 2012 as an example how to map the old shell scripts to the new Isabelle build setup.  I never use afp_build myself, but just plain "isabelle build".  One day I also hope to be able to load all of AFP into a single PIDE session, to edit it without without
> having to think about it.

afp_build doesn’t do anything special, it’s just “build -g AFP” with a few document options.


>> Maybe I cannot keep this up any longer, but are there other people around which prefer a similar setup!?
> 
> "Any longer" sounds as if afp_build would be more up-to-date than plain Isabelle build, but the situation is the opposite.
> 
> 
> So just the canonical questions:  What is the purpose of having these duplicate shadow sessions in the first place?  They look suspiciously like imitations of old IsaMakefiles before Isabelle build -- when it was very difficult to make private ad-hoc sessions for development or special testing.

I don’t see any connection to IsaMakefiles here. They are just smaller sessions to build variants in isolation if you’ve worked on only one variant, which happens often when you develop. No need to wait for 1:40h, if you can wait for 20min to get the same result. If you just have them open in jedit it’s too easy to overlook a small red bar somewhere.

Maybe that use case is now much rarer, so we could indeed move them out into their own file.


> for AODV the situation appears to be more complicated due to the many individual theories in the ROOT.  One way to avoid that is to group theories within the session itself by auxliary theories with suitable imports.  Another way is to make an auxiliary ROOT that resides in some subdirectory of AFP/thys/AODV and is only included by the few people need them occasionally (using -d DIR in "isabelle build" or "isabelle jedit").

We could do that. “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. 

Gerwin