From 141fa6c9dfa50a4df94eb98ade46c4c1a08b4b9c Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 4 May 2020 14:40:47 +0200 Subject: refactor: Remove unneeded auxiliary functions & Use "coq-" prefix --- ci/coq-tests.el | 29 +++++++++-------------------- 1 file changed, 9 insertions(+), 20 deletions(-) diff --git a/ci/coq-tests.el b/ci/coq-tests.el index 323448ae..41bbf0aa 100644 --- a/ci/coq-tests.el +++ b/ci/coq-tests.el @@ -56,18 +56,6 @@ (defconst coq-test-file-prefix "coq_test_") -(defun get-string-from-file (filePath) - "Return filePath's file content." - (with-temp-buffer - (insert-file-contents filePath) - (buffer-string))) - -(defun read-lines (filePath) - "Return a list of lines of a file at filePath." - (with-temp-buffer - (insert-file-contents filePath) - (split-string (buffer-string) "\n" t))) - (defun coq-test-init () "Ensure `coq' is loaded." (unless (featurep 'coq) @@ -85,7 +73,7 @@ ;; DEFINITION OF MOCKS, SEE `coq-mock' BELOW ;; Another solution would consist in using el-mock, mentioned in: ;; https://www.gnu.org/software/emacs/manual/html_mono/ert.html#Mocks-and-Stubs -(defun mock-proof-display-three-b (&rest rest) +(defun coq-mock-proof-display-three-b (&rest rest) (message (concat "Skipping proof-display-three-b on input: " (pp-to-string rest))) ; Result: @@ -108,7 +96,7 @@ (defun coq-mock (f) (require 'pg-response) ; load the feature defining proof-display-three-b first (cl-letf (;((symbol-function 'foo) #'mock-foo) - ((symbol-function 'proof-display-three-b) #'mock-proof-display-three-b)) + ((symbol-function 'proof-display-three-b) #'coq-mock-proof-display-three-b)) (funcall f))) ;; Run on: ;; (coq-mock #'main) @@ -172,7 +160,7 @@ For example, COMMENT could be (*test-definition*)" (goto-char (point-min)) (search-forward comment)) -(defun should-response (message) +(defun coq-should-response (message) (should (equal message (string-trim (with-current-buffer "*response*" @@ -196,7 +184,7 @@ For example, COMMENT could be (*test-definition*)" (coq-test-goto-before "(*test-definition*)") (proof-goto-point) (proof-shell-wait) - (should-response "trois is defined")))) + (coq-should-response "trois is defined")))) (ert-deftest coq-test-position () @@ -233,7 +221,7 @@ For example, COMMENT could be (*test-definition*)" (let ((proof-point (save-excursion (coq-test-goto-after "(*error*)")))) (proof-goto-point) (proof-shell-wait) - (should-response "Error: Unable to unify \"false\" with \"true\".") + (coq-should-response "Error: Unable to unify \"false\" with \"true\".") (should (equal (proof-queue-or-locked-end) proof-point)))))) @@ -241,11 +229,12 @@ For example, COMMENT could be (*test-definition*)" (coq-fixture-on-file (coq-test-full-path "test_wholefile.v") (lambda () - (let ((proof-point (save-excursion (coq-test-goto-after "(*end here*)")))) + (let ((proof-point (save-excursion + (coq-test-goto-before "Theorem") + (search-forward "Qed.")))) (proof-process-buffer) (proof-shell-wait) - (should (equal (proof-queue-or-locked-end) proof-point)))))) - + (should (equal (proof-queue-or-locked-end) proof-point)))))) (provide 'coq-tests) -- cgit v1.2.3