Download

The source code of the tool can be downloaded on the Ocaml forge.

Dependencies

Real2Float 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 and MathComp (optional)

If you are lazy, just install opam version 1.2.0, gmp, blas, lapack and run the following commands to install all the OCaml/Coq dependencies:

$ opam init --comp 4.02.1                                                                # Initialize OPAM with OCaml 4.02.1 

$ opam repo add coq-released https://coq.inria.fr/opam/released                          # opam repository for coq dependencies

$ opam install ocamlfind ocamlgraph zarith.1.2 lacaml.7.1.2 # install all the ocaml dependencies 

$ opam install coq.8.4.5 coq-ssreflect.1.5.0 coq-math-comp.1.5.0 coq-flocq.2.4.0 coq-interval.2.0.0 # install all the coq dependencies 

The Real2Float tool can be compiled using the following commands:

$ tar xzf real2float.tar.gz 

$ cd real2float

$ make

If no error is displayed, the executable file real2float 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).