feature suggestion: parse Dafny/Boogie error strings in M-x compile mode

[0xabu]

I've found the following quite handy in my .emacs file to enable M-x compile to parse Dafny and Boogie error messages and warnings, and give me a clickable link directly to the offending source location. I don't know if this fits in the agenda for this package, so feel free to incorporate it or not, as you like.

(require 'compile)
(push
 '(boogieErr
   "^\\([a-zA-Z0-9_][^($]+\\)(\\([0-9]+\\),\\([0-9]+\\)): \\(Error\\|Verification of .* timed out\\).*$"
   1 2 3) compilation-error-regexp-alist-alist)
(push
 '(boogieInfo
   "^\\([a-zA-Z0-9_][^($]+\\)(\\([0-9]+\\),\\([0-9]+\\)): \\(Warning:\\|Related location\\|Timed out on\\).*$"
   1 2 3 0 nil) compilation-error-regexp-alist-alist)
(push 'boogieErr compilation-error-regexp-alist)
(push 'boogieInfo compilation-error-regexp-alist)

[cpitclaudel]

Thanks! I'm curious, though: what do you use in M-x compile?

I'm asking because boogie-friends already adds similar-looking patterns locally when you run C-c C-c from a boogie buffer.

[0xabu]

I have an external Makefile that coordinates verification of multiple files, so mostly I'm running make. It's also handy to be able to run Dafny with explicit arguments like /proc and /trace.