[isabelle-dev] isabelle build glitch

Makarius makarius at sketis.net
Fri Nov 16 14:09:30 CET 2012


On Tue, 30 Oct 2012, Lars Noschinski wrote:

> I deleted and reverted $ISABELLE_HOME/lib. Now everything seems to work 
> again. As a data point: While executing the first "isa build", another 
> instance of this Isabelle instance was running.

This should already be sufficient to explain it: the build process 
silently assumes sequentialism, like many other administrative scripts in 
Isabelle.

I have been applying the "Clint Eastwood approach" to sequential things in 
regular Isabelle user space in the past couple of years: shooting first 
when they show their face, and then ask questions. For non-user-space 
things like online build of certain components, I don't have any such 
ambitions.  You are supposed to take care of it yourself, like you did 
here already.  It is just one of these difference in comfort of official 
releases compared to self-build repository snapshots.


 	Makarius


More information about the isabelle-dev mailing list