No syntax errors when using Dafny server

[boogie-org]

No syntax errors when using Dafny server

[cpitclaudel]

Hi,

Thanks for the bug report! Do you have a small example of problematic code? I'm having trouble repducing the issue (for example, I'm not seeing this with the following code; I do get an error on the :=)

method A(x: int) returns (y: int) {
  y := true;
}

[ningit]

Hi,

I'm not getting an error on the := with your example.

I can only see the error when (setq dafny-verification-backend 'server) is commented in init.el:

(require 'package)
(add-to-list 'package-archives
    '("melpa" . "https://melpa.org/packages/"))
(package-initialize)

(setq dafny-verification-backend 'server)
(setq flycheck-dafny-executable "dafny")
(setq flycheck-inferior-dafny-executable "dafny-server")

However it seems that dafny-server works because when I add (setq inferior-dafny--debug t) the following appears in the Messages buffer:

[inferior-dafny-filter-live] [/tmp/example.dfy(2,3): Error: RHS (of type bool) not assignable to LHS (of type int)
^[[37mVerification completed successfully!
[SUCCESS] [[DAFNY-SERVER: EOM]]

[cpitclaudel]

Hey there,

Which platform are you using this on? GNU/Linux, or Windows? If Windows, which Emacs are you using? Cygwin?

That ^[[37m in the message looks suspicious.

Clément.

[ningit]

Yes, ^[[37m is suspicious. I should have guessed. It's an ANSI escape code to reset the foreground color back to white after setting it to red to print the error message. The problem seems to be that dafny-server is producing colored output, and the terminal control codes appear in what Emacs reads.

I'm using GNU/Linux Ubuntu and Emacs 24.5 with GTK (from the official repository).

I have carried out some experiments:

1. If I run dafny-server manually at the command line (with the base64 message and all that), the output is colored as if I were using the command line interface.
2. Mono checks whether the output channel is interactive (~isatty) and doesn't write control codes for colors when it is not. In cli mode it's likely the case.
3. In server mode, when called, dafny-server's standard output is interactive (isatty returns true).
4. When using server mode and C-c C-c dafny is called with custom environment variables. One of them is TERM=dumb. When dafny-server is called automatically, there is TERM=xterm-256color instead, the default.

Conclusion: invoking Emacs with TERM=dumb emacs example.dfy solves the problem rudimentaryly. But what I have written in 1 or 3 are unwanted facts, aren't they?

[cpitclaudel]

Sorry for the delay. I can reproduce this when I start Emacs in command line mode with term set to xterm-256color. The details are here. I think number 1 is generally fine; if you pipe into cat, for example, you'll get no colors. 3 is an issue, which I'll fix ASAP :)

[cpitclaudel]

Should be fixed :) Thanks for the report. The issue was that Emacs was using a TTY to talk to dafny-server, instead of a pipe.

[ningit]

Thanks :). I have tried the fixed mode and it works fine.

[cpitclaudel]

Wonderful, thanks so much for the report!