On Thu, 1 Dec 2011, Jasmin Blanchette wrote:
Am 01.12.2011 um 13:06 schrieb Stefan Berghofer:
I just got the very same warnings when updating my copy of the Isabelle
sources. I already got similar warning messages
warning: detected divergent renames of
src/HOL/Tools/Sledgehammer/sledgehammer.ML to:
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
a while ago (January 2011). When I asked Markus about this, he replied to
me that he had noticed them as well, but ignored it, and that he had not
discovered any negative effects so far. Maybe it is time to look at this
issue again rather than ignoring it?
According to Brian, who should be coming back from the coffee break in
15 minutes or so, these things happen when you effectively split a file
into two -- like I did in January with "sledgehammer.ML". There's
apparently some heuristic in Mercurial that tries to detects clones and
relabel them as renames, and that heuristic kind of goes crazy when you
split a file into two. Brian might be able to tell us more about this.
I have now fetched your version 7c8bed80301f and it looks fine to me, both
on Mac OS and Linux.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
