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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
