[isabelle-dev] Regression in the sublocale command

[Florian Haftmann]

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: Locale_Sublocale_Morphism_Cycle.thy
Type: application/x-extension-thy
Size: 643 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150214/19ccaf75/attachment-0002.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150214/19ccaf75/attachment.sig>