diff options
| author | David Aspinall | 2003-02-18 01:11:02 +0000 |
|---|---|---|
| committer | David Aspinall | 2003-02-18 01:11:02 +0000 |
| commit | 916171804ecf073d2da6ccb78e4f2a76fbbc9103 (patch) | |
| tree | 7cac2ee80fb508cfb9cf95bc195710348a2de5fd | |
| parent | 0bbc80a7644642118b2ac3cade070c8b028405dc (diff) | |
Delete
| -rw-r--r-- | README.devel | 100 |
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 |
