Idris for Visual Studio Code

Implemented features

command screenshot	command name
Typecheck the currently open file	idris.typecheck
Print the type of the identifier under the cursor	idris.type-of
Print the documentation of the identifier under the cursor	idris.docs-for
Print the definition of the identifier under the cursor	idris.print-definition
List all active holes in the currently open file	idris.show-holes
Generate an initial pattern match clause for the function under the cursor	idris.add-clause
Generate an initial pattern match clause when trying a proof	idris.add-proof-clause
Generate a case split for a pattern variable under the cursor	idris.case-split
Attempt to fill out any holes by a proof search	idris.proof-search
Create a pattern-matching with-rule for the name under the cursor	idris.make-with
Create a case pattern match template for a hole under the cursor	idris.make-case
Create a top-level function with a type matching the hole under the cursor	idris.make-lemma
Search names, types and documentation	idris.apropos
Evaluate the selected code	idris.eval-selection
Start or refresh a REPL for the currently open file	idris.start-refresh-repl
Send the selected code to the REPL	idris.send-selection-repl
Cleanup all the idris binary files(*.ibc) in the project	idris.cleanup-ibc
Create a new project with scaffolding	idris.new-project
Search for functions by type signature	idris.search

Heads up: All the commands above can also be triggered in the right-click menu

Installation

Within Visual Studio Code, open the command palette (Ctrl-Shift-P / Cmd-Shift-P).
Select Install Extension and search for Idris or run ext install Idris.
Download Idris and make sure the idris executable is on your PATH.
Run cabal install idringen and make sure the idrin executable is on your PATH.

Contributing

Check out CONTRIBUTING.md.

Options

The following Visual Studio Code settings along with their default values that are available for the Idris extension. If you want to change any of these, you can do so in user preferences (cmd+,) or workspace settings (.vscode/settings.json). You don't have to copy these if you don't intend to change them.

{
    "idris.executablePath": "idris",            // The full path to the idris executable.
    "idris.hoverMode": "fallback",              // Controls the hover behavior. 'info' will display Idris documentation, 'type' will display Idris type, 'fallback' will try 'info' first and fallback to 'type' if we can not get the documentation, and 'none' will disable hover tooltips.
    "idris.suggestMode": "allWords"             // Controls the auto-completion behavior. 'allWords' will always include all words from the currently opened documentation, 'replCompletion' will get suggestions from Idris REPL process.
    "idris.warnPartial": false                  // Show warning when a function is partial.
    "idris.showOutputWhenTypechecking": false   //Show output channel when typechecking finished.
    "idris.numbersOfContinuousTypechecking": 10 //Kill Idris process every N times of continuous typechecking to avoid memory leaking.
}

Acknowledgements

The internal design is initially inspired by atom-language-idris.

Thanks

Belleve Invis @be5invis (The maintainer of the syntax files)

License

BSD 3-Clause, the same as Idris.

Idris

zjhmale