You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently we ship 3 .ipkg files with the compiler:
idris2api.ipkg: using the compiler as a library, e.g., as used by the LSP server and katla.
idris2.ipkg: the idris2 executable
ipkg/idris2protocols.ipkg: a standalone library exporting the various protocols (IDE, S-exp, hexadecimal serialisation).
Various tools (notably the LSP server and idris2 --find-ipkg) get confused if the top level directory contains more than one .ipkg file.
That's why we've placed the idris2protocols.ipkg under a sub-directory.
The two idris2api.ipkg and idris2.ipkg don't cause a problem for LSP because one depends on the other so building one will build the other and LSP needs the depended-on package idris2api.ipkg.
This doesn't seem like a robust design.
At the moment, tools like pack can be told (e.g., through a pack.toml configuration file) where the correct .ipkg file ought to be, to resolve ambiguity.
There was some discussion to check whether LSP can be similarly told where to find the .ipkg file to resolve any ambiguity.
Alternatively, we can decree there can be only one .ipkg file upstream from the source-code and other .ipkg files should stay under subdirectory. In that case, we may want to move idris2api.ipkg to the ipkg directory so that only idris2.ipkg is in the top-level directory.
Maybe there are other options --- please discuss below.
As either option would be breaking existing projects, we ought to discuss it publicly (so here, on github) and over time (at least until the next IDM?).
Summary: Current options
keep multiple .ipkg files at the top level, following a period of adjustment to allow projects like LSP to adapt to the change.
keep one .ipkg file at the top level, moving all other .ipkg files to the ipkg subdirectory, following a period of adjustment to allow projects like LSP and katla to adjust.
The text was updated successfully, but these errors were encountered:
Personally, I'm in favor of avoiding disambiguities and allowing only one .ipkg file upstream from the source code. I think I so far have not come upon a use case where you really need to have several .ipkg files in one directory but maybe other people have.
Context
Currently we ship 3
.ipkg
files with the compiler:idris2api.ipkg
: using the compiler as a library, e.g., as used by the LSP server and katla.idris2.ipkg
: the idris2 executableipkg/idris2protocols.ipkg
: a standalone library exporting the various protocols (IDE, S-exp, hexadecimal serialisation).Various tools (notably the LSP server and
idris2 --find-ipkg
) get confused if the top level directory contains more than one.ipkg
file.That's why we've placed the
idris2protocols.ipkg
under a sub-directory.The two
idris2api.ipkg
andidris2.ipkg
don't cause a problem for LSP because one depends on the other so building one will build the other and LSP needs the depended-on packageidris2api.ipkg
.This doesn't seem like a robust design.
At the moment, tools like
pack
can be told (e.g., through apack.toml
configuration file) where the correct.ipkg
file ought to be, to resolve ambiguity.There was some discussion to check whether LSP can be similarly told where to find the
.ipkg
file to resolve any ambiguity.Alternatively, we can decree there can be only one
.ipkg
file upstream from the source-code and other.ipkg
files should stay under subdirectory. In that case, we may want to moveidris2api.ipkg
to theipkg
directory so that onlyidris2.ipkg
is in the top-level directory.Maybe there are other options --- please discuss below.
As either option would be breaking existing projects, we ought to discuss it publicly (so here, on github) and over time (at least until the next IDM?).
Summary: Current options
.ipkg
files at the top level, following a period of adjustment to allow projects like LSP to adapt to the change..ipkg
file at the top level, moving all other.ipkg
files to theipkg
subdirectory, following a period of adjustment to allow projects like LSP and katla to adjust.The text was updated successfully, but these errors were encountered: