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
----------------------------------------------------------------------------_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
