REPL command loadpackage only loads packages that are already loaded

[ohad]

Steps to Reproduce

$ idris2 --no-banner -p contrib
Main> :lp "contrib"
Done
Main> :quit
Bye for now!
$ idris2 --no-banner
Main> :lp "contrib"

Expected Behavior

Package contrib loads fine:

Done

Observed Behavior

Package contrib doesn't load, other, already loaded, packages load fine:

Package not found in the known search directories
Main> :lp "base"
Done
Main> :quit
Bye for now!

[Russoul]

This is expected behavior (w.r.t what I had in mind implementing it). But that would be a nice addition :)

The intention was to load(import) every name from a package already visible with the given REPL instance setup.

(It doesn't just "load" the package. It brings every public export name into scope. So commands like :t and :fs can operate on every single name from the package)

[ohad]

I see.
Does that make this into a feature request?
Also, docs for :lp should be clearer, I think.

[Russoul]

Yeah, I guess it does. I'll try to PR a docs update soonish.