[isabelle-dev] mercurial accident

[Dr A. Koutsoukou-Argyraki]

Just to clarify: the merging problem was the result of certain lemmas 
that had been moved around
among 3 theories (Determinants, Change_of_Vars and 
Finite_Cartesian_Product) by Fabian
simultaneously with me tagging the theories.( Even though I did pull 
several times daily.)
Simple merging did not work and two Isabelle experts from this list  to 
whom I mentioned the problem via email wrote back that merging
theories when content has been moved around can be problematic.
Indeed it required diffmerge as Larry wrote, so yes, it was a tooling 
problem.

Thanks everyone for your input,

Angeliki


On 2019-01-18 10:44, Lawrence Paulson wrote:
> Sorry, I’m to blame for this. When Angeliki mentioned she had merge
> conflicts, it turned out she didn’t have diffmerge (or anything
> similar) on her machine. By the time I got everything configured and
> managed to resolve the conflicts (largely by discarding her work
> unfortunately), I unthinkingly pushed the result without testing.
> 
> Larry
> 
> 
>> On 18 Jan 2019, at 10:42, Lars Hupel <hupel at in.tum.de> wrote:
>> 
>>> The problem behind this: Angeliki got administrative push-access to 
>>> the
>>> Isabelle repository, without anybody at Cambridge showing her how to 
>>> use it.
>> 
>> Before we start blaming individual people, this is not a person 
>> problem,
>> but a tooling problem. Industry has figured out this problem years 
>> ago.
>> One doesn't simply allow pushes to master (or "default" in Mercurial).
>> CakeML has adopted this too.
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev