How to configure packages?

[DejanMilicic]

I am able to compile module with

> idris2 -p contrib Main.idr

but inside of the editor itself, I have an error

I attempted to include contrib into the path but it does not help

[meraymond2]

Hey, thanks for making an issue, I'm able to reproduce this.

I attempted to include contrib into the path but it does not help.

Yeah, the process args are passed to the command separately, so that wouldn't work.

In its current form, the only way to pass packages to the extension is with an .ipkg file. I can also add an option to the extension config that would take a list of packages and pass them to the process, Or maybe just a list of flags.

In the meantime, adding a minimal ipkg file should get it working.

package main
version = 0.0.1

depends = contrib

[DejanMilicic]

Thank you, this helped. Error is gone.
I think you can leave it as it is in this form.
In the meantime, in the search for a solution, I learned that ipkg is not only for "exporting" functions but also for specifying dependencies, etc. In other words, I found out that this is more or less equivalent of "proj" files in other programming languages.

The only thing that confuses me at the moment is that Idris2 compiler is not taking dependencies from ipkg when compiling, so I still need to pass "-p contrib". But this is beyond the scope of this project and is also something that will improve over time with tooling improvements.

Anyway, I think you should leave it as it is now, but document this.
I can create PR for README if you wish

[meraymond2]

Idris2 compiler is not taking dependencies from ipkg when compiling

Depending on your directory structure, I think you might need to pass the --find-ipkg flag.

[DejanMilicic]

--find-ipkg

this option does the job, thanx!

[meraymond2]

#82

[brendanzab]

I’ve found that extension struggles in nested directories, and does not seem to respect Idris 2 package’s sourcedir and builddir fields. To workaround this, you can use the following settings (an iteration on what I posted here #12 (comment)):

{
    "idris.idrisPath": "idris2",
    "idris.idris2Mode": true,
    "idris.processArgs": [
        "--find-ipkg",
        "--source-dir path/to/package/sourcedir",
        "--build-dir path/to/package/builddir",
    ],
}

This seemed to fix it, at when only one package is involved (I imagine multi-package use cases would struggle).

It’s most likely a bit much to ask for a fix at this point (there seems to ongoing work on an idris-lsp?), but in lieu of those being easy to install it’s been great to have this package in spite of needing some workarounds. It’s also really nice that you can just goof around in single files as well. Thanks @meraymond2 for the hard work and the cool extension!

[michaelmesser]

idris2-lsp can be easily installed with pack. https://github.com/idris-community/idris2-lsp#installation-with-pack

[brendanzab]

Oh, I didn't realise pack was an Idris thing! Thought it was some linux package manager. Do you know if there’s a good workflow at all with using NixPkgs?

[michaelmesser]

Someone tried to get Idris2 to work with Nix, but it hasn't been updated since January. https://github.com/claymager/idris2-pkgs

[meraymond2]

I’ve found that extension struggles in nested directories, and does not seem to respect Idris 2 package’s

Is this still an issue, and if so, do you have an example? It's not clear to me whether this is an issue with the extension or with Idris2’s --find-ipkg option.

It’s most likely a bit much to ask for a fix at this point

I haven't had much time for this, so I recognise that changes happen pretty slowly. While most of the development on Idris 2 tooling is happening on the language server, I'll try to keep this working for Idris 2 as long as the ide-protocol is still supported.