This repository provides sources for a toplevel plugin to make Coq speak the
PIDE protocol. If you are looking for a release to go with PIDE, checkout the
PIDEtop branch (the default branch of this repository). 

The source code can also be downloaded as an archive from the [downloads page]( (Under the 'tags' tab).


If you have installed Coq using Opam, you can use Opam to install pidetop:


opam repo add pide
opam install pidetop

Alternatively, building by hand from these sources is driven by coq_makefile and make

$ export COQBIN=/your/path/to/coq/bin/

$ $COQBIN/coq_makefile -f Make > Makefile

$ make install-toploop

For Windows, we provide a [pre-compiled binary](, unpack the zip file in the toploop directory of the Coq installation directory (usually, C:\Coq\lib\toploop)


PIDEtop requires Coq 8.5


This software is available under LGPL license version 2.1 or at your option the MIT/X license.