New files.

1 files changed, 100 insertions, 0 deletions

diff --git a/etc/README.devel b/etc/README.devel
new file mode 100644
index 00000000..b66e857c
--- /dev/null
+++ b/etc/README.devel
@@ -0,0 +1,100 @@
+-*- 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!
+
+Please also join the (very low volume) developers mailing
+list, see http://www.proofgeneral.org/mailinglist
+
+
+** 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.
+
+
+** Testing
+
+Ideally, we would have an automated test suite for Proof General.
+Emacs Lisp is certainly flexible to have such a thing, but it would
+take some effort to set it up.  Although automated tests could test
+functions and states for the right values, a user interface ultimately
+needs some human checks that visible appearances and user-input behave
+as expected.
+
+At the moment, we rely on the tiny example files included for each
+proof system as simple tests that basic scripting works.  Additional
+test scripts to test parsing complex scripts and tests against
+specific fixed bugs are included in etc/<PA>.  Multiple file scripting
+test cases should also be provided in etc/<PA>.
+
+
+** 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, follow
+the following tips.
+
+*** 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