Proof General

See Proof General and scrupulously do as described at https://proofgeneral.github.io/download/. Using Melpa is the best way to go.

For what it’s worth

Here is a relevant fragment of the lecturer’s .emacs file

• in his Devuan-powered computers:

  (require 'package)
  ; (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") ;; for Version 26.1 of Emacs
  (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
  (package-initialize)
  
  ; Please there be 3 windows no matter the size of the screen:
  (setq proof-three-window-mode-policy 'hybrid)
  

• in his aging Ubuntu-powered computer:

  ;;;;;;;;;;
  
  ;;; the Coq Proof Assistant:
  
  (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
  ;; (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t)
  (setq coq-prog-name "~/coq-8.8.0/bin/coqtop")
  
  ;;;;;;;;;;
  
  ;;; Proof General
  
  ;; Open .v files with Proof General's Coq mode
  (load "~/.emacs.d/lisp/PG/generic/proof-site")
  (setq proof-three-window-mode-policy 'hybrid)
  
  ;;;;;;;;;;
  

• in his MacBook at work:

  (setq load-path (cons "/Users/danvy/.emacs.d/lisp" load-path))
  
  (load "~/.emacs.d/lisp/PG/generic/proof-site")
  

Using Proof General to interact with the Coq Proof Assistant

Upon opening a .v file, Prool General’s welcome banner is displayed for a few seconds. (If one is in a hurry, one can type C-l to see the content of one’s .v file straight away.)

In the top bar, of relevance are the Next button (C-c C-n) and the Undo button (C-c C-u) that process the next syntactic unit in the file (comment, command, declaration, tactic, etc.). The first time C-c C-n is issued, the Coq Proof Assistant is started, and 3 windows appear.

The Use button corresponds to issuing C-c C-n repeatedly until the end of the file.

If one’s cursor lies in the middle of the file, clicking on the Goto button (C-c C-return) makes the Coq Proof Assistant process the file until the cursor. (Reminder: return is the enter key.)

This being Emacs, typing C-x 2 splits the current window horizontally, which is useful to have 2 views of the same file.

More generally, typing C-h k invites one to type a key to then read a description of its effect. So for example, typing C-c C-l then tells us that “C-c C-l refresh[es] the display of windows according to the current display mode”.

Suggestions:

• when editing a .v file with the 3 windows open, type C-x 1 to make the 2 other windows disappear, and then type C-c C-l to make them reappear
• type C-h k and then C-x 1
• type C-h k and then C-x 2
• type C-h k and then C-x 3
• type C-h k and then C-c C-n
• type C-h k and then C-c C-u
• type C-h k and then C-c C-return

Pablito: Lemme type C-h k and then C-h k...

Mimer: That’s the spirit, Pablito!

Version

Created [15 Jan 2024]