A problem with Dafny in VSC

[AndrzejBlikle]

Dear All,
I recently came across Dafny and decided to learn more about it. I bought Rustan's "Program Proofs" book and installed VSC with a Dafny extension. Here, my problem starts since this extension's only functionality is the program code edition. If I try to run or debug a program, I am informed that Dafny does not have such an extension. Then VSC kindly offered me the opportunity to search for an extension on the market, but if I asked, it came back immediately with a message that there was no such extension on the market.
Could you help me in any way? I am not seeking necessarily for a free extension, but any extension.
Andrzej Blikle (Polish Academy of Sciences)
[email protected]

[atomb]

The Dafny extension for VSC doesn't deeply integrate with the normal mechanisms for running and debugging programs, but does provided basic functionality for it. The "Dafny: Run" (usually bound to F5) and "Dafny: Test" commands should do what you want. Both are available from the command palette or the right-click context menu.

[AndrzejBlikle]

I must be doing something wrong since it does not work as you say. In the Dafny window of my VSC, I have the following program:

method fib(i: int) returns (result: int)
{
result := if i <= 1 then 1 else fib(i-1) + fib(i-2);
}

method Main()
{
var res := fib(5);
print res;
}

I can neither run it nor debug it if I replace fib(5) with fib("5"). What is wrong with my installation?

[keyboardDrummer]

I can neither run it nor debug it if I replace fib(5) with fib("5")

What method of trying to run or debugging it are you using? You can always fall back to invoking Dafny on the command line. Once you have dafny on your path, then dafny run <file> should do the trick.

[AndrzejBlikle]

I am trying to run it from my VSC Dafny extension. The options Run and Test are there, but they are inactive.