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



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




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