You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
There is exectly the same error when you try to use idris Main.idr, idris Foo.idr, idris Bar.idr in command line (first two cases are ok, but the last one is complaining about import), but in this case it is expected behavior, since Idris (sadly) doesn't know anything about project root. The workaround is pretty simple: idris Bar.idr -i ../../
I think there could be two options of how to fix it:
In settings add an option specifying a project root
Use a convention that .ipkg file should be placed in a root directory and then search for it (I like this one better)
and then add -i root_dir to compiler options when calling Idris.
I'm not sure that I understand correctly how this plugin works, but I hope my suggestion is a good way to fix this bug. It's really annoying to have all this cool features and not being able to use them.
I use Windows 10, Idris 1.1.1, Atom 1.23.1 and atom-language-idris 0.4.10.
The text was updated successfully, but these errors were encountered:
This error happens when there is an import from a parent folder. Let's say that we have a little project:
src\main.ipkg
src\Main.idr
src\Foo\Foo.idr
src\Foo\Bar\Bar.idr
and we use
Ctrl+Alt+A
onbaz1
,baz2
andbaz3
. In case ofbaz1
andbaz2
everything works as expected, butbaz3
throws an error:When you use
Ctrl+Alt+A
onbaz1
,baz2
andbaz3
, developer tools console prints something like this:There is exectly the same error when you try to use
idris Main.idr
,idris Foo.idr
,idris Bar.idr
in command line (first two cases are ok, but the last one is complaining about import), but in this case it is expected behavior, since Idris (sadly) doesn't know anything about project root. The workaround is pretty simple:idris Bar.idr -i ../../
I think there could be two options of how to fix it:
.ipkg
file should be placed in a root directory and then search for it (I like this one better)and then add
-i root_dir
to compiler options when calling Idris.I'm not sure that I understand correctly how this plugin works, but I hope my suggestion is a good way to fix this bug. It's really annoying to have all this cool features and not being able to use them.
I use
Windows 10
,Idris 1.1.1
,Atom 1.23.1
andatom-language-idris 0.4.10
.The text was updated successfully, but these errors were encountered: