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
Scratch.thy
Description: Binary data
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
