Archive | Emacs RSS for this section

Pretty Printing our Pretty Program with Pretty

Tell me if you’ve heard this one before. You’re making some complicated data structure in Haskell. Something like the following:

data Expr = EVal Int | EIdent String | EFunc String [String] [Expr] | ECall String [Expr] | ELet String Expr | EWhile Expr [Expr] | EShizzy Expr Expr Expr | EIfElse Expr Expr Expr | EReturn Expr deriving (Show)

You throw that deriving (Show) because it’ll totally help you debug! Time goes by, and you use your fancy Expr to write a robust imperative function:

test = EFunc "testFunc" ["gatito", "moogle"] [ELet "foo" $ ECall "petCat" $ [EIdent "gatito", EIdent "moogle"], EWhile (ECall "catsPlacated" []) [EShizzy (EIfElse (EVal 5) (ELet "foo" $ ECall "malloc" [ECall "sizeof" [EVal 2]]) (ECall "petCat" $ [EIdent "gatito", EIdent "moogle"])) (ECall "petCat" $ [EIdent "gatito", EIdent "moogle"]) (ELet "foo" $ ECall "safeLeakMemory" []) ], EReturn $ EIdent "foo" ]

You’re still good, you got Rainbow Delimiters to keep that all sorted. Now, more time goes by and you’re in the repl and something doesn’t work. What was this test thing again?

*Shizzy> test EFunc "testFunc" ["gatito","moogle"] [ELet "foo" (ECall "petCat" [EIdent "gatito",EIdent "moogle"]),EWhile (ECall "catsPlacated" []) [EShizzy (EIfElse (EVal 5) (ELet "foo" (ECall "malloc" [ECall "sizeof" [EVal 2]])) (ECall "petCat" [EIdent "gatito",EIdent "moogle"])) (ECall "petCat" [EIdent "gatito",EIdent "moogle"]) (ELet "foo" (ECall "safeLeakMemory" []))],EReturn (EIdent "foo")]

Well that’s unfortunate. What do we do now? Aside from the fact that this is completely useless to us, this certainly wouldn’t be OK to print out to a user…

The good news is that pretty printing is a snap thanks to the HughesPJ Pretty Printer. One simply has to implement the Pretty class for one’s type, and then they can get some reasonable output:

testFunc(gatito moogle) { let foo = petCat(gatito moogle) while(catsPlacated()) { +-- { if (5) let foo = malloc(sizeof(2)) else petCat(gatito moogle) } +++ + + +++ { petCat(gatito moogle) } +++ + + +++ { let foo = safeLeakMemory() } +-- } produceResult foo }

Let’s see how we get there, constructor by constructor.

EVal and EIdent

First up are the easy ones: EVal and EIdent, which represent bare values:

instance Pretty Expr where pPrint (EVal v) = int v pPrint (EIdent s) = text s

First we have to declare our instance, but next we can just print the values. int pretty prints an integer, and text pretty prints a string.

EFunc and ECall

Next we have function calls and definitions:

pPrint (EFunc n a b) = text n <> (parens $ hsep $ fmap text a) <+> lbrace $+$ (nest 2 $ vcat $ fmap pPrint b) $+$ rbrace pPrint (ECall n a) = text n <> (parens $ hsep $ fmap pPrint a)

There are some operators here that require explanation. All of these operators have type (Doc -> Doc -> Doc ), and are used to combine two Doc into one. A Doc is the type of thing that can be pretty printed, which is returned by calls to pPrint and various other primitive pretty printing functions provided by the library (like text and int)

<> glues the thing on the left next to the thing on the right with no space in between, where <+> does the same, but leaves 1 space in between. Similarly, $$ and $+$ glues the thing on the right to the bottom of the thing on the left. $+$ allows the right hand side to overlap with the left (more on this later). There are also hsep, and vcat which takes lists of Doc. These functions work similarly to <>, $$ and friends; they glue Docs together horizontally and vertically. *cat are the non-plus variants, and *sep are the plus variants.

Other functions introduced here are parens, which takes a Doc and surrounds it by parens. lbrace and rbrace insert { and } respectively. There is a braces function as well, but I didn’t use it because I want to control how the braces are shown. Finally, we have nest, which indents its argument. This function is great because it takes into account outer nest calls, so we can get arbitrary nesting.

ELet, EWhile, EIfElse, and EReturn

