Idris and Idris2 setup

Idris.md

Idris

Install

macOS

brew install idris

Atom

Atom is the preferred (i.e., most common and best supported - aside from perhaps emacs). You'll need the Idris language package.

Open the Preferences panel from the Atom menu (or <command+,>) and select the Install tab. Search for Idris and install language-idris.

Once installed, select Packages from the Preferences panel and find language-idris and click its Settings button. Ensure the Idris location matches your install location (e.g., for Homebrew it is likely /usr/local/bin/idris).

VS Code

• vscode-idris

Keybindings

// Place your key bindings in this file to override the defaults
[
  {
    "key": "cmd+alt+r",
    "command": "idris.typecheck",
    "when": "editorTextFocus && editorLangId == idris"
  },
  {
    "key": "cmd+alt+t",
    "command": "idris.type-of",
    "when": "editorTextFocus && editorLangId == idris"
  },
  {
    "key": "cmd+alt+h",
    "command": "idris.docs-for",
    "when": "editorTextFocus && editorLangId == idris"
  },
  {
    "key": "cmd+alt+e",
    "command": "idris.print-definition",
    "when": "editorTextFocus && editorLangId == idris"
  },
  {
    "key": "cmd+alt+a",
    "command": "idris.add-clause",
    "when": "editorTextFocus && editorLangId == idris"
  },
  {
    "key": "cmd+alt+p",
    "command": "idris.add-proof-clause",
    "when": "editorTextFocus && editorLangId == idris"
  },
  {
    "key": "cmd+alt+c",
    "command": "idris.case-split",
    "when": "editorTextFocus && editorLangId == idris"
  },
  {
    "key": "cmd+alt+l",
    "command": "idris.make-lemma",
    "when": "editorTextFocus && editorLangId == idris"
  },
  {
    "key": "cmd+alt+m",
    "command": "idris.make-case",
    "when": "editorTextFocus && editorLangId == idris"
  },
  {
    "key": "cmd+alt+s",
    "command": "idris.proof-search",
    "when": "editorTextFocus && editorLangId == idris"
  },
  {
    "key": "cmd+alt+w",
    "command": "idris.make-with",
    "when": "editorTextFocus && editorLangId == idris"
  },
  {
    "key": "cmd+alt+v",
    "command": "idris.eval-selection",
    "when": "editorTextFocus && editorLangId == idris"
  },
  {
    "key": "cmd+alt+x",
    "command": "idris.start-refresh-repl",
    "when": "editorTextFocus && editorLangId == idris"
  }
]

Packages

Like most langauges, Idris supports the notion of packages the bundle a collection of modules together for distribution. The native format is an ipkg file. Refer to the official documentation for details.

Manual Package Management

If your project depends on other packages, they will need to be installed into the lib location for the version of Idris you have installed.

This Idris library location can be determined using the commandline: idris --libdir.

The currently installed libraries can be determined by: idris --listlibs.

To install a dependency, follow the package's instructions. The usual method is to clone the repository locally and either use make or use the following commands:

idris --clean IPKG
idris --checkpkg IPKG
idris --build IPKG
idris --install IPKG

Elba: Idris Package Manager

*nix

It is recommended to use Rust ('nightly' channel) to install Elba.

curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh

At the prompt, elect to change the options and switch to the nightly toolchain (and accept the defaults for the other settings).

Current installation options:

   default host triple: x86_64-apple-darwin
     default toolchain: nightly
               profile: default
  modify PATH variable: yes

Refresh your terminal or source $HOME/.cargo/env to use the updated PATH.

cargo install elba

IDE Interface

Usually, an IDE (e.g., VS Code, Atom, vim) interfaces with Idris directly. If you are using Elba to manage your project and package dependencies, then you will need to install its interface wrapper.

git clone https://github.com/elba/idris-elba-interface
cd idris-elba-interface
cargo install --path .

Change the path to the Idris executable in your IDE settings to point to idris-elba-interface.

Note: For VS Code, ensure you have "Inherit Env" for your integrated terminal.

Sample Project

Create a project:

elba new my-org/my-proj

This creates a new directory, my-proj, with git repo, config (elba.toml), and basic source layout.

To add an external dependency (i.e., one not in the elba repo), add the spec manually to the the elba.toml file, for example:

[dependencies]
"statebox/idris-ct" = { git = "https://github.com/statebox/idris-ct" }

Idris2

Github

Idris2-vim

Github

Edit plugins.vim:

    " Idris2
    Plug 'edwinb/idris2-vim'

Install the plugin from within Vim:

:PluginInstall

See the documentation for details.

REPL

The idris2 REPL, as of v0.2.1, does not yet have native readline support. The recommended workaround is to use rlwrap:

brew install rlwrap

and add an alias for your shell:

alias idris2="rlwrap idris2"