1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
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
|
