I am trying to run emacs with proof generale to open Coq files. However, when I open emacs I get the following error message:
Symbol's value as variable is void: “/Users/myusername/.opam/default/bin/coqtop”
My emacs file is as follows:
(setq coq-prog-name “/Users/username/.opam/default/bin/coqtop”)
(require 'package) ;; (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") ; see remark below (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t) (package-initialize)
(custom-set-variables ;; custom-set-variables was added by Custom. ;; If you edit it by hand, you could mess it up, so be careful. ;; Your init file should contain only one such instance. ;; If there is more than one, they won't work right. '(package-selected-packages '(proof-general))) (custom-set-faces ;; custom-set-faces was added by Custom. ;; If you edit it by hand, you could mess it up, so be careful. ;; Your init file should contain only one such instance. ;; If there is more than one, they won't work right. )
Any advice on how to make my emacs work with coqtop?
Emacs treats “/Users/myusername/.opam/default/bin/coqtop” as a symbol because it's a sequence of ordinary characters. It does not start with an (ASCII) double quote, it starts with the character “ and ends with the character ”. They non-ASCII left and right double quotes. Use the ASCII quote ", which is the string delimiter in Emacs Lisp (and many other programming languages).
(setq coq-prog-name "/Users/username/.opam/default/bin/coqtop")
Don't edit source code with word processors that insert “smart quotes” and other features meant for text read by humans. The best place to edit your Emacs configuration is Emacs itself. Emacs knows what type of file you're editing and won't do such substitutions in programming modes (unless you've gone out of your way to configure it to do so, in which case, don't).