Change convention around `.ipkg` file naming

[alexhumphreys]

Right now the tendency is to name the ipkg file as $package.ipkg. Eg pack, idrall, idris2.

This makes some sense for repos where there's multiple packages, but maybe as a convention we should have a standard name for this file. Random thoughts would be main.ipkg, package.ipkg, idris.ipkg. I'm not too picky on what name is, just that there's a convention so it's a bit easier to know what to type when I want to "edit the .ipkg file".

Having a standard name would also be similar to other languages, eg. package.json for node, requirements.txt for python, cargo.toml in rust. Some of these are serving slightly different purposes than the .ipkg file, but hopefully the idea across.

Should we land on a name then might make sense to change this proposed new command and the idris2 equivalent --init to match.

I'm also not suggesting any fancy automation based on this "standard" name, but just to have a standard name guideline to begin with.

[stefan-hoeck]

I'd like to take this whole thing a bit further, because this is also related to an issue in the todo list: How should we handle multi-ipkg projects in general? For instance, most of my own libraries have an .ipkg file for the library itself, one for the test executable, and probably a third one for typechecking documentation/tutorials/examples. All of them share the same source directory, because this allows for instance the test executables to have access to the modules to be tested without first having to install the library in question.

This setup does not go very well with tools like idris2-lsp or even Idris itself (when starting a REPL with --find-ipkg), because we cannot be explicit about the .ipkg file to use. The question is, how we should go about such project structures in general? I probably should invite the lsp peoply to this discussion, because they might already have agreed on a best practice to do this.

[iacore]

idris2-lsp currently index packages in ~/.idris2/xxxx (I think it's hard coded). It uses similar/same logic as --find-ipkg to get dependencies. Packages have to be installed with install-src for go-to-declaration to work for dependencies.

As for --find-ipkg: https://github.com/idris-lang/Idris2/issues/2524. Need to modify Idris2 to do that

[stefan-hoeck]

idris2-lsp currently index packages in ~/.idris2/xxxx (I think it's hard coded). It uses similar/same logic as --find-ipkg to get dependencies. Packages have to be installed with install-src for go-to-declaration to work for dependencies.

I'm not sure I follow. idris2-lsp uses the same mechanism to look for packages as does Idris itself. If you set the IDRIS2_PACKAGE_PATH correctly, lsp will find the packages installed by pack (Disclaimer: I'm using lsp plus pack daily and it works very well).

[iacore]

Sorry, I was using an old version of lsp and pack. Now that I upgraded both, it works.

Slight problem: pack install-app lsp doesn't create ~/.pack/bin/idris2-lsp. I did it manually with ln -s.

[stefan-hoeck]

Sorry, I was using an old version of lsp and pack. Now that I upgraded both, it works.

Slight problem: pack install-app lsp doesn't create ~/.pack/bin/idris2-lsp. I did it manually with ln -s.

This will not work correctly: idris2-lsp in ~/.pack/bin should be a wrapper script with the package paths set correctly. It could be that you still had a built version of the lsp app in your pack dirs but the wrapper script was missing, so pack though it was already installed. Could you please try the following: Remove the lsp app: pack remove-app lsp and now re-install it and check, whether the wrapper script has now been generated.

[iacore]

remove-app is unknown command... I don't know how to check pack's app version

Edit: I found the problem. Turns out I have two pack versions installed, and they mess with each other's files.

[emdash]

Does it make sense to have a section in pack.toml which enumerates the .ipkg files which belong to the project?

[stefan-hoeck]

Does it make sense to have a section in pack.toml which enumerates the .ipkg files which belong to the project?

I don't think so. Currently, from pack's point of view, a package must have exactly one .ipkg file and this is already specified in the pack.toml files. If you have several .ipkg files, then that's several packages, each of which can be specified in your pack.toml files.

Or maybe I misunderstood your question and you are asking whether it is necessary to specify the .ipkg file at all? In that case the answer is "yes", because in certain situations it makes sense to have several .ipkg files in a directory because they describe different packages/executables which mostly share the same code base. The pack project itself is an example for such a setup.

[stefan-hoeck]

I'm going to close this since it has not seen any activity for several months and it seems the way we currently handle and name .ipkg files seems to work fine for most people. Feel free to reopen, if this requires further action.