branch: elpa/idris-mode
commit 86c2fd294c3cd1f03ee0daf4dbcfd3f6194f3870
Author: Marek L <nospam.ke...@gmail.com>
Commit: Marek L <nospam.ke...@gmail.com>
Remove idris-tests2.el in favour of using idris-tests.el
The only difference in these files was that
`idris-test-proof-search` is failing under Idris2.
This difference can be expressed in `ert`
using `:expected-result`.
https://www.gnu.org/software/emacs/manual/html_node/ert/Expected-Failures.html
---
Makefile | 3 +-
idris-tests.el | 5 +-
idris-tests2.el | 170 --------------------------------------------------------
3 files changed, 4 insertions(+), 174 deletions(-)
diff --git a/Makefile b/Makefile
index dc64d50660..5b358093a4 100644
--- a/Makefile
+++ b/Makefile
@@ -50,8 +50,7 @@ test: getdeps build
test2: getdeps build
$(BATCHEMACS) -L . \
-eval '(setq idris-interpreter-path (executable-find
"idris2"))' \
- -eval '(setq idris-repl-history-file
"~/.idris2/idris2-history.eld")' \
- -l ert -l idris-tests2.el -f ert-run-tests-batch-and-exit
+ -l ert -l idris-tests.el -f ert-run-tests-batch-and-exit
test3: getdeps build
$(BATCHEMACS) -L . \
diff --git a/idris-tests.el b/idris-tests.el
index 4ee5896ce8..367d4c2618 100644
--- a/idris-tests.el
+++ b/idris-tests.el
@@ -108,8 +108,9 @@ remain."
(ert-deftest idris-test-proof-search ()
"Test that proof search works"
-; (idris-quit)
-
+ :expected-result (if (string-match-p "idris2" idris-interpreter-path)
+ :failed
+ :passed)
(let ((buffer (find-file "test-data/ProofSearch.idr")))
(with-current-buffer buffer
(idris-load-file)
diff --git a/idris-tests2.el b/idris-tests2.el
deleted file mode 100644
index e32c8b8fa2..0000000000
--- a/idris-tests2.el
+++ /dev/null
@@ -1,170 +0,0 @@
-;;; idris-tests.el --- Tests for idris-mode -*- lexical-binding: t -*-
-
-;; Copyright (C) 2014 David Raymond Christiansen
-
-;; Author: David Raymond Christiansen <d...@itu.dk>
-;; Keywords: languages
-
-;; 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:
-
-;; This is a collection of simple tests for idris-mode.
-
-;;; Code:
-
-(require 'idris-mode)
-(require 'inferior-idris)
-(require 'idris-ipkg-mode)
-(require 'cl-lib)
-
-(ert-deftest trivial-test2 ()
- (should t))
-
-(ert-deftest idris-test2-idris-editor-port ()
- (let ((output "Can't find import Prelude\n37072\n"))
- (should (string-match idris-process-port-output-regexp output))
- (should (string= "Can't find import Prelude\n" (match-string 1 output)))
- (should (string= "37072" (match-string 2 output))))
- (let ((output "37072\n"))
- (should (string-match idris-process-port-output-regexp output))
- (should (null (match-string 1 output)))
- (should (string= "37072" (match-string 2 output)))))
-
-(ert-deftest idris-test2-idris-quit ()
- "Ensure that running Idris and quitting doesn't leave behind
-unwanted buffers."
- (let ((before (buffer-list)))
- (idris-repl)
- (dotimes (_ 5) (accept-process-output nil 1))
- (idris-quit)
- (let* ((after (buffer-list))
- (extra (cl-set-difference after before)))
- (should (= (length extra) 0)))))
-
-(ert-deftest idris-test2-idris-quit-logging-enabled ()
- "Ensure that running Idris and quitting doesn't leave behind
-unwanted buffers. In particular, only *idris-events* should
-remain."
- (let ((before (buffer-list))
- (idris-log-events 't))
- (idris-repl)
- (dotimes (_ 5) (accept-process-output nil 1))
- (idris-quit)
- (let* ((after (buffer-list))
- (extra (cl-set-difference after before)))
- (should (= (length extra) 1))
- (should (string= (buffer-name (car extra)) idris-event-buffer-name)))
-
- ;; Cleanup
- (kill-buffer idris-event-buffer-name)))
-
-(ert-deftest idris-test2-hole-load ()
- "Test the hole-list-on-load setting."
- (idris-quit)
- ;;; The default setting should be to show holes
- (should idris-hole-show-on-load)
-
- (let ((buffer (find-file "test-data/MetavarTest.idr")))
- ;;; Check that the file was loaded
- (should (bufferp buffer))
-
- ;;; Check that it shows the hole list with the option turned on
- (with-current-buffer buffer
- (idris-load-file))
- ;;; Allow async stuff to happen
- (dotimes (_ 5) (accept-process-output nil 1))
- (let ((mv-buffer (get-buffer idris-hole-list-buffer-name)))
- ;; The buffer exists and contains characters
- (should (bufferp mv-buffer))
- (should (> (buffer-size mv-buffer) 10)))
- (idris-quit)
-
- ;; Now check that it works with the setting the other way
- (let ((idris-hole-show-on-load nil))
- (with-current-buffer buffer
- (idris-load-file))
- (dotimes (_ 5) (accept-process-output nil 1))
- (let ((mv-buffer (get-buffer idris-hole-list-buffer-name)))
- (should-not (bufferp mv-buffer))
- (should (null mv-buffer))))
- ;; Clean up
- (kill-buffer))
-
- ;; More cleanup
- (idris-quit))
-
-;; Fails on idris2
-;; (ert-deftest idris-test2-proof-search ()
-;; "Test that proof search works"
-;; (idris-quit)
-
-;; (let ((buffer (find-file "test-data/ProofSearch.idr")))
-;; (with-current-buffer buffer
-;; (idris-load-file)
-;; (dotimes (_ 5) (accept-process-output nil 1))
-;; (goto-char (point-min))
-;; (re-search-forward "search_here")
-;; (goto-char (match-beginning 0))
-;; (idris-proof-search)
-;; (dotimes (_ 5) (accept-process-output nil 1))
-;; (should (looking-at-p "lteSucc (lteSucc (lteSucc (lteSucc (lteSucc
lteZero))))"))
-;; (move-beginning-of-line nil)
-;; (delete-region (point) (line-end-position))
-;; (insert "prf = ?search_here")
-;; (save-buffer)
-;; (kill-buffer)))
-;;
-;; ;; More cleanup
-;; (idris-quit))
-
-(ert-deftest idris-test2-find-cmdline-args ()
- "Test that idris-mode calculates command line arguments from .ipkg files."
- ;; Outside of a project, none are found
- (let ((buffer (find-file "test-data/ProofSearch.idr")))
- (with-current-buffer buffer
- (should (null (idris-ipkg-flags-for-current-buffer)))
- (kill-buffer)))
- ;; Inside of a project, the correct ones are found
- (let ((buffer (find-file "test-data/cmdline/src/Command/Line/Test.idr")))
- (with-current-buffer buffer
- (should (equal (idris-ipkg-flags-for-current-buffer)
- (list "-p" "effects")))
- (kill-buffer))))
-
-(ert-deftest idris-test2-error-buffer ()
- "Test that loading a type-incorrect Idris buffer results in an error message
buffer."
- (let ((buffer (find-file "test-data/TypeError.idr")))
- (with-current-buffer buffer
- (idris-load-file)
- (dotimes (_ 5) (accept-process-output nil 1))
- (should (get-buffer idris-notes-buffer-name)))
- (with-current-buffer (get-buffer idris-notes-buffer-name)
- (goto-char (point-min))
- (should (re-search-forward "Nat" nil t))) ;; check that the buffer has
something error-like
- (with-current-buffer buffer
- (kill-buffer))
- (idris-quit)))
-
-(ert-deftest idris-test2-ipkg-packages-with-underscores-and-dashes ()
- "Test that loading an ipkg file can have dependencies on packages with _ or
- in the name."
- (let ((buffer (find-file "test-data/package-test/Packaging.idr")))
- (with-current-buffer buffer
- (should (equal '("-p" "idris-free" "-p" "recursion_schemes")
- (idris-ipkg-pkgs-flags-for-current-buffer)))
- (kill-buffer buffer))
- (idris-quit)))
-
-(provide 'idris-tests2)
-;;; idris-tests.el ends here
