From 98f2e463287e3562dc7b7126e062919a8604ca4a Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sat, 25 Feb 2017 19:35:35 -0500 Subject: 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. --- etc/development-tips.txt | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'etc') 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 -- cgit v1.2.3