My conclusion of this discussion is that with 8fab871a2a6f the sublocale
command immediately visits its target after the qed, which it didn't before.
This now causes the command to loop. Is this correct?
Yes, definitely.
Florian
--
PGP available:
My conclusion of this discussion is that with 8fab871a2a6f the sublocale
command immediately visits its target after the qed, which it didn't before.
This now causes the command to loop. Is this correct?
Clemens
___
isabelle-dev mailing list
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
On 14 February, 2015 10:11 CET, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
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
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
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
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
It appears to be a reading issue.
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
Here the second mixin equation already parses as »loc1.e A ≡ loc1.e A«.
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
It looks like there are more of these kinds of problems lurking, but
unfortunately, I no longer fully understand the code, so I will have to rely
on your help.
In particular, I would like to know what went wrong here.
Can you point me to a source position where you get stuck? Doing a
short
The sublocale statements themselves are operative in Isabelle2013-1.
^
This should read Isabelle2013-2, sorry for the slip.
--
PGP available:
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
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 ==
13 matches
Mail list logo
