Coq Environment

Setup

Build Environment

Install build tools, OCaml, and a few dependencies.

apt-get -qq update
DEBIAN_FRONTEND=noninteractive apt-get install --no-install-recommends \
  build-essential gfortran cmake automake libtool libltdl-dev pkg-config \
  ocaml bubblewrap aspcud libgtksourceview2.0-dev
apt-get clean
rm -r /var/lib/apt/lists/* # Clear package list so it isn't stale

Install OPAM (the OCaml package manager) from a copy downloaded in the Appendix, and then use it to install Coq and CoqIDE.

mkdir -p $OPAMROOT
cp 
opam-2.0.4-x86_64-linux
/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

Install Jupyter, dependencies, and the Coq Jupyter kernel.

pip install --upgrade jupyter jupyter_client future coq-jupyter
python -m coq_jupyter.install

Print info.

du -hsx /
coqc --version
jupyter kernelspec list

Test

Theorem hello_world : (forall A : Prop, A -> A).
Proof.
  intros A.
  intros proof_of_A.
  exact proof_of_A.
Qed.