[isabelle-dev] "set_comprehension_pointfree" simproc losing bounds

Makarius makarius at sketis.net
Fri Oct 19 14:22:06 CEST 2012

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 

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.


More information about the isabelle-dev mailing list