Email Gateway (Aug 19 2022 at 12:40): Email Gateway (Aug 19 2022 at 12:40):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
I would like to report the exceptional behaviour of interpreting a locale inside another
locale in Isabelle2013-1. If there is already a global interpretation of the same locale
available, the interpretation inside the locale raises the exception DUP in table.ML. I
would have expected that the round-up algorithm just ignores duplicate interpretations, as
it does for all other combinations of multiple interpretations in locales that I tested.
Are my expectations wrong, is this a bug or simply unsupported?
Here's an example:
locale foo
interpretation foo .
locale bar begin
interpretation foo .
*** exception DUP ("Scratch.foo", []) raised (line 358 of "General/table.ML")
*** At command "."
Best,
Andreas
Email Gateway (Aug 19 2022 at 12:41):From: Clemens Ballarin <ballarin@in.tum.de>
Thanks for reporting this. The second interpretation should be ignored (as it will be at the global level), but apparently the code that should figure that out fails. I did not implement interpretation in locales myself, but perhaps Florian can comment. The stack trace is this:
Exception trace - exception DUP ("Scratch.foo", []) raised (line 358 of "General/table.ML")
Generic_Data().map(1)(1)
Locale.roundup(7)
Locale.add_registration(5)
Local_Theory.map_first_lthy(1)-E
Basics.#>(1)(1)
Expression.note_eqns_register(9)
o(2)(1)
Seq.maps_results(2)(1)
Seq.append(2)copy(1)(1)
Seq.first_result(2)result(2)
Seq.first_result(2)
Basics.#>(1)(1)
Toplevel.end_proof(1)(1)(1)
It looks like the data passed to roundup is inconsistent (or it's a plain bug in roundup, but that seem less likely since making the interpretation twice either in the global theory or the locale works).
Unfortunately, there is another locale bug, the diagnostic command 'print_interps <locale>' doesn't seem to work anymore either, but I haven't had time to look into that yet.
Clemens
Email Gateway (Aug 19 2022 at 12:41):From: Makarius <makarius@sketis.net>
Do you have an example for that? I did not find one looking 5min.
We need to figure it if and what to do here concerning the Isabelle2013-2
release, which is already the second attempt. The release process needs
to terminate eventually.
I will probably make Isabelle2013-2-RC2 in 48 hours.
Makarius
Email Gateway (Aug 19 2022 at 12:43):From: Clemens Ballarin <ballarin@in.tum.de>
On 25 November, 2013 21:57 CET, Makarius <makarius@sketis.net> wrote:
Unfortunately, there is another locale bug, the diagnostic command
'print_interps <locale>' doesn't seem to work anymore either, but I
haven't had time to look into that yet.Do you have an example for that? I did not find one looking 5min.
locale foo begin
print_interps foo
end
should yield 'foo' not 'no interpretations'. Likewise
locale foo begin
interpretation foo .
print_interps foo
end
which is equivalent. (In the language of locales, entering a context is making an interpretation via an identity morphism.)
We need to figure it if and what to do here concerning the Isabelle2013-2
release, which is already the second attempt. The release process needs
to terminate eventually.
I don't think this is a recent regression and suggest to ignore the problem for the upcoming release.
Clemens
Email Gateway (Aug 19 2022 at 12:43):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
We need to figure it if and what to do here concerning the
Isabelle2013-2
release, which is already the second attempt. The release process needs
to terminate eventually.I don't think this is a recent regression and suggest to ignore the problem for the upcoming release.
Dito. It is definitely not a regression.
I will take care for this issue, though this might take a little time.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 12:59):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Clemens,
I have done an analysis, and it seems to me that the critical spot is
fun init name thy =
activate_all name thy Element.init (Morphism.transfer_morphism o Context.theory_of)
(empty_idents, Context.Proof (Proof_Context.init_global thy))
|-> Idents.put |> Context.proof_of;
Using »empty_idents«, potentially pre-existing idents are chased away,
whereas registrations are taken over from the initial background theory.
This is no problem as long as
a) no further registrations are added (as in »interpret«)
b) the resulting target context is not used to setup further
interpretations (which would not occur prior to Isabelle2013-1)
I suggest to maintain the set of identifiers from the initial context, e.g.
fun init name thy =
let
val context = Context.Proof (Proof_Context.init_global thy);
val marked = Idents.get context;
val (marked', context') = activate_all name thy Element.init
(Morphism.transfer_morphism o Context.theory_of) (empty_idents, context)
in
context'
|> Idents.put (merge_idents (marked, marked'))
|> Context.proof_of
end;
I have glimpsed this pattern from roundup itself.
I did an experimental plausibility check which exhibited no problems.
The only point of manual intervention is in
the »interpret subpcpo ?S by (rule subpcpo_fjc)«, which explicitly
relied on re-interpretation of the fragment subpcpo_syn to obtain a
particular specialized syntax; but this fragment is already shadowed by
a global schematic interpretation »interpretation subpcpo_syn S for S.« in
(sorry for not giving direct links, but SF does not seem to support this).
Touching such a fundamental thing, I would kindly ask for your opinion
whether I should push this in that shape or you know about further
issues which have to be taken care of.
Thanks and all the best,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 13:03):From: Clemens Ballarin <ballarin@in.tum.de>
Hallo, Florian,
thank you for the analysis. I have looked at this more closely now and, yes, I believe this is the correct fix. Please go ahead and push.
Clemens
Last updated: Apr 19 2024 at 04:17 UTC