[isabelle-dev] AODV

[Makarius]

On Mon, 8 Dec 2014, Florian Haftmann wrote:

>> isabelle afp_build -A
>
> thats true, but I must confess I personally prefer the test of the 
> distribution and the AFP in *one* build session.  It gives early 
> feedback since the big AFP sessions start quite early then; when running 
> the AFP separately these sessions are usually »dangling behind«.

Having just one build system was indeed an important motivation for the 
Isabelle/Scala build tool from 2012.  We can be glad that we don't have 
the confusion of Coq, where every major library has its own way to make 
it, or not.  For example, see this interesting thread on Coq-Club "Proof 
assistants as routine tools" 
https://sympa.inria.fr/sympa/arc/coq-club/2014-11/msg00192.html with the 
slides http://www.qmac.ox.ac.uk/events/Talk%20slides/Neil%20Strickland.pdf

On the slide "Which framework?" he lists various library management 
problems of Coq and Agda, with the pro-forma entry "Isabelle etc.: 
mentioned for completeness".  This is odd, because in Isabelle most of the 
problems are solved, but Type-Theory guys usually can't look beyond their 
own system of choice.

Even the notion of "compiled distriution" is somewhat pointless.  Our heap 
images approximate that, but they are strictly speaking not needed at all: 
a proper persistent world image of the PIDE session could replace 
"compilation" for most purposes.


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.


> 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.

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").


 	Makarius

----------------------------------------------------------------------------
                   http://stop-ttip.org  1,063,743 people so far
----------------------------------------------------------------------------