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

[Makarius]

On Wed, 15 May 2013, Ondřej Kunčar wrote:

> 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

I am also confused, and still trying to catch up with the ups and downs of 
this new session. Yesterday I had a working situation in 
Isabelle/ae755fd6c883 and AFP/0b521abc0487.

I have also spent some time to robustify the Isabelle build process 
(leading up to Isabelle/5fdca5bfc0b4) to prevent sessions bombing the JVM 
by producing tons of output.  Here it is via higher-order unification 
going amiss and producing lots of tracing messages.  I guess that is 
actually coming from some transfer tools.

We've had several surprises about HO-unification from TUM people recently, 
but I am still lagging behind to follow-up on all that.  (Basically, 
fully-general HO is rather ambitious and rarely used systematically in 
tool implementations these days.)


 	Makarius