-*- outline -*-

* Developers Notes for Proof General
====================================

David Aspinall,  March 2000.

$Id$

Notes here about development conventions and compatibility
issues.  Please read if you contribute to Proof General!


** Project planning

We don't use any rigorous planning mechanisms, but please use and
maintain the simple "todo" lists.  They can include lists of things to
do as well as notes about outstanding bugs, etc.  Each item is
classified with a priority.  What usually happens is that either
something is fixed quickly, or its priority gradually decreases,
saving much time not implementing unimportant things!  

Items which are based on bug/problem reports by users are given a
higher priority by default (unless to fix them would be unreasonably
difficult).

In the top-level directory, todo holds the list of things to do in the
generic Elisp basis and for other generic parts of the project.  Each
proof assistant then has its own todo file.


** Coding Standards

When writing your modes, please follow the Emacs Lisp Conventions
See the Emacs Lisp reference manual, node Style Tips.




** Standards for each instance of PG

We include a README file and low-level todo file for each prover.


** Using custom library

Please use the custom library for all variable declarations, apart
from very low-level variables.  Follow the customize group conventions
laid out in generic/proof-config.el


** Compatibility with different Emacsen

One of the greatest problems in developing Proof General is
maintaining compatibility across different versions of Emacs.

XEmacs is the primary development (and use) platform, but we'd like to
maintain compatibility with FSF Emacs, and the Japanicised versions of
that.  The development policy is for the main codebase to be written
for the latest stable version of XEmacs.  We follow XEmacs advice on
removing obsolete function calls.

Hopefully one day we may have a proper test suite and mechanism to
test across different versions of Emacs.  For the time being, be
careful of the following tips (gathered from experience).

*** Compatibility hacks collected in proof-compat.el

 - This file contains implementations/emulations of functions to
 provide uniformity between different Emacs versions.  If you
 use a function specific to XEmacs or newer versions, consider adding
 a conditional definition of it here to support other versions
 for a while.

*** Common Lisp macros  -- Japan Emacsen have older versions

 - Use (dolist (var list) body), not (dolist (var list result) body).



** CVS tips

   See etc/cvs-tips.txt