Originally written: November 9th, 2020

Recently, I've started using spacemacs in order to use proof-general, an Emacs plugin for proof-assitant languages. I started out using coqide, but decided to try Emacs for once, thinking it'd probably increase my productivity.

Besides, it's supposedly the best editor: as they say on their website:
e The best editor is neither Emacs nor Vim, it's Emacs and Vim!

Here are some tips that I've learned and googled while learning to use spacemacs (or just emacs).

General guide

This video provided with a great understanding of the basics of spacemacs.

dotspacemacs-default-font doesn't work

You probably need to install Source Code Pro.

Run this bash script:

                #!/usr/bin/env bash
                cd Downloads 
                if [ ! -d "~/.fonts" ] ; then
                    mkdir ~/.fonts 
                cp source-code-pro-*-it/OTF/*.otf ~/.fonts/
                rm -rf source-code-pro*
                cd ~/ 
                fc-cache -f -v 

How to zoom with keyboard?

Space z f + will allow you to zoom, but that's not really that convenient.

Use Ctrl x followed by Ctrl + or Ctrl -. Successive + or - will continue zooming.

Installing Proof General

The following are instructions for emacs26; they have not worked with emacs25 last time I tried it.

In ~/.spacemacs, edit the line dotspacemacs-additional-packages to:

                dotspacemacs-additional-packages '(proof-general company-coq)

If you are using Coq, you probably want .v files associated with coq instead of verilog, so append this line to ~/.emacs.d/init.el:

              (add-hook 'coq-mode-hook #'company-coq-mode)