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

[Dmitriy Traytel]

Am 15.05.2013 16:34, schrieb Makarius:
> 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 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.
>
> 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 push.
Right, I should have referenced "reports" rather than "testboard". From 
that perspective I use the testboard even less.

Dmitriy