boogie-org/boogie-friends

Tools for interacting with Boogie

Boogie friends

A collection of tools for interacting with Boogie and related languages.

Emacs package (boogie-mode, dafny-mode, z3-smt2-mode)

The boogie-friends package is an experimental collection of Emacs modes for writing verified programs in z3 and languages of the Boogie family (including Dafny).

Notable features are listed below:

• Syntax highlighting
• Real-time verification (using flycheck)

In addition, the Dafny and Boogie modes offer:

• Completion (using company)
• Code folding (using hideshow)
• Prettification (using prettify-symbols-mode)

And the Dafny mode additionally also has:

• (A few) Snippets (using yasnippet)
• (Some) In-Emacs documentation
• (Experimental) Navigation between Dafny and Boogie source files
• (Some support for) jumping to a definition
• (Experimental) support for using Dafny as a verification server. This means that Emacs spawns a server process, and uses Dafny's caching facilities to (massively) improve reactivity.

Some pictures:

A Dafny buffer

Notice the error highlighting, the symbol beautification (forall appears as ∀), and the code folding on the last line!

A Z3 buffer

A Boogie buffer

Completion and snippets

Documentation (Dafny only)

Browsing the Boogie translation of a Dafny file

Setup

1. Setup MELPA by adding the following lines to your .emacs if you don't have them already (here's more information if you have trouble with this step):

   (require 'package) ;; You might already have this line
   (add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t)
   (package-initialize) ;; You might already have this line

2. Install the package: M-x package-refresh-contents RET, then M-x package-install RET boogie-friends RET

3. For Dafny, just use M-x lsp to download and run the Dafny language server. For other languages (or to use Dafny's legacy server), configure Flycheck as shown below.

On-the-fly verification

For Boogie and Z3

Use the following settings to point boogie-friends to Boogie and Z3 binaries:

;; To get real-time error highlights (Flycheck) in Boogie files
(setq flycheck-boogie-executable "PATH-TO-BOOGIE-BINARIES/Boogie")

;; To get real-time error highlights (Flycheck) in Z3 files
(setq flycheck-z3-executable "PATH-TO-Z3-BINARIES/z3")

;; To use Z3's axiom profiler
(setq boogie-friends-profile-analyzer-executable "PATH-TO-Z3-AXIOM-PROFILER")

For Dafny

dafny-mode supports three real-time verification mechanisms: cli, server, and lsp. LSP is the recommended one; it supports automatic downloads and advanced IDE features. To use it, open a Dafny buffer and type M-x lsp (optionally, use M-x customize-variable RET lsp-dafny-preferred-version first to chose which version of Dafny to install and run).

As an alternative (if you run into stability or performance issues with LSP), you can either:

• Get on-the-fly verification through the legacy Dafny server, which more basic than LSP but also more robust, by downloading a Dafny release manually and configuring flycheck-inferior-dafny-executable:

  (setq flycheck-inferior-dafny-executable "PATH-TO-DAFNY-BINARIES/DafnyServer")
  (setq dafny-verification-backend 'server)

• Get on-the-fly verification through the command line, which is slower (no caching) but even more robust, by downloading a Dafny release manually and configuring flycheck-dafny-executable:

  (setq flycheck-dafny-executable "PATH-TO-DAFNY-BINARIES/DafnyServer")
  (setq dafny-verification-backend 'cli)

If you run into issues, C-c ! v (flycheck-verify-setup) should have debugging info.

For Boogie

Keybindings

All modes

• C-c C-c re-verifies the current file. With a prefix argument (C-u C-c C-c), extra arguments are sent to the verifier (by default /trace).
• S-TAB manually cycles through reasonable indentation levels.

Dafny and Boogie

• C-c C-t gets a verification trace for the current file, and parses the resulting timings.
• C-c C-p prompts for a method name, generates a tracing profile of that method, and launches the profile analyzer (boogie-friends-profile-analyzer-executable) on the resulting trace.

Dafny only

• TAB auto-indents.

• C-c C-? opens the Dafny docs.

• <C-down-mouse-1> looks for the definition of the function under point in open buffers.

• C-c C-a translates the current file to Boogie and shows the translated file.

• C-c C-j or C-S-down-mouse-1 (aka Ctrl-Shift-Click) jumps to the Boogie line matching the current Dafny line.

• After inserting a snippet, TAB moves to the next snippet field, and C-d removes the current field entirely.

• During completion, C-h shows documentation for the current snippet, if available.

Tips

General

• Completion, indentation, snippets, syntax coloring, and real-time verification should work out of the box.
• Verification happens as you type, and its status is shows in the mode line (FlyC*: busy; FlyC:a/b: done with a errors and b warnings).

Real-time error highlighting

Real-time error highlighting is enabled by default for all languages. You can disable it by adding (setq flycheck-disabled-checkers '(dafny inferior-dafny)) to your .emacs.

Font support

If you see blocks instead of proper characters, or tall characters, or ugly characters:

1. Install a good font and restart Emacs (Arial Unicode, Cambria, Segoe UI Symbol, DejaVu Sans Mono, FreeMono, STIX, Unifont and Symbola should all work).

2. If that doesn't fix it, setup font fallback by adding the following to your .emacs (replace "Symbola" by the name of your font):

   (set-fontset-font t 'unicode (font-spec :name "Symbola") nil 'append)

3. If that still doesn't work, turn of prettification entirely by adding the following to your .emacs:

   (defun no-prettification-in-dafny-mode ()
     (prettify-symbols-mode -1))
   (add-hook 'dafny-mode-hook #'no-prettification-in-dafny-mode)

If you don't like the way one particular symbol is rendered, you can adjust the font for just that one:

(set-fontset-font t (cons ?≔ ?≔) "FreeSerif" nil 'prepend)

Profiling

A typical profiling workflow proceeds as follows:

1. Open a file for which verification is slow, or times out.
2. Use C-c C-t to generate a trace (the default timeout is set to 30s; you can customize it by changing boogie-friends-profiler-timeout).
3. Use C-c C-p to profile a function. The slowest method (as determined by the trace) is presented first.
4. Marvel at the intricacies of the axiom profiler.

Note: The axiom profiler works best if it has a Boogie source file to look at; thus, when profiling a Dafny source file, boogie-friends transparently saves it as a translated Boogie file first, and then runs Boogie (with profiling enabled) on it. Thus the profiler is Boogie in all cases, and custom prover arguments need to be set for Boogie if they are to be taken into account for profiling (for tracing and translation, however, Dafny's settings apply).

Custom prover configurations

Each time boogie-friends calls a prover, it collects arguments from four sources:

• LANGUAGE-prover-args, the list of arguments passed to the prover in the default configuration (i.e. dafny-prover-args and boogie-prover-args). This has pretty good defaults, and probably shouldn't be changed.

• LANGUAGE-prover-custom-args, a list of extra flags. This is empty by default, and is a good place to add your own flags.

LANGUAGE-prover-local-args, another list of extra flags. This is empty by default, and is a good place to add per-file or per-directory flags (see below).

• LANGUAGE-prover-alternate-args, a list of flags added to the prover invocation when running verify/compile with a prefix argument (C-u C-c C-c). This is a good place to add flags that you do not always need; for example "/compile:3" (this is the default).

An example configuration might thus look like this:

;; Don't allow assumptions
(setq dafny-prover-custom-args '("/noCheating:1"))

;; Get more debug output when verifying with C-u C-c C-c
(setq dafny-prover-alternate-args '("/proverWarnings:2" "/traceverify" "/z3opt:TRACE=true" "/trace" "/traceTimes" "/tracePOs"))

The LANGUAGE-prover-local-args is useful if a file requires specific flags (maybe /vcsMaxKeepGoingSplits, for example): in that case you can set the LANGUAGE-prover-local-args in just that file or in the corresponding directory.

For example, you can add the following to the top of a file:

// -*- dafny-prover-local-args: ("/vcsMaxKeepGoingSplits:5" "/proverMemoryLimit:250") -*-

Troubleshooting

• If you run into trouble LSP, consider using the legacy Dafny server. If you run into issues with that, then the CLI-based verification backend should be fine, though slower (see instructions at the top of this README). You can also disable on-the-fly verification using (setq dafny-verification-backend 'cli).

• If the verification seems to be taking forever, M-x inferior-dafny-reset may help when using the legacy server. With LSP, typing any character interrupts verification.

Acknowledgments

The documentation that ships with this package is auto-generated from the Dafny Quick Reference.

Pull requests are welcome!

Clone the repo:

mkdir -p ~/.emacs.d/lisp/ && cd ~/.emacs.d/lisp/
git clone https://github.com/boogie-org/boogie-friends

Then in your .emacs (in addition to the stuff above):

(add-to-list 'load-path "~/.emacs.d/lisp/boogie-friends/emacs/")
(require 'dafny-mode)
(require 'boogie-mode)

boogie-friends's Issues

Flycheck ignores Boogie errors if they lack proper location information

Sometimes, Boogie will report errors without providing location information. (This could be due to the error having no true source-level location, for example.) In that case, the flycheck error patterns simply fail to match the error, which can lead to believing a file verifies, when in fact it does not.

When using `include`, helpful "this is the precondition that might not hold" information is missing from flycheck errors

Consider a that has two files A.dfy and B.dfy. A contains library declarations, which B uses via the include directive.

// A.dfy
method foo(x: int)
  requires x > 0
  requires x % 2 == 0
{
} 

// B.dfy
include "A.dfy"

method bar()
{
  foo(0);
}

Then flycheck will report that a precondition of foo is violated, but it won't tell you which one. This gets annoying when there are many preconditions, and I am reduced to copy-pasting the contents of A into B or to running dafny on the command line.

Would it be possible to get this information into flycheck, preferably including the ability to jump to the precondition, just like when the caller and callee are in the same file?

No syntax errors when using Dafny server

Only verification errors are reported when using the Dafny server backend. Syntax, type checking and symbol resolution errors aren't shown. When the default backend is used instead, all errors are reported.

Could that be related to the fact that Dafny server returns [SUCCESS] when these errors occur? I'm using Dafny 1.9.7.

And thanks for this useful mode!

Flycheck seems to report success when error is in included file

Suppose I create two files, A.dfy and B.dfy, as follows:

A.dfy:

predicate Problem() {
   1 == false
}

B.dfy:

include "A.dfy"

lemma UhOh()
  ensures false
{
}

When viewing A.dfy, the type error in the body of Problem is correctly identified. However, when viewing B.dfy, no error is reported (the Flycheck status in the modeline indicates no errors, and there are no errors to be jumped to via Flycheck keybindings). Commenting the include statement causes the unprovable lemma to be correctly identified.

In general, this problem is: when there is a syntax or type error in an included file (i.e. A.dfy), verification of the including module (i.e. B.dfy) appears to succeed. A verification error in the included file will not cause this effect, and this effect will not mask the reporting of syntax or type errors in the including file—only verification errors are masked by this problem.

It's unclear to me whether the fix to this bug lies with Dafny or with the Emacs mode; paging @RustanLeino for further discussion of this.

dafny-mode fails to parse warnings

This is my file:

function fib(n: int): int {
  if n in {0,1}
    then 1
    else fib(n-1) + fib(n-2)
}

Running dafny on it produces the following error:

$ dafny /compile\:0 /nologo /home/sohum/tmp/1fib.dfy
/home/sohum/tmp/1fib.dfy(4,9): Error: decreases expression must be bounded below by 0
/home/sohum/tmp/1fib.dfy(1,13): Related location
Execution trace:
    (0,0): anon0
    (0,0): anon7_Else
    (0,0): anon8_Else

Dafny program verifier finished with 0 verified, 1 error

Compilation exited abnormally with code 3 at Tue Sep 27 14:45:48

dafny-mode however crashes on it and reports no errors, showing this stack trace:

Debugger entered--Lisp error: (wrong-type-argument arrayp nil)
  replace-regexp-in-string("/home/sohum/tmp/flycheck_1fib\\.dfy" "/home/sohum/tmp/1fib.dfy" nil fixed-case literal)
  flycheck-fix-error-filename([cl-struct-flycheck-error #<buffer 1fib.dfy> dafny "/home/sohum/tmp/1fib.dfy" 1 13 nil warning nil] ("/home/sohum/tmp/flycheck_1fib.dfy") "/home/sohum/tmp/")
  #[257 "\302�\300\301#\207" [("/home/sohum/tmp/flycheck_1fib.dfy") "/home/sohum/tmp/" flycheck-fix-error-filename] 5 "\n\n(fn E)"]([cl-struct-flycheck-error #<buffer 1fib.dfy> dafny "/home/sohum/tmp/1fib.dfy" 1 13 nil warning nil])
  seq-map(#[257 "\302�\300\301#\207" [("/home/sohum/tmp/flycheck_1fib.dfy") "/home/sohum/tmp/" flycheck-fix-error-filename] 5 "\n\n(fn E)"] ([cl-struct-flycheck-error #<buffer 1fib.dfy> dafny "/home/sohum/tmp/1fib.dfy" 1 9 "decreases n" tooltip nil] [cl-struct-flycheck-error #<buffer 1fib.dfy> dafny "/home/sohum/tmp/1fib.dfy" 4 9 "decreases expression must be bounded below by 0" error nil] [cl-struct-flycheck-error #<buffer 1fib.dfy> dafny "/home/sohum/tmp/1fib.dfy" 1 13 nil warning nil]))
  flycheck-finish-checker-process(dafny 3 ("/home/sohum/tmp/flycheck_1fib.dfy") "/home/sohum/tmp/flycheck_1fib.dfy(1,9): Info: decreases n\n/home/sohum/tmp/flycheck_1fib.dfy(4,9): Error: decreases expression must be bounded below by 0\n/home/sohum/tmp/flycheck_1fib.dfy(1,13): Related location\nExecution trace:\n    (0,0): anon0\n    (0,0): anon7_Else\n    (0,0): anon8_Else\n\nDafny program verifier finished with 0 verified, 1 error\n" #[128 "\301\302\300�#\207" [[cl-struct-flycheck-syntax-check #<buffer 1fib.dfy> dafny #<process flycheck-dafny> "/home/sohum/tmp/"] apply flycheck-report-buffer-checker-status] 5 "\n\n(fn &rest ARGS)"] "/home/sohum/tmp/")
  #[0 "\304\300!\211\305=\203��\302\306!\202)�\211\307=\203(�\310\311\300\312\"\313\300!\301\314\300!\302\303&�\202)�\315\207" [#<process flycheck-dafny> ("/home/sohum/tmp/flycheck_1fib.dfy") #[128 "\301\302\300�#\207" [[cl-struct-flycheck-syntax-check #<buffer 1fib.dfy> dafny #<process flycheck-dafny> "/home/sohum/tmp/"] apply flycheck-report-buffer-checker-status] 5 "\n\n(fn &rest ARGS)"] "/home/sohum/tmp/" process-status signal interrupted exit flycheck-finish-checker-process process-get flycheck-checker process-exit-status flycheck-get-output nil] 8 "\n\n(fn)"]()
  funcall(#[0 "\304\300!\211\305=\203��\302\306!\202)�\211\307=\203(�\310\311\300\312\"\313\300!\301\314\300!\302\303&�\202)�\315\207" [#<process flycheck-dafny> ("/home/sohum/tmp/flycheck_1fib.dfy") #[128 "\301\302\300�#\207" [[cl-struct-flycheck-syntax-check #<buffer 1fib.dfy> dafny #<process flycheck-dafny> "/home/sohum/tmp/"] apply flycheck-report-buffer-checker-status] 5 "\n\n(fn &rest ARGS)"] "/home/sohum/tmp/" process-status signal interrupted exit flycheck-finish-checker-process process-get flycheck-checker process-exit-status flycheck-get-output nil] 8 "\n\n(fn)"])
  flycheck-handle-signal(#<process flycheck-dafny> "exited abnormally with code 3\n")

It looks like the structure returned as the warning doesn't include the (flycheck-error-message).

Indentation after datatype declaration

datatype foo = Foo |
  Bar

  lemma hello() {}

dafny-mode seems to not realise that the datatype declaration has completed and wants to indent everything following that extra level. Any ideas?

Strange indentation/whitespace in Boogie mode

Symptom

In the following, ↓ denotes the cursor position and ▯ denotes a space.

Example 1: If I have

procedure foo () {↓

then typing } results in

procedure foo () {}↓▯

Example 2: If I have

procedure foo () {
↓

then typing } results in

procedure foo () {
}↓▯▯▯▯▯▯▯▯▯

Cause

In contrast to Dafny mode (which has dafny-indent-keep-position), Boogie mode does not set a custom indent-line-function. I don't know to which function it actually points to in Boogie mode, but it causes the above behavior in boogie-friends-self-insert-and-indent.

Possible Solutions

1. Move the keybinding for } from boogie-friends.el into dafny-mode.el.
2. Use (a potentially adapted) dafny-indent/dafny-indent-keep-position in Boogie mode. I can't say I understand the code, but in a quick experiment just using these functions in Boogie mode seemed to behave reasonable.

Any advice?

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

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)

inferior-dafny flycheck errors are misplaced when whitespace is edited

When there is an error in the file, adding a line of whitespace above the error causes the flycheck highlighting to incorrectly "move up" (or to incorrectly "stay put", depending on your prospective).

For example, consider the following file.

method Foo() returns (j: int)
  ensures j > 0
{}

When inferior-dafny checks this file, flycheck places an error on the open curly brace and a warning on the greater-than symbol. Now go to the top of the file and add a few newlines. Note that flycheck is now highlighting empty whitespace.

This can be very confusing if you don't realize the highlighting is wrong!

Extract proper filename for flycheck on related locations in refining modules

Example - http://rise4fun.com/Dafny/Ute6

When a error is related to parent module of a refinement, Dafny will output error lines as "X.dfy[Y]: ...",
and current error pattern will interpret the filename as "X.dfy[Y]".

Here is my local fix in .emacs, it also contains a workaround attempt of #8.

(setq old-parse-errors (symbol-function 'inferior-dafny-parse-errors))
;; a workaround for removing [module-name] and dealing with external file locations
(defun inferior-dafny-parse-errors (errors)
(mapc (lambda (e)
        (let ((fname (flycheck-error-filename e)))
          (if (eq fname nil)
              (setq fname buffer-file-name)
            (if (string-match
                 (rx (group (* (not (in "[]")))) (* anything))
                 fname)
                (setq fname (match-string 1 fname)))
            (if (not (string-equal fname buffer-file-name))
                (let ((old-fname (flycheck-error-filename e))
                      (old-msg (flycheck-error-message e))
                      (old-col (flycheck-error-column e))
                      (old-line (flycheck-error-line e)))
                  (setf (flycheck-error-message e)
                        (concat (format "%s(%d:%d)-"
                                        (file-name-nondirectory fname)
                                        old-line
                                        old-col
                                        )
                                old-msg
                                "(" old-fname ")"))
                  (setf (flycheck-error-column e) nil)
                  ;; since line is required ...
                  (setf (flycheck-error-line e) 1)
                  (setq fname buffer-file-name))))
          (setf (flycheck-error-filename e) fname)
          ))
      (funcall old-parse-errors errors)))

forall statement visually looks like forall expression

The emacs mode for Dafny visualizes Dafny's forall keyword in two different ways. For forall expressions (that is, universal quantifications), it visualizes the keyword as an ∀. For forall statements it (mostly) visualizes the keyword as itself (forall). Which one to choose is, I believe, determined by a simple syntactic scan of some things that follow the forall keyword. Here is one case where that simple scan makes the wrong determination, which I think can easily be improved.

When the ensures clause happens on the subsequent line, all is good:

      forall x: int | true
        ensures Ǝ y :: x == y
      {
      }

But when the first line contains a :: (even if there's an ensures in between), then the forall turns into a ∀:

      ∀ x: int | true ensures Ǝ y :: x == y {
      }

It would seem that the syntactic scan could look for an ensures. If it finds an ensures before it finds a ::, then the preceding forall is probably a forall statement.

indentation of case with dafny-mode in emacs

When I write a sequence of case statements, my expectation is that Tab to re-indent dafny code would line up all case occurrences vertically with the same number of space characters from the left of each line. However, each case is lined up with the statements inside of the case above:

method Baz(x:int) returns (y:int)
{
  if {
  case x == 0 =>
    y := 0;
    case 0 < x =>
      y := y + 1;
      case x < 0 =>
        y := y - 1;
  }
}

feature request: scope interactive verification, akin to /proc: on the command-line

I'm working on a large project, with lots of included files and lots of moving parts. When I'm working on a single lemma, I often find I'm more productive by running Dafny on the command line with a suitable /proc: parameter to restrict verification to just the lemma I'm working on, rather than using the flycheck mode. It would be really nice if there was an equivalent to /proc in the Emacs mode, so I could say "just verify this lemma as I work on it, and ignore everything else".

BTW, I guess in theory that DafnyServer's caching should obviate the need for this, but it doesn't because:

• looking up the cache for all the other verification targets still has some non-zero cost, as I can observe in the flycheck progress bar
• the cache is invalidated far too frequently, causing it to go and laboriously reverify the world
• if I change a dependency like part of the spec to try to debug my lemma, I don't want it to go and reverify the world right then and there

Auto-formatting in calc

The automatic formatting that dafny-mode performs does not produce nice results in calc statements. In fact, I find the automatic formatting is working against me, and I constantly have to correct what it's doing. I'd love to see this improved.

Repro:

Start with

lemma L() {
  calc {
  }
}

Then, inside the braces that follow the calc statement, type the following lines in order:

A(x);
==
B(x);
C(x);
==  // here is a comment
D(x);
==  { MyFavoriteLemma(x, y); }
E(x);
{ AnotherLemma(x, y); }
F(x);
<
100;

This produces:

lemma L() {
  calc {
    A(x);
    ==
      B(x);
      C(x);
      ==  // here is a comment
        D(x);
        ==  { MyFavoriteLemma(x, y); }
        E(x);
        { AnotherLemma(x, y); }
        F(x);
        <
          100;
  }
}

but I wish it would instead produce:

lemma L() {
  calc {
    A(x);
  ==
    B(x);
    C(x);
  ==  // here is a comment
    D(x);
  ==  { MyFavoriteLemma(x, y); }
    E(x);
    { AnotherLemma(x, y); }
    F(x);
  <
    100;
  }
}

Debugging inferior-dafny

Thanks for creating this excellent mode!

I am interested in trying the inferior-dafny backend to take advantage of Dafny's caching. But when I enable it, nothing happens. I turned on (inferior-dafny-toggle-debug) and can see that the client is sending messages, but it looks like the server never responds. In fact, while inferior-dafny-live-p returns non-nil, I can find no evidence outside of Emacs that the server is actually running (eg, ps aux | grep -i dafny finds nothing).

I am running OS X and had to patch flycheck-def-executable-var to point to a shell script that runs DafnyServer.exe under mono, similar to the script that runs Dafny.exe. Before I did this, I still got no error message, despite the fact that the executable file it was looking for did not exist.

I am looking for help getting more information about exactly what inferior-dafny is trying to do and why it's not starting the server properly.

flycheck syntax checker doesn't work in Emacs on Mac OS X 10.10, suspicious state from syntax checker dafny

Hello, I got some problem when using the dafny flycheck. I built my dafny-mode in emacs according to README. But when I open a .dfy file I got message like this

But when I checked my dafny flycheck by M-x flycheck-verify-setup, it shows that the Dafny.exe can be found

When I type C-c C-c I got the message like this, it tells me that Dafny.exe can not be found.
And every time I save a .dfy file, the message same as the first picture comes again

mono has been installed in my computer, and I can verify the code in terminal. But how can I do it in emacs?
I don't know what was omitted in my operations.
Appreciate your help ! ! !

Flycheck appears to report success when verification times out

I have a nasty lemma that times out without reporting any specific failures; command-line Dafny gives:

Verifying Impl$$_module.__default.lemma__ARM__L1PTE__Validity ...
  [62.239 s, 67 proof obligations]  timed out
pagedb.i.dfy(227,6): Verification of 'Impl$$_module.__default.lemma__ARM__L1PTE__Validity' timed out after 60 seconds

However, when I open this file in Emacs, I don't see any red squigglies, and the status bar shows only "(Dafny ... FlyC)" as if there were no errors.

Bug: Flycheck & Compilation cannot find .NET Core on Mac OS 11.6

Howdy Boogie-friends,
I really appreciate y'all, and I can live with what I have working and be very grateful for at least the syntax highlighting and other features. But fly-check and compiling internally would be nice...

The problem: Both flycheck and compiling are complaining about discovering .NET Core:

Suspicious state from syntax checker dafny: Flycheck checker dafny returned 1, but its output contained no errors: Error: Dafny requires .NET Core to run on non-Windows systems.

Try installing a more recent version of dafny, and please open a bug report if the issue persists in the latest release.  Thanks!

Suspicious state from syntax checker dafny: Flycheck checker dafny returned 1, but its output contained no errors: Error: Dafny requires .NET Core to run on non-Windows systems.

Try installing a more recent version of dafny, and please open a bug report if the issue persists in the latest release.  Thanks!

Below is a screen shot that best summarizes my state:

• Left Top :: .emacs setup doing everything to find .NET Core and setting up boogie-friends to succeed.

• Left Mid-Top :: Flycheck verification showing dafny working

• Left Mid-Bot :: Error messages from flycheck and compilation

• Left Bottom :: test.dfy buffer

• Right Top :: execution of dafny test.dfy successful. FYI, I am on Dafny 3.2.0.30713

• Right bottom :: execution of quicktest.sh from my dafny source.

I can even compile and test my team's current projects, as long as I am not in emacs.
I will keep track of #23 to see if that resolution de-dupes this. It does not seem likely...

I will say I was confused by the installation directions for Mac OS:

From the README.md/Setup/Automatic/Step 3:

On GNU/Linux or MacOS, use the path to the dafny and dafny-server wrapper scripts for the first two.

Are you sure it is the first two? I had imagined it would be flycheck-dafny-executable and flycheck-inferior-dafny-executable.

That won't solve my problem, but being explicit in the README may prevent other's confusion.

Happy to support in any way. Tony

Move temporary file for current buffer outside current folder

When the buffer is opened the temporary file for flycheck to verify is annoying, especially when you want to do stuff with git. Would it be better to move them to more convenient temporary file provided by mktemp or so?

Could not start checker for Dafny

Hi. I'm trying to set up dafny for Emacs but i'm getting the message

Could not start checker for Dafny: '~/Programs/dafny/' not found. Please fix 'flycheck-dafny-executable'.

I've tried changing the path to '~/Programs/dafny/Dafny.exe' and that doesn't work either, just in case you were wondering.

How do i fix this?

Consider documenting the value of /printTooltips

Thanks for dafny-mode and friends. By accident, I discovered that if I add:

(setq dafny-prover-custom-args '("/printTooltips"))

... to my .emacs, then I get handy tooltips for selected triggers and decreases clauses. Perhaps consider documenting this feature in the README?

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

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.