Skip to content


Folders and files

Last commit message
Last commit date

Latest commit



3 Commits

Repository files navigation


The current version of AutoG&P requires the C++ libraries NTL and libfactory, the Ocaml compiler and various Ocaml libraries. To use the interactive mode, Emacs and an extended version of Proof General are required. To install all dependencies, proceed as follows.

Ocaml compiler and C++ build dependencies


We recommend using homebrew to install most of the dependencies. The required commands are:

brew install opam
brew install libtool
brew install gmp
brew install libffi
brew link --force libffi
brew install pkg-config


Most distributions should offer packages for gmp and libffi. Make sure to install the development packages. Please follow the instructions on to install the opam package manager for Ocaml.

C++ libraries

To get the required C++ libraries, follow these instructions.

  1. download and install NTL from

On Linux:

cd src
./configure NTL_GMP_LIP=on SHARED=on
sudo make install

On OS X:

cd src
./configure NTL_GMP_LIP=on SHARED=on LIBTOOL="glibtool --tag=CC"
sudo make install
  1. download and install libfactory from

On Linux and OS X:

./configure --disable-streamio --without-Singular --disable-static
sudo make install

Compiling AutoG&P

We recommend cloning the AutoG&P repository, compiling the tool, and running it directly from the cloned directory. To achieve this, perform the following steps:

Clone the repos

# clone the AutoG&P repo
git clone
# clone the extended Proof General mode
git clone PG-AutoGnP

Compile and test AutoG&P:

cd AutoGnP
# tell the opam package manager to use the cloned repo
opam pin add autognp . -n
# install all Ocaml dependencies
opam install autognp --deps-only
# compile autognp
# run test-suite
make test-examples

Compile Proof General:

cd PG-AutoGnP
# use make EMACS=/Applications/
# if make fails

Configuring Proof General

Add the following lines to your .emacs with GIT_DIR replaced by the directory containing the cloned repos.

(load "GIT_DIR/PG-AutoGnP/generic/proof-site.el")
(setq autognp-prog-name "GIT_DIR/AutoGnP/autognp -emacs")

Now, you can test everything by opening examples/ok/bb1.zc in Emacs and executing regions of the file using Ctrl-c Ctrl-enter.


The examples can be found in examples/ok.

Status of current version

Currently, the extraction to EasyCrypt is disabled.