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.

4
  • 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, 2020 at 14:37
  • Thanks Dan. I'm trying to use Emacs for proving theorems in the Coq proof assistant along with Proof General (github.com/ProofGeneral/PG). I'm also using SSReflect which is a part of the Mathematical Components Library (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. Mar 11, 2020 at 7:42
  • Please let me know if you need any more information. Mar 11, 2020 at 7: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, 2020 at 10:16

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.