Skip to content

zjhmale/vscode-idris

Repository files navigation

Idris for Visual Studio Code

Version Installs Ratings

Build Status Build Status

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

menu

Installation

  1. Within Visual Studio Code, open the command palette (Ctrl-Shift-P / Cmd-Shift-P).
  2. Select Install Extension and search for Idris or run ext install Idris.
  3. Download Idris and make sure the idris executable is on your PATH.
  4. 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

Thanks

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

License

BSD 3-Clause, the same as Idris.