[isabelle-dev] mercurial accident
Dr A. Koutsoukou-Argyraki
ak2110 at cam.ac.uk
Fri Jan 18 15:23:28 CET 2019
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
Thanks everyone for your input,
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.
>> 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
>>> Isabelle repository, without anybody at Cambridge showing her how to
>>> use it.
>> Before we start blaming individual people, this is not a person
>> but a tooling problem. Industry has figured out this problem years
>> 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
More information about the isabelle-dev