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-...@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
Locale_Sublocale_Morphism_Cycle.thy
Description: application/extension-thy
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
