CODEWITHSUNDEEP
emacspathcoqssreflectproof-general
Vedant Chavda
Vedant Chavda

Reputation: 3

SSreflect not working with Emacs, Coq and ProofGeneral. How to install SSreflect in MacOS?

If I do something like - From mathcomp Require Import ssreflect. it gives me the following error.

Error: Cannot load mathcomp.ssreflect.ssreflect: no physical path bound to
mathcomp.ssreflect

But if I do this instead - Require Import ssreflect. It compiles just fine. This is probably because I have ssreflect installed but not exactly the way I want.

But the thing is I want the first way to work, because I have a lot of programs written that way, and it doesn't seem logical to change the line in each and every one of them.

This is what I have in my .emacs file - (I think maybe I need to add anything like a path to mathcomp/ssreflect.. I don't know)

(load "~/.emacs.d/lisp/PG/generic/proof-site")

(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.
 '(coq-prog-name "/usr/local/Cellar/coq/8.10.2_1/bin/coqtop")
 '(package-selected-packages (quote (company-coq)))
 '(proof-three-window-enable t))

;; Load company-coq when opening Coq files
(add-hook 'coq-mode-hook #'company-coq-mode)

It would be really helpful to me if someone can help me to get From mathcomp Require Import ssreflect. working.

Upvotes: 0

Views: 193

Answers (1)

Cyril
Cyril

Reputation: 367

The recommended way to install non system versions of Coq is through opam cf https://coq.inria.fr/opam-using.html, mainly because it facilitates the installation of packages (such as mathcomp-* packages), and you can focus on a single problem at a time (coq vs emacs)

If you still decide to perform a custom install of Coq, and then of mathcomp, do not forget the make install step which is supposed to copy compiled library files to the subfolder user-contrib/ of your local install.

I noticed that in your original post, your .emacs config file sets "/usr/local/Cellar/coq/8.10.2_1/bin/coqtop" as the coq-prog-name while your terminal seems to use /usr/local/bin/coqtop, which might very well be two distinct versions of Coq. So if you compiled and installed mathcomp using this one, you will not have them for the other one.

Upvotes: 0

Related Questions