-
Make sure you have all the prerequisites for compiling Coq. These are
OCaml,camlp5,git, andmake. If you want to build the HoTT version of the graphical user interfacecoqideyou also need thelablgtk2andlablgtksourceview2libraries. To get these, check your package manager. On Debian or any distribution with apt-get you can run the script./etc/install_coq_deps.shwhich installs the dependencies automatically. -
Get the HoTT library (skip this step if you already have it):
git clone https://github.com/HoTT/HoTT.git
cd HoTT
- From the HoTT directory run the following commands:
etc/install_coq.sh
./autogen.sh
./configure COQBIN="`pwd`/coq-HoTT/bin"
make
It may take a while to compile the custom Coq.
- You can now use the HoTT library in place by running
./hoqtopand./hoqc. You can also use./hoqidewhich is the version ofcoqiderunning thehoqtoptoplevel if you have compiled it successfully. If you want the commandshoqtop,hoqc,hoqideavailable system-wide, run:
make install