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 <hu...@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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
