[nongnu] elpa/idris-mode ed88191c43 01/10: [ flymake ] Improvment to flycheck checkers.

[ELPA Syncer]

branch: elpa/idris-mode
commit ed88191c4320c63cd5d7d741c0912918e1c70633
Author: Jan de Muijnck-Hughes <jan.deMuijnck-Hughes@glasgow.ac.uk>
Commit: Marek L <nospam.keram@gmail.com>

    [ flymake ] Improvment to flycheck checkers.
    
    1. Move them to an external file.
    2. Define a checker for Idris2.
    
    There is a bug which means that, althought the patterns are valid, I cannot 
work out why errorful files are not reporting their errors....
---
 Makefile                    | 13 +++++--
 flycheck-idris.el           | 93 +++++++++++++++++++++++++++++++++++++++++++++
 idris-mode.el               | 20 ----------
 idris-test-flycheck.el      | 59 ++++++++++++++++++++++++++++
 test/test-data/Flycheck.idr |  8 ++++
 5 files changed, 170 insertions(+), 23 deletions(-)

diff --git a/Makefile b/Makefile
index 46994f0f13..541d2c3ee9 100644
--- a/Makefile
+++ b/Makefile
@@ -3,7 +3,7 @@
 
 EMACS ?= emacs
 
-NEED_PKGS=prop-menu
+NEED_PKGS=prop-menu flycheck
 
 BATCHEMACS=$(EMACS) --batch --no-site-file -q \
        -eval '(add-to-list (quote load-path) "${PWD}/")' \
@@ -37,8 +37,9 @@ OBJS =        idris-commands.elc              \
        idris-syntax.elc                \
        idris-warnings.elc              \
        idris-warnings-tree.elc         \
-       idris-xref.elc \
-       inferior-idris.elc
+       idris-xref.elc                  \
+       inferior-idris.elc              \
+       flycheck-idris.elc
 
 .el.elc:
        $(BYTECOMP) $<
@@ -53,6 +54,12 @@ test2: getdeps build
                -eval '(setq idris-interpreter-path (executable-find 
"idris2"))' \
                -l ert -l test/idris-tests.el -f ert-run-tests-batch-and-exit
 