pPrint (ELet n e) = text "let" <+> text n <+> equals <+> pPrint e pPrint (EWhile p b) = text "while" <> (parens $ pPrint p) <+> lbrace $+$ (nest 2 $ vcat $ fmap pPrint b) $+$ rbrace pPrint (EIfElse p t f) = text "if" <+> (parens $ pPrint p) <+> pPrint t $+$ text "else" <+> pPrint f pPrint (EReturn v) = text "produceResult" <+> pPrint v

Nothing particularly fancy here. in ELet, we have equals which inserts an equals sign and we have more nesting throughout. As you can see, this is very simple once you get the hang of it; there are few abstract instances involved, and most functions do what they say.


As we all know, any programming language that doesn’t have Shizzy statements isn’t worth knowing, so of course I implement them:

pPrint (EShizzy u d t) = onFire $+$ (nest 6 (lbrace $+$ (nest 2 (pPrint u)) $+$ rbrace)) $+$ noRules $+$ (lbrace $+$ (nest 2 (pPrint d)) $+$ rbrace) $+$ noRules $+$ (nest 6 (lbrace $+$ (nest 2 (pPrint t)) $+$ rbrace)) $+$ onFire where onFire = nest 2 $ text "+--" noRules = nest 2 $ (text "+++" $$ text "+ +" $$ text "+++")

This produces the following output as we’d expect:

+-- { if (5) let foo = malloc(sizeof(2)) else petCat(gatito moogle) } +++ + + +++ { petCat(gatito moogle) } +++ + + +++ { let foo = safeLeakMemory() } +--

and this gives me a good opportunity to demonstrate the difference between $$ and $+$. Let’s swap all the plus variants out:

onFire $$ (nest 6 (lbrace $$ (nest 2 (pPrint u)) $$ rbrace)) $$ noRules $$ (lbrace $$ (nest 2 (pPrint d)) $$ rbrace) $$ noRules $$ (nest 6 (lbrace $$ (nest 2 (pPrint t)) $$ rbrace)) $$ onFire where onFire = nest 2 $ text "+--" noRules = nest 2 $ (text "+++" $$ text "+ +" $$ text "+++")

Now, the pretty printer outputs the following:

+-- { if (5) let foo = malloc(sizeof(2)) else petCat(gatito moogle) } +++ + + +++ { petCat(gatito moogle) } +++ + + +++ { let foo = safeLeakMemory() } +--

Basically, if something is nested far enough that it would appear after the end of the left hand side argument, it is pasted to the right of it instead of below it. Honestly, it’s pretty strange behavior to me, I say just avoid $$ for the most part and you’ll be fine. It’s not a huge stretch for me to think of a use for this, but I think I’d just use <> or <+> if I wanted this to happen.

Regardless, I’ve worked on projects that use this pretty printing library before, and now that I’ve given it a shot I know why!

Baby’s First Proof

Unlike many languages that you learn, in Coq, things are truly different. Much like your first functional language after using nothing but imperative languages, you have to re-evaluate things. Instead of just defining functions, you have to prove properties of them. So, let’s take a look at a few basic ways to do that.

Simpl and Reflexivity

Here we have two basic “tactics” that we can use to prove simple properties. Suppose we have some function addition. We’re all familiar with how this works; 2 + 2 = 4, right? Prove it:

Lemma two_plus_two: 2 + 2 = 4. Proof. Admitted.

First, what is this Admitted. thing? Admitted basically tells Coq not to worry about it, and just assume it is true. This is the equivalent of your math professor telling you “don’t worry about it, Aristotle says it’s true, are you calling Aristotle a liar?” and if you let this make it into live code, you are a bad person. We must make this right!

Lemma two_plus_two: 2 + 2 = 4. Proof. simpl. reflexivity. Qed.

That’s better. This is a simple proof; we tell Coq to simplify the expression, then we tell Coq to verify that the left-hand-side is the same as the right-hand-side. One nice feature of Coq is that lets you step through these proofs to see exactly how the evaluation is proceeding. If you’re using Proof General, you can use the buttons Next, Goto, and Undo to accomplish this. If you put the point at Proof. and click Goto, Coq will evaluate the buffer up to that point, and a window should appear at the bottom with the following:

1 subgoals, subgoal 1 (ID 2) ============================ 2 + 2 = 4

This is telling you that Coq has 1 thing left to prove: 2 + 2 = 4. Click next, the bottom should change to:

1 subgoals, subgoal 1 (ID 2) ============================ 4 = 4

