[isabelle-dev] Global build failures of the AFP in the testboard
makarius at sketis.net
Wed May 15 16:34:48 CEST 2013
On Wed, 15 May 2013, Dmitriy Traytel wrote:
> 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
> Another use case is the process making SML/NJ happy. I am aware that it is
> currently (e.g. in 4517ceb545c1) unhappy about BNFs.
I am using the mira results on http://isabelle.in.tum.de/reports/Isabelle
myself a lot to navigate quickly to points where Isabelle and AFP diverge.
Is that already testboard? I thought that would be a slightly different
mode of operation to check quasi-interactively if something is ready for
More information about the isabelle-dev