Archive | Emacs Lisp RSS for this section

Getting Started With Coq and Proof General

Today we’ll be talking about Coq. Coq is a dependently typed programming language and theorem proof assistant. Given that I’ve just now got the toolchain installed, I’m hardly qualified to say much more than that. However, I am qualified to talk about installing the toolchain, which is precisely what I intend to do.

To get started with Coq, you’ll need the usual things: a properly configured editor and the Coq compiler. Installing these isn’t terribly difficult. First, let’s install the compiler. If you’re running Ubuntu, this is quite simple:

$ sudo apt-get install coq

After this is done, you should have access to the compiler (coqc) and the REPL (coqtop):

$ which coqc /usr/bin/coqc $ which coqtop /usr/bin/coqtop $ coqc --version The Coq Proof Assistant, version 8.4pl4 (July 2014) compiled on Jul 27 2014 23:12:44 with OCaml 4.01.0

OK! Now for the (slightly) harder part: our properly configured editor. Here we have two choices: CoqIDE or Proof General. CoqIDE is a simple IDE that ships with Coq, so if you’re satisfied with this, then feel free to stop reading now: CoqIDE comes with Coq and should be already installed at this point!

However, if you want to be truly cool, you’ll opt for Proof General. Proof General is an Emacs plugin. Unfortunately, Proof General is not available in Melpa, so we get to install it manually. Fortunately for us, Proof General is in the repos, so if you’re running Ubuntu you can just apt-get it:

$ sudo apt-get install proofgeneral proofgeneral-doc

This will install Proof General, and set Emacs to load it up when you open a .v file. (My condolences to all those who write Verilog and Coq on the same machine) However, some configuration remains to be done. First fire up emacs and execute:

M-x customize-group <enter> proof-general <enter>

Expand Proof Assistants and ensure Coq is selected. Now open up a .v file and behold the glory!

Wait a minute, where’s my undo-tree? My rainbow-delimiters? My whitespace-mode? It’s not your imagination, Proof General has inexplicably ignored your fancy .emacs config. This is all a bit irritating, but you can work around it by re-adding these things to the coq-mode-hook:

(add-hook 'coq-mode-hook 'rainbow-delimiters-mode) (add-hook 'coq-mode-hook 'whitespace-mode) (add-hook 'coq-mode-hook 'undo-tree-mode)

This is a bit of a sorry state of affairs, and if anybody reading this knows a better way I’d love to hear it. For now, I got my shinies back, so it’ll do.

Regardless, Proof General should be ready to go at this point. We are ready to continue our journey down the rabbit hole into wonderland… See you all on the other side!

Fun With Undo-Tree-Mode

No more. This ends now. This will not stand!

What’s my problem, you ask? I’ll tell you what. Emacs’ stupid undo system is my problem. Humor me for a second; fire up Emacs, and type the following:

foo bar baz

Still with me? Good, now press

C-x u

…baz disappeared. “Well, duh! If you’re gonna whine about the fact that C-u doesn’t undo, then maybe you shouldn’t be using Emacs…” you say. Were that my issue, I’d be inclined to agree. Unfortunately, the problem is much worse. Enter the following into your buffer:

oof

…then…

C-x u C-x u

See that? Yeah… Not OK. The buffer should be:

foo

with the entry of oof and bar having been undone. Instead, the buffer is:

foo bar baz

with the entry of oof and the undoing of the undoing of the entry of baz having been undone.

Apparently, an undo operation itself goes onto the undo stack in Emacs. Meaning that if you undo enough times, it will redo all the undone operations, then undo them again, then undo the operations before. This lets us get the buffer back into any state it has ever been in, which sounds nice on paper. In practice, it’s yet another way that Emacs goes its own way, the rest of the world be darned. And I gotta say, its pretty annoying. In a normal program, you can just hold Ctrl+u, and watch the undoes fly. In Emacs, you get to press C-x, release, press u, and release to undo one thing. Then do it again n times.

