How to disable Verilog mode in emacs?

Question

I'm trying to use coq with ProofGeneral, but the built-in Verilog mode shadows *.v filetype recognition. Can I somehow disable it and let ProofGeneral remap them to its coq mode?

Answer 1

You are going to have to override the binding in auto-mode-alist in your .emacs or whatnot.

This SO post does something similar with VHDL:

How do I turn off vhdl-mode in emacs?

Also, I googled for "auto-mode-alist remove" and found this link. Copy/Pasting the important bit:

;; Remove all annoying modes from auto mode lists

(defun replace-alist-mode (alist oldmode newmode)
  (dolist (aitem alist)
    (if (eq (cdr aitem) oldmode)
    (setcdr aitem newmode))))

;; not sure what mode you want here. You could default to 'fundamental-mode
(replace-alist-mode auto-mode-alist 'verilog-mode 'proof-general-mode)

Answer 2

I'm not familiar with ProofGeneral, but if I understand your question correctly, you need to modify the auto-mode-alist variable to associate the correct major with files with the .v extension. So, you need to add something like this to your .emacs file:

(add-to-list 'auto-mode-alist '("\\.v$" . proof-general-coq-mode))

Answer 3

The following line worked:

(setq auto-mode-alist (remove (rassoc 'verilog-mode auto-mode-alist) auto-mode-alist))

Answer 4

That might be an XY-problem.

I got the same problem today, firstly, I tried the same thing as you, I add following into my ~/.spacemacs under dotspacemacs/user-init:

(setq auto-mode-alist (remove (rassoc 'verilog-mode auto-mode-alist) auto-mode-alist))

And then the mode becomes fundamental, and then I realized that the real reason is that the spacemacs coq layer isn't installed automatically, and you need a lot of effort to install it and it's dependencies well.

Following is my summarize about the installation steps after I successfully run Coq up on Emacs: https://gist.github.com/luochen1990/68e5e38496b79790e70d82814bdfc69a

Hope this helpful :)