\( \def\sc#1{\dosc#1\csod} \def\dosc#1#2\csod{{\rm #1{\small #2}}} \def\nlcertify{\textrm{NLCertify}} \def\xb{\mathbf{x}} \def\ocaml{\sc{OCAML}} \def\coq{\sc{COQ}} \def\ssreflect{\sc{SSREFLECT}} \def\hol{\sc{HOL-LIGHT}} \def\sdpa{\sc{SDPA}} \newcommand{\sollya}{\mathtt{Sollya}} \def\opam{\sc{OPAM}} \)

Download

The source code of the tool can be downloaded on the $\ocaml$ forge.

Dependencies

$\nlcertify$ needs external software libraries to be compiled. Optional packages are also included in the following list and we recommend their installation. If you are lazy, just install $\opam$ and run the following commands to install all the $\ocaml$/$\coq$ dependencies:
$ opam repo add coq-released https://coq.inria.fr/opam/released                          # opam repository for coq dependencies
$ opam switch 4.02.1
$ opam install ocamlfind ocamlgraph camlp5.6.12 zarith.1.2 lacaml.7.1.2 coq.8.4.5 coq:interval.2.0.0 # install all the dependencies 
The $\nlcertify$ tool can be compiled using the following commands:
$ tar xzf nlcertify.tar.gz 
$ cd nlcertify
$ make
If no error is displayed, the executable file nlcertify is created in the main directory. Now, you can try it on sample problems.

Source code organization

The code includes $\ocaml$ files (.ml, .mll, .mly), $\coq$ vernacular files (.v). Some $\hol$ files (.hl) issued from the Flyspeck repository are also available.