[isabelle-dev] mercurial accident

Fabian Immler immler at in.tum.de
Thu Jan 17 22:54:51 CET 2019


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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190117/f5226ca5/attachment.bin>


More information about the isabelle-dev mailing list