You can try it online in Binder.
Make sure that CoqIDE (8.6 or newer) is installed and
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.
All commands are run from the top level repo of this folder - where the
Install from PyPi:
Install from locally checked out source code:
pip install coq-jupyter python -m coq_jupyter.install
jupyter kernelspec uninstall coq pip uninstall coq-jupyter
Alternatively, use Conda to install both
coq_jupyter. For this,
install Conda (either Anaconda, Miniconda, Minimamba) and do:
$ conda config --add channels conda-forge $ conda create -n coq coq-jupyter $ conda activate coq
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 (
--coqtop-args to supply additional arguments to
coqtop when installing kernel. In this case you might also want to set custom kernel name/display name using
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"