2

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?

2

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
  • Worked great. Much appreciated. – Keith Pinson Jan 12 at 19:41
1

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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.