diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2017-02-25 19:35:35 -0500 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2017-03-08 15:06:17 -0500 |
| commit | 98f2e463287e3562dc7b7126e062919a8604ca4a (patch) | |
| tree | e2fc6e477e8c82f4cc1db25cb81931ca9e680a84 /etc | |
| parent | 673082b2bee3ca327db56bdc559f7f925259d1c8 (diff) | |
Remove compile-time calls to proof-ready-for-assistant
Compilation used to run in a separate Emacs process for each file, but that's not
what happens when installing PG with package.el.
Diffstat (limited to 'etc')
| -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 |