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



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.