[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

[coq] coq-mode doesn't work in emacs



Dear maintainer of Coq,

I'm using Debian testing and I noticed that Coq-mode packaged with coq
doesn't work.  The debugger says:

Debugger entered--Lisp error: (file-missing "Cannot open load file"
"没有那个文件或目录" "coq")
  coq-mode()
  set-auto-mode-0(coq-mode nil)
  set-auto-mode()
  normal-mode(t)
  after-find-file(t t)
  find-file-noselect-1(#<buffer b.v> "/tmp/b.v" nil nil "/tmp/b.v" nil)
  find-file-noselect("/tmp/b.v" nil nil t)
  find-file("/tmp/b.v" t)
  funcall-interactively(find-file "/tmp/b.v" t)
  call-interactively(find-file nil nil)
  command-execute(find-file)

I looked at /etc/emacs/site-start.d/50coq.el and found
  (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)

However, coq.el[c] was not found in /usr/share/emacs/site-lisp/coq. 
Instead, coq-mode is defined in gallina.el.  Indeed, changing that
autoload to (autoload 'coq-mode "gallina" "Major mode for editing Coq
vernacular." t) fixes this problem.

I am not sure if this is intentional as I didn't have this problem
before.  I hope you can consider fixing this problem.  Thanks!

Regards
_rika


Additional information that might be relevant:

~$ dpkg-query -W coq emacs
coq	8.6-5
emacs	1:26.1+1-3.2
~$ cat /etc/debian_version 
buster/sid
~$ dpkg -L coq | grep ^/usr/share/emacs/site-lisp/coq
/usr/share/emacs/site-lisp/coq
/usr/share/emacs/site-lisp/coq/coq-font-lock.el
/usr/share/emacs/site-lisp/coq/coq-inferior.el
/usr/share/emacs/site-lisp/coq/gallina-db.el
/usr/share/emacs/site-lisp/coq/gallina-syntax.el
/usr/share/emacs/site-lisp/coq/gallina.el




Reply to: