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 https://scm.gforge.inria.fr/anonscm/git/metalibm/metalibm-lutetia.git
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
- Download and install the needed dependencies (could be found on the web-site)
- Download the latest version with git clone https://scm.gforge.inria.fr/anonscm/git/sollya/sollya.git
- Inside the directory execute the following commands in the following order: ./autogen, ./configure, make
- 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:
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"
used to be developped by Arénaire
is now developped by
and written by Olga Kupriianova
and Christoph Lauter
using code contributed by Serge Torres
and Nathalie Revol.
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.