Contributing to ProofPower
[ProofPower Logo]

Contributing to ProofPower

Contributing Documentation Download Examples Getting Home Mailing List Papers Patches Specifications

Anyone is welcome to contribute to the ProofPower development and patches are a convenient way of distributing contributions. The ProofPowerq mailing list is a forum you can use to distribute contributions supplied as patches (see patch(1) in the UN*X manual pages). There is a list of available patches together with instructions for using them here. This page gives some advice on what is involved in supplying a contribution in this form.

In the following "you" means someone wanting to make a patch available, "YOU" is your initials, "YYMMDD" is the date and I'm assuming you're using GNU diff & patch not the Solaris ones). "A.B.C" is the version of OpenProofPower that you're working on (e.g., 2.7.1).

  1. You construct a directory containing the clean source which is your starting point. E.g., this could be the directory OpenProofPower-A.B.C which you get by unpacking the distribution tarball or it could be the result of applying some other patches.

  2. Alongside OpenProofPower-A.B.C you create a copy say, OpenProofPower-A.B.C.YOU.YYMMDD, in which you apply the changes you want to make. Be careful when working in this copy, since distclean (called from configure) will remove things it finds in the src directory that it doesn't like with extreme prejudice - so it's probably best to do your actual development in a safer place.

  3. Typically, a change to the ML code or to a specification or proof script will involve a change to an implementation document src/impNNN.doc. If it involves changes to an ML signature or changes to or additions to the error messages, then you will also need to change the associated detailed design document src/dtdNNN.doc. To test new functionality or changes to existing functionality, you will also want to change the associated module test document src/mdtNNN.doc. To build a version of the relevant package to test go into the src directory and do, e.g., for a change to PPZed:

    make -f install.mkf zed_build

    This will build your package and any others that it depends on (in this case that's PPZed, PPDev and PPHol). To run the tests do, e.g. to test PPZed,

    make -f zed.mkf test

    This will run the tests, resulting in a set of test result files mdtXXX.ttd and intXXX.ttd. It will then look for success or failure indicators in these files. If you see "mdtNNN.ttd:All module tests passed" then all is well. If you don't see anything about mdtNNN.ttd or a line suggesting that execution of mdtNNN.doc failed in some way, then the test has failed and you will probably want to execute the code in mdtNNN.doc interactively a line at a time to find out what has gone wrong.

    If you are changing PPXpp, then most of the above does not apply, its source files have names like xmisc.c and it doesn't have batch tests. For any of the packages, the best way to find out what the source files are is by looking at the package makefile: xpp.mkf, hol.mkf etc.

  4. Once you are happy with your changes, it is time to create a patch which can be used to apply your changes to the original release source. To help recipients of the patch know what they've done, you create a directory OpenProofPower-A.B.C.YOU.YYMMDD/patches (if it's not already there) and include in it a text file patch-A.B.C.YOU.YYMMDD.txt containing a description of your patch. E.g.,:

    Date: 14th May 2003
    Source: Rob Arthan rda@lemma-one.com
    Purpose: Support ProofPower build using SML/NJ 100.42
    Description: The "visible compiler" interface in SML/NJ 100.42 has
    changed relative to 100.0.7. This patch allows you to build
    ProofPower with SML/NJ 100.42.
    Notes: The changes in SML/NJ 100.42 are not backwards compatible.
    Do not apply this patch if you are using SML/NJ 100.0.7.

  5. To make the patch, run distclean in each of OpenProofPower-A.B.C and OpenProofPower-A.B.C.YOU.YYMMDD. Then, in the common parent of OpenProofPower-A.B.C and OpenProofPower-A.B.C.YOU.YYMMDD run:

    diff -urP OpenProofPower-A.B.C OpenProofPower-A.B.C.YOU.YYMMDD >patch-A.B.C.YOU.YYMMDD
    gzip patch-A.B.C.YOU.YYMMDD

  6. Now to publish your patch, post a message with patch-A.B.C.YOU.YYMMDD.gz as an attachment to the ProofPower mailing list.

      7. Copyright © Lemma 1 Ltd.
      Created by  Rob Arthan [rda at lemma-one dot com]
      Last updated: $Date: 2004/06/28 13:13:54 $
      [Lemma 1 Logo]