How to disable Verilog mode in emacs?

Question

I am trying to use coq with ProofGeneral, but the built-in Verilog mode shadows *.v recognizes the file name. Can I somehow disable it and let ProofGeneral reassign them to coq mode?

Answer 1

You will have to override the binding in auto-mode-alist in your .emacs or something else.

This SO entry does something similar with VHDL:

How to disable vhdl mode in emacs?

Also, I googled for "auto-mode-alist remove" and found this link . Copy / Paste 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 am not familiar with ProofGeneral, but if I understand your question correctly, you need to change the auto-mode-alist variable to associate the correct file with files with the extension .v . 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

This may be an XY issue.

I have the same problem today, firstly, I tried the same thing as you, and add the following to 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 coma spacemacs layer is not installed automatically, and you need a lot of effort to install it, and it depends well.

The following is a brief description of the installation steps after successfully launching Coq on Emacs: https://gist.github.com/luochen1990/68e5e38496b79790e70d82814bdfc69a

Hope this is helpful :)