v0.9.8 broken on Windows

[dcastro]

As of 0.9.8, vscode-idris no longer works for me in Windows 7 and 10, using the latest version of vscode and idris v1.0.

Auto-completion, build/typecheck-on-save, shortcuts such as case-split, etc.

Also, when I open an Idris project and switch to the Output tab, I get this in the dev tools console.

ENOENT: no such file or directory, open 'C:\Program Files (x86)\Microsoft VS Code\extension-output-#4': Error: ENOENT: no such file or directory, open 'C:\Program Files (x86)\Microsoft VS Code\extension-output-#4' at Object.fs.openSync (fs.js:558:18) at Object.module.(anonymous function) [as openSync] (ELECTRON_ASAR.js:173:20) at Object.fs.readFileSync (fs.js:468:33) at Object.fs.readFileSync (ELECTRON_ASAR.js:506:29) at Object.getIdents (C:\Users\dcastro.vscode\extensions\zjhmale.idris-0.9.8\out\analysis\common.js:116:20) at Maybe.of.map (C:\Users\dcastro.vscode\extensions\zjhmale.idris-0.9.8\out\providers\ipkg\completionProvider.js:11:24) at module.exports.Maybe.map (C:\Users\dcastro.vscode\extensions\zjhmale.idris-0.9.8\out\maybe.js:19:19) at Object.buildCompletionList (C:\Users\dcastro.vscode\extensions\zjhmale.idris-0.9.8\out\providers\ipkg\completionProvider.js:9:44) at context.subscriptions.push.vscode.window.onDidChangeActiveTextEditor (C:\Users\dcastro.vscode\extensions\zjhmale.idris-0.9.8\out\extension.js:63:20) at e.invoke (c:\Program Files (x86)\Microsoft VS Code\resources\app\out\vs\workbench\node\extensionHostProcess.js:23:14715) at e.fire (c:\Program Files (x86)\Microsoft VS Code\resources\app\out\vs\workbench\node\extensionHostProcess.js:23:53565) at c:\Program Files (x86)\Microsoft VS Code\resources\app\out\vs\workbench\node\extensionHostProcess.js:23:390025 at e.invoke (c:\Program Files (x86)\Microsoft VS Code\resources\app\out\vs\workbench\node\extensionHostProcess.js:23:14715) at e.fire (c:\Program Files (x86)\Microsoft VS Code\resources\app\out\vs\workbench\node\extensionHostProcess.js:23:53565) at t.$acceptDocumentsAndEditorsDelta (c:\Program Files (x86)\Microsoft VS Code\resources\app\out\vs\workbench\node\extensionHostProcess.js:23:346353) at t.e.handle (c:\Program Files (x86)\Microsoft VS Code\resources\app\out\vs\workbench\node\extensionHostProcess.js:23:312304) at s (c:\Program Files (x86)\Microsoft VS Code\resources\app\out\vs\workbench\node\extensionHostProcess.js:23:176531) at h (c:\Program Files (x86)\Microsoft VS Code\resources\app\out\vs\workbench\node\extensionHostProcess.js:23:177208) at _combinedTickCallback (internal/process/next_tick.js:67:7) at process._tickCallback (internal/process/next_tick.js:98:9)

I don't get this error in non-idris projects.

An entry for "idris" seems to also be missing from the list of outputs:

Manually download and reverting back to 0.9.3 and 0.9.6 seems to work fine.

[zjhmale]

@dcastro Thanks for the reporting, I think the potential reason is the fake maybe monad here https://github.com/zjhmale/vscode-idris/blob/master/src/maybe.js. I will address this ASAP.

[be5invis]

@dcastro What is "the last version of vscode" exactly? Could you please provide a file that causes the error?

[zjhmale]

Yes, providing a sample file which causes the error will help us a lot to indicate the issue.

[dcastro]

@be5invis Well, I've updated vscode to 1.13.0 this morning, but it hasn't been working for a couple of days now.

This happens with any file, really. I just created a brand new folder, with the default main module, and I'm getting this issue.

