# Re: [isabelle] Problems with code generation for the reals

*To*: Jesus Aransay <jesus-maria.aransay at unirioja.es>
*Subject*: Re: [isabelle] Problems with code generation for the reals
*From*: Makarius <makarius at sketis.net>
*Date*: Tue, 21 May 2013 14:38:27 +0200 (CEST)
*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
*In-reply-to*: <CAL0S8BeMMQuVpfw5p3zDMfFaS9irN=BMLs76EJVxWyFppp=xOA@mail.gmail.com>
*References*: <CAL0S8BfPE0=UT6e-zryCwvYqXaL99E7rNnbMZxnHUASJ4tFwig@mail.gmail.com> <517BCC93.50808@informatik.tu-muenchen.de> <CAL0S8BeMMQuVpfw5p3zDMfFaS9irN=BMLs76EJVxWyFppp=xOA@mail.gmail.com>
*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Mon, 29 Apr 2013, Jesus Aransay wrote:

`I just wanted to add some figures about the performance of our algorithm
``computing the reduced row echelon form of a matrix; the algorithm is
``refined to "iarrays"
``(http://isabelle.in.tum.de/library/HOL/HOL-Library/IArray.html) to
``represent matrices. We implemented the algorithm over fields, and
``generated the ML code associated to the algorithm.
`

`We used MLton to compile the code and execute it over some instances of
``matrices; the results obtained when profiling are the following ones.
`

`The following are the results obtained for the very same matrix as in
``the previous example, but now the elements are labelled as being of type
``"real"; following the standard setup for code generation of reals they
``are generated in SML to fractions of "IntInf.int" (execution time gets
``multiplied by 100, most of the time is spent in computing quotients and
``remainders):
`

`Just curious: How does that compared to Poly/ML, instead of Mlton? It is
``important here to distinguish Poly/ML with GNU MP and without. (The
``version that is shipped with Isabelle2013 includes libgmp only for Linux,
``and it should work for Windows/Cygwin as well, but not for Mac OS X -- I
``did not know how to compile that in a portable manner.)
`
Makarius

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*