lean-mode customizations

lean-mode-customizations.el

;; jesse-michael-han's Emacs lean-mode hooks

;; append this to your init file (init.el or .emacs)

(require 'lean-mode)

(require 'lean-leanpkg)

(require 'smartparens)

(require 'company-lean)

(require 'yasnippet-lean)

(defun my-lean-insert-hole ()
  (interactive)
  (insert "{!_!}")
  (backward-char 3))

(defun my-lean-insert-french ()
  (interactive)
  (insert "‹_›"))

(defun lean-build-project ()
  (interactive)
  (let ((dir (file-name-as-directory (lean-leanpkg-find-dir-safe)))
        (lean-exe (f-full (lean-get-executable "leanpkg"))))
    (let ((default-directory dir)) (compile (lean-compile-string lean-exe "build" "")))))

(defun lean-test-project ()
  (interactive)
  (let ((dir (file-name-as-directory (lean-leanpkg-find-dir-safe)))
        (lean-exe (f-full (lean-get-executable "leanpkg"))))
    (let ((default-directory dir)) (compile (lean-compile-string lean-exe "test" "")))))

(defun lean-make-file ()
  (interactive)
  (lean-execute "--make"))

(defun my-lean-mode-hook ()
  (company-quickhelp-mode)
  (set-fringe-mode '(5 . 5)) ;; makes fringe larger so it's easier to see what lean is thinking about
  (yas-minor-mode 1)
  (local-set-key (kbd "C-c C-p C-f") 'lean-make-file)
  (local-set-key (kbd "M-p") #'company-complete)
  (local-set-key (kbd "C-c C-SPC") 'my-lean-insert-hole) ;; C-c C-SPC C-c SPC inserts a hole and opens menu of hole commands
  (local-set-key (kbd "C-c C-f") 'my-lean-insert-french)
  (local-set-key (kbd "C-c n") 'flycheck-next-error)
  (local-set-key (kbd "C-c p") 'flycheck-previous-error)
  (local-set-key (kbd "C-c C-s") 'sp-rewrap-sexp) ;; use for swapping implicit/explicitness of parameters
  (local-set-key (kbd "C-c C-p C-b") 'lean-build-project) ;; opens compilation-mode buffer with hyperlinks to errors
  (local-set-key (kbd "C-c C-p C-t") 'lean-test-project)
  (define-key lean-mode-map (kbd "C-c C-t") 'lean-diff-types)
  (lean-input-incorporate-changed-setting
   'lean-input-user-translations
   `( ("func" "⥤")
      ("McE" "ℰ")
      ("iP" "⨿")
      ("boxvert" "◫")
      ("no" "の")
      ("tf" "⟨╯°□°⟩╯︵┻━┻")  ))
  (column-number-mode)
  (sp-local-pair 'lean-mode "⟨" "⟩")
  (sp-local-pair 'lean-mode "⟦" "⟧")
  (smartparens-mode))

(add-hook 'lean-mode-hook 'my-lean-mode-hook)

It didn't find lean-leanpkg in MELPA, how to install it?

Oops, I think that require is extraneous. It should be available after lean-mode is installed.