Bug: Flycheck & Compilation cannot find .NET Core on Mac OS 11.6

[texastony]

Howdy Boogie-friends, I really appreciate y'all, and I can live with what I have working and be very grateful for at least the syntax highlighting and other features. But fly-check and compiling internally would be nice...

The problem: Both flycheck and compiling are complaining about discovering .NET Core:

Suspicious state from syntax checker dafny: Flycheck checker dafny returned 1, but its output contained no errors: Error: Dafny requires .NET Core to run on non-Windows systems.

Try installing a more recent version of dafny, and please open a bug report if the issue persists in the latest release.  Thanks!

Suspicious state from syntax checker dafny: Flycheck checker dafny returned 1, but its output contained no errors: Error: Dafny requires .NET Core to run on non-Windows systems.

Try installing a more recent version of dafny, and please open a bug report if the issue persists in the latest release.  Thanks!

Below is a screen shot that best summarizes my state:

• Left Top :: .emacs setup doing everything to find .NET Core and setting up boogie-friends to succeed.

• Left Mid-Top :: Flycheck verification showing dafny working

• Left Mid-Bot :: Error messages from flycheck and compilation

• Left Bottom :: test.dfy buffer

• Right Top :: execution of dafny test.dfy successful. FYI, I am on Dafny 3.2.0.30713

• Right bottom :: execution of quicktest.sh from my dafny source.

I can even compile and test my team's current projects, as long as I am not in emacs. I will keep track of #23 to see if that resolution de-dupes this. It does not seem likely...

I will say I was confused by the installation directions for Mac OS:

From the README.md/Setup/Automatic/Step 3:

On GNU/Linux or MacOS, use the path to the dafny and dafny-server wrapper scripts for the first two.

Are you sure it is the first two? I had imagined it would be flycheck-dafny-executable and flycheck-inferior-dafny-executable.

That won't solve my problem, but being explicit in the README may prevent other's confusion.

Happy to support in any way. Tony

[cpitclaudel]

Sorry for the delay. A few questions:

• Which verification backend are you using? Do you have (setq dafny-verification-backend 'server)?
• What do you see when you run C-c ! C-v (aka M-x flycheck-verify-setup)?
• What output do you see if you run C-c ! C-c and select dafny? (aka M-x flycheck-compile)
• Emacs invokes a separate binary, not dafny.exe; could it be that flycheck-inferior-dafny-executable points to a binary that wasn't compiled properly?

[texastony]

Sorry for the delay. A few questions:

You are great, this is open source. Your timing is above and beyond.

Which verification backend are you using? Do you have (setq dafny-verification-backend 'server)?

I know I have tried both. Since flycheck-verify-setup reported the non-server option as healthy, I have stuck with that one. I am using dafny as the backend.

What do you see when you run C-c ! C-v (aka M-x flycheck-verify-setup)?

That dafny-server does not work but that dafny should work.

What output do you see if you run C-c ! C-c and select dafny? (aka M-x flycheck-compile)

That dafny cannot find .NET Core:

Emacs invokes a separate binary, not dafny.exe; could it be that flycheck-inferior-dafny-executable points to a binary that wasn't compiled properly?

No. I can compile test.dfy and other dafny files just fine by using the same executable. But I do not think that boogie-friends (or emacs) is finding the .NET Core library for dafny to work.

Does the .NET Core library need to be on exec-path or another path variable? Which one?

[cpitclaudel]

OK, two more experiments:

1. Use the terminal to run the exact command that M-x flycheck-compile prints, see what that returns
2. Use emacs' built-in terminal (try M-x shell and also M-!) to run the exact command that M-x flycheck-compile prints, see what that returns

Does the .NET Core library need to be on exec-path or another path variable? Which one?

Likely, and no idea. Depending on how you install emacs on macOS things can get very messy. Almost all problems can be solved by exec-path-from-shell, https://github.com/purcell/exec-path-from-shell

[texastony]

OK, two more experiments:

1. Use the terminal to run the exact command that M-x flycheck-compile prints, see what that returns

Everything runs fine.

❯ dafny /compile\:0 /timeLimit:\20 /autoTriggers\:1 /printTooltips  test.dfy

Dafny program verifier finished with 4 verified, 0 errors

2. Use emacs' built-in terminal (try `M-x shell` and also `M-!`)  to run the exact command that `M-x flycheck-compile` prints, see what that returns

That does not work. Error says missing .NET Core:

❯ dafny /compile\:0 /timeLimit:\20 /autoTriggers\:1 /printTooltips  test.dfy
dafny /compile\:0 /timeLimit:\20 /autoTriggers\:1 /printTooltips  test.dfy
Error: Dafny requires .NET Core to run on non-Windows systems.

Does the .NET Core library need to be on exec-path or another path variable? Which one?

Likely, and no idea. Depending on how you install emacs on macOS things can get very messy. Almost all problems can be solved by exec-path-from-shell, https://github.com/purcell/exec-path-from-shell

I have high confidence that this will solve the matter. Will confirm, update, and close if so. Thank you!

[texastony]

Exec-path-from-shell worked like a charm!