From 322910dc0b07c1b59bc968b1fb0d4c1d8bfb988e Mon Sep 17 00:00:00 2001 From: Scott Bonds Date: Thu, 10 Aug 2017 13:09:58 -0700 Subject: [PATCH] Add linter for Idris (#838) * Add linter for Idris * Fix parsing warnings and column ranges in Idris linter * Make Idris linter configurable. Fix help tag. --- README.md | 1 + ale_linters/idris/idris.vim | 87 +++++++++++++++++++ doc/ale-idris.txt | 23 +++++ doc/ale.txt | 3 + .../test_idris_command_callbacks.vader | 42 +++++++++ test/handler/test_idris_handler.vader | 52 +++++++++++ 6 files changed, 208 insertions(+) create mode 100644 ale_linters/idris/idris.vim create mode 100644 doc/ale-idris.txt create mode 100644 test/command_callback/test_idris_command_callbacks.vader create mode 100644 test/handler/test_idris_handler.vader diff --git a/README.md b/README.md index 5d2e798..305430d 100644 --- a/README.md +++ b/README.md @@ -84,6 +84,7 @@ name. That seems to be the fairest way to arrange this table. | Handlebars | [ember-template-lint](https://github.com/rwjblue/ember-template-lint) | | Haskell | [ghc](https://www.haskell.org/ghc/), [stack-ghc](https://haskellstack.org/), [stack-build](https://haskellstack.org/), [ghc-mod](https://github.com/DanielG/ghc-mod), [stack-ghc-mod](https://github.com/DanielG/ghc-mod), [hlint](https://hackage.haskell.org/package/hlint), [hdevtools](https://hackage.haskell.org/package/hdevtools) | | HTML | [HTMLHint](http://htmlhint.com/), [proselint](http://proselint.com/), [tidy](http://www.html-tidy.org/) | +| Idris | [idris](http://www.idris-lang.org/) | | Java | [checkstyle](http://checkstyle.sourceforge.net), [javac](http://www.oracle.com/technetwork/java/javase/downloads/index.html) | | JavaScript | [eslint](http://eslint.org/), [jscs](http://jscs.info/), [jshint](http://jshint.com/), [flow](https://flowtype.org/), [standard](http://standardjs.com/), [prettier](https://github.com/prettier/prettier) (and `prettier-eslint`, `prettier-standard`), [xo](https://github.com/sindresorhus/xo) | JSON | [jsonlint](http://zaa.ch/jsonlint/) | diff --git a/ale_linters/idris/idris.vim b/ale_linters/idris/idris.vim new file mode 100644 index 0000000..115d04f --- /dev/null +++ b/ale_linters/idris/idris.vim @@ -0,0 +1,87 @@ +" Author: Scott Bonds +" Description: default Idris compiler + +call ale#Set('idris_idris_executable', 'idris') +call ale#Set('idris_idris_options', '--total --warnpartial --warnreach --warnipkg') + +function! ale_linters#idris#idris#GetExecutable(buffer) abort + return ale#Var(a:buffer, 'idris_idris_executable') +endfunction + +function! ale_linters#idris#idris#GetCommand(buffer) abort + let l:options = ale#Var(a:buffer, 'idris_idris_options') + + return ale#Escape(ale_linters#idris#idris#GetExecutable(a:buffer)) + \ . (!empty(l:options) ? ' ' . l:options : '') + \ . ' --check %s' +endfunction + +function! ale_linters#idris#idris#Handle(buffer, lines) abort + " This was copied almost verbatim from ale#handlers#haskell#HandleGHCFormat + + " Look for lines like the following: + " foo.idr:2:6:When checking right hand side of main with expected type + " bar.idr:11:11-13: + let l:pattern = '\v^([a-zA-Z]?:?[^:]+):(\d+):(\d+)(-\d+)?:(.*)?$' + let l:output = [] + + let l:corrected_lines = [] + + for l:line in a:lines + if len(matchlist(l:line, l:pattern)) > 0 + call add(l:corrected_lines, l:line) + elseif len(l:corrected_lines) > 0 + if l:line is# '' + let l:corrected_lines[-1] .= ' ' " turn a blank line into a space + else + let l:corrected_lines[-1] .= l:line + endif + let l:corrected_lines[-1] = substitute(l:corrected_lines[-1], '\s\+', ' ', 'g') + endif + endfor + + for l:line in l:corrected_lines + let l:match = matchlist(l:line, l:pattern) + + if len(l:match) == 0 + continue + endif + + if !ale#path#IsBufferPath(a:buffer, l:match[1]) + continue + endif + + let l:errors = matchlist(l:match[5], '\v([wW]arning|[eE]rror) - ?(.*)') + + if len(l:errors) > 0 + let l:ghc_type = l:errors[1] + let l:text = l:errors[2] + else + let l:ghc_type = '' + let l:text = l:match[5][:0] is# ' ' ? l:match[5][1:] : l:match[5] + endif + + if l:ghc_type is? 'Warning' + let l:type = 'W' + else + let l:type = 'E' + endif + + call add(l:output, { + \ 'lnum': l:match[2] + 0, + \ 'col': l:match[3] + 0, + \ 'text': l:text, + \ 'type': l:type, + \}) + endfor + + return l:output +endfunction + +call ale#linter#Define('idris', { +\ 'name': 'idris', +\ 'executable_callback': 'ale_linters#idris#idris#GetExecutable', +\ 'command_callback': 'ale_linters#idris#idris#GetCommand', +\ 'callback': 'ale_linters#idris#idris#Handle', +\}) + diff --git a/doc/ale-idris.txt b/doc/ale-idris.txt new file mode 100644 index 0000000..c7500b0 --- /dev/null +++ b/doc/ale-idris.txt @@ -0,0 +1,23 @@ +=============================================================================== +ALE Idris Integration *ale-idris-options* + +=============================================================================== +idris *ale-idris-idris* + +g:ale_idris_idris_executable *g:ale_idris_idris_executable* + *b:ale_idris_idris_executable* + Type: |String| + Default: `'idris'` + + This variable can be changed to change the path to idris. + + +g:ale_idris_idris_options *g:ale_idris_idris_options* + *b:ale_idris_idris_options* + Type: |String| + Default: `'--total --warnpartial --warnreach --warnipkg'` + + This variable can be changed to modify flags given to idris. + +=============================================================================== + vim:tw=78:ts=2:sts=2:sw=2:ft=help:norl: diff --git a/doc/ale.txt b/doc/ale.txt index 869a557..eb31b82 100644 --- a/doc/ale.txt +++ b/doc/ale.txt @@ -49,6 +49,8 @@ CONTENTS *ale-contents* html..................................|ale-html-options| htmlhint............................|ale-html-htmlhint| tidy................................|ale-html-tidy| + idris.................................|ale-idris-options| + idris...............................|ale-idris-idris| java..................................|ale-java-options| checkstyle..........................|ale-java-checkstyle| javac...............................|ale-java-javac| @@ -191,6 +193,7 @@ The following languages and tools are supported. * Handlebars: 'ember-template-lint' * Haskell: 'ghc', 'stack-ghc', 'stack-build', 'ghc-mod', 'stack-ghc-mod', 'hlint', 'hdevtools' * HTML: 'HTMLHint', 'proselint', 'tidy' +* Idris: 'idris' * Java: 'javac' * JavaScript: 'eslint', 'jscs', 'jshint', 'flow', 'prettier', 'prettier-eslint', 'xo' * JSON: 'jsonlint' diff --git a/test/command_callback/test_idris_command_callbacks.vader b/test/command_callback/test_idris_command_callbacks.vader new file mode 100644 index 0000000..03a69f3 --- /dev/null +++ b/test/command_callback/test_idris_command_callbacks.vader @@ -0,0 +1,42 @@ +Before: + Save g:ale_idris_idris_executable + Save g:ale_idris_idris_options + + unlet! g:ale_idris_idris_executable + unlet! b:ale_idris_idris_executable + unlet! g:ale_idris_idris_options + unlet! b:ale_idris_idris_options + + runtime ale_linters/idris/idris.vim + +After: + Restore + unlet! b:command_tail + unlet! b:ale_idris_idris_executable + unlet! b:ale_idris_idris_options + call ale#linter#Reset() + +Execute(The executable should be configurable): + AssertEqual 'idris', ale_linters#idris#idris#GetExecutable(bufnr('')) + + let b:ale_idris_idris_executable = 'foobar' + + AssertEqual 'foobar', ale_linters#idris#idris#GetExecutable(bufnr('')) + +Execute(The executable should be used in the command): + AssertEqual + \ ale#Escape('idris') . ' --total --warnpartial --warnreach --warnipkg --check %s', + \ ale_linters#idris#idris#GetCommand(bufnr('')) + + let b:ale_idris_idris_executable = 'foobar' + + AssertEqual + \ ale#Escape('foobar') . ' --total --warnpartial --warnreach --warnipkg --check %s', + \ ale_linters#idris#idris#GetCommand(bufnr('')) + +Execute(The options should be configurable): + let b:ale_idris_idris_options = '--something' + + AssertEqual + \ ale#Escape('idris') . ' --something --check %s', + \ ale_linters#idris#idris#GetCommand(bufnr('')) diff --git a/test/handler/test_idris_handler.vader b/test/handler/test_idris_handler.vader new file mode 100644 index 0000000..1c20be7 --- /dev/null +++ b/test/handler/test_idris_handler.vader @@ -0,0 +1,52 @@ +Before: + runtime ale_linters/idris/idris.vim + +Execute(The idris handler should parse messages that reference a single column): + call ale#test#SetFilename('/tmp/foo.idr') + + AssertEqual + \ [ + \ { + \ 'lnum': 4, + \ 'col': 5, + \ 'type': 'E', + \ 'text': 'When checking right hand side of main with expected type IO () When checking an application of function Prelude.Monad.>>=: Type mismatch between IO () (Type of putStrLn _) and _ -> _ (Is putStrLn _ applied to too many arguments?) Specifically: Type mismatch between IO and \uv => _ -> uv' + \ } + \ ], + \ ale_linters#idris#idris#Handle(bufnr(''), [ + \ '/tmp/foo.idr:4:5:', + \ 'When checking right hand side of main with expected type', + \ ' IO ()', + \ '', + \ 'When checking an application of function Prelude.Monad.>>=:', + \ ' Type mismatch between', + \ ' IO () (Type of putStrLn _)', + \ ' and', + \ ' _ -> _ (Is putStrLn _ applied to too many arguments?)', + \ '', + \ ' Specifically:', + \ ' Type mismatch between', + \ ' IO', + \ ' and', + \ ' \uv => _ -> uv', + \ ]) + +Execute(The idris handler should parse messages that reference a column range): + call ale#test#SetFilename('/tmp/foo.idr') + + AssertEqual + \ [ + \ { + \ 'lnum': 11, + \ 'col': 11, + \ 'type': 'E', + \ 'text': 'When checking right hand side of Main.case block in main at /tmp/foo.idr:10:10 with expected type IO () Last statement in do block must be an expression' + \ } + \ ], + \ ale_linters#idris#idris#Handle(bufnr(''), [ + \ '/tmp/foo.idr:11:11-13:', + \ 'When checking right hand side of Main.case block in main at /tmp/foo.idr:10:10 with expected type', + \ ' IO ()', + \ '', + \ 'Last statement in do block must be an expression', + \ ])