[isabelle-dev] "set_comprehension_pointfree" simproc losing bounds

[Makarius]

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