Working in Spacemacs (on Linux Mint, if that is relevant), using the Idris layer, one of my major mode commands is
SPC m-r (Vim-style keybindings):
idris-load-file. This causes Spacemacs to load up an Idris REPL instance and use it to type check the file. Once the REPL is loaded, other IDE-like functionality is enabled such as split case, proof search, etc. Thus the ability to load the file is crucial for smooth Idris development.
Idris has the concept of a package; for example, if you want a set implementation, there is one in the
contrib package. Thus, for example, this code depends on
module NeedsContrib import Data.SortedSet foo : SortedSet Int -> Maybe Int
If I try to load this code in the Idris REPL outside Spacemacs, I must provide the
-p contrib command-line argument. If I do not, I get
Can't find import Data/SortedSet. In my Vim development workflow, I launch Idris myself, manually, so I am able to specify this argument and it works. However, in Spacemacs' fancy way of doing things, it loads the Idris process itself, and I do not know how to indicate to it that I need
contrib - I get
Can't find import Data/SortedSet in the errors window, indicating the REPL has been loaded without
When I write much serious Idris code at all, I almost always end up using
contrib, or other packages. I would really like to transition from using Vim to Spacemacs for Idris development but this is hanging me up.
How do I get Spacemacs to launch the Idris process with the appropriate
-p <package> argument as necessary, or perhaps to connect to an existing running Idris instance with the arguments that I have already supplied?