ale_linters: add 'dafny' linter

README.md

@@ -87,6 +87,7 @@ formatting.
 | CSS | [csslint](http://csslint.net/), [stylelint](https://github.com/stylelint/stylelint), [prettier](https://github.com/prettier/prettier) |
 | Cython (pyrex filetype) | [cython](http://cython.org/) |
 | D | [dmd](https://dlang.org/dmd-linux.html) |
+| Dafny | [dafny](https://rise4fun.com/Dafny) |
 | Dart | [dartanalyzer](https://github.com/dart-lang/sdk/tree/master/pkg/analyzer_cli) !!, [language_server](https://github.com/natebosch/dart_language_server) |
 | Dockerfile | [hadolint](https://github.com/lukasmartinelli/hadolint) |
 | Elixir | [credo](https://github.com/rrrene/credo), [dogma](https://github.com/lpil/dogma) !! |

ale_linters/dafny/dafny.vim

@@ -0,0 +1,24 @@
+" Author: Taylor Blau <me@ttaylorr.com>
+
+function! ale_linters#dafny#dafny#Handle(buffer, lines) abort
+    let l:pattern = '\v(.*)\((\d+),(\d+)\): (.*): (.*)'
+    let l:output = []
+
+    for l:match in ale#util#GetMatches(a:lines, l:pattern)
+        call add(l:output, {
+        \    'bufnr': a:buffer,
+        \    'col': l:match[3] + 0,
+        \    'lnum': l:match[2] + 0,
+        \    'text': l:match[5],
+        \    'type': l:match[4] =~# '^Error' ? 'E' : 'W'
+        \ })
+    endfor
+    return l:output
+endfunction
+
+call ale#linter#Define('dafny', {
+\    'name': 'dafny',
+\    'executable': 'dafny',
+\    'command': 'dafny %s /compile:0',
+\    'callback': 'ale_linters#dafny#dafny#Handle',
+\ })

doc/ale.txt

@@ -270,6 +270,7 @@ Notes:
 * CSS: `csslint`, `stylelint`, `prettier`
 * Cython (pyrex filetype): `cython`
 * D: `dmd`
+* Dafny: `dafny`!!
 * Dart: `dartanalyzer`!!, `language_server`
 * Dockerfile: `hadolint`
 * Elixir: `credo`, `dogma`!!

test/handler/test_dafny_handler.vader

@@ -0,0 +1,26 @@
+Execute(The Dafny handler should parse output correctly):
+  runtime ale_linters/dafny/dafny.vim
+  AssertEqual
+  \ [
+  \   {
+  \     'bufnr': 0,
+  \     'col': 45,
+  \     'lnum': 123,
+  \     'text': 'A precondition for this call might not hold.',
+  \     'type': 'E'
+  \   },
+  \   {
+  \     'bufnr': 0,
+  \     'col': 90,
+  \     'lnum': 678,
+  \     'text': 'This is the precondition that might not hold.',
+  \     'type': 'W'
+  \   }
+  \ ],
+  \ ale_linters#dafny#dafny#Handle(0, [
+  \ 'File.dfy(123,45): Error BP5002: A precondition for this call might not hold.',
+  \ 'File.dfy(678,90): Related location: This is the precondition that might not hold.'
+  \ ])
+
+After:
+  call ale#linter#Reset()