Learning Coq(Work in Progress)
I started dabbling in Programs and proofs recently by using Spacemacs and its Coq layer. Since I didn’t study this subject before I start by setting up and using the tools.
My primary learning material is CS6225 Programs and Proofs @ IITM (Coq + F*) but I will add more once I am past the preliminary stage.
Install Coq
During the installation of coq using homebrew an issue was identified which I reported here and it seems to have been fixed promptly.
coqc the compiler works like when it is invoked by C-c C-RET
There is something pleasing about this IDE.
IDE setup
The colour scheme of Spacemacs is very pleasing. I think. So Spacemacs is what I like to use whenever possible. The other options are VSCode and CoqIDE.
Install Proof-general
Proof-general is a generic Emacs interface for proof assistants.
Commands are M-x package-install and install-package
.spacemacs configuration
Enable the coq layer like this.
;; List of configuration layers to load.
dotspacemacs-configuration-layers
'(racket
javascript
;; ----------------------------------------------------------------
;; Example of useful layers you may want to use right away.
;; Uncomment some layer names and press `SPC f e R' (Vim style) or
;; `M-m f e R' (Emacs style) to install them.
;; ----------------------------------------------------------------
auto-completion
;; better-defaults
emacs-lisp
;; git
helm
(haskell :variables
haskell-enable-hindent-style "johan-tibell")
coq
;; lsp
;; markdown
multiple-cursors
;; org
(shell :variables
shell-default-height 30
shell-default-position 'bottom
shell-default-shell 'eshell)
;; spell-checking
;; syntax-checking
;; version-control
treemacs)I added add-hook to activate Company-coq to enable auto-completion features.
(defun dotspacemacs/user-config ()
"Configuration for user code:
This function is called at the very end of Spacemacs startup, after layer
configuration.
Put your configuration code here, except for variables that should be set
before packages are loaded."
( global-company-mode t)
(setq-default
dotspacemacs-configuration-layers
'((auto-completion :variables
spacemacs-default-company-backends '(company-files company-capf))))
(add-hook 'coq-mode-hook #'company-coq-mode)
)The auto-completion feature is powerful enough.
