Could not start checker for Dafny

[BunnyFiscuit]

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?

[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! :)