using inigo build

[bbarker]

Hi,

Just trying out inigo and ran into an issue on a new project with the build command:

$ inigo build
1/1: Building idris-concur-core (idris-concur-core.idr)
idris-concur-core.idr:1:13--1:13:Parse error: Couldn't parse declaration (next tokens: [symbol -, identifier concur, symbol -, identifier core, identifier main, symbol :, identifier IO, symbol (, symbol ), identifier main])

I'll admit I haven't looked into this much yet, but I uploaded the generated files and empty project (except for what GitHub and inigo initialized) here (commit link for posterity).

[hayesgm]

Thanks, I'll take a look.

[hayesgm]

Got it. I think Idris will only allow packages to be named "MyPackageName" and so currently this is saying module idris-concur-core. We should add more checks in Inigo and/or let people specify casual names. I can make a PR to convert this to IdrisConcurCore if you'd like!

[bbarker]

Great, no worries, I decided to just rename it ConcurCore. Thanks!

On Sun, Sep 20, 2020 at 9:16 PM Geoff Hayes notifications@github.com wrote:

Got it. I think Idris will only allow packages to be named "MyPackageName" and so currently this is saying module idris-concur-core. We should add more checks in Inigo and/or let people specify casual names. I can make a PR to convert this to IdrisConcurCore if you'd like!

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/hayesgm/inigo/issues/2#issuecomment-695864225, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAG7XDX4SZIJUEPPVNSR3KTSG2SONANCNFSM4RT35EJA .

-- Brandon Barker brandon.barker@gmail.com

[hayesgm]

Cool, feel free to raise issues for any future problems. I'll create a separate ticket to address valid naming conventions.