Re: [isabelle-dev] mercurial accident
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 3:54 PM, Makarius wrote: 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. 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 -a -r 56acd449da41 $ hg commit -m "revert to 56acd449da41" This looks fine and obvious. 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: After every local commit, use "hg view" (or equivalent) to ensure that the change is really what you want to make eternal when pushed to public. Makarius smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] mercurial accident
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: > > After every local commit, use "hg view" (or equivalent) to ensure that > the change is really what you want to make eternal when pushed to public. Here is another (minor) error by Angeliki: 6b8d78186947 is actually a merge (a clean one according to "hg view"), but the log message makes it appear like a regular change. (README_REPOSITORY explains proper treatment of merge nodes.) I've seen that incident already on Monday -- still with a high temperature, and not in proper shape to look more closely or write private mails etc. Instead, I was watching silly things like https://www.youtube.com/watch?v=FOJtmDYcFMg -- not totally unrelated to this thread. Maybe Larry can show Angeliki how to operate the "hg" chainsaw adequately. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] mercurial accident
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. > >> 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 -a -r 56acd449da41 > $ hg commit -m "revert to 56acd449da41" This looks fine and obvious. 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: After every local commit, use "hg view" (or equivalent) to ensure that the change is really what you want to make eternal when pushed to public. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] mercurial accident
> 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 -a -r 56acd449da41 $ hg commit -m "revert to 56acd449da41" Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] mercurial accident
The changesets a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7 seem to be the result of some mercurial/merge accident. They break HOL-Analysis, and it is not really clear from the history why and how to repair it. The last working version is 56acd449da41. Any opinions on what would be the best way to continue from here? Strip the accidental changes from the repository? Back out the changes? Or do a no-op merge from a successor of the last working version? Fabian smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
