Getting started with Coq can be straightforward, using docker.
Installation
Put it in a docker container. Save this Dockerfile:
FROM ubuntu
RUN apt update; apt install -y coqThen build it:
docker build --tag coq .Installing the Latest Coq
The above instructions may give you a Coq version that is a little old.
To get the latest version, use opam (inside a container).
Instead of the above Dockerfile, use this one:
FROM ocaml/opam:alpine
RUN sudo apk add m4; opam install --yes coq
RUN sudo mkdir -p /workspace
WORKDIR /workspace
ENTRYPOINT ["opam", "config", "exec", "--"]Build it:
docker build --tag coq .This can take a long time to complete.
Run the Interactive CLI
The interactive CLI executable is called coqtop. Run it:
docker run --rm -ti coq coqtopYou should see a command line prompt like this:
Coq <To exit, type Quit. and hit enter (the final dot/period is needed because it terminates the expression):
Coq < Quit.That should leave the interactive CLI.
Mounting Local Files
Mount your current working directory to the /workspace folder in the container:
docker run --rm -ti -v $(pwd):/workespace coq ls -laThis way, the files in your local working directory are accessible to Coq inside the container, in its /workspace folder.
Compile and Import a File
Create a file with nothing but a comment in it. Call it Sample.v:
(* This is a comment. *)To compile that file, you normally run coqc Sample.v. To do this in the container, mount your current working directory to the /workspace, and run the same command:
docker run --rm -ti -v $(pwd):/workspace coq coqc Sample.vThat will take Sample.v and produce a compiled version, called Sample.vo.
If you look at your current working directory, you’ll see the new file:
ls -laNow you can start the interactive CLI again (be sure to mount your local working directory):
docker run --rm -ti -v $(pwd):/workspace coq coqtopThen load/import the compiled file by name:
Coq < Require Import Sample.If all works fine, you should see no errors.
