Coq in WSL (OPAM)

Quite a few of my students were having trouble with using Coq inside Windows, so here are detailed instructions on how to do that with WSL 2 and opam:
  1. Install the Windows Subsystem for Linux. This is as simple as running the following command from a PowerShell with admin priviledges:

    wsl --install

    The above installs Ubuntu by default (which is probably the easiest choice and what I use for my lecture setup), but you can find more customization options from Microsoft.

  2. Once you have Ubuntu set up, fire it up (and finish customizing username/password settings as needed).
    I highly recommend updating and upgrading the default packages. sudo apt update
    sudo apt upgrade
  3. Then install opam with the first script available at the opam installation website.

  4. Having opam install, try running

    opam init

    If everything goes right, you will be prompted that certain packages are recommended (make, cc) and required (unzip, bwrap).

  5. Install these packages using apt:

    sudo apt install make gcc unzip bubblewrap
    When installing gcc, you might get prompted about "missing packages". Run:

    sudo apt-get update

    and then try reinstalling gcc.
  6. Now you are ready to initialize opam: opam init

    This should take a while and install OCaml in your system. You will be prompted to add a couple of options to your .profile configuration file. I'd suggest doing that as it allows you to avoid having to type eval $(opam env) every time you open a shell.

    After opam is installed, to bring the current shell up to date, run:

    eval $(opam env)

  7. Install coq using opam with the instructions available here. For the Fall 2023 iteration of CMSC 631, the Coq version we will be using is 8.17.1 :

    opam pin add coq 8.17.1

    This could take a while, as it builds Coq from source. After it is complete, run "coqc" to ensure everything works:

    coqc -v

  8. Install emacs:

    sudo apt install emacs

  9. Install proof general using the instructions available here.

    At your home directory create a .emacs file and paste the (require ... initialize) stub from the website, then restart emacs and execute the package-refresh-contents and package-install commands. (M-x means pressing the Alt key together with 'x', similarly C- means Ctrl)

    Opening a .v file with emacs should now greet you with a proof general logo.


    10. At this point you should be good to go.
    But here are a couple more quality of life changes that make graphical applications run inside WSL actually readable:


  10. If you're running Windows 10, you need an external display server:

    vcxsrv: Back in your normal windows machine, install the VcXsrv X server for windows.

    Launch vcxsrv through xlaunch; select display 0 and "disable access controls" when prompted.
    Back in Ubuntu land, edit your .bashrc file by adding the following line. This tells ubuntu to use the xserver you just launched to display graphical applications.

    export DISPLAY=$(cat /etc/resolv.conf | grep nameserver | awk '{print $2}'):0

    If you're running Windows 11: you only need to edit your .bashrc file by adding the following line.

    export DISPLAY=:=0
  11. Launch a new ubuntu terminal (for the .bashrc changes to take effect). Run emacs in the background by adding "&" at the end:

    emacs file &

    This should open emacs in a new x window while allowing you to use the terminal for other things.

  12. Customize emacs. This is obviously a personal preference, but here is my default configuration, that you can include in your .emacs:

    ;;; Always newline in end of file
    (setq require-final-newline nil)

    ;;; Proper Indentations...
    (setq standard-indent 2)
    (setq-default indent-tabs-mode nil)

    ;;; Remove Backup File Creation
    (setq make-backup-files nil)

    ;;; Set background/foreground to black/white
    (set-background-color "black")
    (set-foreground-color "white")

    ;;; Aligning with C-= within a region
    (global-set-key (kbd "C-=") 'align-regexp)

    ;;; CUA mode for rectangles (This allows you to operate on multiple lines at the same time with C-RET)
    (cua-mode)
    (setq cua-auto-tabify-rectangles nil)
    (setq cua-enable-cua-keys nil)

    ;;; ido completion stuff (File-system completion)
    (require 'ido)
    (setq ido-enable-flex-matching t)
    (setq ido-everywhere t)
    (setq ido-file-extensions-order '(".v" ".tex" ".org" ".txt" ".py" ".emacs" ".xml" ".el" ".ini" ".cfg" ".cnf"))
    (setq ido-ignore-extensions t)
    (setq ido-auto-merge-delay-time 1000)
    (ido-mode 1)

    ;;; Proof General QoL (Disables startup screen and ensures the Coq buffers are on the "right")
    (setq proof-splash-enable nil)
    (setq proof-three-window-mode-policy 'hybrid)