search

bamboo / idris2-lsp-vscode

Visual Studio Code integration for the Idris 2 language server
MIT License
29 stars 11 forks source link

Source file not in directory "." on every file #3

Open xiaopong opened 3 years ago

xiaopong commented 3 years ago

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

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