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

[Makarius]

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.


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