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

[Christian Sternagel]

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
>