aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
Diffstat (limited to 'coq')
-rw-r--r--coq/coq-autotest.el6
-rw-r--r--coq/coq-db.el16
-rw-r--r--coq/coq-par-compile.el34
-rw-r--r--coq/coq-par-test.el35
-rw-r--r--coq/coq-seq-compile.el5
-rw-r--r--coq/coq-syntax.el17
6 files changed, 58 insertions, 55 deletions
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))
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 09:03:44 +0000