[zjhmale]

Hi @be5invis, do you got the same issue on Windows10 with v0.9.8?

[be5invis]

@zjhmale I can reproduce the latter one. However typechecking or hover is usable on my PC.

[munael]

Nothing works at all here on Windows 8.1 and VS Code 1.15.

The menu exists and the Idris output window exists but no matter the command it's always stuck "Loading...".

[zjhmale]

Hi @dcastro, I can reproduce the same error message on Windows, but just for the newly created Idris files, v0.9.8 should work well with already opened files.

[zjhmale]

@Enamex I can work with Windows10 and VSCode 1.14.2

It will be really helpful if you provide some screenshot for me to see your scenario more clearly.

[munael]

@zjhmale commented on Jul 31, 2017, 7:10 PM GMT+2:

@Enamex I can work with Windows10 and VSCode 1.14.2

[gif snip]

It will be really helpful if you provide some screenshot for me to see your scenario more clearly.

I'm not sure what to screenshot (and can't take gifs) but in summary: exactly what you're doing in the gif except for me the Loading... never changes.

Update: I got it to work. It appears that the idris path doesn't work if it's from the $PATH or otherwise so long as it is a symlink. Further, now that several functionalities I've tested work, I'd tried something I'm not sure what and it gave me an error:

[Error] Invalid option for idris.hoveMode                               [Close]

Update 2: The error occurred when displaying tooltips as I hovered over words. I'd set the tooltip config to "none" (had been trying random things to get the extension to work); reverting it makes the tooltips work with no errors.

So as far as I know the only real issue now is that it doesn't recognize symlinks on Windows (made with mklink).

[ErikSchierboom]

@Enamex I also have the "Loading..." problem. I tried to fix this by setting the Idris executable path to the full path: "idris.executablePath": "C:\\Users\\erikschierboom\\Bin\\idris\\idris". Unfortunately, this does not work for me. Is there anything more I have to do?

[munael]

@ErikSchierboom commented on Aug 3, 2017, 11:50 AM GMT+2:

@Enamex I also have the "Loading..." problem. I tried to fix this by setting the Idris executable path to the full path: "idris.executablePath": "C:\\Users\\erikschierboom\\Bin\\idris\\idris". Unfortunately, this does not work for me. Is there anything more I have to do?

Just to be sure you have the right path: go to the executable and right click it while holding Shift, then choose "Copy as path" and use that. Make sure it has the extension .exe in the end.

Also Update 3: Not sure whether this's the extension's fault (probably not) but the issue is that it's trying to call idris from cmd.exe no matter what default shell I'd configured in VS Code (MSYS2 in my case).

[ErikSchierboom]

@Enamex I've tried that but unfortunately I still have the "Loading..." message. As for the terminal, I only have one terminal installed (cmd.exe) and I can successfully run idris or idrin from VS Code's terminal.

[zjhmale]

@ErikSchierboom Hmm, really wired.

1. Pls check can you run idris executable in the terminal with its explicit path, I mean C:\\Users\\erikschierboom\\Bin\\idris\\idris, since on OSX and Linux you can run an executable with its full path, but I don't know whether it is legal on Windows.
2. You can run idris directly from the terminal, so you have already added idris executable path to Windows $PATH right?

[ErikSchierboom]

@zjhmale The answer to both questions is: yes. I'll see if I can find anything else being wrong.

[magnus-madsen]

I have the same issue. Windows 10. Idris 1.1.1. Visual Code 1.16.

Interestingly, selecting "Start or refresh Idris repl" works. Everything else seems to not work.

I can run idris from the command line.

I noticed Windows has both environment variables at the user and system level. I tried setting the path to include idris in both, but no luck.

Output shows: Errors (0)

[magnus-madsen]

I had the files store on my desktop, which has the path: \\MyDomain\Users\MyUserName\Desktop\idris

Notice this is a domain path. I moved my idris file to C:\tmp\ and then it works.

[mrakgr]

I encountered this error when I made a file named IO.idr in the project. Removing it fixed the issue for me.