On 05/15/2013 01:28 PM, Gerwin Klein wrote:
On 15.05.2013, at 8:01 PM, Ondřej Kunčar <[email protected]> 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