Luckily for us, this being Emacs, there is likely a better way out there.

undo-tree-mode

Undo tree mode is a minor mode for Emacs that helps us deal with this undo behavior. In the short amount of time that I’ve played with it, I’d say it makes the on-paper benefit of Emacs’ undo behavior a reality. But first, some installation.

Undo-tree-mode is in Melpa stable, however, I was unable to get it to work. To install undo-tree-mode, you can install it via Melpa, then add the following to your .emacs file:

(global-undo-tree-mode)

Unfortunately, when I restarted Emacs, I got the following error:

Symbol's function definition is void: global-undo-tree-mode

Adding:

(require 'undo-tree)

does nothing to alleviate this situation, neither does opening undo-tree.el and entering:

M-x byte-compile-file

However, I was able to install it manually. First, I deleted all the files for undo-tree-mode from my .emacs.d/ directory. Then I downloaded the current version of the plugin from the author's website, and placed it in my ~/.emacs.d/, naming it undo-tree.el. Finally, I added the following lines to my .emacs file:

(add-to-list 'load-path "~/.emacs.d/") (require 'undo-tree) (global-undo-tree-mode t)

That first line is only required if you haven’t already added it elsewhere. Restart Emacs, and you should see that the Undo-Tree minor mode is active.

Climbing The Tree

Now, let’s try that previous sequence of events.

foo bar baz C-x u

A new window should appear with the following in it:

s | | o | | o | | o | | o | | x

Neat. This represents the operations that you did. Try clicking through them (you can also use the arrow keys to browse). Each node is a state of the document, x is the current state, and s is the initial state. Select the node two nodes up from the leaf to undo entry of baz. Lets continue our sequence:

oof C-x u

You should see a new tree that looks something like this:

s | | o | | o | | o | | o | / \ x o | | o

If you click around the tree, you’ll see the various states of your buffer. You’ll see that it is simple to restore any previous state of the buffer.

Now this is something I can get used to!

Giving Emacs A Shot

For the last year or so, I’ve been using GEdit to write Haskell code. It’s worked pretty well for the most part. Haskell is a pretty simple language, and thanks to the REPL, I find myself not really missing most fancy IDE features. However, GEdit has its limitations. While GEdit has plugin capabilities, they are somewhat limited in what they can do. Additionally, there doesn’t really seem to be a vibrant plugin culture. Most people just use what Gnome provides, and that’s mostly sufficient. Put simply: I’ve made do. Honestly, I had a pretty effective setup: With my file browser on the left, and my built-in terminal on the bottom, I had 95% of what I needed. However, one always wants more.

Recently, I started at UCSD, and if any of you are familiar with its Computer Science program, you’ll know that they push Vim. They push it Hard; deep down your throat. They have basically an entire class dedicated to learning Vim, and programming assignments are set up in ways that break IDEs. Due to this, I’ve had plenty of time to consider my editor choices. So far, I’ve worked around these issues; using NetBeans to code my C, C++, and Java like a civilized person. However, I can’t help but feel that I’m swimming up river. Surely my life would be easier if I gave in.

Don’t get me wrong, I don’t care for Vim. I learned to use Vim over ten years ago in my various sysadmin jobs, so it’s not that I don’t know how to use it. I’d just rather not. Sure, for a quick edit to a file at the command line nothing beats Vim. However, I find the idea of trying to use a command line editor for a large software development laughable. I’m a fan of the GUI. Keyboard shortcuts can save time, but at some point the brainpower you devote to remembering the correct incantation for an operation you perform maybe once a week could be better spent solving some software engineering problem.

Now I know what you’re probably thinking: “But Mr. DMP-Man! Emacs is a command line editor fraught with arcane keyboard combinations, each more inscrutable than the last!” And you’d be right. However, I feel that Emacs has more effectively made the leap into the 21st century. It’s GUI isn’t the greatest, but I give it the edge. Additionally, since all editor functions are just elisp functions, and you can call them by name and by shortcut, it supports discovery more effectively. Where in Vim, you’re likely going to turn to google to tell you how to do something, in Emacs, you can just do M-x foo-do [TAB] and get a list of things that are probably what you want. In short, I can learn a few incantations if the benefits are worth it.

But I digress: the point of this post is not to proclaim what editor you should use. Some people like Vim, some people like Emacs, some people don’t care. All three are valid points of view, and there is no objective right answer.

What Benefits?

So, what compels me to give Emacs a shot? The vast library of plugins, of course. I spent a few days configuring plugins for Haskell development, and I do believe I’ve settled on a setup that’s going to improve my productivity. I’d like to share my findings.

Most of what’s in here is inspired by this excellent tutorial by serras.

But First…

Before we get started, we need to add a repository to Emacs. Emacs comes with a built-in repository system, similar to what you’d find in your favorite linux distro. However, this repo is more Debian than Ubuntu; it’s missing a lot of stuff. Thankfully, the community has stood up more robust repositories. The two big ones are Marmalade and Melpa. You can use both, or one or the other.

I settled on Melpa, of which there are two: melpa and melpa stable. Some bad experiences with Debian Sid, I’ve learned to stick with stable repos.

Either way, go ahead and add a repo to your Emacs, and you’ll have a much better selection of plugins. To setup melpa-stable, add the following to your .emacs file:

(require 'package) (add-to-list 'package-archives '("melpa-stable" . "http://stable.melpa.org/packages/") t

haskell-mode

Of course something called haskell-mode would be a good candidate to download for Haskell development. Haskell-mode provides quite a bit of functionality: syntax highlighting, formatting help, and integration with quite a few external programs to facilitate development. haskell-mode can be installed from Melpa.

Details on configuring this can be found in Serras' tutorial

For indentation, I recommend the hi2 plugin mentioned in the tutorial. It provides visual cues as to where the tabs are located, and the behavior is much less wonky than the basic haskell-indentation

ghc-mod

The next thing to install is ghc-mod. ghc-mod Provides integration with GHC. Most notably: ghc-mod provides IDE-style error and warning messages inline with your source file! It also provides simple code completion, and is required infrastructure for a lot of other plugins. Recommended.

Unfortunately, it takes a bit of configuration. Check Serras' tutorial for more info.

whitespace-mode

Lately, I’ve become a fan of the 80-columns rule. I used to think that it was silly in this age of widescreen monitors. However, I’ve been forced to abide for the last quarter, and I’ve realized that it helps readability. Additionally, Haskell code tends to slide to the right thanks to extensive indentation. Due to this, some discipline is good to keep the left half of your screen from being filled with whitespace characters.

GEdit has a feature that it shows the 80th and beyond in a different shade than the first 79. Unfortunately, EMacs is somewhat lacking in this department. However, whitespace-mode serves just fine in this case.

It doesn’t mimic the GEdit behavior, but it can be configured to highlight code that goes past 80 columns. To enable whitespace mode for programming modes, add the following to your .emacs:

(add-hook 'prog-mode-hook 'whitespace-mode)

whitespace-mode can be configured using the visual customize functions within Emacs. Enter M-x customize-group [ENTER] whitespace [ENTER] to access the visual customization. I have mine set up to put a dreadful red box around anything that passes the 80th line:

gross

rainbow-delimiters

rainbow-delimiters is a plugin that color codes matching parenthesis. It’s pretty simple, but it can help greatly when working with lots of matching brackets.

rainbow-delimeters

Configuration is simple using the visual customization: M-x customize-group [ENTER] rainbow-delimiters [ENTER] should get you going. rainbow-delimiters can be found in Melpa.

In Conclusion

My journey with Emacs has just begun. Maybe I’ll fall off the wagon, maybe I’ll become a Priest of the Church of Emacs. Either way, I’m sure you’ll likely hear about it here!

%d bloggers like this: