An Idris Mode for Atom

A work-in-progress Idris Mode for Atom.

It supports:

• Typechecking (ctrl-alt-r)
  • compiles the file and reports errors
• Case-splitting (ctrl-alt-c)
  • split a variable which can be pattern matched
• Clause-adding (ctrl-alt-a)
  • add a clause to a function
• Proof-search (ctrl-alt-s)
  • search for a proof of a hole
• Showing the types of a variable (ctrl-alt-t)
  • show the type of a hole
• Show the doc for a function (ctrl-alt-d)
• make-with (ctrl-alt-w)
  • add further variables on the left hand side of a function
• make-case (ctrl-alt-m)
• make-lemma (ctrl-alt-l)
  • lift a hole into a function context
  • Add proof case
  • alternate version of clause adding when trying to proof a type. http://docs.idris-lang.org/en/latest/reference/misc.html#match-application
• Showing holes
• ipkg highlighting
• REPL (ctrl-alt-enter)
• Apropos view

Usage

The package should work after installation. The only thing you might need to set is the path to the idris executable in the config of this package. If it doesn't work it's probably a bug.

There is a tutorial on how to use the editor under documentation/tutorial.md.

Working with ipkg files

Place your ipkg file in the top level directory of your project. There is more information available in a in a separate documentation.

Todo

• Add better support for drawing attention to error-messages
• Improve the syntax-highlighting (the current is based on the Sublime plugin)
• Add autocompletion
• ...

Development

To work on this plugin you need to clone it into your atom directory and rename the folder to language-idris or the package settings won't get picked up. Then you need an apm install from the language-idris folder to install the dependencies.

Or you can execute apm dev language-idris. This will install the package in a separate directory and you need to start Atom in dev-mode to load the development packages (atom -d your/folder).