Awesome Open Source
Awesome Open Source

PyPI version Conda version CI Tests Join the chat at https://gitter.im/coq_jupyter/community badge

A Jupyter kernel for Coq.

You can try it online in Binder.

Installation

Prerequisites

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 MAKE

All commands are run from the top level repo of this folder - where the Makefile lives.

Install from PyPi:

make

Install from locally checked out source code:

make install-local

Uninstall:

make uninstall

Step-by-Step Install

Install with pip:

pip install coq-jupyter
python -m coq_jupyter.install

Uninstall with pip:

jupyter kernelspec uninstall coq
pip uninstall coq-jupyter

Alternatively, use Conda to install both coqidetop and 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

Backtracking

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).

coqtop arguments

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"

Contributing

Give feedback with issues or gitter, send pull requests. Also check out CONTRIBUTING.md for instructions.



Alternative Project Comparisons
Related Awesome Lists
Top Programming Languages

Get A Weekly Email With Trending Projects For These Topics
No Spam. Unsubscribe easily at any time.
Python (888,878
Jupyter Notebook (178,660
Kernel (21,765
Conda (5,941
Coq (1,310
Dependent Types (235
Jupyter Kernels (130
Proof Assistant (124
Theorem Proving (111
Jupyter Extension (14