[isabelle-dev] "Divergent renames"

[Jasmin Blanchette]

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.

Jasmin