Easy way to have flycheck detect that current file is in the Dafny or Boogie test suite?

[wilcoxjay]

I am wondering if it would be possible to have flycheck autodetect that the current buffer is a Dafny or Boogie test, and to use the flags in the // RUN: comment at the top of the file instead of the otherwise configured flags.

This would solve the issue of flycheck reporting spurious errors when editing a test due to using different flags than the ones the test expects.

Perhaps the easiest way to implement this is just to look for such comments in any files and use them as flags.

Since this behavior could be surprising, it might be best if it was guarded by a customizable variable.

I'm planning to prototype it for my own use, but was curious to see whether others would fine it helpful.

[wilcoxjay]

I've pushed a prototype to wilcoxjay/boogie-friends/parse-run-line.

[cpitclaudel]

This is a nice feature, sorry that I let it fall through. I think it's certainly nice to have that option, and indeed it has to be conditional somehow to avoid security issues. Emacs has a mechanism for that, file-local variables, and I expect we might be able to hook into that case. There's an additional difficulty, though: Dafny's lsp mode only supports a small set of flags at the moment, and we'd like to move to LSP in Emacs as well eventually.