$\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}}$

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.
• $\ocaml$
• $\opam$ (optional)
• Mandatory $\ocaml$ libraries: ocamlfind ocamlbuild ocamlgraph zarith.1.2 lacaml.7.1.2. We highly recommend to install them with $\opam$.
• $\sdpa$
• $\coq$ with $\ssreflect$ (optional)
• $\sollya$ (optional)
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.