search

idris-community / idris2-lsp

Language Server for Idris2
BSD 3-Clause "New" or "Revised" License
160 stars 32 forks source link

getting error when creating my first file #78

Closed rambip closed 3 years ago

rambip commented 3 years ago

after installing the idris2 lsp here, I used the neovim configuration and tried to get started.

I created an empty test.idr, but when I save it I immediatly get an error: Error: Source file "/home/rambi/test.idr" is not in the source directory "."

How do I have to understand this error ? Is there a project layout I have to follow to be able to use the lsp ?

michaelmesser commented 3 years ago

Do you have a .ipkg?

rambip commented 3 years ago

I didn't have one, and I think I figured out how to use it. I just wanted to play with the language server, so I used a standalone file.

It would be nice if it were written in the docuentation that you need a .ipkg, and how to do otherwise.

ShinKage commented 3 years ago

The first note in the README specifies that a .ipkg is mandatory. I will add a note also in the configuration snippet.

rambip commented 3 years ago

Is there a link to the documentation for the .ipkg file ?

It would be nice to have an example foo.ipkg file just to understand the ise of it

ShinKage commented 3 years ago

There is a brief introduction in the tutorial https://idris2.readthedocs.io/en/latest/tutorial/packages.html. And the proper documentation for the format https://idris2.readthedocs.io/en/latest/reference/packages.html. If you need to quickly and interactively setup an ipkg you can use the command idris2 --init.