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

Thu Dec 13 15:14:15 CET 2012

Stripping did not work (even on lxbroy10 with some older Mercurial). 
However, Johannes managed to apparently fix everything by doing a fresh 
clone, copying some files (such as hgrc) and adjusting permissions (cf. 
https://isabelle.in.tum.de/community/Reconstructing_the_Isabelle_repository).

Some more data points: 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).

Dmitriy

On 13.12.2012 13:58, Dmitriy Traytel wrote:
> The test run was ok, but the repository is corrupted once again. 
> Trying to repair by stripping.
>
> Dmitriy
>
> On 13.12.2012 13:23, Dmitriy Traytel wrote:
>> It worked for me. I'm currently building (or more precisely running 
>> the build tool ;-) ) and will push if it succeeds.
>>
>> Dmitriy
>>
>> On 13.12.2012 12:53, Tobias Nipkow wrote:
>>> I tried to apply your patch but failed (see below). Since I had a 
>>> problem with
>>> somebody else's patch before, I wonder if something is wrong at my 
>>> end? Any
>>> suggestions?
>>>
>>> Tobias
>>>
>>> $ hg import emb
>>> applying emb
>>> patching file NEWS
>>> Hunk #1 FAILED at 172
>>> Hunk #2 FAILED at 181
>>> 2 out of 2 hunks FAILED -- saving rejects to file NEWS.rej
>>> patching file src/HOL/BNF/Examples/TreeFI.thy
>>> Hunk #1 FAILED at 11
>>> 1 out of 1 hunks FAILED -- saving rejects to file
>>> src/HOL/BNF/Examples/TreeFI.thy.rej
>>> patching file src/HOL/BNF/Examples/TreeFsetI.thy
>>> Hunk #1 FAILED at 11
>>> 1 out of 1 hunks FAILED -- saving rejects to file
>>> src/HOL/BNF/Examples/TreeFsetI.thy.rej
>>> patching file src/HOL/Library/Sublist.thy
>>> Hunk #1 FAILED at 2
>>> Hunk #2 FAILED at 10
>>> Hunk #3 FAILED at 22
>>> Hunk #4 FAILED at 30
>>> Hunk #5 FAILED at 42
>>> Hunk #6 FAILED at 87
>>> Hunk #7 FAILED at 105
>>> Hunk #8 FAILED at 190
>>> Hunk #9 FAILED at 206
>>> Hunk #10 FAILED at 267
>>> Hunk #11 FAILED at 419
>>> 11 out of 11 hunks FAILED -- saving rejects to file 
>>> src/HOL/Library/Sublist.thy.rej
>>> patching file src/HOL/Library/Sublist_Order.thy
>>> Hunk #1 FAILED at 20
>>> Hunk #2 FAILED at 39
>>> 2 out of 2 hunks FAILED -- saving rejects to file
>>> src/HOL/Library/Sublist_Order.thy.rej
>>> abort: patch failed to apply
>>>
>>>
>>> Am 09/12/2012 12:50, schrieb Christian Sternagel:
>>>> I fixed an error that only came up during document preparation 
>>>> (which I should
>>>> have tested previously, sorry).
>>>>
>>>> cheers
>>>>
>>>> chris
>>>>
>>>> On 12/09/2012 02:27 PM, Christian Sternagel wrote:
>>>>> Dear all,
>>>>>
>>>>> I have the following changes in my local patch queue:
>>>>>
>>>>> - In src/HOL/Library/Sublist.thy:
>>>>>     renamed "emb" ~> "list_hembeq" and "sub" ~> "sublisteq";
>>>>>     slightly changed definition of list_hembeq to make it reflexive
>>>>> independent of the base order;
>>>>>     dropped predicate "transp_on"
>>>>>
>>>>> Reasons: the name "emb" was very unspecific (hence the "list_" 
>>>>> prefix to
>>>>> make clear that it is on lists, and "h" for "homeomorphic" since 
>>>>> there
>>>>> is an important difference between "plain" embedding (which is 
>>>>> just the
>>>>> sublist relation) and homeomorphic embedding, where we are allowed to
>>>>> replace elements by smaller elements w.r.t. some base order) and in a
>>>>> later development I will need an irreflexive variant (hence "eq").
>>>>> Furthermore, since the basic use of embedding is as a 
>>>>> well-quasi-order
>>>>> and wqos are reflexive it seems natural to have a definition where
>>>>> embedding is reflexive independent of the base order.
>>>>>
>>>>> I will add "transp_on" to Restricted_Predicates from the AFP. At some
>>>>> point I would like to have the definitions of "reflp_on", 
>>>>> "transp_on",
>>>>> "irreflp_on", "antisymp_on", ... in the main distribution (but 
>>>>> that is
>>>>> an orthogonal issue).
>>>>>
>>>>> Any comments? Any takers (for pushing my changes to the main repo)? I
>>>>> checked the changes against f2241b8d0db5 with 'isabelle build -a' and
>>>>> prepared a changeset for the AFP (which I can push myself).
>>>>>
>>>>> cheers
>>>>>
>>>>> chris
>>>>>
>>>>> PS: As stated above, currently my changes are in my local patch queue
>>>>> and I attached the corresponding patch file from .hg/patches (which
>>>>> contains a commit message at the top). Should I transform this 
>>>>> into an
>>>>> hgbundle?
>>>>>
>>>>>
>>>>> _______________________________________________
>>>>> isabelle-dev mailing list
>>>>> isabelle-dev at in.tum.de
>>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>>>>>
>>>>>
>>>>
>>>> This body part will be downloaded on demand.
>>>>
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>