Coq processed the simpl tactic and now the thing it needs to prove is that 4 = 4. Obviously this is true, so if we click next…

No more subgoals.

reflexivity should succeed, and it does. If we click next one more time:

two_plus_two is defined

This says that this Lemma has been defined, and we can now refer to it in other proofs, much like we can call a function. Now, you may be wondering “do I really have to simplify 2 + 2?” No, you don’t, reflexivity will simplify on it’s own, this typechecks just fine:

Lemma two_plus_two: 2 + 2 = 4. Proof. reflexivity. Qed.

So, what’s the point of simpl then? Let’s consider a more complicated proof.


Lemma n_plus_zero_eq_n: forall (n : nat), n + 0 = n.

This lemma state that for any n, n + 0 = n. This is the same as when you’d write in some math. Other bits of new syntax is n : nat, which means that n has the type nat. The idea here is that no matter what natural number n is, n + 0 = n. So how do we prove this? One might be tempted to try:

Lemma n_plus_zero_eq_n: forall (n : nat), n + 0 = n. Proof. reflexivity. Qed.

One would be wrong. What is Coq stupid? Clearly n + 0 = n, Aristotle told me so! Luckily for us, this is a pretty easy proof, we just need to be explicit about it. We can use induction to prove this. Let me show the whole proof, then we’ll walk through it step by step.

Lemma n_plus_zero_eq_n: forall (n : nat), n + 0 = n. Proof. intros n. induction n as [| n']. { reflexivity. } { simpl. rewrite -> IHn'. reflexivity. } Qed.

Place the point at Proof and you’ll see the starting goal:

1 subgoals, subgoal 1 (ID 6) ============================ forall n : nat, n + 0 = n

Click next and step over intros n.

1 subgoals, subgoal 1 (ID 7) n : nat ============================ n + 0 = n

What happened here is intros n introduces the variable n, and names it n. We could have done intros theNumber and the bottom window would instead show:

1 subgoals, subgoal 1 (ID 7) theNumber : nat ============================ theNumber + 0 = theNumber

