diff options
| -rw-r--r-- | coq/coq-autotest.el | 7 | ||||
| -rw-r--r-- | coq/coq-compile-common.el | 6 | ||||
| -rw-r--r-- | coq/coq-system.el | 3 | ||||
| -rw-r--r-- | coq/coq.el | 3 | ||||
| -rw-r--r-- | etc/development-tips.txt | 7 | ||||
| -rw-r--r-- | generic/pg-pamacs.el | 4 | ||||
| -rw-r--r-- | hol-light/hol-light-autotest.el | 6 | ||||
| -rw-r--r-- | isar/isabelle-system.el | 7 | ||||
| -rw-r--r-- | isar/isar-autotest.el | 6 | ||||
| -rw-r--r-- | isar/isar-profiling.el | 5 | ||||
| -rw-r--r-- | isar/isar.el | 7 | ||||
| -rw-r--r-- | obsolete/demoisa/demoisa-easy.el | 5 |
12 files changed, 26 insertions, 40 deletions
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el index a8367b5c..e3c4b978 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -10,11 +10,8 @@ (require 'pg-autotest) -(eval-when (compile) - (require 'proof-site) - (proof-ready-for-assistant 'coq) - (defvar coq-compile-before-require nil)) - +(require 'proof-site) +(defvar coq-compile-before-require) (unless (bound-and-true-p byte-compile-current-file) diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 48772889..c557f474 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -15,14 +15,12 @@ (require 'proof-shell) (require 'coq-system) +(require 'compile) (eval-when (compile) ;;(defvar coq-pre-v85 nil) - (require 'compile) (defvar coq-confirm-external-compilation); defpacustom - (defvar coq-compile-parallel-in-background) ; defpacustom - (proof-ready-for-assistant 'coq)) ; compile for coq - + (defvar coq-compile-parallel-in-background)) ; defpacustom ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; diff --git a/coq/coq-system.el b/coq/coq-system.el index 67081ea4..ad85a960 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -16,8 +16,7 @@ (eval-when-compile (require 'cl) - (require 'proof-compat) - (proof-ready-for-assistant 'coq)) + (require 'proof-compat)) (eval-when (compile) (defvar coq-prog-args) @@ -30,8 +30,7 @@ (defvar coq-time-commands) ; defpacustom (defvar coq-use-project-file t) ; defpacustom (defvar coq-use-editing-holes) ; defpacustom - (defvar coq-hide-additional-subgoals) - (proof-ready-for-assistant 'coq)) ; compile for coq + (defvar coq-hide-additional-subgoals)) (require 'proof) (require 'coq-system) ; load path, option, project file 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 diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el index 4bc61c15..8b9b83c7 100644 --- a/generic/pg-pamacs.el +++ b/generic/pg-pamacs.el @@ -257,10 +257,6 @@ Additional properties in the ARGS prop list may include: askprefs message. This macro also extends the `proof-assistant-settings' list." - (eval-when-compile - (if (boundp 'proof-assistant-symbol) - ;; declare variable to compiler to prevent warnings - (eval `(defvar ,(proof-ass-sym name))))) `(proof-defpacustom-fn (quote ,name) (quote ,val) (quote ,args))) diff --git a/hol-light/hol-light-autotest.el b/hol-light/hol-light-autotest.el index b9924c41..5c1cb011 100644 --- a/hol-light/hol-light-autotest.el +++ b/hol-light/hol-light-autotest.el @@ -8,10 +8,8 @@ (eval-when-compile (require 'cl)) -(eval-when-compile - (require 'proof-site) - (proof-ready-for-assistant 'coq) - (defvar coq-compile-before-require nil)) +(require 'proof-site) +(proof-ready-for-assistant 'hol-light) (require 'pg-autotest) diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el index 64cd768f..d4ef3762 100644 --- a/isar/isabelle-system.el +++ b/isar/isabelle-system.el @@ -16,13 +16,12 @@ (require 'cl)) ; mapcan, eval-when (eval-when (compile) - (require 'span) - (require 'scomint) + (require 'span) + (require 'scomint) (require 'proof-site) (require 'proof-menu) (require 'proof-syntax) - (proof-ready-for-assistant 'isar) ; compile for isar - (defvar proof-assistant-menu nil)) + (defvar proof-assistant-menu)) (declare-function mapcan "cl-extra") ; spurious bytecomp warning diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el index 10ce61a1..091d2a0a 100644 --- a/isar/isar-autotest.el +++ b/isar/isar-autotest.el @@ -11,10 +11,10 @@ (require 'pg-autotest) (eval-when (compile) - (require 'cl) - (require 'proof-site) - (proof-ready-for-assistant 'isar)) + (require 'cl)) +(require 'proof-site) +(proof-ready-for-assistant 'isar) (declare-function isar-tracing:auto-quickcheck-toggle "isar.el") (declare-function isar-tracing:auto-solve-direct-toggle "isar.el") diff --git a/isar/isar-profiling.el b/isar/isar-profiling.el index 101d04ee..0cf19348 100644 --- a/isar/isar-profiling.el +++ b/isar/isar-profiling.el @@ -8,9 +8,8 @@ (eval-when-compile (require 'cl)) -(eval-when (compile) - (require 'proof-site) - (proof-ready-for-assistant 'isar)) +(require 'proof-site) +(proof-ready-for-assistant 'isar) (declare-function isar-tracing:auto-solve-toggle "isar.el") (declare-function isar-tracing:auto-quickcheck-toggle "isar.el") diff --git a/isar/isar.el b/isar/isar.el index 556a4973..b8119ee6 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -25,10 +25,9 @@ (require 'pg-goals) (require 'pg-vars) (require 'outline) - (defvar comment-quote-nested nil) - (defvar isar-use-find-theorems-form nil) - (defvar isar-use-linear-undo nil) - (proof-ready-for-assistant 'isar)) ; compile for isar + (defvar comment-quote-nested) + (defvar isar-use-find-theorems-form) + (defvar isar-use-linear-undo)) (require 'proof) (require 'isabelle-system) ; system code diff --git a/obsolete/demoisa/demoisa-easy.el b/obsolete/demoisa/demoisa-easy.el index f2e84837..b6e0e67d 100644 --- a/obsolete/demoisa/demoisa-easy.el +++ b/obsolete/demoisa/demoisa-easy.el @@ -25,9 +25,8 @@ ;; To test this file you must rename it demoisa.el. ;; -(eval-and-compile - (require 'proof-site) ; compilation for demoisa - (proof-ready-for-assistant 'demoisa)) +(require 'proof-site) +(proof-ready-for-assistant 'demoisa) (require 'proof) (require 'proof-easy-config) ; easy configure mechanism |