1

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.

Stefan
  • 26,154
  • 3
  • 46
  • 84
Vedant Chavda
  • 11
  • 1
  • Welcome to Emacs.SE! This question is hard to follow. Could you please provide more context for people to work with, and explain exactly what the relationship to Emacs is? – Dan Mar 10 '20 at 14:37
  • Thanks Dan. I'm trying to use Emacs for proving theorems in the Coq proof assistant along with Proof General (https://github.com/ProofGeneral/PG). I'm also using SSReflect which is a part of the Mathematical Components Library (https://math-comp.github.io/) in my project. Now if you want to import anything from SSReflect into your Coq project, you can do `Require Import ssreflect` or something like `From mathcomp Require Import ssreflect`. I think there's something related to the path from where Emacs gets the mathcomp folder, maybe we have to edit something in the .emacs file, I'm not sure. – Vedant Chavda Mar 11 '20 at 07:42
  • Please let me know if you need any more information. – Vedant Chavda Mar 11 '20 at 07:56
  • Please edit your original post and put the additional information in there. It will help readers identify your problem more easily. – Dan Mar 11 '20 at 10:16

0 Answers0