[isabelle-dev] "Divergent renames"

[Makarius]

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