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 contrib
:
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 -p contrib
.
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?