Source file not in directory "." on every file

[xiaopong]

It just reports error

Error: Source file "/path/to/source/file.idr" is not in the source directory "." Idris2 [1, 1]

on all .idr files that compile perfectly fine.

New to Idris and not a vscode extension programmer, so just taking a guess here: the source file path should be relative instead of an absolute file path?

Environment:
Idris 2, version 0.4.0-f77670814
with latest idris2-lsp.

[chespinoza]

Hi @xiaopong, it's an issue due to a missing local ipkg file, in order to create it just run idris2 --init in the folder where you have your files and enter the package name:

➜  idris2-stuff idris2 --init

Package name: my-package
Package authors:
Package options:
Source directory:

After that open your file again, that should sort the problem out.
Here you can read more about packages: https://idris2.readthedocs.io/en/latest/reference/packages.html