Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Module needs reloading on any command #93

Open
nilp0inter opened this issue Oct 12, 2019 · 1 comment
Open

Module needs reloading on any command #93

nilp0inter opened this issue Oct 12, 2019 · 1 comment

Comments

@nilp0inter
Copy link

nilp0inter commented Oct 12, 2019

Hi,

I am new to Idris and idris-vim. I am trying to test the functionality provided by the plugin like show type an case split. When I try it in a fresh open file it works perfectly, but after I made any change to the code all commands result in this message:

"hello.idr" 4L, 50C written

Loading /home/nil/hello.ibc failed: Module needs reloading:
        SRC : "/home/nil/hello.idr"
        Modified at: 2019-10-12 10:55:16.873346829 UTC
        IBC : "/home/nil/hello.ibc"
        Modified at: 2019-10-12 10:53:44.870012464 UTC


Loading /home/nil/hello.ibc failed: Module needs reloading:
        SRC : "/home/nil/hello.idr"
        Modified at: 2019-10-12 10:55:16.873346829 UTC
        IBC : "/home/nil/hello.ibc"
        Modified at: 2019-10-12 10:53:44.870012464 UTC

I tried reloading the file with <LocalLeader>r, but the same message appears.

The only solution I found is close vim and REPL, remove the .idc file and open everything again.

I am missing something or is this a bug?

My Idris version is Version 1.3.2-git:PRE, btw.

Thank you!

@austinChesnut
Copy link

Is your working file short? I am getting the same error but only on smaller files. I'm thinking there might be a timing error in the Idris REPL as I also get the same error when I reload from the REPL some times. I just want to see if we have the same error.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants