[isabelle-dev] Proposing extensions to the Isabelle library?

Christian Sternagel c.sternagel at gmail.com
Tue Jan 8 05:56:16 CET 2013 

Dear Alessandro,

sorry for the late answer. I can only tell you what I usually do (which 
does not mean that it is the best thing to do... maybe one of the 
developers could comment which way is the most convenient one for 
adopting external changes).

* I use 'hg qpop; hg pull; hg update; hg qpush' (I guess that is 
equivalent to 'hg qpop; hg pull -u; hg qpush'; the reason for not using 
--rebase is that I want to avoid any modification of the repository 
history, even for my local clone)

* For the same reason I do not qfinish a patch before I "submit" it to 
the mailing list ... since it could "pollute" my local history (I 
think). Instead I wait until the change is adopted by somebody with push 
access, then pull again from the Isabelle repo and delete my local 
patch. What I send to the mailing list is just the patch file which is 
stored at .hg/patches/ (under the name that you chose for your patch).

cheers

chris

PS: I did not always proceed as described above (and already caused some 
unnecessary changes in the history)... this is just my latest try. I 
hope it's not a bad one ;)

On 01/07/2013 06:39 AM, Alessandro Coglio wrote:
> Hi Christian,
>
> Thank you very much for the helpful information. Using mq sounds like a
> good idea. I have some familiarity with hg, but none with mq. I looked
> at some documentation, but I was wondering if you could quickly point me
> in the right direction:
>
>   * Assuming I'll be working with just one patch, should I update from
>     upstream by doing 'hg pull --rebase' or 'hg qpop; hg pull -u; hg
>     qpush'? Or in some other way?
>   * Once I have a completed, qrefreshed patch that builds with the
>     latest changesets from upstream, should I qfinish it (which, if I
>     understand, generates a local commit) or not? How do I package this
>     patch to send it to the isabelle-dev mailing list -- via 'hg bundle'
>     or in some other way?
>
> Thanks!
>
>
>
> On 12/28/12 5:10 AM, Christian Sternagel wrote:
>> Dear Alessandro,
>>
>> the necessary steps are outlined in the community wiki, here
>>
>> https://isabelle.in.tum.de/community/Publish_contributions_as_an_external
>>
>> Since the status of the wiki is not clear at the moment. I summarize
>> the steps also in this e-mail for later reference.
>>
>> 0) confirm with any of the isabelle developers that your work would be
>> appreciated and pushed after you finished (you already did that)
>>
>> 1) consult
>>
>> http://isabelle.in.tum.de/repos/isabelle/file/tip/README_REPOSITORY
>>
>> for how to work with the development repo (as well as conventions,
>> e.g., for mercurial commit messages etc.)
>>
>> 2) testing changes:
>> Before publication, pull any changes from the official repository.
>> (This might effect a merge.) Now test your changes at least by
>>
>>    isabelle build -a -o browser_info -o document=pdf -o document_graph
>>
>> 3) The archive of formal proofs is a separate mercurial repository
>> (which also has a development version). Often, this is adapted by some
>> isabelle developer (you have to confirm this). Otherwise you would
>> have to checkout this repo and test it against your changes yourself.
>>
>> 4) Creating a bundle:
>> Packaging your changes into a single file can be done with
>>
>>   hg bundle somefilename.hgbundle
>>
>> 5) Publishing contributions:
>> Finally, the previously created bundle can be sent to someone with
>> push access to the Isabelle main repository, either directly (assuming
>> mutual agreement) or indirectly via the mailing list. An alternative
>> is exchange through an external repository service like github.
>>
>> hope this helps,
>>
>> cheers
>>
>> chris
>>
>> PS: personally I found the "mq" extension of mercurial (for patch
>> queues) very helpful. Using "mq" I can collect all my changes as
>> patches (that are not commited to the repo) as well as continuously
>> update the repo from upstream. At the end I just send a patch to the
>> mailing list (without ever changing the history besides the final
>> commit that is done by a developer).
>>
>> On 12/28/2012 07:59 AM, Alessandro Coglio wrote:
>>> Hi Florian, I followed the instructions and things seems to be working
>>> fine in my clone of the repo.
>>>
>>> Before I start trying out the change outlined in your email, I'd like to
>>> double-check a few things:
>>>
>>>   * In order to modify Orderings and other theories that are part of
>>>     Main, I should start Isabelle with the '-l Pure' option and
>>>     load/change the files manually, correct?
>>>   * Once Main runs fine, I should check/change any files under the
>>>     src/HOL tree that may depend on Orderings. Does any file under the
>>>     other src/... trees depend on anything under the src/HOL tree?
>>>   * Is the successful completion of 'isabelle build -a' the final
>>>     criterion for determining that everything has been modified
>>>     correctly? I didn't see any separate test suites in the repo.
>>>   * Should the AFP (which I didn't see in the repo) be checked/changed
>>>     as well? Or is it updated only when there is a release?
>>>
>>> Thanks!
>>>
>>>
>>>
>>> On 12/22/12 4:01 AM, Alessandro Coglio wrote:
>>>> Hi Florian, I'd be happy to contribute, so I'll look into that. I
>>>> don't have a lot of spare time, so it may take me a while. The Jan or
>>>> Feb release is "safe" :)
>>>>
>>>>
>>>>
>>>> On 12/18/12 12:18 PM, Florian Haftmann wrote:
>>>>> Hi Alessandro,
>>>>>
>>>>>> Is there any plan to make things in the library more uniform (one
>>>>>> way or
>>>>>> the other)? Is there a preference for new type classes should be
>>>>>> developed (purely syntactic or with assumptions)?
>>>>> well, there is no big masterplan.  Usually things evolve: somebody
>>>>> thinks about an extended or more fine-grained hierarchy and thinks how
>>>>> to accomplish things without breaking more than necessary.
>>>>>
>>>>>> Personally, I like syntactic classes because they are more
>>>>>> modular. For
>>>>>> example, in the library extensions that I sent the other day, the
>>>>>> definition of type class finite_lattice_complete would be perhaps
>>>>>> slightly cleaner if bot and top were syntactic classes like Inf and
>>>>>> Sup.
>>>>>> Just my 2 cents.
>>>>> I.e. something like
>>>>>
>>>>>     class bot ~> class order_bot
>>>>>     class top ~> class order_top
>>>>>     class bot = fixes bot :: "'a"
>>>>>     class top = fixes top :: "'a"
>>>>>
>>>>> Could make sense.  The question is whether somebody is willing to
>>>>> undertake this change.  If you would consider this, you find the first
>>>>> clues at
>>>>> http://isabelle.in.tum.de/repos/isabelle/file/c5e0073558f3/README_REPOSITORY.
>>>>>
>>>>>
>>>>>   Get back here if questions remain.
>>>>>
>>>>> Note that currently we are heading towards a next release in
>>>>> January or
>>>>> February, and time might be too terse to polish and incorporate a
>>>>> change
>>>>> like the one sketched above.
>>>>>
>>>>> Hope this helps,
>>>>>     Florian
>>>>>
>>>>
>>>>
>>>
>>>
>>>
>>> _______________________________________________
>>> 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
>>
>

More information about the isabelle-dev mailing list