How to load an Idris file that depends on a package?

Question

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?

Answer 1

The layer for idris in Spacemacs use this https://github.com/idris-hackers/idris-mode.

So for my part, using spacemacs and helm, I succesfully load a file using contrib using the following shortcut:

• SP+:
• idris-set-idris-load-packages + RET
• contrib + RET
• CTR + RET

Answer 2

After trying @luc-duzan's answer, Spacemacs prompted me for whether to persist the setting. When I selected yes, the following was added to my buffer:

-- Local Variables:
-- idris-load-packages: ("contrib")
-- End:

Sure enough, this caused it to work after closing and re-opening Spacemacs, without going back through the steps. It's a bit of noise added to the buffer, but perhaps useful nonetheless.