Re: [isabelle] Name clashes in theory names



Seconded. I also ran into this problem a few times.

Andreas

On 05/02/14 18:07, René Thiemann 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.