Support for Idris, the dependently-typed, functional language.
- Installation
- Idris 2
- Commands
- Code Navigation
- Code Editing
- Diagnostics
- Testing
- Debugging
- Others
- Add Clause
- Add Missing
- Apropos
- Apropos At Cursor
- Browse Namespace
- Case Split
- Documentation For
- Documentation At Cursor
- Generate Definition
- Interpret Selection
- List Metavariables
- Print Definition
- Print Definition At Cursor
- Make Case
- Make Lemma
- Make With
- Proof Search
- Version
- Keybindings
- Semantic Highlighting
- To Do
- About
- License
The plugin itself can be installed from within VSCode or VSCodium through the Extensions Panel. It should come up if you search for ‘Idris’. The extension id is meraymond.idris-vscode.
You can also download the vsix file from the Releases page on Github, or from the VSCode Marketplace, or from the Open VSX Registry.
You will need Idris or Idris 2 installed separately. If it’s not on your $PATH, you can specify the absolute path to the executable in the config. The extension will not download or install anything on the user’s behalf.
If you want to test local changes to the extension, build it with npm install && npm run watch, then you can launch the local version with Run > Start Debugging inside VS.
Currently the extension will default to v1. If you want it to use Idris 2, change the path in the configuration to your Idris 2 binary, and tick the Idris 2 Mode checkbox.
Only the current version of Idris 2 is supported, which at the moment is 0.4.0. If you experience problems, please make sure you are using the most recent version.
At the moment, some of the IDE commands haven’t been implemented in Idris 2. There are no completions yet either.
Generate the initial clause for the function definition under the cursor.
Generate pattern matches for any missing clauses for the function definition or case statement under the cursor.
Search the documentation for references to a string.
Search the documentation for references to the word under the cursor.
Show all declarations and sub-modules for a given namespace.
Split the variable under the cursor into all possible pattern matches.
Show the documentation for a given function.
Show the documentation for the function under the cursor.
Generate complete definition for the function definition under the cursor.
Interpret the highlighted code and show the result in the editor.
Show a list of all the holes (metavariables) in the current namespace.
Show the definition for a given function.
Show the definition for the function under the cursor.
Turn the variable under the cursor into a case statement.
Create a new function declaration, and use it to solve the hole under the cursor.
Turn the variable under the cursor into a with statement.
Solve the hole under the cursor.
Show the current version of Idris.
The extension doesn’t set any key-bindings out of the box, but here are some suggested bindings based on the Atom plugin. Just copy them to your User/keybindings.json.
[
{
"key": "ctrl+alt+a",
"command": "idris.addClause",
"when": "editorLangId == idris && editorTextFocus"
},
{
"key": "ctrl+alt+b",
"command": "idris.browseNamespace",
"when": "editorLangId == idris && editorTextFocus"
},
{
"key": "ctrl+alt+c",
"command": "idris.caseSplit",
"when": "editorLangId == idris && editorTextFocus"
},
{
"key": "ctrl+alt+d",
"command": "idris.docsForSelection",
"when": "editorLangId == idris && editorTextFocus"
},
{
"key": "ctrl+alt+g",
"command": "idris.generateDef",
"when": "editorLangId == idris && editorTextFocus"
},
{
"key": "ctrl+alt+i",
"command": "idris.interpretSelection",
"when": "editorLangId == idris && editorTextFocus"
},
{
"key": "ctrl+alt+m",
"command": "idris.makeCase",
"when": "editorLangId == idris && editorTextFocus"
},
{
"key": "ctrl+alt+l",
"command": "idris.makeLemma",
"when": "editorLangId == idris && editorTextFocus"
},
{
"key": "ctrl+alt+w",
"command": "idris.makeWith",
"when": "editorLangId == idris && editorTextFocus"
},
{
"key": "ctrl+alt+p",
"command": "idris.proofSearch",
"when": "editorLangId == idris && editorTextFocus"
}
]
The extension should work equally well for literate Idris files. For Idris 1, this only applies to .lidr files. Idris 2 extends this this to embedded code blocks in Markdown, LaTeX and Org-Mode files. However, the extension will only activate automatically for .idr and .lidr files. In order to use it for other file types, it may need be activated manually, with the Idris: Activate Extension command, if you have not previously opened any Idris files.
LaTeX and Org-Mode are not yet implemented, but Markdown support is.
The apropos, browse namespace, documentation and definition commands use VS’s semantic highlighting API to colourise their output. If you don’t see any highlighting, it’s likely that your theme doesn’t support it yet.
Currently, Idris source files don’t use semantic highlighting. There are a few issues to work out to get it to sync with Idris in a non-terrible way. Also Idris 2 does not yet return the metadata required for semantic highlighting.
- implement Show References
- there is more information to add to the metavariables command output
- semantic highlighting for source code
- more ipkg integration
The extension should be mostly stable for Idris 1, though there a few remaining unimplemented actions. Current work is focused on fixing bugs and maintaining support for Idris 2.
If you run into any problems, please raise an issue, or raise a PR if you want to.
There is not, nor will there ever be, telemetry in this extension (though that may not apply to VS itself).
The syntax files are adapted from vscode-idris’s port of the Atom plugin’s grammars.