Interacting with Idris from Racket

This is the start of a library for interacting with Idris in graphical Racket applications. It uses Idris’s IDE protocol to communicate with the compiler, just like idris-mode for Emacs and the Atom plugin do.

My main motivation is to have something better than Emacs for doing slide shows with compiler interaction.

Current features

• Start an Idris process and communicate over a socket
• Parsing and unparsing Idris messages
• Demo REPL app, including semantic highlights
• Demo editor app, including file editor and REPL
• Embedded Idris editors and REPLS in Slideshow

Planned

• Proper translation between Idris error results and Racket exceptions
• An organized, properly documented public API

Not planned, but patches welcome

• #lang idris in DrRacket
• Full-featured editor support, with doc lookup, etc.
• Compiling and running Idris programs from Racket
• Interactive prover/elaborator support

How to test

First, if Idris isn’t on your PATH, then edit the invocation of subprocess to point at its absolute path.

To launch the REPL, run $ racket idris-repl.rkt. To run the editor, run $ racket idris-editor.rkt.

If you’d like to use this package for a talk, please refer to the contents of example-slideshow.rkt for a starting point to work with. Because it launches external processes, these slides should be run with $ slideshow --trust example-slideshow.rkt.