-------------- next part --------------
Übertrage nach ssh://macbroy21.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
Suche nach Änderungen
Entfernt: not trusting file /home/isabelle-repository/repos/isabelle/.hg/hgrc from untrusted user wenzelm, group isabelle
Entfernt: not trusting file /mnt/home/isabelle-repository/repos/isabelle/.hg/hgrc from untrusted user wenzelm, group isabelle
Entfernt: Füge Änderungssätze hinzu
Entfernt: Transaktion abgebrochen!
Entfernt: Zurückrollen abgeschlossen
Entfernt: ** Unbekannter Fehler - bitte melden auf:
Entfernt: ** http://mercurial.selenic.com/wiki/BugTracker
Entfernt: ** Python 2.7.3 (default, Apr 14 2012, 08:58:41) [GCC]
Entfernt: ** Mercurial Distributed SCM (Version 2.4)
Entfernt: ** Erweiterungen geladen:
Entfernt: Traceback (most recent call last):
Entfernt:   File "/usr/bin/hg", line 38, in <module>
Entfernt:     mercurial.dispatch.run()
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/dispatch.py", line 28, in run
Entfernt:     sys.exit((dispatch(request(sys.argv[1:])) or 0) & 255)
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/dispatch.py", line 65, in dispatch
Entfernt:     return _runcatch(req)
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/dispatch.py", line 88, in _runcatch
Entfernt:     return _dispatch(req)
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/dispatch.py", line 741, in _dispatch
Entfernt:     cmdpats, cmdoptions)
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/dispatch.py", line 514, in runcommand
Entfernt:     ret = _runcommand(ui, options, cmd, d)
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/dispatch.py", line 831, in _runcommand
Entfernt:     return checkargs()
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/dispatch.py", line 802, in checkargs
Entfernt:     return cmdfunc()
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/dispatch.py", line 738, in <lambda>
Entfernt:     d = lambda: util.checksignature(func)(ui, *args, **cmdoptions)
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/util.py", line 472, in check
Entfernt:     return func(*args, **kwargs)
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/commands.py", line 5210, in serve
Entfernt:     s.serve_forever()
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/sshserver.py", line 94, in serve_forever
Entfernt:     while self.serve_one():
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/sshserver.py", line 112, in serve_one
Entfernt:     rsp = wireproto.dispatch(self.repo, self, cmd)
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/wireproto.py", line 351, in dispatch
Entfernt:     return func(repo, proto, *args)
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/wireproto.py", line 625, in unbundle
Entfernt:     r = repo.addchangegroup(gen, 'serve', proto._client())
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/localrepo.py", line 2332, in addchangegroup
Entfernt:     efiles.update(self[c].files())
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/context.py", line 187, in files
Entfernt:     return self._changeset[3]
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/util.py", line 246, in __get__
Entfernt:     result = self.func(obj)
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/context.py", line 138, in _changeset
Entfernt:     return self._repo.changelog.read(self.rev())
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/changelog.py", line 273, in read
Entfernt:     text = self.revision(node)
Entfernt:   File "/usr/lib64/python2.7/site-packages/mercurial/revlog.py", line 915, in revision
Entfernt:     text = mdiff.patches(text, bins)
Entfernt: mpatch.mpatchError: invalid patch
Abbruch: Unerwartete Antwort: leere Zeichenkette