[isabelle-dev] Regression in the sublocale command

[Florian Haftmann]

A few first traces.

The sublocale statements themselves are operative in Isabelle2013-1.
However, if put into a local context, the same situation as in
Isabelle2014 occurs:

context loc1
begin

sublocale x: loc2 A c (* sigma_1 *)
  where "x.b == B" and "x.d == e" (* tau_1 *)
sorry

end

context loc2
begin

sublocale x: loc1 A b (* sigma_2 *)
  where "x.c == C" and "x.e == d" (* tau_2 *)
sorry (* loops! *)

end

This might indicate that something is wrong in the local theory stack
here, maybe the last line in

> fun locale_dependency locale dep_morph mixin export =
>   (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
>   #> Locale.activate_fragment_nonbrittle dep_morph mixin export;

from generic_target.ML

However, I have to investigate this further to get a clear picture.

Note that »print_locale loc2« is already looping in Isabelle2013-1.

So far,
	Florian

Am 14.02.2015 um 16:27 schrieb 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
>  
>  
>  
>  
> 
> 
> 
> _______________________________________________
> 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: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150214/35c65b66/attachment.sig>