Module name does not match file name with Idris2

[michaelmesser]

Module name (name) does not match file name How can I fix this error? idris2 --build main.ipkg --cg javascript works. My source files are in src and the module and file names are the same.

[meraymond2]

Thanks for making an issue, I'm able to reproduce this :+1:

Just to make sure I'm fixing the right problem, are you using version 0.2.1?

I've read through this, and as far as I understand, the IDE process used to find the ipkg file on its own, but now the caller is expected to locate it. If the ipkg isn't manually loaded, it doesn't account for the sourcedir. I'll take a look at it this week.

As a temporary workaround, you can always rename your module to just module Main. I know that's not a proper solution, but it'll make the editor stop complaining until I've got a real fix.

[michaelmesser]

I'm using: Idris 2, version 0.2.1-910711afe

[meraymond2]

This should hopefully be working in the latest version, but please reopen if you still have problems.

One thing to note is that the workspace needs to correspond to the Idris project directory, so it may not work if you open the parent directory of your project.

[michaelmesser]

There seems to be some weirdness with file paths. I noticed this when clicking on an error in the problems pane. I get /path/to/project/path/to/project/src/file.idr and it should be /path/to/project/src/file.idr. The errors don't show up on the file either. Sometimes they show up but I'm not sure when. It seems to works initially but stops after I edit files.

Idris 2, version 0.2.1-910711afe Idris Language v0.0.5 with Idris2 Mode checked

[meraymond2]

The v1 protocol returns absolute file paths for file errors, while the v2 protocol in 0.2.1 has relative file paths. If Idris2 Mode is checked, it prepends the workspace path so that I get a correct file uri — which I need to attach errors to a window.

But your error sounds like it has returned absolute file paths and the extension is over-correcting. I've had a quick skim of the Idris2 code, and it looks like each error is responsible for capturing its own location including filename, which could mean that some errors return absolute file paths and some relative. Or it could be something else.

It occurred to me as I was typing that rather than rely on the Idris2 Mode, it's probably easier just to check whether it's an absolute or relative file path, so that should be a pretty easy fix.

[meraymond2]

Can you try version 0.0.6?

[michaelmesser]

It initially appears to work. I'll let you know if I run into any bugs.

[nothingnesses]

I'm running into this in v0.0.9 of the extension using v0.3.0 of Idris2 (I think commit 299a31de5bd64a584a2f7d9090eb2f5680efaeac). Occurs with or without an .ipkg file.

[meraymond2]

Sorry, I haven't had time to investigate. I'll try to have a look sometime this week.

[brendanzab]

I used the following settings, but it seems like this would only work if I was working on one package at a time:

{
    "idris.idrisPath": "idris2",
    "idris.idris2Mode": true,
    "idris.processArgs": ["--find-ipkg", "--source-dir experiments/idris"]
}