*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Problems with code generation for the reals*From*: Jesus Aransay <jesus-maria.aransay at unirioja.es>*Date*: Wed, 22 May 2013 11:48:25 +0200*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1305211433010.7058@macbroy21.informatik.tu-muenchen.de>*References*: <CAL0S8BfPE0=UT6e-zryCwvYqXaL99E7rNnbMZxnHUASJ4tFwig@mail.gmail.com> <517BCC93.50808@informatik.tu-muenchen.de> <CAL0S8BeMMQuVpfw5p3zDMfFaS9irN=BMLs76EJVxWyFppp=xOA@mail.gmail.com> <alpine.LNX.2.00.1305211433010.7058@macbroy21.informatik.tu-muenchen.de>*Sender*: jmaransay at gmail.com

Hi Makarius, the times compare as follows; a matrix of dimension 70 * 70 of real numbers (randomly generated, with entries between 0 and 1000) mapped to fractions of "IntInf.int" elements takes: - with MLton, 9 seconds to compile the stand-alone executable, 45 seconds of execution; - with PolyML 5.5 (the version dispatched with Isabelle 2013), 111 seconds of execution; - just for the record, with PolyML 5.2 (the version packaged for ubuntu), 350 seconds of execution. Thanks for your interest, Jesus On Tue, May 21, 2013 at 2:38 PM, Makarius <makarius at sketis.net> wrote: > 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 > > -- Jesús María Aransay Azofra Universidad de La Rioja Dpto. de Matemáticas y Computación tlf.: (+34) 941299438 fax: (+34) 941299460 mail: jesus-maria.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España

**References**:**Re: [isabelle] Problems with code generation for the reals***From:*Makarius

- Previous by Date: [isabelle] I/O error after "Isabelle build -o browser_info -v -c -a"
- Next by Date: Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy
- Previous by Thread: Re: [isabelle] Problems with code generation for the reals
- Next by Thread: Re: [isabelle] Probelm with the "definition" command
- Cl-isabelle-users May 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list