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

[TalentSSS]

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

[texastony]

Can you do us a favor? Could you save that buffer, and try to run Dafny on the file with the same executable?

That would be something like dafny main.dfy.

I could be wrong, but my dafny path does not include an .exe on Mac OS 11.6. Most of the time, if there is an .exe on my path on my mac, it's because I did something wrong. How did you install dafny? Can you run dafny's quicktest.sh?

Did you notice the note after step 3 of the Automatic Setup? They are asking Mac OS users to use the wrapper scripts.

[cpitclaudel]

Sorry that I didn't reply quickly to this question. For future visitors, my guess is that this is a configuration issue, trying to invoke Dafny.exe directly instead of through the macOS wrapper script.