[isabelle-dev] push request (Sublist.thy)
makarius at sketis.net
Mon Dec 17 15:45:04 CET 2012
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
>> 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
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
$ hg verify
50503: unpacking changeset c4a27ab89c9b: integrity check failed on
manifest@?: rev 50501 points to unexpected changeset 50503
manifest@?: 666117bb338e not in changesets
crosschecking files in changesets and manifests
src/HOL/TPTP/mash_export.ML@?: rev 47 points to unexpected changeset
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
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.
More information about the isabelle-dev