Blog

Customizing Emacs and coq

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


EMACS

0. Get MELPA

Add the following to ~/.emacs 

;; Add 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

Add the following to ~/.emacs 

(savehist-mode 1)

2. Let...

Read more about Customizing Emacs and coq

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:

Use mermelade or melpa:
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-...
Read more about Setting Emacs for mac

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...
  • Read more about Ocaml resources

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

    Read more about Einstein's Puzzle

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

    Read more about Balance and coins, analysis

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

    Read more about Balance and coins

    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,...

    Read more about Deduction Trees in LaTeX

    Solving 2048

    I recently stumbled upon this amazing puzzle: 2048 the puzzle.

    The idea is simple, use your arrow keys to push all squares in that direction. Equal squares will merge into larger numbers and a new square will appear in a random empty spot. You win if you create a square with the number 2048. For example in the image bellow you can press right to combine the 8's and move the two in that column to the right or press up to move the squares in the first...

    Read more about Solving 2048