[isabelle-dev] Regression in the sublocale command
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Sat Feb 14 10:11:59 CET 2015
Hi Clemens,
thanks for investigating this.
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.
I guess you found out using bisection. But I read some incertainty in
your words »appears to have been introduced«. Is the changeset
8fab871a2a6f a reliable entrance point or a first approximation?
I will have a closer look at this.
Cheers,
Florian
--
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: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150214/f811345c/attachment.sig>
More information about the isabelle-dev
mailing list