[isabelle-dev] Regression in the sublocale command

[Clemens Ballarin]

I forgot to attach the example.  Loops here also for 4862f3dc9540 (12 Feb 2015).

Clemens


On 14 February, 2015 14:25 CET, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote: 
 
> Hi Clemens,
> 
> I am struggling to reproduce the behaviour you describe.  Find attached
> my attempt to contrieve an example.  Unfortunately, the looping is not
> reproducible in c3ca292c1484.  Can you provide more detail?
> 
> Thanks,
> 	Florian
> 
> Am 12.02.2015 um 22:19 schrieb Clemens Ballarin:
> > Hi Florian,
> > 
> > I'm investigating a regression which prevents identifying certain equivalent locales through circular sublocale declarations:
> > 
> >   sublocale loc1 < x: loc2 A c (* sigma_1 *)
> >     where "x.b == B" and "x.d == e" (* tau_1 *)
> >   sorry
> > 
> >   sublocale loc2 < x: loc1 A b (* sigma_2 *)
> >     where "x.c == C" and "x.e == d" (* tau_2 *)
> >   sorry (* loops from changeset 8fab871a2a6f *)
> > 
> > The last "sorry" loops, which is unfortunate, because it forces certain workarounds on my current project.  In a fairly lengthy debug session I figured out that it is the simplifier that loops.  This is an indication that the morphisms tau_1 and tau_2 are applied simultaneously, which they should not.  In any case, the behaviour appears to have been introduced quite a while ago in 8fab871a2a6f, which is in the first batch of your changes to the locale interpretation commands.
> > 
> > Clemens
> > 
> > _______________________________________________
> > isabelle-dev mailing list
> > isabelle-dev at in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> > 
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
 
 
 
 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Scratch.thy
Type: application/octet-stream
Size: 551 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150214/a2253c93/attachment-0002.obj>