diff options
Diffstat (limited to 'etc/development-tips.txt')
-rw-r--r-- | etc/development-tips.txt | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/etc/development-tips.txt b/etc/development-tips.txt index 96701285..a6bd0709 100644 --- a/etc/development-tips.txt +++ b/etc/development-tips.txt @@ -29,8 +29,11 @@ Top-level forms, or forms that appear at top-level after compilation 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. +be used to avoid this and optimise compilation (CPC 2017-02-25: this +sounds fishy: this document seems to assume that compilation is done in +a separate instance of Emacs, but that's not what happens when with +package.el. Calling `proof-ready-for-assistant' at compile time will +tie the rest of that Emacs session to a specific proof assistant). Finally, the compiler will warn over-eagerly (and ususally spuriously) about unknown functions. Adding extra requires can get these to go |