[isabelle-dev] "set_comprehension_pointfree" simproc losing bounds

[Lukas Bulwahn]

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