# Customizing Emacs and coq

Here are the things I add to my Emacs and coq, to have nice environment.

### EMACS

0. Get MELPA

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

You will need to restart emacs.

1. Remeber buffer history in emacs

(savehist-mode 1)

2. Let...

# How I set up my mac (brew, opam, emacs and coq)

I've had to switch computers a couple times, so here is what I do to get al my things started. I'll make another entry for further customization.

0. Open your terminal. All the commands bellow are for the terminal.

1. Install hombrew.

/usr/bin/ruby -e "\$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/master/install)"

2. Install wget:

brew install wget --with-libressl

​​​​​You can also do

brew install wget...

Read more about How I set up my mac (brew, opam, emacs and coq)

# Setting Emacs for mac

I've had a great experience using Aquamacs, until I installed company-coq which made it unbearably slow. So I'm switching to Emacs. The painfull part is that Emacs does not behave natively and needs some work to tune up. Here are some tricks:

1. Setting up the correct path:

M-x package-install-file RET exec-path-from-shell

Then add the following to .emacs:

(when (memq window-system '(mac ns))
(exec-path-from-shell-...

# Installing SML/NJ

I'm currently reading Modern Compiler Implementation in ML and I found that documentation for installing SML/NJ is not very good online. Here is how I did it.

1. Installation

I'm going to describe how to install SML/NJ using Homebrew, which I found to be very convenient. Obviously, you can download the latest version from the main site SMLNJ.

Just type in...

# Ocaml resources

This is a short list of resources to code comfortably in OCaml.

1. Package Managers and  main site:
• Homebrew (OS X package manager. To install OCaml and opam)
• OPAM (OCaml package manager. Install with homebrew)
• OCaml (Main webpage. Install with opam)
• Emacs mode and other...

# Einstein's Puzzle

This puzzle, also known as the Einsteins Riddle or the Zebra Puzzle, is often attributed to Albert Einstein, who supposedly predicted that only 2% of the world population would be able to solve. Such stories are likely false and the earliest known appearance of the puzzle is in a 1962 issue of Life International magazine. In any case, this puzzle is a challenging and fun one. So here it goes:

Along one road, there are five houses of different colors on a row. In each house lives a man with a different nationality, who smokes a different brand of...

# Balance and coins, analysis

In a previous post, I presented some examples of Balance and Coins puzzles. More than just challenging brain-teasers, those puzzles allow interesting formal analysis. Here I will try analyse them using some Information Theory.
Spoiler alert: This text will give strong hints on the solution of the puzzles. Make sure you have solved the...

# Balance and coins

"A long time ago, merchants from all corners of the world used balances to distinguish counterfeit gold coins..."

Whether history or fiction, the story of the merchant and the fake coin has inspired a large number of interesting puzzles. The main idea is always the same: a merchant has some gold coins some fair and some counterfeit. The fake coins have been made by a skillful thief and look identical to the real coins, except for their weight. The merchant has a balance that allows him to compare the weight of two groups of coins. Can he distinguish...

# Deduction Trees in LaTeX

I have been working with deduction trees and found irritating to write them in LaTeX. I know LaTeX is generally temperamental and frustrating but I found deduction trees to be far superior in their unnecessary complexity. If you need help adding new packages to LaTeX,...