Metalibm-lutetia is a child project of ANR Metalibm project developed in LIP6/UPMC by Christoph Lauter and Olga Kupriianova

Metalibm-lutetia is available on git clone

How to install and use Metalibm-Lutetia

Our Metalibm version is based on Sollya, a numerical tool for safe computations. In order to launch Metalibm, you have to install Sollya first.

To install Sollya you need
  1. Download and install the needed dependencies (could be found on the web-site)
  2. Download the latest version with git clone
  3. Inside the directory execute the following commands in the following order: ./autogen, ./configure, make
  4. Now you can launch Sollya with sollya command
The full documentation on Sollya commands is available by this link.

Once Sollya runs, you'll need Gappa formal proof tool available at Gappa web-site
Add to your .bashrc file pathes to Sollya and Gappa:
export PATH="$PATH:/SollyaPath/:GappaPath/"

After executing make in Metalibm directory, you can generate the functions. The default specification for the function can be found in a file problemdef.sollya. We advise you not to modify this file, but to make your own. You can run Metalibm on default specification file with the command "./metalibm.sollya" or run with your own file with "./metalibm.sollya myProblemdef.sollya"
Metalibm used to be developped by Arénaire is now developped by PEQUAN and written by Olga Kupriianova and Christoph Lauter using code contributed by Serge Torres and Nathalie Revol.
License: Metalibm is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.