Coq Environment

This notebook creates the default Coq environment in Nextjournal.

Setup

Build Environment

Install OCaml and a few dependencies.

apt-get -qq update
DEBIAN_FRONTEND=noninteractive apt-get install --no-install-recommends \
  ocaml bubblewrap aspcud \
  libexpat1-dev libgtk-3-dev libgtksourceview-3.0-dev
apt-get clean
rm -r /var/lib/apt/lists/* # Clear package list so it isn't stale
62.9s
Coq (Bash)
Jupyter Base

Download the OCaml package manager, OPAM.

URL="https://github.com/ocaml/opam/releases/download/${OPAM_VERSION}/opam-${OPAM_VERSION}-x86_64-linux"
wget --progress=bar:force -P /results $URL
2.1s
Coq (Bash)
Jupyter Base
opam-2.0.5-x86_64-linux

Install OPAM and use it to install Coq and CoqIDE.

mkdir -p $OPAMROOT
cp NJ__REF_ /usr/local/bin/opam
chmod a+x /usr/local/bin/opam
opam init -ay --disable-sandboxing
opam config env
opam pin add coq -y ${COQ_VERSION}
opam install -y coqide
1452.9s
Coq (Bash)
Jupyter Base

Install Jupyter, dependencies, and the Coq Jupyter kernel.

pip install future coq-jupyter
python3 -m coq_jupyter.install
5.5s
Coq (Bash)
Jupyter Base

Print info.

du -hsx /
coqc --version
jupyter kernelspec list
13.9s
Coq (Bash)
Jupyter Base

Test

Theorem hello_world : (forall A : Prop, A -> A).
Proof.
  intros A.
  intros proof_of_A.
  exact proof_of_A.
Qed.
0.8s
Coq Test (Coq)
Coq
Runtimes (2)
Runtime Languages (1)