[isabelle-dev] "Divergent renames"
makarius at sketis.net
Thu Dec 1 13:44:53 CET 2011
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:
>> 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.
More information about the isabelle-dev