From 70dfbc54d9a6b559dbfcfd6105a7e8c80d78d888 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Sun, 26 Feb 2017 00:28:18 -0500
Subject: Fix incorrect assumption that noninteractive == byte-compiling

The PG Makefile does ensure (using --batch) that noninteractive is non-nil while
compiling, but package.el doesn't.
---
 generic/pg-user.el        | 4 ++--
 generic/proof-splash.el   | 2 +-
 generic/proof-useropts.el | 1 +
 generic/proof.el          | 2 +-
 4 files changed, 5 insertions(+), 4 deletions(-)

(limited to 'generic')

diff --git a/generic/pg-user.el b/generic/pg-user.el
index 513b477b..effe1eb5 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -563,9 +563,9 @@ last use time, to discourage saving these into the users database."
 ;; NB: completion table is expected to be set when proof-script
 ;; is loaded!  Call `proof-script-add-completions' to update.
 
-(unless noninteractive ; during compilation
+(unless (bound-and-true-p byte-compile-current-file)
   (eval-after-load "completion"
-  '(proof-add-completions)))
+    '(proof-add-completions)))
 
 (defun proof-script-complete (&optional arg)
   "Like `complete' but case-fold-search set to proof-case-fold-search."
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index 25db0946..7e7b8d54 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -264,7 +264,7 @@ binding to remove this buffer."
 (defun proof-splash-message ()
   "Make sure the user gets welcomed one way or another."
   (interactive)
-  (unless (or proof-splash-seen noninteractive)
+  (unless (or proof-splash-seen noninteractive (bound-and-true-p byte-compile-current-file))
     (if proof-splash-enable
 	(progn
 	  ;; disable ordinary emacs splash
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index b2cbb97a..eb9942a7 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -43,6 +43,7 @@ approximation we test whether proof-config is fully-loaded yet."
   (set-default sym value)
   (when (and
 	 (not noninteractive)
+	 (not (bound-and-true-p byte-compile-current-file))
 	 (featurep 'pg-custom)
 	 (featurep 'proof-config))
       (if (fboundp sym)
diff --git a/generic/proof.el b/generic/proof.el
index 1acfae71..4e7ddbea 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -26,7 +26,7 @@
 
 (require 'proof-site)			; site/prover config, global vars, autoloads
 
-(unless noninteractive
+(unless (or noninteractive (bound-and-true-p byte-compile-current-file))
   (proof-splash-message))		; welcome the user now.
 
 (require 'proof-compat)			; Emacs and OS compatibility
-- 
cgit v1.2.3


From 33614d35a25b54c23171c360a61b913f0c1158ce Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
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-compile-common.el |  4 ++--
 coq/coq-indent.el         |  2 +-
 coq/coq-local-vars.el     |  4 ++--
 coq/coq-par-compile.el    |  8 ++++----
 coq/coq-seq-compile.el    |  8 ++++----
 coq/coq-syntax.el         |  9 ++-------
 coq/coq-system.el         |  4 ++--
 coq/coq.el                | 24 ++++++++++++------------
 generic/pg-pamacs.el      |  2 +-
 generic/proof-menu.el     | 16 +++-------------
 generic/proof-site.el     |  2 +-
 lib/holes.el              |  4 +---
 lib/proof-compat.el       |  4 +---
 phox/phox-tags.el         |  6 +++---
 phox/phox.el              |  2 +-
 15 files changed, 40 insertions(+), 59 deletions(-)

(limited to 'generic')

diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 72a16881..48772889 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -19,8 +19,8 @@
 (eval-when (compile)
   ;;(defvar coq-pre-v85 nil)
   (require 'compile)
-  (defvar coq-confirm-external-compilation nil); defpacustom
-  (defvar coq-compile-parallel-in-background nil) ; defpacustom
+  (defvar coq-confirm-external-compilation); defpacustom
+  (defvar coq-compile-parallel-in-background) ; defpacustom
   (proof-ready-for-assistant 'coq))     ; compile for coq
 
 
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index e5179390..878fb895 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -22,7 +22,7 @@
 ;     (message "%.06f" (float-time (time-since time)))))
 
 (eval-when-compile
-  (defvar coq-script-indent nil))
+  (defvar coq-script-indent))
 
 (defconst coq-any-command-regexp
   (proof-regexp-alt-list coq-keywords))
diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el
index 846371b4..cd29e218 100644
--- a/coq/coq-local-vars.el
+++ b/coq/coq-local-vars.el
@@ -15,8 +15,8 @@
   (require 'cl))
 
 (eval-when (compile)
-  (defvar coq-prog-name nil)
-  (defvar coq-load-path nil))
+  (defvar coq-prog-name)
+  (defvar coq-load-path))
 
 
 ;;; Code:
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index f9b317c2..fbe38a1e 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -28,10 +28,10 @@
   (require 'proof-compat))
 
 (eval-when (compile)
-  (defvar queueitems nil)       ; dynamic scope in p-s-extend-queue-hook
-  (defvar coq-compile-before-require nil)       ; defpacustom
-  (defvar coq-compile-parallel-in-background nil) ; defpacustom
-  (defvar coq-confirm-external-compilation nil)); defpacustom
+  (defvar queueitems)       ; dynamic scope in p-s-extend-queue-hook
+  (defvar coq-compile-before-require)       ; defpacustom
+  (defvar coq-compile-parallel-in-background) ; defpacustom
+  (defvar coq-confirm-external-compilation)); defpacustom
 
 (require 'coq-compile-common)
 
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index a1b2d30a..5ecfbf4b 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -19,10 +19,10 @@
   (require 'proof-compat))
 
 (eval-when (compile)
-  (defvar queueitems nil)       ; dynamic scope in p-s-extend-queue-hook
-  (defvar coq-compile-before-require nil)       ; defpacustom
-  (defvar coq-compile-parallel-in-background nil)       ; defpacustom
-  (defvar coq-confirm-external-compilation nil)); defpacustom
+  (defvar queueitems)       ; dynamic scope in p-s-extend-queue-hook
+  (defvar coq-compile-before-require)       ; defpacustom
+  (defvar coq-compile-parallel-in-background)       ; defpacustom
+  (defvar coq-confirm-external-compilation)); defpacustom
 
 (require 'coq-compile-common)
 
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 5844be74..fc0e547a 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -9,14 +9,9 @@
 (require 'proof-syntax)
 (require 'proof-utils)                  ; proof-locate-executable
 (require 'coq-db)
+(require 'span)
 
-(eval-when-compile
-  (require 'span)
-  (defvar coq-goal-command-regexp nil)
-  (defvar coq-save-command-regexp-strict nil))
-
-
- ;;; keyword databases
+;;; keyword databases
 
 (defcustom coq-user-tactics-db nil
   "User defined tactic information.  See `coq-syntax-db' for
diff --git a/coq/coq-system.el b/coq/coq-system.el
index aad7d386..67081ea4 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -20,8 +20,8 @@
   (proof-ready-for-assistant 'coq))
 
 (eval-when (compile)
-  (defvar coq-prog-args nil)
-  (defvar coq-debug nil))
+  (defvar coq-prog-args)
+  (defvar coq-debug))
 
 (defcustom coq-prog-env nil
   "List of environment settings d to pass to Coq process.
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
diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el
index 4958b360..4bc61c15 100644
--- a/generic/pg-pamacs.el
+++ b/generic/pg-pamacs.el
@@ -260,7 +260,7 @@ 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) nil "Dummy for compilation."))))
+	(eval `(defvar ,(proof-ass-sym name)))))
   `(proof-defpacustom-fn (quote ,name) (quote ,val) (quote ,args)))
 
 
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index df617347..f029afcb 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -10,23 +10,13 @@
 (require 'cl)				; mapcan
 
 ;;; Code:
-(eval-when (compile)
-  (defvar proof-assistant-menu nil) ; defined by macro in proof-menu-define-specific
-  (defvar proof-mode-map nil))
-
-(require 'proof-utils)    ; proof-deftoggle, proof-eval-when-ready-for-assistant
-(require 'proof-useropts)
-(require 'proof-config)
-
-
-    
-
-
 (eval-when-compile
   (defvar proof-assistant-menu)	  ; defined by macro in proof-menu-define-specific
   (defvar proof-mode-map))
-    
 
+(require 'proof-utils)    ; proof-deftoggle, proof-eval-when-ready-for-assistant
+(require 'proof-useropts)
+(require 'proof-config)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 671c3c82..17ca325c 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -163,7 +163,7 @@ You can use customize to set this variable."
 (require 'proof-autoloads)
 
 (eval-when-compile
-  (defvar Info-dir-contents nil))
+  (defvar Info-dir-contents))
 
 ;; Add the info directory to the Info path
 (if (file-exists-p proof-info-directory) ; for safety
diff --git a/lib/holes.el b/lib/holes.el
index 09eb9dde..c0a864b0 100644
--- a/lib/holes.el
+++ b/lib/holes.el
@@ -30,9 +30,7 @@
 ;;
 ;; See documentation of `holes-mode'.
 
-
-(eval-when-compile 
-  (require 'span))
+(require 'span)
 (require 'cl)
 
 ;;; Code:
diff --git a/lib/proof-compat.el b/lib/proof-compat.el
index 1816ed0e..4eb942cb 100644
--- a/lib/proof-compat.el
+++ b/lib/proof-compat.el
@@ -17,9 +17,7 @@
 ;; Since Proof General 4.0, XEmacs is not supported at all.
 ;;
 
-(eval-when-compile
-  (require 'easymenu))
-
+(require 'easymenu)
 (require 'cl)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/phox/phox-tags.el b/phox/phox-tags.el
index 603622a6..73ed659b 100644
--- a/phox/phox-tags.el
+++ b/phox/phox-tags.el
@@ -18,9 +18,9 @@
 (require 'etags)
 
 (eval-when-compile
-  (defvar phox-doc-dir nil)
-  (defvar phox-lib-dir nil)
-  (defvar phox-etags nil))
+  (defvar phox-doc-dir)
+  (defvar phox-lib-dir)
+  (defvar phox-etags))
 
 
 (defun phox-tags-add-table(table)
diff --git a/phox/phox.el b/phox/phox.el
index 27b9cac0..79b8e747 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -7,7 +7,7 @@
 ;; loaded).
 
 (eval-when-compile
-  (defvar phox-toolbar-entries nil))
+  (defvar phox-toolbar-entries))
 
 (eval-after-load "pg-custom"
   '(setq phox-toolbar-entries
-- 
cgit v1.2.3


From 5b85cc7793fbedd656d118454682e43d71dd05dc Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Sat, 25 Feb 2017 19:09:32 -0500
Subject: Remove some Emacs <24.1 compatibility cruft

---
 generic/pg-response.el | 46 ++++++++++++++++------------------------------
 lib/unicode-tokens.el  |  6 +-----
 2 files changed, 17 insertions(+), 35 deletions(-)

(limited to 'generic')

diff --git a/generic/pg-response.el b/generic/pg-response.el
index 893d1f6f..8b6a413a 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -99,33 +99,21 @@ Internal variable, setting this will have no effect!")
   "List of GNU Emacs frame parameters for secondary frames.")
 
 (defun proof-multiple-frames-enable ()
-  ; special-display-regexps is obsolete, let us let it for a while and
-  ; remove it later
-  (unless (eval-when-compile (boundp 'display-buffer-alist))
-    (let ((spdres (cons
-		   pg-response-special-display-regexp
-		   proof-multiframe-parameters)))
-      (if proof-multiple-frames-enable
-	  (add-to-list 'special-display-regexps spdres)
-	(setq special-display-regexps
-	      (delete spdres special-display-regexps)))))
-  ; This is the current way to do it
-  (when (eval-when-compile (boundp 'display-buffer-alist))
-    (let
-	((display-buffer-entry
-	  (cons pg-response-special-display-regexp
-	    `((display-buffer-reuse-window display-buffer-pop-up-frame) .
-	      ((reusable-frames . t)
-	       (pop-up-frame-parameters
-		.
-		,proof-multiframe-parameters))))))
-      (if proof-multiple-frames-enable
-	  (add-to-list
-	   'display-buffer-alist
-	   display-buffer-entry)
-	;(add-to-list 'display-buffer-alist (proof-buffer-dislay))
-	(setq display-buffer-alist
-	      (delete display-buffer-entry display-buffer-alist)))))
+  (let
+      ((display-buffer-entry
+        (cons pg-response-special-display-regexp
+          `((display-buffer-reuse-window display-buffer-pop-up-frame) .
+            ((reusable-frames . t)
+             (pop-up-frame-parameters
+              .
+              ,proof-multiframe-parameters))))))
+    (if proof-multiple-frames-enable
+        (add-to-list
+         'display-buffer-alist
+         display-buffer-entry)
+      ;(add-to-list 'display-buffer-alist (proof-buffer-dislay))
+      (setq display-buffer-alist
+            (delete display-buffer-entry display-buffer-alist))))
   (proof-layout-windows))
 
 (defun proof-three-window-enable ()
@@ -521,9 +509,7 @@ and start at the first error."
 			  ;; Pop up a window.
 			  (display-buffer
                            proof-response-buffer
-                           (and (eval-when-compile
-                                  (boundp 'display-buffer-alist))
-                                proof-multiple-frames-enable
+                           (and proof-multiple-frames-enable
                                 (cons nil proof-multiframe-parameters))))))
 		  ;; Make sure the response buffer stays where it is,
 		  ;; and make sure source buffer is visible
diff --git a/lib/unicode-tokens.el b/lib/unicode-tokens.el
index ba3d036a..d05bfc1e 100644
--- a/lib/unicode-tokens.el
+++ b/lib/unicode-tokens.el
@@ -45,11 +45,7 @@
 (require 'quail)
 
 (eval-when-compile
-  (require 'maths-menu)		; nuke compile warnings
-  ;; Emacs <24 compatibility
-  (when (and (fboundp 'flet)
-	     (not (get 'flet 'byte-obsolete-info)))
-    (defalias 'cl-flet 'flet)))
+  (require 'maths-menu))		; nuke compile warnings
 
 ;;
 ;; Customizable user options
-- 
cgit v1.2.3


From 673082b2bee3ca327db56bdc559f7f925259d1c8 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
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 'generic')

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 <clement.pitclaudel@live.com>
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 'generic')

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 d3170a0cbe470cd620bc16e04eb148e554047d35 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Sat, 25 Feb 2017 20:15:09 -0500
Subject: Remove uses of defpgdefault in coq-abbrev

This file is `require'-d when compiling coq.el, and at that point the proof
assistant isn't set to coq yet, so it would define variables prefixed by `nil-'
instead of `coq'.
---
 coq/coq-abbrev.el    | 10 ++++------
 generic/pg-pamacs.el |  2 ++
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'generic')

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index a05c9853..30ec60c4 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -98,7 +98,7 @@ It was constructed with `proof-defstringset-fn'.")
 
 ;; The coq menu partly built from tables
 
-;; Common part (scrit, response and goals buffers)
+;; Common part (script, response and goals buffers)
 (defconst coq-menu-common-entries
   `(
     ["Toggle 3 Windows Mode" proof-three-window-toggle
@@ -300,7 +300,7 @@ It was constructed with `proof-defstringset-fn'.")
     ["ML4PG" (coq-activate-ml4pg) :help "Activates ML4PG: machine-learning methods for Proof General"]
     ))
 
-(defpgdefault menu-entries
+(setq-default coq-menu-entries
   (append coq-menu-common-entries
   `(
     ""
@@ -338,12 +338,10 @@ It was constructed with `proof-defstringset-fn'.")
      ["help" coq-local-vars-list-show-doc t]
      ["Compile" coq-Compile t]))))
 
-(defpgdefault help-menu-entries
+(setq-default coq-help-menu-entries
   '(["help on setting prog name persistently for a file" 
      coq-local-vars-list-show-doc t]))
 
-(defpgdefault other-buffers-menu-entries coq-menu-common-entries)
-
-
+(setq-default coq-other-buffers-menu-entries coq-menu-common-entries)
 
 (provide 'coq-abbrev)
diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el
index 8b9b83c7..d7bb1bf3 100644
--- a/generic/pg-pamacs.el
+++ b/generic/pg-pamacs.el
@@ -155,6 +155,8 @@ Usage: (defpgdefault SYM VALUE)"
 ;;;###autoload
 (defun proof-defpacustom-fn (name val args)
   "As for macro `defpacustom' but evaluating arguments."
+  (unless (and proof-assistant (not (string= proof-assistant "")))
+    (error "No proof assistant defined"))
   (let (newargs setting evalform type descr)
     (while args
       (cond
-- 
cgit v1.2.3