On 10/19/2012 02:22 PM, Makarius wrote:
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")
I was aware that there are still a couple of open issues, caused by the
newly introduced simproc.
At the moment, I am still hunting errors in the Isabelle repository, but
soon the errors in the AFP will be next.
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.
I am certainly in favour of this. First, tool developers mainly react on
errors with test runs, but do not see the warnings. Secondly, users do
not know who to report those warnings and do not know if they are caused
by their scripts or the tools.
Lukas
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
