diff options
37 files changed, 198 insertions, 202 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 062f7580..79231ad9 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -71,7 +71,7 @@ ;; DA: how about above, just temporarily disable saving? (message "Coq default abbrevs loaded"))) -(unless noninteractive +(unless (or noninteractive (bound-and-true-p byte-compile-current-file)) (coq-install-abbrevs)) ;;;;; @@ -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 @@ -304,7 +304,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 `( "" @@ -342,12 +342,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/coq/coq-autotest.el b/coq/coq-autotest.el index b6b361ed..e3c4b978 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -10,13 +10,10 @@ (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 noninteractive +(unless (bound-and-true-p byte-compile-current-file) (pg-autotest start 'debug) diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 72a16881..f6adc5cd 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 nil); defpacustom - (defvar coq-compile-parallel-in-background nil) ; defpacustom - (proof-ready-for-assistant 'coq)) ; compile for coq - + (defvar coq-confirm-external-compilation); defpacustom + (defvar coq-compile-parallel-in-background)) ; defpacustom ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -34,7 +32,7 @@ ;; coq-par-compile, respectively. However, the :initialization ;; function of a defcustom seems to be evaluated when reading the ;; defcustom form. Therefore, these functions must be defined already, -;; when the defpacustum coq-compile-parallel-in-background is read. +;; when the defcustom coq-compile-parallel-in-background is read. (defun coq-par-enable () "Enable parallel compilation. @@ -157,7 +155,7 @@ Ignore any quick setting for Coq versions before 8.5." :group 'coq :package-version '(ProofGeneral . "4.1")) -(defpacustom compile-before-require nil +(defcustom coq-compile-before-require nil "If non-nil, check dependencies of required modules and compile if necessary. If non-nil ProofGeneral intercepts \"Require\" commands and checks if the required library module and its dependencies are up-to-date. If not, they @@ -169,7 +167,9 @@ This option can be set/reset via menu :safe 'booleanp :group 'coq-auto-compile) -(defpacustom compile-parallel-in-background nil +(proof-deftoggle coq-compile-before-require) + +(defcustom coq-compile-parallel-in-background nil "Choose the internal compilation method. When Proof General compiles itself, you have the choice between two implementations. If this setting is nil, then Proof General @@ -184,8 +184,12 @@ This option can be set/reset via menu `Coq -> Auto Compilation -> Compile Parallel In Background'." :type 'boolean :safe 'booleanp - :group 'coq-auto-compile - :eval (coq-switch-compilation-method)) + :group 'coq-auto-compile) + +(proof-deftoggle coq-compile-parallel-in-background) + +(defun coq-compile-parallel-in-background () + (coq-switch-compilation-method)) ;; defpacustom fails to call :eval during inititialization, see trac #456 (coq-switch-compilation-method) @@ -407,7 +411,7 @@ This option can be set via menu ;; define coq-lock-ancestors-toggle (proof-deftoggle coq-lock-ancestors) -(defpacustom confirm-external-compilation t +(defcustom coq-confirm-external-compilation t "If set let user change and confirm the compilation command. Otherwise start the external compilation without confirmation. 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..05703e45 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -28,10 +28,7 @@ (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 (require 'coq-compile-common) diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el index a1b2d30a..ee4181ae 100644 --- a/coq/coq-seq-compile.el +++ b/coq/coq-seq-compile.el @@ -19,10 +19,7 @@ (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 (require 'coq-compile-common) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index e97d268c..156d39e1 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..ad85a960 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -16,12 +16,11 @@ (eval-when-compile (require 'cl) - (require 'proof-compat) - (proof-ready-for-assistant 'coq)) + (require 'proof-compat)) (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. @@ -19,19 +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 - (proof-ready-for-assistant 'coq)) ; compile for coq + (defvar coq-use-editing-holes) ; defpacustom + (defvar coq-hide-additional-subgoals)) (require 'proof) (require 'coq-system) ; load path, option, project file etc. @@ -306,27 +305,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. @@ -1199,7 +1194,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 @@ -1210,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) diff --git a/easycrypt/easycrypt.el b/easycrypt/easycrypt.el index 017b2563..f7f0059f 100644 --- a/easycrypt/easycrypt.el +++ b/easycrypt/easycrypt.el @@ -6,7 +6,6 @@ ;; -------------------------------------------------------------------- (require 'proof) -(require 'pg-custom) (require 'easycrypt-syntax) (require 'easycrypt-hooks) (require 'easycrypt-abbrev) 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-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/pg-pamacs.el b/generic/pg-pamacs.el index 4958b360..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 @@ -257,10 +259,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) nil "Dummy for compilation.")))) `(proof-defpacustom-fn (quote ,name) (quote ,val) (quote ,args))) 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/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-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-shell.el b/generic/proof-shell.el index 4547a835..f79b78c2 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1912,7 +1912,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/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/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 diff --git a/hol-light/hol-light-autotest.el b/hol-light/hol-light-autotest.el index 20c16727..5c1cb011 100644 --- a/hol-light/hol-light-autotest.el +++ b/hol-light/hol-light-autotest.el @@ -8,14 +8,12 @@ (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) -(unless noninteractive +(unless (bound-and-true-p byte-compile-current-file) (pg-autotest start 'debug) (pg-autotest log ".autotest.log") ; convention diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el index 5352043d..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 @@ -73,6 +72,7 @@ unverified. Otherwise, returns non-nil if isa-isabelle-command is surely an executable with full path." (interactive "p") (when (and (not noninteractive) + (not (bound-and-true-p byte-compile-current-file)) (not proof-rsh-command) (or force isabelle-not-found @@ -139,7 +139,7 @@ generated with the Lisp form `(isa-tool-list-logics)'." :type (list 'string) :group 'isabelle) -(unless noninteractive +(unless (or noninteractive (bound-and-true-p byte-compile-current-file)) (setq isabelle-logics-available (isa-tool-list-logics))) (defcustom isabelle-chosen-logic nil @@ -287,7 +287,7 @@ for you, you should disable this behaviour." :help (format "Switch to %s logic" l))) isabelle-logics-available))))) -(unless noninteractive +(unless (or noninteractive (bound-and-true-p byte-compile-current-file)) (isabelle-logics-menu-calculate)) (defvar isabelle-time-to-refresh-logics t diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el index 60fa2ebc..091d2a0a 100644 --- a/isar/isar-autotest.el +++ b/isar/isar-autotest.el @@ -11,16 +11,16 @@ (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") (declare-function isar-proof:parallel-proofs-toggle "isar.el") -(unless noninteractive +(unless (bound-and-true-p byte-compile-current-file) (pg-autotest start) ; can add 'debug flag for debug-on-error @@ -89,10 +89,10 @@ (pg-autotest script-randomjumps "isar/Example.thy" 8) (when isar-long-tests - (pg-autotest remark "Larger files...") - (pg-autotest script-wholefile "etc/isar/AHundredTheorems.thy") - (pg-autotest script-wholefile "isar/ex/Tarski.thy") - (pg-autotest script-randomjumps "isar/ex/Tarski.thy" 10)) ; better test? + (pg-autotest remark "Larger files...") + (pg-autotest script-wholefile "etc/isar/AHundredTheorems.thy") + (pg-autotest script-wholefile "isar/ex/Tarski.thy") + (pg-autotest script-randomjumps "isar/ex/Tarski.thy" 10)) ; better test? (pg-autotest remark "Testing restarting the prover") diff --git a/isar/isar-profiling.el b/isar/isar-profiling.el index 8984f1b0..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") @@ -19,7 +18,7 @@ (require 'pg-autotest) (require 'pg-dev) -(unless noninteractive +(unless (bound-and-true-p byte-compile-current-file) (pg-autotest log ".profile.log") ; convention diff --git a/isar/isar.el b/isar/isar.el index bc28d34d..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 @@ -303,28 +302,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/lego/lego.el b/lego/lego.el index 1ead4b9c..d1bd7532 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -149,15 +149,14 @@ Activates extended printing routines required for Proof General.") (lego-shell-mode-config)) (define-derived-mode lego-mode proof-mode - "lego" nil - (lego-mode-config)) - -(eval-and-compile - (define-derived-mode lego-response-mode proof-response-mode - "LEGOResp" nil - (setq proof-response-font-lock-keywords lego-font-lock-terms) - (lego-init-syntax-table) - (proof-response-config-done))) + "lego" nil + (lego-mode-config)) + +(define-derived-mode lego-response-mode proof-response-mode + "LEGOResp" nil + (setq proof-response-font-lock-keywords lego-font-lock-terms) + (lego-init-syntax-table) + (proof-response-config-done)) (define-derived-mode lego-goals-mode proof-goals-mode "LEGOGoals" "LEGO Proof State" 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/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." 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/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 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 diff --git a/pg-init.el b/pg-init.el new file mode 100644 index 00000000..8f2fab4c --- /dev/null +++ b/pg-init.el @@ -0,0 +1,56 @@ +;;; pg-init.el --- Init file used for compatibility with package.el and ELPA -*- lexical-binding: t; -*- + +;; Copyright (C) 2017 Clément Pit-Claudel + +;; Author: Clément Pit-Claudel <clement.pitclaudel@live.com> + +;; This program is free software; you can redistribute it and/or modify +;; it under the terms of the GNU General Public License as published by +;; the Free Software Foundation, either version 3 of the License, or +;; (at your option) any later version. + +;; This program is distributed in the hope that it will be useful, +;; but WITHOUT ANY WARRANTY; without even the implied warranty of +;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +;; GNU General Public License for more details. + +;; You should have received a copy of the GNU General Public License +;; along with this program. If not, see <http://www.gnu.org/licenses/>. + +;;; Commentary: + +;; Proof General's initialization code (in generic/proof-site) is relatively +;; complex, in part because it was written before package.el existed, and in +;; part because package.el still doesn't look for autoloads in subdirectories. +;; This file is a thin, package.el-friendly wrapper around generic/proof-site, +;; suitable for execution on Emacs start-up. It serves two purposes: +;; +;; * Setting up the load path when byte-compiling PG. +;; * Loading a minimal PG setup on startup (not all of Proof General, of course; +;; mostly mode hooks and autoloads). + +;;; Code: + +;;;###autoload +(eval-and-compile + (defvar pg-init--script-full-path + (or (and load-in-progress load-file-name) + (bound-and-true-p byte-compile-current-file) + (buffer-file-name))) + (defvar pg-init--pg-root + (file-name-directory pg-init--script-full-path))) + +;;;###autoload +(unless (bound-and-true-p byte-compile-current-file) + ;; This require breaks compilation, so it must only run when loading the package. + (require 'proof-site (expand-file-name "generic/proof-site" pg-init--pg-root))) + +(eval-when-compile + (let ((byte-compile-directories + '("contrib/mmm" "generic" "lib" + "coq" "easycrypt" "pghaskell" "pgocaml" "pgshell"))) + (dolist (dir byte-compile-directories) + (add-to-list 'load-path (expand-file-name dir pg-init--pg-root))))) + +(provide 'pg-init) +;;; pg-init.el ends here 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 diff --git a/proof-general-pkg.el b/proof-general-pkg.el new file mode 100644 index 00000000..489731e9 --- /dev/null +++ b/proof-general-pkg.el @@ -0,0 +1,2 @@ +(define-package "proof-general" "4.4.1~pre" "A generic front-end for proof assistants (interactive theorem provers)" + '((emacs "24.4"))) |