[isabelle-dev] push request (Sublist.thy)

[Johannes Hölzl]

Am Freitag, den 14.12.2012, 13:47 +0100 schrieb Makarius:
> On Fri, 14 Dec 2012, Makarius wrote:
> 
> > When I did the re-cloning last time, I documented it explicitly in 
> > http://isabelle.in.tum.de/repos/isabelle/rev/71136069089d see also 
> > http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg02978.html
> 
> I have compared the wiki advice with the authentic version above.  Since 
> Mediawiki lacks good version control, I copy the content here for 
> reference:
> 
>   When this does not work another solution is:
> 
>   Clone the revisions up to the faulty one:
> 
>   hg clone --config=format.dotenode=0 --pull -U -r <rev number> isabelle isabelle-new
> 
>   cd isabelle-new
>   cp ../isabelle/Mercurial .
>   cd .hgrc
>   cp ../../isabelle/.hgrc/hgrc .
>   cp ../../isabelle/.hgrc/shamap .
>   chgrp -R isabelle .
>   chmod -R g+rwX .
>   find . -type d -exec chmod g+s "{}" \;
> 
> 
> Instead of "cd .hgrc" you probably meant "cd .hg".  What was also missing 
> is the "mkdir .hg/strip-backup", which is important for the next one doing 
> a strip, otherwise nobody else can strip with backup the afterwards -- I 
> have done that now.
> 
> I sincerely hope that the rest is equivalent with what I wrote in 
> 71136069089d 4 months ago, where I spent extra care in getting the order 
> of permission changes right, and fine-tune the sequence of shell commands.

I see two differences:

 * I used "find" to update the g+s flag in all sub-directories of .hg
   (there are some in .hg/store) I don't know how important this is.

 * I also copied shamap. It is related to the convert extension hence I
   assume it contains informations how the hg repository was generated
   from the CVS repo.

> And I am not asking to update the wiki, but to remove that page from it.

It now only mentions Admin/Mercurial/Central .

> Anythying that needs to be added to Admin/Mercurial/Central/README can be 
> discussed here (or privately).

I think we should add the trick by Alex to use strip. 


 * When the Isabelle repository is corrupted "hg verify" can be used to
   find the corrupt revision:

 * With "hg strip -r <rev number>" this revision can be removed. Then
   try to push your changes again

 * If this is not possibly try to clone the repository:
   ...


I know its a bad idea to perform a non-monotonic change like strip to
the repository. But I think it is less error prone than cloning the
repository with all these steps.

> The Admin/ area within the Isabelle 
> repository remains the one place for administrative information, not some 
> odd wiki where I am not participating. (Hopefully it will attract a 
> genuine Isabelle user community at some point, when hints on funny 
> technical incidents at TUM have disappeared.)