[nongnu] elpa/idris-mode 86c2fd294c 1/5: Remove idris-tests2.el in favour of using idris-tests.el

[ELPA Syncer]

branch: elpa/idris-mode
commit 86c2fd294c3cd1f03ee0daf4dbcfd3f6194f3870
Author: Marek L <nospam.keram@gmail.com>
Commit: Marek L <nospam.keram@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 <drc@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