Re: [isabelle] Name clashes in theory names
Seconded. I also ran into this problem a few times.
On 05/02/14 18:07, René Thiemann wrote:
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.
Chris and René
This archive was generated by a fusion of
Pipermail (Mailman edition) and