Could not start checker for Dafny

[boogie-org]

Could not start checker for Dafny

[cpitclaudel]

What error do you get for ~/Programs/dafny/Dafny.exe?

[BunnyFiscuit]

There's no error until i write a small program and do C-c C-c
Then it says

Prover dafny is improperly configured

Edit: ah misread, i get the same error for that

[cpitclaudel]

Hmm. Does the file ~/Programs/dafny/Dafny.exe actually exist? What happens if you run M-: ~/Programs/dafny/Dafny.exe /??

[BunnyFiscuit]

I'm sorry, I don't know how to run that code. Are you missing an 'x' for M-x ?
Do i run this in emacs or on the terminal?
I run Debian GNU/Linux 8 (jessie) btw.

[cpitclaudel]

I mean to run M-: (that is alt-shift-colon), then type ~/Programs/dafny/Dafny.exe /?, then press RET (in Emacs)

[BunnyFiscuit]

Hi, sorry for late reply.
I get

Trailing garbage following expression

The file exists as i can open up my terminal and see it (see attached image)

[cpitclaudel]

Ah, sorry I got confused between M-: and M-! :/

Can you open a Dafny file and run M-x flycheck-verify-setup RET? This should pop up a Flycheck checkers buffer, the contents of which will be very useful for debugging.

Thanks!

[bkragl]

@BunnyFiscuit: your ls output indicates that your Dafny.exe is not marked as executable.
Try chmod +x ~/Programs/dafny/Dafny.exe.

[BunnyFiscuit]

@bkragl I think that did the trick, as i don't get an error message at startup anymore. However i'm not sure if when i do C-c C-c that it verifies the program. This is what it tells me:

-- mode: compilation; default-directory: "~/programming/tdv/LAB2/" --
Compilation started at Mon Dec 5 13:01:23

~/Programs/dafny/Dafny.exe /compile:0 /nologo /home/bunnyfiscuit/programming/tdv/LAB2/LimitedStack.dfy
/bin/bash: ~/Programs/dafny/Dafny.exe: No such file or directory

Compilation exited abnormally with code 127 at Mon Dec 5 13:01:23

@cpitclaudel This is what the debugger says:

Syntax checkers for buffer LimitedStack.dfy in dafny-mode:

dafny
- may enable: yes
- predicate: t
- executable: Found at /home/bunnyfiscuit/Programs/dafny/Dafny.exe

dafny-server
- may enable: yes
- predicate: nil
- executable: not found
- self-test: failed

Flycheck Mode is enabled. Use C-u C-c ! x to enable disabled
checkers.

---

Flycheck version: 31snapshot (package: 20161117.144)
Emacs version: 24.4.1
System: x86_64-pc-linux-gnu
Window system: x

[cpitclaudel]

@BunnyFiscuit Flycheck suggests that everything is fine, so at least real-time checking should work now. Can you try changing to an absolute path, and see if that fixes C-c C-c as well?

[BunnyFiscuit]

yes that seems to do the trick! Thank you! :)

[cpitclaudel]

Great, sorry for the long back-and-forth!

[BunnyFiscuit]

haha nah, i appreciate you getting back to me so quickly! :)