Dealing with multiple .ipkg files

[ohad]

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 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.

[stefan-hoeck]

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.