front-end improvements: Emacs mode

[kiniry]

Incorporate and extend Austin's cryptol-mode.

[david-christiansen]

It might be interesting to explore having a common editor interaction protocol for Idris and Cryptol, so that one mode could support the basics of both, with language-specific additions for each.

[kiniry]

Hmmmm....

[thoughtpolice]

Hmmm, maybe I'm very confused, but the only kind of abstraction I can see that's possible is a library for both Emacs and Haskell, so that Emacs Lisp can easily interact with an arbitrary backend interpreter written in Haskell (or preferrably any language). Things like providing sensible autocomplete for the REPL would fall into this category, or sending commands to it. But that's a project that would be greatly beneficial to a lot of projects, not just Idris and Cryptol.

But I can't see anything else between the two toolsets that would facilitate further reuse; aside from fundamental syntax and semantic differences, there are fundamental workflow and tool differences (there's no interactive proving in Cryptol for example, which substantially simplifies a lot of the interaction, and often you want to not just manipulate Cryptol, but verify it against external resources like C or Java code, which comes with its own set of challenges about how to structure your projects. There isn't really a "best practices" to go by here.)

I suppose my point is the improvements suggested seem largely like an orthogonal task - you're still going to need pretty much everything in cryptol-mode for it to be usable (and even then, only barely). But cryptol-mode could certainly leverage any theoretical improvements from an editor protocol. So in the mean time, I think improving cryptol-mode itself further (indentation, literate file support, proving theorems for you) will still give you bang for your buck.

[david-christiansen]

I don't think you're confused at all - this is what I meant. Sorry if it was unclear.

Idris-mode has gotten a lot of mileage out having an easily-parseable protocol for communication between Emacs or other tools and itself. A lot of the core infrastructure, like parsing this protocol, keeping track of continuations for each command on the Emacs side, and the Emacs side of a few commands like completion could be shared in a base mode that others could be derived from.

But I'm in total agreement that this doesn't subsume things like indentation support and the other features you list. The reason I commented here is that I'm one of the two main authors of idris-mode, and I'm coming to visit Galois for a few months, and it might be fun to have a little side project. I'm crazy enough that I actually enjoy working on Emacs modes!

[kiniry]

We'll coordinate with Austin about this for 2.2.

https://github.com/thoughtpolice/cryptol-mode

[atomb]

We've come to general agreement that there's no need for us to maintain it ourselves. If @thoughtpolice ever gets tired of maintaining it, we would happily take over.