[isabelle-dev] Global build failures of the AFP in the testboard

Dmitriy Traytel traytel at in.tum.de
Wed May 15 16:14:49 CEST 2013


Am 15.05.2013 15:48, schrieb Makarius:
> What is still unclear to me after so many years of testboard is how it 
> actually used in practice.  I just do "isabelle build -j4 -a -d 
> '$AFP'" to see immediately how everything works out.  It is also 
> possible to make a quick integrity check via "isabelle build -n -a -d 
> '$AFP'".
Actually, "isabelle build -j4 -a -d '$AFP'" was almost exactly what I 
did before I ran into this error. Here, I've used the testboard merely 
as a reference.

Another use case is the process making SML/NJ happy. I am aware that it 
is currently (e.g. in 4517ceb545c1) unhappy about BNFs.

But there are also heavier users of the testboard than me.

Dmitriy



More information about the isabelle-dev mailing list