[isabelle-dev] I don't understand isatest AFP report
makarius at sketis.net
Wed May 15 13:09:41 CEST 2013
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):
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.)
More information about the isabelle-dev