Dear Coq users and more specifically ProofGeneral users.
The emacs (melpa) package of ProofGeneral (and the corresponding github master branch has been updated to support rocq-9 with or without the new CLI. It is probably still a bit rough on the edges and we would encourage gentle testers to give it a try. Note that Rocq is still named “Coq” everywhere in PG and it is not clear this will change soon for technical reasons. Bug reports welcome!