[isabelle-dev] Global build failures of the AFP in the testboard
traytel at in.tum.de
Wed May 15 16:51:05 CEST 2013
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
> 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.
More information about the isabelle-dev