diff --git a/src/emacs/.gitignore b/src/emacs/.gitignore
new file mode 100644
index 000000000..d4691b73a
--- /dev/null
+++ b/src/emacs/.gitignore
@@ -0,0 +1 @@
+.cask
diff --git a/src/emacs/Cask b/src/emacs/Cask
new file mode 100644
index 000000000..8c078d9ec
--- /dev/null
+++ b/src/emacs/Cask
@@ -0,0 +1,14 @@
+(source melpa)
+(package-file "lean-mode.el")
+(development
+ (depends-on "cl-lib")
+ (depends-on "dash" 2.8.0)
+ (depends-on "dash-functional" "1.1.0")
+ (depends-on "f")
+ (depends-on "flycheck")
+ (depends-on "flymake")
+ (depends-on "fill-column-indicator")
+ (depends-on "whitespace-cleanup-mode")
+ (depends-on "lua-mode")
+ (depends-on "mmm-mode")
+ (depends-on "s"))
diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index 4b40aed92..0aab77fe7 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -1,13 +1,19 @@
+;;; lean-mode.el --- Emacs mode for Lean theorem prover
+;;
 ;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved.
+;;
+;; Author: Leonardo de Moura <leonardo@microsoft.com>
+;;         Soonho Kong       <soonhok@cs.cmu.edu>
+;; Maintainer: Soonho Kong   <soonhok@cs.cmu.edu>
+;; Created: Jan 09, 2014
+;; Keywords: languages
+;; Version: 0.1
+;; URL: https://github.com/leanprover/lean/blob/master/src/emacs
+;;
+;;
 ;; Released under Apache 2.0 license as described in the file LICENSE.
 ;;
-;; Author: Leonardo de Moura
-;;         Soonho Kong
 ;;
-;; URL: https://github.com/leanprover/lean/blob/master/src/emacs
-;; Keywords: languages
-;; Package-Requires: ((emacs "24") (dash "2.8.0") (dash-functional "1.1.0"))
-;; Version: 0.1
 
 (require 'cl-lib)
 (require 'eri)
@@ -210,3 +216,4 @@ Invokes `lean-mode-hook'.
     '(lean-flycheck-init)))
 
 (provide 'lean-mode)
+;;; lean-mode.el ends here