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

[Christian Sternagel]

Dear Dmitriy,

thanks for pushing! (I hope the repository trouble is not connected to 
my changesets ;))

cheers

chris

On 12/13/2012 09:58 PM, 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