Re: [isabelle] Name clashes in theory names



The theory loader indeed doesn’t cope with this situation very well. The namespace for theory names is completely global. The only sure remedy for the moment is to avoid generic theory names, and Auxiliary is a perfect example.

Larry Paulson


On 5 Feb 2014, at 17:07, René Thiemann <rene.thiemann at uibk.ac.at> wrote:

> Dear all,
> 
> we just spent one hour to detect why a singleton entry in the AFP compiled successfully, 
> whereas just adding this entry within a larger development resulted in an error.
> 
> The problem would have been easy to detect, provided there would have been any warning message
> that there are two theories called "Auxiliary" where silently only the one theory is kept. 
> However, starting isabelle build -v ... just complained about some unknown facts, which at least 
> to us did not at all point to real error of the name clash.
> (We imported none of the "Auxiliary"-theories directly)
> 
> In order to ease such debugging in the future, we would appreciate any integration of warning messages
> in the case of name clashes of theories.
> 
> Kind regards,
> Chris and René
> 
> 





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