search

idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.44k stars 644 forks source link

Adding a package with -p (in the REPL) shouldn't be necessary #4740

Open deliciouslytyped opened 5 years ago

deliciouslytyped commented 5 years ago

I can expand a bit on this later if needed, but why is it necessary to pass -p something as an argument to idris to be able to import a module? IDRIS_LIBRARY_PATH already specifies the root of where to search (though it can only take a single path for some reason, which would also be nice to fix...), so why do I additionally need to specify what to search for again?

I don't need to do this for python, nor do I need to do it for ghci.

(context: I'm trying to improve idris usage with nixpkgs)

deliciouslytyped commented 5 years ago

@jfdm @eraserhd

deliciouslytyped commented 5 years ago

By the way, the first place any real processing is actually done on -p at the moment seems to be https://github.com/idris-lang/Idris-dev/blob/c5c8ede51742d03afc701e9fd854f979a5362550/src/Idris/Main.hs#L146 , namely pkgdirs.

Further relevant code is: https://github.com/idris-lang/Idris-dev/blob/c5c8ede51742d03afc701e9fd854f979a5362550/src/Idris/Main.hs#L247

This appears to be where imports are actually handled: (found by somehow via "ibc_imports") https://github.com/idris-lang/Idris-dev/blob/f445c51466375a0d2e7d58b4d91bac466e7123e2/src/Idris/IBC.hs#L587

deliciouslytyped commented 5 years ago

Well, I don't know where the above gets me, but couldn't we just map addPkgDirover all the top level names everything in the search directory or somethng?