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.
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.