Russoul/Idris2-Lua

Error: Module Libraries.Data.Bool.Extra not found

I-B-3 opened this issue · 3 comments

I-B-3 commented

Trying to install with Idris 2, v0.3.0, and I get this:

$ make all && make install
idris2 --build idris2-lua.ipkg
1/4: Building LuaCommon (src\LuaCommon.idr)
2/4: Building OrderDefs (src\OrderDefs.idr)
3/4: Building LuaAst (src\LuaAst.idr)
Error: Module Libraries.Data.Bool.Extra not
found

LuaGen:9:1--9:33
 5 |
 6 | import Core.Context
 7 | import Core.Directory
 8 |
 9 | import Libraries.Data.Bool.Extra
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

make: *** [Makefile:36: build/exec/idris2-lua] Error 1

Is Idris2-Lua compatible with v0.3.0?

Russoul commented

Are you using the release build? Probably won’t work, too much has changed internally in Idris 2 since 0.3.0. Please use the version (commit) of Idris 2 mentioned in the README of Idris2-Lua. You can try building against the latest master too, but I can’t guarantee it will work.

I-B-3 commented

I was building against the latest master. Have just tried it with 0.3.0-349308396 but ran into different errors, I don't know if it's worth creating issues for them though as they're because I'm on Windows and I don't know if you expect that to work. I'll close this issue as with the supported version of Idris 2 this wasn't an issue.

Russoul commented

Yeah, I haven't tested it on Windows at all. And don't really plan to.