Hi David and Matthew,
thanks for your encouraging answers. The SML code directly generated from Isabelle/HOL is available from the input [ADb] in the paper bibliography, in http://www.unirioja.es/cu/jodivaso/Isabelle/Gauss-Jordan/ under the link "View the generated code".
The matrices used for the benchmarks are in a zip file (9MB compressed, 160MB uncompressed) in the link "Download the benchmarks" in the previous website. Uncompressing the folder three different folders appear (RAT, REAL, Z2). In each of these folders there is a "Readme" file where we describe how we carried out the computations (we would be very glad to hear if there is a more proper way, both in MLton and Poly/ML).
The segmentation fault was raised with Poly/ML 5.5 trying to compute the matrix "Benchmarks/REAL/800_real.sml". There is also the issue of lack of performance from Poly/ML 5.5 to Poly/ML 5.2. As an example, the matrix "Benchmarks/REAL/200_real.sml" sums up 3.7 (processing) + 0.7 (executing) seconds with Poly/ML 5.5 and 31.0 (processing) + 0.4 (executing) seconds with Poly/ML 5.2 (the version shipped as an Ubuntu package); the same matrix in MLton took 9145.0 (processing) + 0.5 (executing) seconds.
Thanks in advance for your advice, do not hesitate to contact us for further questions,
Jesus
On Thu, Jul 25, 2013 at 4:59 PM, Matthew Fluet <matthew.fluet at gmail.com> wrote:
On Thu, Jul 25, 2013 at 8:03 AM, David Matthews <David.Matthews at prolingua.co.uk> wrote:
On 25/07/2013 11:29, Jesus Aransay wrote:
Jose Divas?n and I wrote a short paper for a Spanish workshop on functional programming ("Taller de Programaci?n Funcional 2013", http://babel.ls.fi.upm.es/tpf2013/) in which we test a SML program obtained with the Isabelle code generator tool to perform the Gauss Jordan elimination algorithm over matrices.
That is interesting work. Is it possible to get a copy of the code you ran for the various tests so I can check this out?
Seconded! I would love to investigate why MLton is performing so poorly on the input processing.
-Matthew
-- 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
-- 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