The intros tactic reads from left to right, so if we had some Lemma foo : forall (n m : nat), [stuff], we could do intros nName mName., and it would read in n, and bind it to nName, and then read in m and bind it to mName. Click next and evaluate induction n as [| n'].

2 subgoals, subgoal 1 (ID 10) ============================ 0 + 0 = 0 subgoal 2 (ID 13) is: S n' + 0 = S n'

The induction tactic implements the standard proof by induction, splitting our goal into two goals: the base case and the n + 1 case. Similarly to intros, this will create subgoals starting with the first constructor of an ADT, and ending with the last.

On Natural Numbers in Coq

Let us take a second to talk about how numbers are represented in Coq. Coq re-implements all types within itself, so nat isn’t a machine integer, it’s an algebraic datatype of the form:

Inductive nat : Set := | O : nat | S : nat -> nat.

O is zero, S O is one, and S (S (S (O))) is three. There is a lot of syntax sugar in place that lets you write 49 instead of S (S ( ... ( S O) ... )), and that’s a good thing.

The point of all of this is that we can pattern match on nat much like we can a list.

More Induction

…anyways, all this brings us back to induction and this mysterious as [| n']. What this is doing is binding names to all the fields of the ADT we are deconstructing. The O constructor takes no parameters, so there is nothing to the left of the |. The S constructor takes a nat, so we give it the name n'. Click next and observe the bottom change:

1 focused subgoals (unfocused: 1) , subgoal 1 (ID 10) ============================ 0 + 0 = 0

The curly braces “focuses” the current subgoal, hiding all irrelevant information. Curly braces are optional, but I find them to be very helpful as the bottom window can become very cluttered in large proofs. Here we see the base case goal being to prove that 0 + 0 = 0. Obviously this is true, and we can have Coq verify this by reflexivity. Click next until the next opening curly brace is evaluated. We see the next subgoal:

1 focused subgoals (unfocused: 0) , subgoal 1 (ID 13) n' : nat IHn' : n' + 0 = n' ============================ S n' + 0 = S n'

So, what do we have here? This is the n + 1 case; here the n’ in S n' is the original n. A particularly bored reader may try to prove forall (n : nat), S n = n + 1 and I’ll leave that as an exercise. However, this follows from the definition of nat.

Also of note here is IHn'. IH stands for induction hypothesis, and this is that n’ + 0 = n’. So, how do we proceed? Click next and observe how the subgoal changes:

1 focused subgoals (unfocused: 0) , subgoal 1 (ID 15) n' : nat IHn' : n' + 0 = n' ============================ S (n' + 0) = S n'

It brought the + 0 inside the S constructor. Notice that now there is n' + 0 on the left hand side. Click next and watch closely what happens:

1 focused subgoals (unfocused: 0) , subgoal 1 (ID 16) n' : nat IHn' : n' + 0 = n' ============================ S n' = S n'

Here we use the induction hypothesis to rewrite all occurrences of n' + 0, which was the left hand side of the induction hypothesis as n', which was the right hand side of the induction hypothesis. This is what the rewrite tactic does. Notice now that the subgoal is S n' = S n' which reflexivity will surely find to be true. So, what would happen if we had done rewrite <- IHn'.?

1 focused subgoals (unfocused: 0) , subgoal 1 (ID 16) n' : nat IHn' : n' + 0 = n' ============================ S (n' + 0 + 0) = S (n' + 0)

It rewrote all instances of n', which was the right hand side of the induction hypothesis with n' + 0 which was the left hand side of the induction hypothesis. Obviously, this isn’t what we want. I should note that you can undo this by rewriting to the right twice…

{ simpl. rewrite <- IHn'. rewrite -> IHn'. rewrite -> IHn'. reflexivity. }

…and it will technically work. But don’t do this, it’s silly and there’s no room for silliness in a rigorous mathematical proof.

Personally, I have a hard time keeping it straight what the left and right rewrites do. I sometimes find myself just trying one, and then the other if I guessed wrong. Think of it like this: rewrite -> foo rewrites the current goal, replacing all occurrences of the thing on the left hand side of the equation of foo with the thing on the right hand side of the equation. It changes from the left to the right. And vice-versa for rewrite <-, which changes from the right to the left.

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!

Getting Started With GLib in Emacs

Recently, I decided to start doing some C. In the past, I’ve used GLib in my C programs, and I’m a fan. I decided that I’d like to use GLib in my current endeavors. All that said, before I can use it, I have to be able to build it. Unfortunately, nothing in my life just works, so it took some configuring.

The Makefile

In my last post, I talked about creating a Makefile, and walked through it. I forgot one huge thing though: pkg-config!

Previously in DMP Photobooth, I used pkg-config to manage my library compiler flags. To that end, let’s make some changes to the Makefile I wrote previously. First, let’s refer back to what I wrote before:

COMPILE_FLAGS = -c -g -Wall -Wextra -std=c11 $(OPTIMIZE_LEVEL) LINK_FLAGS = -g -Wall -Wextra -std=c11 $(OPTIMIZE_LEVEL) LINKER_LIBS = -lSDL2 -ldl -lGL

It’s pretty straightforward. I have a compile flag set for compiling a .o, and for compiling a program. I also have a LINKER_LIBS variable to pass to the compile command. This isn’t part of the COMPLIE/LINK_FLAGS because the sources and object code being compiled must appear first or GCC complains. Now, let’s take a look at the new snippet:

COMPILE_FLAGS = -c -g -Wall -Wextra -std=c11 $(OPTIMIZE_LEVEL) \ $(shell pkg-config --cflags $(PKG_CONFIG_LIBS)) LINK_FLAGS = -g -Wall -Wextra -std=c11 $(OPTIMIZE_LEVEL) \ $(shell pkg-config --cflags $(PKG_CONFIG_LIBS)) PKG_CONFIG_LIBS = glib-2.0 gl sdl2 MANUAL_LIBS = -ldl LINKER_LIBS = $(MANUAL_LIBS) $(shell pkg-config --libs $(PKG_CONFIG_LIBS))

Things are getting just a bit more complicated now. You’ll notice there are three LIBS related variables. PKG_CONFIG_LIBS is the list of libraries to be passed to the pkg-config command. MANUAL_LIBS, as the name implies, is a list of manually configured -l strings. For the life of me, I couldn’t figure out what to pass to pkg-config to get it to spit out -ldl, so I’m forced to do it this way.

Regardless, LINKER_LIBS now contains the MANUAL_LIBS, and the output of $(shell pkg-config --libs $(PKG_CONFIG_LIBS)) which produces the necessary -l strings for all the PKG_CONFIG_LIBS.

On top of that, I’ve added the output of $(shell pkg-config --cflags $(PKG_CONFIG_LIBS)) to the COMPILE_FLAGS and LINK_FLAGS. This will ensure that if any pkg-config library needs special compiler flags, that they get used.

Great, now that’s done. A quick make, and everything seems to be working. We’re in business! …right?

Convincing Flycheck

If only it could be that easy. I created a new source and entered the following:

#include <glib.h>

Flycheck wasn’t convinced though; it put some red jaggies under this, and a quick mouse over of the error shows that flycheck doesn’t think that file exists. I began getting deja vu. After some googling, I determined that I can add arbitrary paths to flycheck-clang-include-path (I’m using the flycheck clang checker, if you’re using gcc this variable is going to be different. I’m guessing flycheck-gcc-include-path) to rectify the issue. To do this, enter:

M-x customize-variable [ENTER] flycheck-clang-include-path [ENTER]

This will get you a customize window for this variable. I added the following:

/usr/include/glib-2.0 /usr/lib/x86_64-linux-gnu/glib-2.0/include

…and things seem to be working fine. That said, I imagine if I get more involved in the GLib stack, I’m going to have to add all of these guys:


Not a huge deal, but I’ll cross that bridge when I come to it.

My Kingdom For a File Browser

As you may know, lately I’ve been trying to get used to using emacs. This has been going well, but there are some things I find myself missing from my old editors. One of them is the files list on the left side:


Sure, I can use dired, Speedbar, or any number of other solutions. But none of these work exactly like my old file browser. In despair, I got used to the C-x C-f Do [tab] c [tab] [tab] d [tab] p [tab] [tab] ... workflow that autocompletion brings us. However, it never quite settled with me.

Lately, I’ve found myself using org-mode in a way that has been quieting the proverbial fire. I’ve been able to use org-mode as a project browser, let me show you how!

Some Background

As you may know, org-mode is kind of a catch-all tool for organizing, note taking, and keeping todo lists. You can create hierarchical trees of headings. Hierarchical trees… Sound like anything we know?

I’ve been trying to use org-mode primarily as a TODO list to keep track of all the stuff I have going on. For projects that I’m working on, I’ve been creating TODO lists for the various source files I’m writing. A few links later, and we have the beginning of a project browser.

* TODO programming project

One of the nice things about tracking your own project is that you can decide what the tree looks like. An embedded project might group C and assembly source files separately, where a Haskell project might group source files by module nesting level.

Let’s talk C. We can create a file in the root of our project directory (where the Makefile is). Next, let’s create some headers:

* C * ASM * Unit Tests * Misc

Here, I’ve created 4 groups. C source goes in the C group, Assembly source goes in ASM, Unit test source files go in Unit Tests, and miscellaneous stuff like Makefiles, .gitignores, and READMEs go in Misc.

Next, let’s add some source files:

* C ** [[./main.c]] * ASM * Unit Tests * Misc

Here, I’ve added a link to main.c to the C group. At this point, this file doesn’t exist. If you click on main.c with org-mode enabled, the file will be opened in emacs, creating it if doesn’t exist! Sure, it’s manual, but I find it is not hard to keep up. If you commit your to your version control system, all members of the project can keep it updated and in sync.

However, what the manual updating buys you is the freedom to organize it how you like! We can add tasks to the tree:

* C ** [[./main.c]] *** TODO implement main *** TODO file header *** TODO add to git * ASM * Unit Tests * Misc

We can add deadlines:

*C ** [[./main.c]] *** TODO implement main DEADLINE: <2015-02-13 Fri> *** TODO file header *** TODO add to git * ASM * Unit Tests * Misc

We can add commentary:

* C ** [[./main.c]] *** TODO implement main DEADLINE: <2015-02-13 Fri> - I tried to implement main, but printf is such a hard function to use! I'll revisit this after I've had four beers... *** TODO file header *** TODO add to git * ASM * Unit Tests * Misc

…and this can lead to more tasks!

* C ** [[./main.c]] *** TODO implement main DEADLINE: <2015-02-13 Fri> - I tried to implement main, but printf is such a hard function to use! I'll revisit this after I've had four beers... **** TODO drink four beers *** TODO file header *** TODO add to git * ASM * Unit Tests * Misc

Let’s see your silly little file browser window do that!

Doing My Math Homework…

Well, it was bound to happen some day… Recently, a new quarter began, and with it new classes. One of said classes is a boolean algebra class, which means lots of fancy math runes to be drawn on pieces of dead trees. One problem though; homework in this class needs to be submitted as a .pdf online. Crap.

I’ve written about this sort of thing before, however, I also remember that being a gigantic hassle. Not to mention the fact that boolean algebra involves drawing logic gates, which is outside the scope of that. I decided it was high time I get onboard the LaTex train.

One Problem…

What problem? Learning LaTeX sounds like a huge hassle. I have enough problems without spending God knows how long learning a new markup language just to submit what would take 20 minutes to write on a piece of paper. In short: I don’t got time for that! Luckily for us, we have tools for this sort of thing.

Last month I wrote about giving Emacs a shot. So far, things have been going well. In fact, one tool that Emacs is known for, org-mode, is actually suited particularly well for this problem. I’ll spare you the basics, and just link to the excellent David O'Toole Org tutorial. If you are unfamiliar with org-mode, I suggest you go give it a read before continuing here.

…back? Good. Among the many things that org-mode is good for, it can be used to produce different kinds of output. Among them are html and our good friend LaTeX.

Document Structure

Let me assign some homework to myself, and we’ll work through it!

Show that AB + B'C + AC = AB + B'C without directly applying the Consensus Theorem

As you can imagine, AB + B’C + AC = AB + B’C because some fancy Consensus Theorem says so. Our task is to do stuff until the left-hand-side turns into the right-hand-side. And to do it in LaTeX!

First, we need to set up our document structure. Create a new file called, and create a heading:

* Show using boolean algebra:

This will create a new heading. Now, we need to do some boilerplate first. Add the following to the top of your file:

#+OPTIONS: toc:nil

This will prevent org-mode from creating a table of contents for your homework. I think a table of contents is silly for something with only a few pages, but it sure looks neat! Next, our equations will be automatically numbered, but we want them numbered by section. Add the following below the options line:


Now, let’s do some LaTeX. org-mode allows us to do inline LaTeX, and it will use it in the final document. Let’s add an equation block:

* Show using boolean algebra: \begin{equation} AB + \overline{B}C + AC = AB + \overline{B}C \end{equation}

If you save, then press: C-c C-e, then l o, your default .pdf reader should launch with a fancy new page that looks something like this:


Let’s do some more math! You can write comments inside of your heading, and they will be part of that section:

Apply identity law and complement law: \begin{equation} AB + \overline{B}C + AC(B + \overline{B}) \end{equation} Apply distributive law: \begin{equation} AB + \overline{B}C + ACB + AC\overline{B} \end{equation}

Re-export your new document and you should see something like this:


You may have noticed that we are basically done. Let’s write our answer down along with a fancy box so the professor knows it’s the answer:

\begin{equation} \boxed{AB + \overline{B}C} \end{equation}

And we’re done! If you export your document you should see:


I thought you didn’t want to learn LaTex…

I know, there’s a whole lot of LaTeX in there. But it could be worse, let’s take a look at the source file that org-mode creates:

% Created 2015-01-26 Mon 18:26 \documentclass[11pt]{article} \usepackage[utf8]{inputenc} \usepackage[T1]{fontenc} \usepackage{fixltx2e} \usepackage{graphicx} \usepackage{longtable} \usepackage{float} \usepackage{wrapfig} \usepackage{rotating} \usepackage[normalem]{ulem} \usepackage{amsmath} \usepackage{textcomp} \usepackage{marvosym} \usepackage{wasysym} \usepackage{amssymb} \usepackage{hyperref} \tolerance=1000 \author{Chris Tetreault} \date{\today} \title{homework} \hypersetup{ pdfkeywords={}, pdfsubject={}, pdfcreator={Emacs 24.3.1 (Org mode 8.2.10)}} \begin{document} \maketitle \numberwithin{equation}{section} \section{Show using boolean algebra:} \label{sec-1} \begin{equation} AB + \overline{B}C + AC = AB + \overline{B}C \end{equation} Apply identity law and complement law: \begin{equation} AB + \overline{B}C + AC(B + \overline{B}) \end{equation} Apply distributive law: \begin{equation} AB + \overline{B}C + ACB + AC\overline{B} \end{equation} \begin{equation} AB(1 + C) + \overline{B}C(1 + A) \end{equation} LHS now equals RHS, yay! \begin{equation} \boxed{AB + \overline{B}C} \end{equation} % Emacs 24.3.1 (Org mode 8.2.10) \end{document}

Yeah… Doesn’t seem so bad now. Thanks to org-mode, we can use just enough LaTeX to do what we need to do, and not have to worry about all that boilerplate!

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:



C-x u C-x u

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


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 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:


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

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


(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!

%d bloggers like this: