The Coq mailing list

[<dmitrii.pasechnik AT cs.ox.ac.uk>]

One working option is http://cloud.sagemath.com
Basically, in your browser you'd get a full-blown Ubuntu Linux console
interface,
with already installed Coq and ProofGeneral;
so you can run ProofGeneral/Coq in console emacs.
(and e.g. all the pre-reqs for https://github.com/UniMath/UniMath).

You have total flexibility to work with modified Coq versions (e.g. UniMath).

It should be possible and relatively easy to create a proper notebook-like
interface to Coq,
akin to ProofGeneral -- cloud.sagemath.com has such interfaces for
Python, R, Sage (a Python extension).

Best,
Dima