[isabelle-dev] I don't understand isatest AFP report

[Ondřej Kunčar]

On 05/15/2013 01:28 PM, Gerwin Klein wrote:
>
> On 15.05.2013, at 8:01 PM, Ondřej Kunčar <kuncar at in.tum.de> wrote:
>
>> Hi!
>>
>> This is the last report about AFP from isatest:
>> The status of the following AFP entries changed or remains FAIL:
>> [Containers] was removed. Last status was ok.
>> [Launchbury] is new. Status is ok.
>>
>> Full entry status at http://afp.sourceforge.net/status.shtml
>>
>> AFP version: development -- hg id 3f56bba4ee3a
>> Isabelle version: devel -- hg id e116eb9e5e17
>> Test ended on: macbroy2, Tue May 14 12:28:46 CEST 2013.
>>
>> ========
>>
>> It says that Containers was removed. But does it actually mean FAIL? Because Containers is currently broken because of my changeset but I didn't learn about it. And this web page doesn't list Containers at all (because it was removed? but it's still in the repository though):
>> http://afp.sourceforge.net/status.shtml
>
> What's going on is that the somewhat primitive AFP test doesn't understand the output of "isabelle build" correctly.
>
> It's currently getting its list of sessions by scanning through the output, trying to find messages for failed or successful sessions. This worked reliably for IsaMakefiles, because there was a separate invocation for each session and there was delimiting output before/after each session. Of course, that didn't provide any parallelism or other goodies.
>
> In this instance, there was some kind of JVM problem which then caused the scan on the AFP test side to miss the Container session entirely and the tool therefore concluded that it must have been removed.
>
> We've had other failures before, were "build" failed globally because a file dependency was missing, and the AFP test then concluded that all sessions must have been removed.
>
> All of that is pretty unstable communication based on a lot of assumptions on my part. I should probably re-think how AFP test determines if a session was successful or not.
>
> First cut a this:
> - get a list of entries separately, i.e. from the thys/ROOTS file
> - try to identify only successful sessions from "build" output
>
> With that, we'd get correct "removed/new" messages, and failure messages when anything unexpected happens.
>
> Does this sound reasonable?

For me it does.

Thanks for the explanation.

Ondrej