On Wed, 17 Oct 2012, Lukas Bulwahn wrote:
If you update to changeset 89b118c0c070, the issue should be resolved.
There still seem to be remaining issues: Isabelle/d1ecb3554b25 and
AFP/15527cc14202:
Girth_Chromatic FAILED
(see also
/Volumes/Macintosh_HD/Users/makarius/.isabelle/heaps/polyml-5.5.0_x86-darwin/log/Girth_Chromatic)
### Simplifier: renamed bound variable ":000" to ":000a" (line 588 of
"/Volumes/Macintosh_HD/Users/makarius/isabelle/afp-devel/thys/Girth_Chromatic/Girth_Chromatic.thy")
...
*** Tactic failed
*** The error(s) above occurred for the goal statement:
*** {(a, b). a : :000 & b : :000 & a < b} =
*** {(a, b) |a b. a : :000 & b : :000 & a < b}
*** (line 168 of
"/Volumes/Macintosh_HD/Users/makarius/isabelle/afp-devel/thys/Girth_Chromatic/Ugraphs.thy")
The final crash is one thing, the long list of the above warnings another.
The warning means that the context for a nested simplifier invocation is
not right. Operations like Simplifier.context, Simplifier.inherit_context
should help here. Once that is repaired, I will see if the warning can
now be made an error that is more explicit about the reasons.
Generally, there has been quite some breakage of AFP during the week, even
though it is now quite simple to run a full test of it over lunchtime. It
now takes 45min for Isabelle + AFP all-inclusive on 8 cores: Damien
Doligez calls this the "commuter constant", the time that is bearable to
spend for recurrent moves in everyday life.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
