aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall2003-02-18 01:11:02 +0000
committerDavid Aspinall2003-02-18 01:11:02 +0000
commit916171804ecf073d2da6ccb78e4f2a76fbbc9103 (patch)
tree7cac2ee80fb508cfb9cf95bc195710348a2de5fd
parent0bbc80a7644642118b2ac3cade070c8b028405dc (diff)
Delete
-rw-r--r--README.devel100
1 files changed, 0 insertions, 100 deletions
diff --git a/README.devel b/README.devel
deleted file mode 100644
index b66e857c..00000000
--- a/README.devel
+++ /dev/null
@@ -1,100 +0,0 @@
--*- 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