You can try it online in Binder.
Make sure that CoqIDE (8.6 or newer) is installed and coqidetop or coqidetop.opt (coqtop for Coq versions before 8.9.0) is in your PATH. Also, make sure the python command is recognized on your machine. If not, you can set up an alias for it e.g. python-is-python3 on Ubuntu.
Install with pip:
pip install coq-jupyter
python -m coq_jupyter.install
Uninstall with pip:
jupyter kernelspec uninstall coq
pip uninstall coq-jupyter
All commands are run from the top level folder of this repo (where Makefile is located).
Install from PyPi:
make
Install from locally checked out source code:
make install-local
Uninstall:
make uninstall
There are number of convenience improvements over standard Jupyter notebook behaviour that are implemented to support Coq-specific use cases.
By default, running cell will rollback any code that was executed in that cell before. If needed, this can be disabled on a per-cell basis (using Auto rollback checkbox).
Manual cell rollback is also available using Rollback cell button (at the bottom of executed cell) or shortcut (Ctrl+Backspace).
Use --coqtop-args to supply additional arguments to coqidetop/coqidetop.opt/coqtop when installing kernel. In this case you might also want to set custom kernel name/display name using --kernel-name/--kernel-display-name.
For example, to add kernel that instructs coqidetop to load /workspace/init.v on startup:
python -m coq_jupyter.install --kernel-name=coq_with_init --kernel-display-name="Coq (with init.v)" --coqtop-args="-l /workspace/init.v"
Give feedback with issues or gitter, send pull requests. Also check out CONTRIBUTING.md for instructions.