From 33614d35a25b54c23171c360a61b913f0c1158ce Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sat, 25 Feb 2017 19:06:26 -0500 Subject: Fix incorrect uses of defvar It didn't really matter that these variables were defined and set to nil during compilation, since we ran compilation in a clean Emacs in --batch mode; it does matter now, however, since package.el compiles PG in the user's currently running Emacs instance. --- coq/coq.el | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'coq/coq.el') diff --git a/coq/coq.el b/coq/coq.el index 0c366df5..16e69d00 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -19,18 +19,18 @@ (require 'newcomment) (require 'etags) (unless (proof-try-require 'smie) - (defvar smie-indent-basic nil) - (defvar smie-rules-function nil)) - (defvar proof-info nil) ; dynamic scope in proof-tree-urgent-action - (defvar action nil) ; dynamic scope in coq-insert-as stuff - (defvar string nil) ; dynamic scope in coq-insert-as stuff - (defvar old-proof-marker nil) - ; dynamic scoq in coq-proof-tree-enable-evar-callback - (defvar coq-auto-insert-as nil) ; defpacustom - (defvar coq-time-commands nil) ; defpacustom + (defvar smie-indent-basic) + (defvar smie-rules-function)) + (defvar proof-info) ; dynamic scope in proof-tree-urgent-action + (defvar action) ; dynamic scope in coq-insert-as stuff + (defvar string) ; dynamic scope in coq-insert-as stuff + (defvar old-proof-marker) + ; dynamic scoq in coq-proof-tree-enable-evar-callback + (defvar coq-auto-insert-as) ; defpacustom + (defvar coq-time-commands) ; defpacustom (defvar coq-use-project-file t) ; defpacustom - (defvar coq-use-editing-holes nil) ; defpacustom - (defvar coq-hide-additional-subgoals nil) ; defpacustom + (defvar coq-use-editing-holes) ; defpacustom + (defvar coq-hide-additional-subgoals) (proof-ready-for-assistant 'coq)) ; compile for coq (require 'proof) @@ -1199,7 +1199,7 @@ flag Printing All set." ;; Check (eval-when (compile) - (defvar coq-auto-adapt-printing-width nil)); defpacustom + (defvar coq-auto-adapt-printing-width)); defpacustom ;; Since Printing Width is a synchronized option in coq (?) it is retored ;; silently to a previous value when retracting. So we reset the stored width -- cgit v1.2.3 From 673082b2bee3ca327db56bdc559f7f925259d1c8 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sat, 25 Feb 2017 19:18:16 -0500 Subject: Remove unnecessary calls to 'eval-and-compile' --- coq/coq.el | 26 +++++++++++--------------- generic/pg-assoc.el | 13 ++++++------- generic/proof-shell.el | 1 - isar/isar.el | 12 ++++-------- lib/pg-fontsets.el | 3 +-- 5 files changed, 22 insertions(+), 33 deletions(-) (limited to 'coq/coq.el') diff --git a/coq/coq.el b/coq/coq.el index 16e69d00..b60606c3 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -306,27 +306,23 @@ See also `coq-hide-additional-subgoals'." ;; Derived modes ;; -(eval-and-compile ;; FIXME: Why? - (define-derived-mode coq-shell-mode proof-shell-mode - "Coq Shell" nil - (coq-shell-mode-config))) +(define-derived-mode coq-shell-mode proof-shell-mode + "Coq Shell" nil + (coq-shell-mode-config)) -(eval-and-compile ;; FIXME: Why? - (define-derived-mode coq-response-mode proof-response-mode +(define-derived-mode coq-response-mode proof-response-mode "Coq Response" nil - (coq-response-config))) + (coq-response-config)) -(eval-and-compile ;; FIXME: Why? - (define-derived-mode coq-mode proof-mode "Coq" - "Major mode for Coq scripts. +(define-derived-mode coq-mode proof-mode "Coq" + "Major mode for Coq scripts. \\{coq-mode-map}" - (coq-mode-config))) + (coq-mode-config)) -(eval-and-compile ;; FIXME: Why? - (define-derived-mode coq-goals-mode proof-goals-mode - "Coq Goals" nil - (coq-goals-mode-config))) +(define-derived-mode coq-goals-mode proof-goals-mode + "Coq Goals" nil + (coq-goals-mode-config)) ;; Indentation and navigation support via SMIE. diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el index 6a27cd29..a8a52099 100644 --- a/generic/pg-assoc.el +++ b/generic/pg-assoc.el @@ -16,13 +16,12 @@ (require 'proof-utils) -(eval-and-compile ; defines proof-universal-keys-only-mode-map at compile time - (define-derived-mode proof-universal-keys-only-mode fundamental-mode - proof-general-name "Universal keymaps only" - ;; Doesn't seem to supress TAB, RET - (suppress-keymap proof-universal-keys-only-mode-map 'all) - (proof-define-keys proof-universal-keys-only-mode-map - proof-universal-keys))) +(define-derived-mode proof-universal-keys-only-mode fundamental-mode + proof-general-name "Universal keymaps only" + ;; Doesn't seem to supress TAB, RET + (suppress-keymap proof-universal-keys-only-mode-map 'all) + (proof-define-keys proof-universal-keys-only-mode-map + proof-universal-keys)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 51305eef..93f1bbef 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1911,7 +1911,6 @@ Error messages are displayed as usual." ;; Proof General shell mode definition ;; -;(eval-and-compile ; to define vars ;;;###autoload (define-derived-mode proof-shell-mode scomint-mode "proof-shell" "Proof General shell mode class for proof assistant processes" diff --git a/isar/isar.el b/isar/isar.el index bc28d34d..556a4973 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -303,28 +303,24 @@ This is called when Proof General spots output matching ;; ;; use eval-and-compile to define vars for byte comp. -(eval-and-compile (define-derived-mode isar-shell-mode proof-shell-mode "Isabelle Shell" nil - (isar-shell-mode-config))) + (isar-shell-mode-config)) -(eval-and-compile (define-derived-mode isar-response-mode proof-response-mode "Isar Messages" nil - (isar-response-mode-config))) + (isar-response-mode-config)) -(eval-and-compile (define-derived-mode isar-goals-mode proof-goals-mode "Isar Proofstate" nil - (isar-goals-mode-config))) + (isar-goals-mode-config)) -(eval-and-compile (define-derived-mode isar-mode proof-mode "Isar" "Major mode for editing Isar proof scripts. \\{isar-mode-map}" - (isar-mode-config))) + (isar-mode-config)) diff --git a/lib/pg-fontsets.el b/lib/pg-fontsets.el index 2c0528cc..c4d76efc 100644 --- a/lib/pg-fontsets.el +++ b/lib/pg-fontsets.el @@ -21,8 +21,7 @@ ;;; Code: -(eval-and-compile - (require 'fontset)) ; needed for some emacsen without X +(require 'fontset) (defcustom pg-fontsets-default-fontset nil "*Name of default fontset to use with Proof General." -- cgit v1.2.3 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. --- coq/coq-autotest.el | 7 ++----- coq/coq-compile-common.el | 6 ++---- coq/coq-system.el | 3 +-- coq/coq.el | 3 +-- etc/development-tips.txt | 7 +++++-- generic/pg-pamacs.el | 4 ---- hol-light/hol-light-autotest.el | 6 ++---- isar/isabelle-system.el | 7 +++---- isar/isar-autotest.el | 6 +++--- isar/isar-profiling.el | 5 ++--- isar/isar.el | 7 +++---- obsolete/demoisa/demoisa-easy.el | 5 ++--- 12 files changed, 26 insertions(+), 40 deletions(-) (limited to 'coq/coq.el') 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) diff --git a/coq/coq.el b/coq/coq.el index b60606c3..2c8e4cfa 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -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 -- cgit v1.2.3 From cb3f86402688e2f920d0cdc326874505d5e3aa6f Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sat, 25 Feb 2017 20:16:28 -0500 Subject: Add a FIXME in coq.el --- coq/coq.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'coq/coq.el') diff --git a/coq/coq.el b/coq/coq.el index 2c8e4cfa..deb40ec4 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1205,7 +1205,7 @@ flag Printing All set." ;; we can remove this. (defun coq-set-auto-adapt-printing-width (&optional symb val); args are for :set compatibility "Function called when setting `auto-adapt-printing-width'" - (setq symb val) + (setq symb val) ;; FIXME this is wrong (it should be 'set', but it would set nil sometimes) (if coq-auto-adapt-printing-width (progn (add-hook 'proof-assert-command-hook 'coq-adapt-printing-width) -- cgit v1.2.3