From 9a25320acf24020fc0e2b97589f9d996f3d1d4fb Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Thu, 13 Dec 2018 22:57:15 -0500 Subject: Fix remaining uses of CL; Make files more declarative MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Emacs occasionally loads Elisp files just to get more info (e.g. for C-h f), so loading a file should "no effect". Fix the most obvious such effects: the splash screen and the autotests by moving those effects into a function. * coq/coq-autotest.el: Make it declarative. Use lexical-binding. (coq-autotest): New function holding the code that used to be at top-level. * generic/proof.el: Use lexical-binding. Don't call proof-splash-message just because we're being loaded. * generic/proof-script.el: Use lexical-scoping; fix all warnings. (pg-show-all-portions): Simplify the code with a closure. (proof-activate-scripting): Declare activated-interactively as dyn-scoped. (proof--splash-done): New var. (proof-mode): Call proof-splash-message upon first use. * generic/proof-splash.el (proof-splash-message): Don't check byte-compile-current-file now that we're only called when the mode is activated. * acl2/acl2.el (auto-mode-alist): Use `add-to-list` and \'. * coq/coq-db.el (coq-build-menu-from-db-internal): Avoid silly O(N²). * coq/coq-seq-compile.el: * coq/coq-par-test.el: * coq/coq-par-compile.el: Fix leftover uses of CL's `assert`. * generic/proof-utils.el: * generic/pg-movie.el: * etc/testsuite/pg-test.el: * coq/coq-syntax.el: Fix leftover uses of CL's `incf`. * generic/pg-autotest.el: Fix leftover uses of CL's `decf`. * obsolete/plastic/plastic.el (plastic-preprocessing): Fix leftover use of CL's `loop`. * generic/pg-user.el (proof-add-completions): Do nothing if no proof-assistant is set yet (i.e. during byte-compilation). (byte-compile-current-file): No need to test this any more. * generic/proof-syntax.el (proof-regexp-alt-list): Use mapconcat. Remove unnecessary "\\(?:...\\)". (proof-regexp-alt): Redefine in terms of proof-regexp-alt-list. --- coq/coq-autotest.el | 6 ++++-- coq/coq-db.el | 16 +++++++--------- coq/coq-par-compile.el | 34 +++++++++++++++++----------------- coq/coq-par-test.el | 35 ++++++++++++++++++----------------- coq/coq-seq-compile.el | 5 +++-- coq/coq-syntax.el | 17 +++++++++-------- 6 files changed, 58 insertions(+), 55 deletions(-) (limited to 'coq') diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el index 8be4bed9..5ca66706 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -1,4 +1,4 @@ -;;; coq-autotest.el --- tests of Coq Proof General (in progress). +;;; coq-autotest.el --- tests of Coq Proof General (in progress) -*- lexical-binding:t -*- ;; This file is part of Proof General. @@ -21,7 +21,9 @@ (require 'proof-site) (defvar coq-compile-before-require) -(unless (bound-and-true-p byte-compile-current-file) +;;;###autoload +(defun coq-autotest () + (interactive) (pg-autotest start 'debug) diff --git a/coq/coq-db.el b/coq/coq-db.el index 36812c4c..7e59bffb 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -25,7 +25,7 @@ (eval-when-compile (require 'cl-lib)) ;decf -(require 'proof-config) ; for proof-face-specs, a macro +(require 'proof-config) (require 'proof-syntax) ; for proof-ids-to-regexp (require 'holes) @@ -187,7 +187,7 @@ Used by `coq-build-menu-from-db', which you should probably use instead. See (let ((l db) (res ()) (size lgth) (keybind-abbrev (substitute-command-keys " \\[expand-abbrev]"))) (while (and l (> size 0)) - (let* ((hd (car l)) + (let* ((hd (pop l)) (menu (nth 0 hd)) ; e1 = menu entry (abbrev (nth 1 hd)) ; e2 = abbreviation (complt (nth 2 hd)) ; e3 = completion @@ -209,10 +209,9 @@ Used by `coq-build-menu-from-db', which you should probably use instead. See ;;insertion function if present otherwise insert completion (if insertfn insertfn `(holes-insert-and-expand ,complt)) t))) - (setq res (nconc res (list menu-entry)))));; append *in place* - (setq l (cdr l)) + (push menu-entry res))) (cl-decf size))) - res)) + (nreverse res))) (defun coq-build-title-menu (db size) @@ -289,10 +288,9 @@ See `coq-syntax-db' for DB structure." ;;A new face for tactics which fail when they don't kill the current goal (defface coq-solve-tactics-face - (proof-face-specs - (:foreground "red") ; pour les fonds clairs - (:foreground "red1") ; pour les fonds foncés - ()) ; pour le noir et blanc + `((((background light)) :foreground "red") + (((background dark)) :foreground "red1") + ()) ; pour le noir et blanc "Face for names of closing tactics in proof scripts." :group 'proof-faces) diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index c6822dc5..ac2e82bf 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -35,7 +35,7 @@ ;;; Code: (defvar queueitems) ; dynamic scope in p-s-extend-queue-hook - +(eval-when-compile (require 'cl-lib)) (require 'coq-compile-common) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -712,7 +712,7 @@ function returns () if MODULE-ID comes from the standard library." ;; error-message))) ;; (coq-seq-display-compile-response-buffer) (error error-message))) - (assert (<= (length result) 1) + (cl-assert (<= (length result) 1) nil "Internal error in coq-seq-map-module-id-to-obj-file") (car-safe result))) @@ -949,7 +949,7 @@ errors are reported with an error message." (defun coq-par-run-vio2vo-queue () "Start delayed vio2vo compilation." - (assert (not coq--last-compilation-job) + (cl-assert (not coq--last-compilation-job) nil "normal compilation and vio2vo in parallel 3") (setq coq--compile-vio2vo-in-progress t) (setq coq--compile-vio2vo-delay-timer nil) @@ -1011,7 +1011,7 @@ somewhere after the last require command." (defun coq-par-add-queue-dependency (dependee dependant) "Add queue dependency from child job DEPENDEE to parent job DEPENDANT." - (assert (and (not (get dependant 'queue-dependant-waiting)) + (cl-assert (and (not (get dependant 'queue-dependant-waiting)) (not (get dependee 'queue-dependant))) nil "queue dependency cannot be added") (put dependant 'queue-dependant-waiting t) @@ -1202,13 +1202,13 @@ when they transition from 'waiting-queue to 'ready: This function can safely be called for non-top-level jobs. This function must not be called for failed jobs." - (assert (not (get job 'failed)) + (cl-assert (not (get job 'failed)) nil "coq-par-retire-top-level-job precondition failed") (let ((span (get job 'require-span)) (items (get job 'queueitems))) (when (and span coq-lock-ancestors) (dolist (anc-job (get job 'ancestors)) - (assert (not (eq (get anc-job 'lock-state) 'unlocked)) + (cl-assert (not (eq (get anc-job 'lock-state) 'unlocked)) nil "bad ancestor lock state") (when (eq (get anc-job 'lock-state) 'locked) (put anc-job 'lock-state 'asserted) @@ -1290,7 +1290,7 @@ case, the following actions are taken: (let ((dependant (get job 'queue-dependant))) (if dependant (progn - (assert (not (eq coq--last-compilation-job job)) + (cl-assert (not (eq coq--last-compilation-job job)) nil "coq--last-compilation-job invariant error") (put dependant 'queue-dependant-waiting nil) (when coq--debug-auto-compilation @@ -1309,7 +1309,7 @@ case, the following actions are taken: (proof-script-clear-queue-spans-on-error nil)) (proof-release-lock) (when (eq coq-compile-quick 'quick-and-vio2vo) - (assert (not coq--compile-vio2vo-delay-timer) + (cl-assert (not coq--compile-vio2vo-delay-timer) nil "vio2vo timer set before last compilation job") (setq coq--compile-vio2vo-delay-timer (run-at-time coq-compile-vio2vo-delay nil @@ -1362,7 +1362,7 @@ if it reaches 0, the next transition is triggered for DEPENDANT. For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for 'clone jobs this 'waiting-dep -> 'waiting-queue." ;(message "%s: CPDCD with time %s" (get dependant 'name) dependee-time) - (assert (eq (get dependant 'state) 'waiting-dep) + (cl-assert (eq (get dependant 'state) 'waiting-dep) nil "wrong state of parent dependant job") (when (coq-par-time-less (get dependant 'youngest-coqc-dependency) dependee-time) @@ -1371,7 +1371,7 @@ For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for (append dependee-ancestors (get dependant 'ancestors))) (put dependant 'coqc-dependency-count (1- (get dependant 'coqc-dependency-count))) - (assert (<= 0 (get dependant 'coqc-dependency-count)) + (cl-assert (<= 0 (get dependant 'coqc-dependency-count)) nil "dependency count below zero") (when coq--debug-auto-compilation (message "%s: coqc dependency count down to %d" @@ -1439,7 +1439,7 @@ This function makes the following actions. "maybe kickoff queue") (get job 'name) (if dependant-alive "some" "no"))) - (assert (or (not (get job 'failed)) (not dependant-alive)) + (cl-assert (or (not (get job 'failed)) (not dependant-alive)) nil "failed job with non-failing dependant") (when (or (and (not dependant-alive) (not (get job 'require-span)) @@ -1512,7 +1512,7 @@ coqdep or coqc are started for it." (get job 'required-obj-file)))) ((eq job-state 'ready) (coq-par-start-vio2vo job)) - (t (assert nil nil "coq-par-start-task with invalid job"))))) + (t (cl-assert nil nil "coq-par-start-task with invalid job"))))) (defun coq-par-start-jobs-until-full () "Start background jobs until the limit is reached." @@ -1622,7 +1622,7 @@ Return t if job has a direct or indirect dependant that has not failed yet and that is in a state before 'waiting-queue. Also, return t if JOB has a dependant that is a top-level job which has not yet failed." - (assert (not (eq (get job 'lock-state) 'asserted)) + (cl-assert (not (eq (get job 'lock-state) 'asserted)) nil "coq-par-ongoing-compilation precondition failed") (cond ((get job 'failed) @@ -1653,7 +1653,7 @@ not yet failed." (setq res (coq-par-ongoing-compilation dep))) res)) (t - (assert nil nil + (cl-assert nil nil "impossible ancestor state %s on job %s" (get job 'state) (get job 'name))))) @@ -1680,7 +1680,7 @@ Mark JOB with 'queue-failed, and, if JOB is in state appropriate." (unless (or (get job 'failed) (get job 'queue-failed)) (put job 'queue-failed t) - (assert (not (eq (get job 'state) 'ready)) + (cl-assert (not (eq (get job 'state) 'ready)) nil "coq-par-mark-queue-failing impossible state") (when coq--debug-auto-compilation (message "%s: mark as queue-failed, %s" @@ -1893,7 +1893,7 @@ there is no last compilation job." ;; add the asserted items to the last compilation job (if coq--last-compilation-job (progn - (assert (not (coq-par-job-is-ready coq--last-compilation-job)) + (cl-assert (not (coq-par-job-is-ready coq--last-compilation-job)) nil "last compilation job from previous compilation ready") (put coq--last-compilation-job 'queueitems (nconc (get coq--last-compilation-job 'queueitems) @@ -1979,7 +1979,7 @@ the maximal number of background compilation jobs is started." (cancel-timer coq--compile-vio2vo-delay-timer) (setq coq--compile-vio2vo-delay-timer nil)) (when coq--compile-vio2vo-in-progress - (assert (not coq--last-compilation-job) + (cl-assert (not coq--last-compilation-job) nil "normal compilation and vio2vo in parallel 2") ;; there are only vio2vo background processes (coq-par-kill-all-processes) diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el index ebc5ecd7..f2e3f01d 100644 --- a/coq/coq-par-test.el +++ b/coq/coq-par-test.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -31,6 +31,7 @@ ;;; Code: (require 'coq-par-compile) +(eval-when-compile (require 'cl-lib)) (defconst coq--par-job-needs-compilation-tests ;; for documentation see the doc string following the init value @@ -753,7 +754,7 @@ relative ages.") (lambda (test) (let ((test-id (format "%s" (car test)))) ;; a test is a list of 4 elements and the first element is a list itself - (assert + (cl-assert (and (eq (length test) 4) (listp (car test))) @@ -761,22 +762,22 @@ relative ages.") (mapc (lambda (variant) ;; a variant is a list of 4 elements - (assert (eq (length variant) 4) nil (concat test-id " 2")) + (cl-assert (eq (length variant) 4) nil (concat test-id " 2")) (let ((files (coq-par-test-flatten-files (car test))) (quick-mode (car variant)) (compilation-result (nth 1 variant)) (delete-result (nth 2 variant)) (req-obj-result (nth 3 variant))) ;; the delete field, when set, must be a member of the files list - (assert (or (not delete-result) + (cl-assert (or (not delete-result) (member delete-result files)) nil (concat test-id " 3")) ;; 8.4 compatibility check (when (and (or (eq quick-mode 'no-quick) (eq quick-mode 'ensure-vo)) (not (member 'vio files))) - (assert (not delete-result) + (cl-assert (not delete-result) nil (concat test-id " 4")) - (assert (eq compilation-result + (cl-assert (eq compilation-result (not (eq (car (last (car test))) 'vo))) nil (concat test-id " 5"))))) (cdr test)))) @@ -789,7 +790,7 @@ relative ages.") ((eq sym 'dep) "dep.vo") ((eq sym 'vo) "a.vo") ((eq sym 'vio) "a.vio") - (t (assert nil))))) + (t (cl-assert nil))))) (concat dir "/" file))) (defun test-coq-par-one-test (counter dir file-descr variant dep-just-compiled) @@ -832,7 +833,7 @@ test the result and side effects wth `assert'." ;; different-counter (current-time)) (setq different-not-ok nil) (setq different-counter (1- different-counter)) - (assert (> different-counter 0) + (cl-assert (> different-counter 0) nil "create files with different time stamps failed") (dolist (same-descr file-descr) (when (symbolp same-descr) @@ -845,7 +846,7 @@ test the result and side effects wth `assert'." (setq same-not-ok t) (while same-not-ok (setq same-counter (1- same-counter)) - (assert (> same-counter 0) + (cl-assert (> same-counter 0) nil "create files with same time stamp filed") (dolist (file file-list) (with-temp-file file t)) @@ -875,40 +876,40 @@ test the result and side effects wth `assert'." (put job 'youngest-coqc-dependency 'just-compiled)) (setq result (coq-par-job-needs-compilation job)) ;; check result - (assert (eq result compilation-result) + (cl-assert (eq result compilation-result) nil (concat id " result")) ;; check file deletion - (assert (or (not delete-result) + (cl-assert (or (not delete-result) (not (file-attributes (test-coq-par-sym-to-file dir delete-result)))) nil (concat id " delete file")) ;; check no other file is deleted (dolist (f file-descr-flattened) (unless (eq f delete-result) - (assert (file-attributes (test-coq-par-sym-to-file dir f)) + (cl-assert (file-attributes (test-coq-par-sym-to-file dir f)) nil (format "%s non del file %s: %s" id f (test-coq-par-sym-to-file dir f))))) ;; check value of 'required-obj-file property - (assert (equal (get job 'required-obj-file) + (cl-assert (equal (get job 'required-obj-file) (test-coq-par-sym-to-file dir req-obj-result)) nil (concat id " required-obj-file")) ;; check 'obj-mod-time property (if obj-mod-result - (assert + (cl-assert (equal (get job 'obj-mod-time) (nth 5 (file-attributes (test-coq-par-sym-to-file dir obj-mod-result)))) nil (concat id " obj-mod-time non nil")) - (assert (not (get job 'obj-mod-time)) + (cl-assert (not (get job 'obj-mod-time)) nil (concat id " obj-mod-time nil"))) ;; check 'use-quick property - (assert (eq (not (not (and compilation-result (eq req-obj-result 'vio)))) + (cl-assert (eq (not (not (and compilation-result (eq req-obj-result 'vio)))) (get job 'use-quick)) nil (concat id " use-quick")) ;; check vio2vo-needed property - (assert (eq + (cl-assert (eq (and (eq quick-mode 'quick-and-vio2vo) (eq req-obj-result 'vio) (or (eq delete-result 'vo) diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el index 4889ccaf..3cdcd02a 100644 --- a/coq/coq-seq-compile.el +++ b/coq/coq-seq-compile.el @@ -24,6 +24,7 @@ ;;; Code: +(eval-when-compile (require 'cl-lib)) (defvar queueitems) ; dynamic scope in p-s-extend-queue-hook (require 'coq-compile-common) @@ -335,8 +336,8 @@ function returns () if MODULE-ID comes from the standard library." ;; error-message))) ;; (coq-display-compile-response-buffer) (error error-message))) - (assert (<= (length result) 1) - "Internal error in coq-seq-map-module-id-to-obj-file") + (cl-assert (<= (length result) 1) + "Internal error in coq-seq-map-module-id-to-obj-file") (car-safe result))) (defun coq-seq-check-module (coq-object-local-hash-symbol span module-id &optional from) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index bb32fc52..e1a9a7e3 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -19,6 +19,7 @@ ;;; Code: +(eval-when-compile (require 'cl-lib)) (require 'proof-syntax) (require 'proof-utils) ; proof-locate-executable (require 'coq-db) @@ -509,12 +510,12 @@ so for the following reasons: ) ;; modules and section are indented like goal starters -;;; PC TODO: this category is used only for indentation, because -;;; scripting uses information from coq to decide if a goal is -;;; started. Since it is impossible for some commands to know -;;; syntactically if they start something (ex: Instance), the -;;; right thing to do would be to indent only on "Proof." and forget -;;; about this category for indentation. +;; PC TODO: this category is used only for indentation, because +;; scripting uses information from coq to decide if a goal is +;; started. Since it is impossible for some commands to know +;; syntactically if they start something (ex: Instance), the +;; right thing to do would be to indent only on "Proof." and forget +;; about this category for indentation. (defvar coq-goal-starters-db '( @@ -991,7 +992,7 @@ so for the following reasons: Empty matches are counted once." (let ((nbmatch 0) (str strg)) (while (and (proof-string-match regexp str) (not (string-equal str ""))) - (incf nbmatch) + (cl-incf nbmatch) (if (= (match-end 0) 0) (setq str (substring str 1)) (setq str (substring str (match-end 0))))) nbmatch)) -- cgit v1.2.3