Hi all,

I love Sublime Text 2, but I was wondering if it could support some fairly esoteric features for a language I love, called Agda. Agda is a proof assistant/language and most of its users currently use emacs for it right now because it’s fairly heavily integrated in emacs. A lot of Agda development can be seen as “a conversation with the typechecker” which runs in the background. The features the language would probably need include:

• Custom highlighting information from an external source. The TextMate highlighting format isn’t flexible enough for the syntax Agda supports, and it’s easiest to just call out to the Agda implementation’s own parser to produce highlighting information. The information can be provided in any format, but we need to be able to call an external program to generate it. This isn’t crucial, as Agda kind of resembles Haskell in syntax, but the highlighting would be pretty imprecise in the presence of a lot of mixfix, if we pretended Agda was Haskell for highlighting.

• “Holes”: currently, in emacs, I can create a “hole” in my code that lets me do things in a specific context. For a proof assistant, this is an enormously useful feature because you can ask for what your goal type and context is in the hole, and have context-aware operations when your cursor is in the hole. To create one in emacs, we simply type a question mark and then type a key combination to load the file. The question mark then turns into the green region you see in snapplr.com/zm95, and when your cursor is in that hole, you can do all sorts of special operations.

• A lot of this interaction with the typechecker has low overhead because we keep a persistent Agda typechecker/compiler process open behind the scenes, and communicate with it in emacs. The communication protocol isn’t set in stone, but we’d need to be able to run a background process/library in some way and talk to it in a context-aware manner (as mentioned above in the “Holes” point).

I realize these requests sort of blur the distinction between an editor and an IDE, but for a proof assistant, you really can’t write code without a lot of help from the typechecker. I like where the current agda-mode for emacs sits on the IDE <-> text editor spectrum, but I dislike emacs apart from that, so would love to get a more polished experience with sublime text.

Does anyone have any comments? How much of this is already possible with sublime text?

Thanks,
Dan

Hi copumpkin,

I’m really interested in this too. I just started using Sublime Text so I obviously don’t have the answer to your questions but I’m seriously thinking about giving a plugin a go just to see what’s possible. Maybe if enough people are interested it wouldn’t be too difficult to get something working together.

I think an obvious first approach would be to try and emulate what the current agda-mode does with some sort of plugin. It would be nice to have a proper protocol defined for interfacing interactive editing modes with agda, but I guess that will take a lot of work and might not lead to anything concrete any time soon.

Just having an alternative to the emacs mode could lead to some interesting possibilities for experimenting with new interactive editing features though.

I did a bit of digging around and it seems most of this is possible.

Highlighting can be done with add_regions. It’s not perfect though because in some cases we don’t just want solid color or outline highlighting, but instead want to change the color or style of the text (e.g., for constructors) based on feedback from the agda type checker. But the style of some text is determined by its syntax scope, which comes from the grammar definition file.

It’s possible to extract the scope of some text but there doesn’t seem to be a way to programmatically modify or set it. In fact, that wouldn’t probably make much sense unless you could also specify that a scope should be persistent somehow between subsequent highlighting passes.

Maybe someone else has some ideas about setting scope like this? If it’s not possible, it’d be really nice to have that functionality added to the api.

It seems like the rest of the stuff should be doable with the existing api functions. For example, it should be possible to tell when the point is within a region marked as a goal and based on that allow special commands to be executed like showing the current typing context, refining or giving a solution, etc.

Actually, maybe it’s possible to get the kind of highlighting we want where we’d otherwise have to modify scope by setting the background/foreground colors of a region to the match with the values currently used by the buffer.

In that case, I guess the user would have to modify their theme to add the scopes we’d use for dynamic highlighting and make sure that the respective colors fit in with everything else. But that’s probably not so bad and maybe that step could be automated.