Re: [isabelle-dev] mercurial accident
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 "isabelle build -a" invocations faster and less painful than ever -- the normal routine of many years. There are reasons why Isabelle + AFP has become so great in the past 10 years, and I am serious about continuing this. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] mercurial accident
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 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 Tobias has just pushed a bad merge again: Isabelle/aeceb14f387a. I can only quote README_REPOSITORY once more: Testing of changes (before push) The integrity of the standard pull/push area of Isabelle needs the be preserved at all time. This means that a complete test with default configuration needs to be finished successfully before push. If the preparation of the push involves a pull/merge phase, its result needs to covered by the test as well. Such testing of local changes plus the resulting merge is not optional, but mandatory. There is a natural routine of "hg commit" vs. "isabelle build -a" to make it all work well without any effort. 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 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 Tobias has just pushed a bad merge again: Isabelle/aeceb14f387a. I can only quote README_REPOSITORY once more: Testing of changes (before push) The integrity of the standard pull/push area of Isabelle needs the be preserved at all time. This means that a complete test with default configuration needs to be finished successfully before push. If the preparation of the push involves a pull/merge phase, its result needs to covered by the test as well. Such testing of local changes plus the resulting merge is not optional, but mandatory. There is a natural routine of "hg commit" vs. "isabelle build -a" to make it all work well without any effort. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] mercurial accident
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 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
Re: [isabelle-dev] mercurial accident
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. 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. I did not blame anybody, merely pointed out the actual problem. README_REPOSITORY gives a lot of explanations, including our important model of having just one branch, i.e. no branches at all. With further branches, the situation would become much worse, like the average project on github. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] mercurial accident
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 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
Re: [isabelle-dev] mercurial accident
> 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
