boogie-org/boogie-friends

Tools for interacting with Boogie

boogie-friends's Issues

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).

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?

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.

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;
  }
}

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.

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 ! ! !

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;
  }
}

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.

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.

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?

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?

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

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!

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.

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)

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?

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?

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)))