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 "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

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 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

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 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

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 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

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. 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

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 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

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.
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


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 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

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:
> 
>   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

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.
> 
>> 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

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 -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