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

[Andreas Lochbihler]

Here's a summary of the story with Containers:

AFP/db25a6127308 to AFP/58dc11da7731 add the Containers entry to AFP-devel in the version 
that works with Isabelle2013.

In AFP/664abd899c58, Gerwin dropped the import of Code_Char_ord that Florian removed in 
Isabelle/599ff65b85e2. This implicitly dropped the import of Char_ord, which caused some 
even more errors.

In AFP/599ff65b85e2, Dmitriy dropped the session Containers-Benchmarks to avoid crashes in 
the build tool.

AFP/3f56bba4ee3a contains all the necessary adaptations to run with Isabelle/ae755fd6c883 
and re-activates Containers-Benchmarks.

Unfortunately, this situation lasted only for less than 4 hours. Isabelle/a4d81cdebf8b 
breaks Containers again, but Ondřej did not notice because the AFP test report is strange.

Andreas

On 15/05/13 13:09, Makarius wrote:
> 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
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>