diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2008-01-25 14:10:36 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2008-01-25 14:10:36 +0000 |
| commit | e8afda5769020ebf6393f46068c7cd5f9f9ead24 (patch) | |
| tree | 28bb674d67d64454da06dcf239b02694ec1eb84c /etc/development-tips.txt | |
| parent | 7fab2fcb320d72fd528b365c4f52dac0fbd4594b (diff) | |
Updated.
Diffstat (limited to 'etc/development-tips.txt')
| -rw-r--r-- | etc/development-tips.txt | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/etc/development-tips.txt b/etc/development-tips.txt index 60b70e0f..066b98a0 100644 --- a/etc/development-tips.txt +++ b/etc/development-tips.txt @@ -14,7 +14,23 @@ and that the bytecode runs correctly. Compilation not only speeds up the running code, but conducts some useful static analysis. To ensure correctness of running code, care is needed with macros (see -the Lisp reference manual) and load order. +the Lisp reference manual) and load order. For example, to expand macros +from proof-utils.el during compilation, use + + (eval-when-compile + (require 'proof-utils)). + +Without using this, compilation can be incorrect (macro calls compiled +as function calls: e.g., symptom unbound 'foobar' assistant variable +with "(proof-ass foobar)" call). + +Top-level forms, or forms that appear at top-level after compilation +(these get evaluated when compiling later files) need extra care. If +these forms depend on runtime information, e.g., the value of +proof-assistant symbol (proof-ass), they will produce the wrong result +(symptom: unbound nil-foobar). Running `proof-ready-for-assistant' can +be used to avoid this and optimise compilation. Byte compiler also +optimises some conditionals that appear constant, be wary. Some Emacs Resources |