Re: [isabelle-dev] mercurial accident

2019-01-18 Thread Makarius
On 18/01/2019 21:55, Tobias Nipkow wrote: > Hey, I wanted to join the party! But all bugs have been fixed now and > Makarius will notify you of the correct changeset. Yes, see Isabelle/b18353d3fe1a. Despite the carnival season, I am presently working with David Matthews to make the canononical

Re: [isabelle-dev] mercurial accident

2019-01-18 Thread Tobias Nipkow
Hey, I wanted to join the party! But all bugs have been fixed now and Makarius will notify you of the correct changeset. Tobias On 18/01/2019 21:42, Makarius wrote: On 17/01/2019 22:54, Fabian Immler wrote: Luckily, a diff with a8faf6f15 revealed quite obviously what went wrong during the

Re: [isabelle-dev] mercurial accident

2019-01-18 Thread Makarius
On 17/01/2019 22:54, Fabian Immler wrote: > > Luckily, a diff with a8faf6f15 revealed quite obviously what went wrong > during the merges, so I could easily redo Angeliki's tagging (689997a8). > > We should be back to normal (regarding isabelle build -a). That was Isabelle/94284d4dab98, but

Re: [isabelle-dev] mercurial accident

2019-01-18 Thread 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

Re: [isabelle-dev] mercurial accident

2019-01-18 Thread Makarius
On 18/01/2019 11:42, Lars Hupel 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.

Re: [isabelle-dev] mercurial accident

2019-01-18 Thread Lawrence Paulson
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

Re: [isabelle-dev] mercurial accident

2019-01-18 Thread Lars Hupel
> 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.

Re: [isabelle-dev] mercurial accident

2019-01-17 Thread Fabian Immler
Thanks for your feedback! I did what Lars suggested (96a43caa). Luckily, a diff with a8faf6f15 revealed quite obviously what went wrong during the merges, so I could easily redo Angeliki's tagging (689997a8). We should be back to normal (regarding isabelle build -a). Fabian On 1/17/2019

Re: [isabelle-dev] mercurial accident

2019-01-17 Thread Makarius
On 17/01/2019 21:54, Makarius wrote: > > The problem behind this: Angeliki got administrative push-access to the > Isabelle repository, without anybody at Cambridge showing her how to use it. > > There is of course README_REPOSITORY, but the text is long. Here is the > ultra-short version: > >

Re: [isabelle-dev] mercurial accident

2019-01-17 Thread Makarius
On 17/01/2019 21:42, Lars Hupel wrote: >> Strip the accidental changes from the repository? > > Never strip public changesets. Indeed. "Fixing" a desaster by non-monotonic operations is a desaster squared. > >> Back out the changes? > > You can't really back out merges, as far as I know. >

Re: [isabelle-dev] mercurial accident

2019-01-17 Thread Lars Hupel
> Strip the accidental changes from the repository? Never strip public changesets. > Back out the changes? You can't really back out merges, as far as I know. > Or do a no-op merge from a successor of the last working version? This is also not possible, I think. Do this instead: $ hg revert