Running JavaScript does not output anything

[MikaelMayer]

Here is the setting

It puts the following command on my command line:

> & "C:\Program Files\dotnet\dotnet.EXE" "...\Dafny.dll" "...\issue-vscode.dfy" /verifyAllModules /compile:3 /compileTarget:js
Dafny program verifier finished with 0 verified, 0 errors
Wrote textual form of target program to issue-vscode.js
Running...

>

So nothing is output. However, when I add /spillTargetCode:1 it display a javascript file that, when I execute it using node, correctly outputs:

and that works also on PowerShell.
I'm not sure what's going on here.

[camrein]

The run feature is currently provided by the Dafny compiler itself. Therefore, if the compiler doesn't implement run for a specific target, so doesn't the IDE.
We could think about implementing the compile & run feature independently from the compiler. I think this change would make sense anyways because the C# implementation loads the generated assembly. That's ok from compiler perspective as the process stops right after. However, the language server stays alive and keeps loading more and more code. At this time, there's no possibility to unload code from C#; thus, we have in fact a memory leak there.

[keyboardDrummer]

The run feature is currently provided by the Dafny compiler itself. Therefore, if the compiler doesn't implement run for a specific target, so doesn't the IDE. We could think about implementing the compile & run feature independently from the compiler. I think this change would make sense anyways because the C# implementation loads the generated assembly. That's ok from compiler perspective as the process stops right after. However, the language server stays alive and keeps loading more and more code. At this time, there's no possibility to unload code from C#; thus, we have in fact a memory leak there.

We could think about implementing the compile & run feature independently from the compiler.

What do you mean by that? It seems good to me to run the user C# program in a different process than the compiler, but the code organisation doesn't have to change for that.

[MikaelMayer]

I fixed it here: dafny-lang/dafny#1824
Indeed, it was a problem on the Dafny side, not the IDE-VSCode

[camrein]

What do you mean by that? It seems good to me to run the user C# program in a different process than the compiler, but the code organisation doesn't have to change for that.

Sorry, I forgot that I changed this behavior long ago. If I remember correctly, the original VSCode extension that used DafnyServer used a custom LSP API to implement compile & run. Due to the problematic with unfreed code I changed that to the way we have now: Run a command in the terminal that invokes the Dafny compiler. This both solved the issue with the unfreed code as well as allowed Dafny users use two distinct compilations for the language server and compiler.

However, what I meant with compile & run indepedently from the compiler: Fire one command to compile the program, another command to execute it. However, if Dafny's /compile:3 switch is meant to work for any compilation target, we should stick to this implementation.