Improve error messages around usage of depends folder

[andrevidela]

Steps to Reproduce

setup a project like this:

├── depends
│   └── dep-0
│       ├── dep.ipkg
│       └── src
│           └── Dep.idr
├── main.ipkg
└── src
    └── Main.idr

With main.ipkg containing:

package main
depends = dep 

sourcedir = "src"

and dep.ipkg containing:

package dep
version = 0

modules = Dep

sourcedir = "src"

Main.idr:

module Main
import Dep

main : IO ()
main = putStrLn str

Dep.idr:

module Dep
str : String
str = "hello"

Expected Behavior

Compiling main with idris2 --build main.ipkg should work.

Observed Behavior

Uncaught error: "Depends/depends/dep-0/dep.ipkg":4:11--6:1:Dep not found

If the dependency is instead installed globally with --install and the depends folder removed, the project works just fine

[buzden]

I'm sure it's an expected behaviour. Compiler itself does not have any facility to compile dependencies. depends directory is a directory where compiled *.ttc files are placed. Currently most of the packages e.g. when installed using pack are installed with sources, so there are *.idr files near to compiled *.ttc files, but this is not obligatory, so you can install libraries without sources, and they will be found fine. --install action copied *.ttc files in the first place.

[andrevidela]

There are two ways to take this from here:

• Should it be possible to compile file from subobjects in depends? The error message seems to imply it's possible and looking at the logs it looks like that's what the compiler is trying to do, except the working directory is set to the wrong sub-folder
• What should be an appropriate error message for this scenario? Clearly "module not found" does not convey the intended behaviour. What's the correct series of steps to take for the user to achieve their goal?

[mattpolzin]

It’s possible this is only because I’m biased by knowing the depends folder to be an install location from the start, but I don’t think there’s a need for the compiler to build dependencies as opposed to just bringing installed dependencies into scope. I think this both because Pack (or the nix tooling alternatively) do this quite well already and also because if the compiler did have a concept for “build this if needed” then I’m not sure we would want to have the “location of dependency source code” and the “location of dependency build artifacts” to necessarily be the same thing anyway. Throwing source code into install artifacts works well for downstream IDE integrations that want to be able to map to the source code but aside from that use case I think the compiler has already gotten a bit fast and loose with how it interprets its different configured “paths” in the past and it made things more confusing rather than less — for example, I disentangled the compiler’s concepts of “package search path” and “package directories” a little while ago because they are distinct things but paths of each kind were confusingly thrown together which made it hard to determine what was wrong for anyone unaware of the dual purpose of the path.

I see something similar happening if the same path can contain (a) just the source code for a dependency, (b) just the build artifacts, or (c) both and the compiler behaves differently depending on which is the case.

Regardless, I’m totally and perpetually in favor of better error messages and documentation naturally.

[mattpolzin]

FWIW, I've wanted some sort of install-local option (naming unimportant) to pair with the install option where the new option would compile/install to the depends folder for a given directory instead of the global install location.

That's tangential but certainly related because it speaks to the depends folder being awkward and unintuitive because although the compiler treats it as an install location when searching it does not offer a way to put dependencies into it in the way it needs them to be in there.

[andrevidela]

I think those two things could be part of adepends overhaul. Maybe right now we should focus on improving the feedback when its content is malformed. I'm not sure I'll have time to look at it soon, but it would be nice to at least scope out what the end result should be.

I feel like there should be a difference between "there are unexpected files here" and "I cannot find the module advertised". Right now the compiler does not even say where it looked for modules so maybe that's the first step. What would you think for the following:

• List out what folders were looked at when looking at modules
• Inspect the depends folder to check for project files and report them
• See if we can make a compiler flat to install in depends for a local installation rather than global

[mattpolzin]

That all sounds good and we’ve got most of the machinery and logic in place for the suggested logging too (not the depends folder inspection though) because of the list-packages and paths commands. Just need to put better errors together and write something that inspects the depends folder if present.

[mattpolzin]

Related: #3445