Debugging inferior-dafny

[boogie-org]

Debugging inferior-dafny

[cpitclaudel]

Hi there (small world),

I'm surprised you had to patch flycheck-def-executable-var. Did you try customizing flycheck-inferior-dafny-executable instead? Are the results the same?

Clément.

[wilcoxjay]

Ah, that's what I get for trying too hard :) It works!

The reason I went down that path is that, uncustomized and unpatched, inferior-dafny hung just as I described above, because there was nothing in my path matching flycheck-def-executable-var, but no error was issued. Would it be possible to report an error in this case? Alternatively, something could be added to the README stating that this customization is necessary on OS X.

Thanks for your help!

[cpitclaudel]

Is it the case that without that tweak, flycheck-verify-setup (C-c ! v) says executable not found? In any case, I could definitely add that line to the README (the ones for the other executables are there, but that one is missing :/).

[wilcoxjay]

Ah, cool! I didn't know about that function. Without the customization, it does indeed report that the executable was not found. But it still seems like an error should be more aggressively reported in this case. Could you run this check programmatically when starting a new instance of the inferior process and loudly report an error if the executable is not found?

[cpitclaudel]

The new instance doesn't start at all if the executable isn't found, actually (flycheck is responsible for starting it, and it doesn't when it can't find the executable). I could try to add extra checks, though.

[wilcoxjay]

Right, obviously the dafny server doesn't start when it can't be found :) But it seems like some code in inferior-dafny.el still runs in that case, because I saw debugging output when I turned it on. What about doing something in inferior-dafny-init to check that the executable exists? I guess at a higher level my question is why doesn't flycheck complain more loudly when asked to start something that it can't find?

[cpitclaudel]

Ah, I see the issue. There is a loud complaint, but the check is for flycheck-dafny-executable, regardless of the backend being used.

[cpitclaudel]

Also, my previous comment above is not exactly true. The server process is started by inferior-dafny using process-start.

[cpitclaudel]

Hmm. I'm actually having trouble reproducing this. When I run this:

(setq-default flycheck-inferior-dafny-executable "nonexistent-binary")

I get this:

Error while checking syntax automatically: (file-error "Searching for program" "No such file or directory" "nonexistent-binary")

[cpitclaudel]

I'm going to move away from inferior-dafny (to LSP), and I'm guessing that after 5 years this issue is resolved ^^