How does one save and close a file in Proof General without all of Evil shutting down?

Question

I am using evil (emacs+vim). I am also using Proof General for the theorem prover Coq. I was trying to work with emacs but whenever I do:

:x

or

:q

in my coq .v file all of emacs closes as well (with all my buffers going down). I tried just pressing q on it own but it doesn't work.

I did:

C-x C-c

but that also kills everything and emacs it seems.

I also tried C-x 0 but it says:

Attempt to delete minibuffer or sole ordinary window.

Which doesn't mean much to me. I googled the error and got this Attempt to delete minibuffer or sole ordinary window which didn't clarify things to much.

Does anyone know how I can just close the current coq text file .v without having all of emacs close?

---

Now I have a new error that after I process part of the Coq script and try to save it and exit, the rest of the panes (buffers? frames?) where the proof context and errors messages are have not been closed...so I end up having to close stuff more times or get stuck...any help?

How do I close a Coq file without it not fully closing and staying within emacs?

---

To give some more context I am used to using Tmux with Vim + terminal. So doing :x closed my text file and saved it and sent me back to terminal. Thats why I expected it to close my text file but not close emacs (just like it wouldn't close my terminal). I am not saying I necessarily want this behaviour. Perhaps what the issue is that I don't understand what a typical/recommended emacs workflow looks like with ProofGeneral.

---

Ok, I tried doing what someone suggested which was not to close buffers. Fine. I tried that but now C-x C-f doesn't open files anymore cuz of ProofGeneral :(

Answer 1

I'm not sure why you expect :x or :wq to save and kill the buffer. From Vim's built-in help:

:[range]x[it][!] [++opt] [file]
            Like ":wq", but write only when changes have been
            made. [...]

:wq [++opt] Write the current file and quit.  Writing fails when
            the file is read-only or the buffer does not have a
            name.  Quitting fails when the last file in the
            argument list has not been edited.

:q[uit] Quit the current window.  Quit Vim if this is the last
        window.  This fails when changes have been made and
        Vim refuses to |abandon| the current buffer, and when
        the last file in the argument list has not been
        edited.

Clearly, :wq saves the buffer, however it either closes the window or quits the program. Apparently you only have one window open which explains why it quits Emacs for you. If you want different behavior, either find a command doing what you want or write your own. :bd is a good candidate here if you want to stick to Ex commands.