Proof General on Emacs

[dyoum117]

Is it possible to get a tutorial on installing Proof General? I know it's a lot to ask for, but I have been struggling to correctly install Proof General and there aren't many internet resources for it.

To be a bit more precise on where I'm stuck.

I have installed emacs correctly (at least I think I have) on my Windows computer. In my .emacs.d\init.el file, I type the following command

(load-file "Proof General directory....") and I continue to get the error on emacs that the file will not load.

[jeehoonkang]

I will upload my .emacs files; or please come to my office this Tuesday (tomorrow) 13:00-17:00 or 18:15-20:00.

Jeehoon

[jeehoonkang]

@dyoum117 Hi Danny! Would you please write some short tutorial on how to use ProofGeneral? Thanks!

Jeehoon

[dyoum117]

I apologize for such a late reply.

Installation instructions for Windows PC only.

1. Downloaded emacs24.4-bin-i686-pc-mingw32.zip from the following: (https://ftp.gnu.org/gnu/emacs/windows/).
2. Created directory structure in C drive as C:\emacs\emacs24.4-bin-i686-pc-mingw32
3. Set up environment variables so HOME: C:\emacs\
4. Ran addpm.exe from the C:\emacs\emacs24.4-bin-i686-pc-mingw32\bin directory to set up shortcut.
5. Ran runemacs.exe to run emacs for the first time. This should create .emacs.d directory inside C:\emacs\ directory.
6. Downloaded .emacs folder from @jeehoonkang to install Proof General on emacs. Unfortunately, I can't seem to find the URL to find @jeehoonkang's personal .emacs. If TA could repost link below, that'd be nice.
7. Copying and downloading TA's .emacs folder is probably best, but downloading Proof General and copying the following into init.el file in .emacs should also work.

;; ProofGeneral (load-file "~/.emacs.d/ProofGeneral-4.2/generic/proof-site.el") (setq-default coq-prog-name "C://Coq/bin/coqtop.exe") (setq-default proof-three-window-enable t) (setq-default proof-shell-process-connection-type nil) (add-to-list 'auto-mode-alist '(".*.v\'" . coq-mode)

"Error running timer `show-paren-function': (wrong-type-argument characterp nil)"

I received this error while I was using Proof General. This particular modification to .emacs will be needed to prevent a conflict between Proof General and show-paren-mode as indicated on the following issue (http://proofgeneral.inf.ed.ac.uk/trac/ticket/496)

(add-hook 'proof-ready-for-assistant-hook (lambda () (show-paren-mode 0)))

Basic Proof General and Emacs usage

If not familiar with emacs, go through the emacs tutorial on emacs itself.

Basic Proof General commands that will be needed.

ProofGeneral commands C-c C-n (next step) C-c C-u (undo step) C-c C-Enter (goto point) C-c C-l C-c C-b (use buffer)

@jeehoonkang

I'm still trying to figure out loading libraries into the loadpath. For example, on Induction.v, the first line is:

Require Export Basic.

I know that I have to compile Basic.v and get the object file. I have done that. But for some reason there seems to be a lot of errors on my side. At the moment though, I have made Proof General work. I will ask more specific questions regarding Proof General and update this tutorial.

[jeehoonkang]

@dyoum117 Thanks Danny! Feel free to ask questions. I will answer questions ASAP.

Jeehoon