search

idris-hackers / idris-vim

Idris mode for vim
221 stars 52 forks source link

Module needs reloading on any command #93

Open nilp0inter opened 4 years ago

nilp0inter commented 4 years ago

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 commented 4 years ago

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.