Cannot run extension on Windows

[Pzixel]

I followed the instruction as it says: i've installed extension, idris, idrin, then restarted my shell processes, restarted VSCode but I get no autocompletion. It only says "Didn't load filename" and that's all.

I'm not sure what to do or what additional information I could provide.

[ninjazoete]

same here ;/

but I am on OSX

[malte-v]

Same issue on Linux.

[ChessMax]

I have the same problem either on Windows((

[raptazure]

That should be caused by type checking error. Hovering on anything or using idris repl to get the error message, fix it and this will go away.

[Pzixel]

1. no, it's not related to error
2. autocomplete should work when code doesn't compile otherwise it's useless. You started typing something and expect it to suggest some items, but atm code doesn't compile, you have some fooBa name which is not complete therefore is not a valid idris code.

[raptazure]

1. no, it's not related to error

2. autocomplete should work when code doesn't compile otherwise it's useless. You started typing something and expect it to suggest some items, but atm code doesn't compile, you have some `fooBa` name which is not complete therefore is not a valid idris code.

Mine (didn't load message) is caused by type error... Every time after fixing the bad code, it just goes away and loads successfully...

[RaoulSchaffranek]

Hi,

I had the same error. In my case, the ipkg-filename had a typo (it ended on .ipgk rather than on .ipkg).
After fixing the typo, I ran idris --checkpkg .\MyPackage.ipkg to make sure that Idris can read my package-file.
I then ran idris --clean .\MyPackage.ipkg (just in case).
After restarting VSCode, the annoying error-message was gone and the extension was working again.

Hope, it helps someone out there with the same problem.