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

[Dmitriy Traytel]

On 17.12.2012 15:45, Makarius wrote:
> On Mon, 17 Dec 2012, Dmitriy Traytel wrote:
>
>> On 17.12.2012 15:23, Makarius wrote:
>>> On Thu, 13 Dec 2012, Dmitriy Traytel wrote:
>>>
>>>> I use Mercurial 2.2 and after pushing ed6b40d15d1c the attached 
>>>> error log was generated. hg verify on the server says that 
>>>> c4a27ab89c9b is the first damaged changeset. The corrupted 
>>>> repository is still on the server 
>>>> (/home/isabelle-repository/repos/isabelle.13.12.2012.backup).
>>>
>>> We need to find more physical side-conditions for this kind of 
>>> reactor meltdown.  What is your operating system platform? Are you 
>>> using bookmarks and/or patch queues locally?
>>
>> Ubuntu 12.10 (Linux kernel 3.5.0-20-generic, 64 bit). No bookmarks, 
>> but I do have a local patch queue.
>
> Just empirically, I see at the moment a correlation of "Debian/Ubuntu 
> + patch queue" with repository meltdown: Dmitriy, Alex, Johannes.
>
> Jasmin (Mac OS X user) is also using patch queus routinely, but never 
> had this effect so far.  Is this correct?
>
>
>> Also note that the changeset I was pushing (attached in previous mail 
>> on this thread), was imported via hg import (after adding the user 
>> name manually).
>
> So the patch queue was not used for that particular change?  I wonder 
> if it can somehow interact nonetheless.
Right, no patch queue for that specific import. Changeset 50503 
mentioned below was the tip at the moment, when I pushed.

Dmitriy
>
>
> Studying briefly the core-dump 
> /home/isabelle-repository/repos/isabelle.13.12.2012.backup leads to 
> the following:
>
> $ hg verify
> checking changesets
>  50503: unpacking changeset c4a27ab89c9b: integrity check failed on 
> 00changelog.i:50503
> checking manifests
>  manifest@?: rev 50501 points to unexpected changeset 50503
>  manifest@?: 666117bb338e not in changesets
> crosschecking files in changesets and manifests
> checking files
>  src/HOL/TPTP/mash_export.ML@?: rev 47 points to unexpected changeset 
> 50503
>  (expected )
> 9128 files, 50504 changesets, 130872 total revisions
> 1 warnings encountered!
> 4 integrity errors encountered!
> (first damaged changeset appears to be 50503)
>
>
> This fits to the description of 
> http://mercurial.selenic.com/wiki/RepositoryCorruption
>
>   4.4. Fixing changeset reference for index files from a patch queue
>
>   If the revision being repaired was part of an applied patch queue,
>   recovery is somewhat more complicated because the index file copied 
> from
>   the cloned repo will reference the wrong changeset.
>
> The advice is then like "what to do in case of nuclear attack on your 
> home town", as was common place in the 1950/60ies in the US.
>
>
>     Makarius