Re: [isabelle] Interpretation inside locale raises DUP



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


> 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
 
 
 
 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.