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