aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/development-tips.txt
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-10 23:04:40 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-10 23:04:40 +0000
commitee91c3f2f1dd5f2f731db385134f38726b37b7ca (patch)
treed9cb381181a462fdbfab57f7e1f0d4e67ce567b2 /etc/development-tips.txt
parenta060c0dc046e526f8bf88b512e3c7c27e93421f8 (diff)
Experimental changes to queue several commands at once and to allow pre-processing of commands when they're queued from script
Diffstat (limited to 'etc/development-tips.txt')
-rw-r--r--etc/development-tips.txt12
1 files changed, 12 insertions, 0 deletions
diff --git a/etc/development-tips.txt b/etc/development-tips.txt
index 066b98a0..d8b766cd 100644
--- a/etc/development-tips.txt
+++ b/etc/development-tips.txt
@@ -32,6 +32,18 @@ proof-assistant symbol (proof-ass), they will produce the wrong result
be used to avoid this and optimise compilation. Byte compiler also
optimises some conditionals that appear constant, be wary.
+Finally, the compiler will warn over-eagerly (and ususally spuriously)
+about unknown functions. Adding extra requires can get these to go
+away, but watch out for introducing cycles in the require graphs.
+
+Rough dependency graph:
+
+
+proof-autoloads ->
+ pg-vars -> proof-site -> pg-vars
+
+
+
Some Emacs Resources
====================