+flycheck: 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-test-flycheck.el -f ert-run-tests-batch-and-exit
+
 clean:
        -${RM} -f $(OBJS)
        -${RM} -f test/test-data/*ibc
diff --git a/flycheck-idris.el b/flycheck-idris.el
new file mode 100644
index 0000000000..1570aa1c0d
--- /dev/null
+++ b/flycheck-idris.el
@@ -0,0 +1,93 @@
+;;; flycheck-idris.el --- Major mode for editing Idris code -*- 
lexical-binding: t -*-
+
+;; Copyright (C) 2022
+
+;; Author:
+;; URL: https://github.com/idris-hackers/idris-mode
+;; Keywords: languages
+;; Package-Requires: ((emacs "24") (prop-menu "0.1") (cl-lib "0.5"))
+;; Version: 1.1.0
+
+
+;;; Commentary:
+
+;; FlyCheck checkers for Idris(2)
+
+;;; Code:
+
+(require 'flycheck)
+(require 'idris-mode)
+
+(flycheck-define-checker idris
+  "An Idris syntax and type checker."
+  :command ("idris"
+            "--check" "--nocolor" "--warnpartial"
+            ;; Compute the command-line options similarly to inferior-idris
+            (eval (idris-compute-flags))
+            source)
+  :error-patterns
+  ((warning line-start
+            (file-name)
+            ":"
+            line
+            ":"
+            column
+            ":Warning - "
+            (message (and (* nonl) (* "\n" (not (any "/" "~")) (* nonl)))))
+   (error line-start
+          (file-name)
+          ":"
+          line
+          ":"
+          column
+          ":"
+          (message (and (* nonl) (* "\n" (not (any "/" "~")) (* nonl))))))
+  :modes idris-mode)
+
+
+(flycheck-define-checker idris2
+  "An Idris2 syntax and type checker."
+  :command ("idris2"
+            "-q"
+            "--check" "--nocolor" "--warnpartial"
+            ;; Compute the command-line options similarly to inferior-idris
+            (eval (idris-compute-flags))
+            source)
+  :error-patterns ((warning line-start
+                            "Warning: "
+                            (message (seq (and (* nonl)
+                                               (* "\n"
+                                                  (not (any "/" "~"))
+                                                  (* nonl)))
+                                          (+ "\n")))
+                            (file-name)
+                            ":"  line
+                            ":"  column
+                            "--" end-line
+                            ":"  end-column
+                            )
+                   (error line-start
+                          "Error: "
+                          (message (seq (and (* nonl)
+                                             (* "\n"
+                                                (not (any "/" "~"))
+                                                (* nonl)))
+                                        (+ "\n")))
+                          (file-name)
+                          ":"  line
+                          ":"  column
+                          "--" end-line
+                          ":"  end-column
+                          )
+                   )
+  :modes idris-mode)
+
+(setq flycheck-idris2-executable "idris2")
+
+;;; ###autoload
+(add-to-list 'flycheck-checkers 'idris)
+(add-to-list 'flycheck-checkers 'idris2)
+
+
+(provide 'flycheck-idris)
+;;; flycheck-idris.el ends here
diff --git a/idris-mode.el b/idris-mode.el
index 4ac0a22123..7809e9a912 100644
--- a/idris-mode.el
+++ b/idris-mode.el
@@ -173,25 +173,5 @@ Invokes `idris-mode-hook'."
 (push '("\\.lidr$" . idris-mode) auto-mode-alist)
 
 
-;;; Handy utilities for other modes
-(eval-after-load 'flycheck
-  '(eval
-    '(progn
-       (flycheck-define-checker idris
-         "An Idris syntax and type checker."
-         :command ("idris"
-                 "--check" "--nocolor" "--warnpartial"
-                 ;; Compute the command-line options similarly to 
inferior-idris
-                 (eval (idris-compute-flags))
-                 source)
-         :error-patterns
-         ((warning line-start (file-name) ":" line ":" column ":Warning - "
-                   (message (and (* nonl) (* "\n" (not (any "/" "~")) (* 
nonl)))))
-          (error line-start (file-name) ":" line ":" column ":"
-                 (message (and (* nonl) (* "\n" (not (any "/" "~")) (* 
nonl))))))
-         :modes idris-mode)
-
-       (add-to-list 'flycheck-checkers 'idris))))
-
 (provide 'idris-mode)
 ;;; idris-mode.el ends here
diff --git a/idris-test-flycheck.el b/idris-test-flycheck.el
new file mode 100644
index 0000000000..5fadfcdc7e
--- /dev/null
+++ b/idris-test-flycheck.el
@@ -0,0 +1,59 @@
+(require 'flycheck)
+(require 'idris-mode)
+(require 'flycheck-idris)
+(require 'idris-commands)
+(require 'inferior-idris)
+(require 'idris-ipkg-mode)
+(require 'cl-lib)
+(require 'idris-test-utils)
+
+;;; Code:
+
+(flycheck-parse-error-with-patterns
+(concat "Warning: We are about to implicitly bind the following lowercase 
names.\n"
+        "You may be unintentionally shadowing the associated global 
definitions:\n"
+        "  plus is shadowing Main.plus, Prelude.Types.plus\n"
+        "\n"
+        "Temp:5:3--5:4\n"
+        " 1 | plus : Nat -> Nat -> Nat    \n"
+        " 2 | plus x y = plus x \"w\"      \n"
+        " 3 |                             \n"
+        " 4 | data Foo : Nat -> Type where\n"
+        " 5 |   F : Foo plus              \n"
+        "       ^                         \n"
+        "\n")
+(flycheck-checker-get 'idris2 'error-patterns)
+'idris2)
+
+(flycheck-parse-error-with-patterns
+ (concat "Error: While processing right hand side of plus. Ambiguous 
elaboration. Possible results:\n"
+        "    Main.plus x (Builtin.fromString \"w\")          \n"
+        "    Prelude.plus x (Builtin.fromString \"w\")       \n"
+        "\n                                "
+        "Temp:2:12--2:16                 \n"
+        " 1 | plus : Nat -> Nat -> Nat   \n"
+        " 2 | plus x y = plus x \"w\"      \n"
+        "                ^^^^            \n"
+        "\n")
+ (flycheck-checker-get 'idris2 'error-patterns)
+ 'idris2)
+
+(flycheck-parse-error-with-patterns
+ (concat "Error: While processing right hand side of double. Undefined name 
rhs.\n"
+         "\n"
+         "Temp:8:12--8:15                   \n"
+         " 4 | data Foo : Nat -> Type where \n"
+         " 5 |   F : Foo plus               \n"
+         " 6 |    a                          \n"
+         " 7 | double : Nat -> Nat          \n"
+         " 8 | double x = rhs x x           \n"
+         "                ^^^               \n"
+         "\n")
+ (flycheck-checker-get 'idris2 'error-patterns)
+ 'idris2)
+
+
+(null nil)
+
+(provide 'idris-test-flycheck)
+;;; idris-test-flycheck.el ends here
diff --git a/test/test-data/Flycheck.idr b/test/test-data/Flycheck.idr
new file mode 100644
index 0000000000..88499cf468
--- /dev/null
+++ b/test/test-data/Flycheck.idr
@@ -0,0 +1,8 @@
+plus : Nat -> Nat -> Nat
+plus x y = plus x "w"
+
+data Foo : Nat -> Type where
+  F : Foo plus
+
+double : Nat -> Nat
+double x = rhs x x