8000 GitHub - rocq-community/pocklington: Pocklington's criterion for primality in Coq [maintainer=@Casteran]
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

rocq-community/pocklington

Repository files navigation

Docker CI Nix CI Contributing Code of Conduct Zulip

Coq formalization of Pocklington's criterion for checking primality of large natural numbers. Includes a formal proof of Fermat's little theorem.

Meta

Building and installation instructions

The easiest way to install the latest released version of Pocklington is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-pocklington

To instead build and install manually, do:

git clone https://github.com/coq-community/pocklington.git
cd pocklington
make   # or make -j <number-of-cores-on-your-machine> 
make install
0