Poly/ML

polyml@lists.polyml.org

695 discussions

tracing
by ramana＠member.fsf.org 13 Oct '15

13 Oct '15

Hi all, Does Poly/ML include any facility for tracing calls to (certain) functions? I am interested in generating a log of all calls to certain functions (including their arguments), in order, during the run of some program. Perhaps there is something in the profiler that can help with this? Cheers, Ramana

2 3

Using a finalizer with multiple arguments
by phil.clayton＠lineone.net 12 Oct '15

12 Oct '15

I am trying to create an SML binding to a C function that returns an array that the caller must free. Usually, there is a free function that takes just the array (as a pointer) which can be attached as a finalizer with CInterface.setFinal. I have encountered a case [1] where the caller must also pass the size of the array, returned when the array is created, to the free function. Simplifying the example, we have, for some C type Elem: Elem *new (..., int *n_elems); /* n_elems is an 'out' parameter */ void free (Elem *elems, int n_elems); and want an SML function like val new : ... -> elem vector Unfortunately, the function given to CInterface.setFinal is called with only one argument, the vol that is being finalized. Therefore this free function cannot be used. Does the current FFI architecture allow a variant of setFinal that passes extra arguments to the finalization function? For example: val setFinal1 : sym -> 'a Conversion -> vol -> 'a -> unit This isn't particularly common so is probably not a show-stopper. Another benefit could be enabling use of functions g_slice_alloc and g_slice_free1 that needs the number of bytes to free: https://developer.gnome.org/glib/stable/glib-Memory-Slices.html Thanks, Phil 1. The C function in question is gtk_target_table_new_from_list that returns an array and its size. The array should be freed with gtk_target_table_free which should be passed the size. See: - https://developer.gnome.org/gtk3/stable/gtk3-Selections.html#gtk-target-tab… - https://developer.gnome.org/gtk3/stable/gtk3-Selections.html#gtk-target-tab…

4 21

New Foreign Function Interface
by artella.coding＠googlemail.com 12 Oct '15

12 Oct '15

Hi, I was trying out the new foreign function interface that was committed today, and I find that if one tries to load a symbol that does not exist no error message is returned. For example in https://github.com/polyml/polyml/blob/598ff7841e5e155c1fff89bf75cd2a91ee779… if I do val sumTree2 = call1 ( getSymbol mylib "SumTreeDoesNotExist" ) cTree cInt; then no error message is reported. Then upon the call to sumTree aTree; an error is encountered and the program just terminates. Thanks

2 8

InternalError: AllocStore found but last allocation not complete
by phil.clayton＠lineone.net 08 Oct '15

08 Oct '15

After integrating the new Finalizable module in a library, I am getting an internal error from the compiler: Exception- InternalError: AllocStore found but last allocation not complete raised while compiling This affects Poly/ML 5.5.2 and the very latest commit with the compiler rebuilt (twice). An example is attached showing this. I have reduced this as far as I can but still a few small library files are required. The file 'polyml.sml' is the top-level file that uses the other files. Regards, Phil

2 3

Weak references
by ramana＠member.fsf.org 08 Oct '15

08 Oct '15

Hello, I am interested in using Poly/ML's Weak structure ( http://polyml.org/documentation/Reference/Weak.html) for hash-consing. The documentation would perhaps suggest that this is not an intended use of Weak, so I'd like to ask the list whether it is suitable and, if not, whether there are alternatives. An abstract of the problem is as follows. For a certain datatype, t, we want there to be at most one copy of any value of type t created by applying a constructor to unique arguments. To achieve this, we implement "hash-consing" constructors for t, which check whether the desired value exists already and return it if so, and only otherwise create a new value. To be able to check which values exist already, we maintain a hash table of all existing values. To allow values to be garbage collected when they are no longer needed, we make the hash table store only weak references to the values. The Weak structure allows weak references to be made to other references, but not to other non-reference values. Thus, the values in the hash table can be of type (t ref option ref), as produced by Weak.weak, but not of type (t option ref). Thus, on the face of it, it seems like using Poly/ML's Weak implementation will require unnecessary references and indirections. Is that indeed the case, or is Poly/ML smart about avoiding unnecessary indirections somehow? For hash-consing, we are not using Weak in the way described in its documentation, wherein the contents of the reference don't matter and the reference itself is only used as a token to track an external resource. Is there, perhaps, an alternative interface to Poly/ML's garbage collector more suitable for hash-consing? Cheers, Ramana

2 5

type real in polyml
by David.Matthews＠prolingua.co.uk 07 Oct '15

07 Oct '15

Hi Fabian, This was a bit bizarre particularly as when I tried it on Windows there didn't seem to be a problem. It is a problem with the precision and when rounding occurs. Poly/ML uses the old x87 floating point unit on both X86/32 and X86/64. As far as I'm aware all x86/64 machines support the SSE2 instructions so other compilers use SSE2 instructions on 64-bit but, by default use the x87 instructions on 32-bit. The x87 instructions use 80-bit registers internally and only round to 64-bits when the registers are stored to double-precision values. The SSE2 instructions are 64-bit so all the results are the same whether values are stored to memory or not. The x87 has bits in the control word that can allow it to compute intermediate results to 80-bit, 64-bit or 32-bit precision. The question is whether this should be set to 80-bit or 64-bits? Currently Poly/ML sets it to 80-bit precision at the start. As far as I've been able to ascertain that is what other x86/32 compilers do. The idea is, I suppose, to compute intermediate results to the best precision available. It does, though, produce the strange results that you've encountered. I think the reason for the difference in results is whether the function can be computed at compile-time or not. I'm coming round to the view that it should instead set the FPU to 64-bits so that intermediate results are the same whether they remain in the register or are written out to memory and reloaded. It looks as though the libraries in Visual C set that anyway which is why I only saw the problem when I tested on Linux. This would also mean that results would not change when, as I plan, I change to using the SSE2 instructions on x86/64. Best regards, David On 07/10/2015 14:07, Fabian Immler wrote: > Hi David, > > Perhaps I should rephrase my enquiry to: "Do I get any guarantees from the implementation of type real in PolyML"? > Naively, I would have expected, that every subexpression is evaluated according to the IEEE-754 standard (in double precision). > > I skimmed the implementation in libpolyml/reals.cpp, it looks like all intermediate results are stored in and retrieved from memory (real_arg, real_result). Is that sufficient to comply to IEEE-754? I.e., can there not occur "double rounding" (as in [1, section 3.3.1])? Or isn't there the need to use something like FLT_EVAL_METHOD=1 [2,3]? > > [1] http://www.springer.com/us/book/9780817647049 > [2] https://en.wikipedia.org/wiki/C99#IEEE.C2.A0754_floating_point_support > [3] http://www.cplusplus.com/reference/cfloat/ > > Best regards, > Fabian > > >> Am 07.10.2015 um 12:26 schrieb Fabian Immler <immler at in.tum.de>: >> >> Hi David, >> >> I noticed some strange behavior when working with type real in PolyML: >> In the following example, where I have "testres = twosum a", depending on whether I call >> "testres" or "twosum a" I get different results. >> >> If I take the definitions out of the structure Test, the results are the same. They are also the same if e.g. print-statements are inserted in between the assignments to b, s, sb and r. The results are also the same when evaluating inside Isabelle with the debugger turned on. >> >> Do you have an idea what is going on there? >> Is it possible that some intermediate results are kept in higher precision in the FPU? >> Does the compiler perform some "optimizations" on expressions of type real? >> >> Best regards, >> Fabian >> >> >> structure Test = struct >> >> fun one n = (if n = 0 then 100.0 else one (n - 1)); >> >> val a : real = one 1; >> >> fun twosum a = >> let >> val b = 1.0/1243313.0; >> val s = a + b >> val sb = s - b >> val r = s - sb >> in >> r >> end; >> >> val testres = twosum a; >> end; >> >> open Test; >> val a = twosum a >> val b = testres >> >> >>

1 0

polyc with different base executable
by Michael.Norrish＠nicta.com.au 24 Sep '15

24 Sep '15

It would be useful for HOL4 if polyc could be used with a different base executable. At the moment, the shell-script is hardcoded to use e.g., /usr/local/bin/poly. If HOL has created a different heap H with a lot of preloaded context, but for which the main function is still PolyML.rootFunction, creating a new heap H' that is a delta on top of H seems to become difficult: my impression is that all of the source files that went into generating H have to be re-used before the new stuff making up H' can be looked at. Or is there another way of getting what I need? I'd like to dispense with explicit calls in our own code to PolyML.export, and then needing to call the linker, but we do want to be able to build heaps in this way, layer by layer. Thanks, Michael ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

3 3

FFI overhead
by artella.coding＠googlemail.com 21 Sep '15

21 Sep '15

Hi, I thought that I would try to speed up the SML code at http://stackoverflow.com/questions/32425267/how-to-improving-array-benchmar… by using the FFI, but this results in significant slowdown. Non ffi code : ************************************************************************* ************************************************************************* ************************************************************************* val size:int = 50000; val loops:int = 30; val cap:int = 50000; val data = IntArray.array(size,0); fun loop () = let fun loopI i = if i = size then let val _ = () in IntArray.update(data,0,IntArray.sub(data,size-1)); () end else let val previous = IntArray.sub(data,i-1) val use = if previous > cap then 0 else previous in IntArray.update(data,i,use+1); loopI (i+1) end in loopI 1 end fun benchmarkRun () = let fun bench i = if i = loops then () else let val _ = () in loop (); bench (i+1) end in bench 1 end fun sum (i,value) = if i = size then value else sum(i+1,value+Array.sub(data,i)) fun main () = let val _ = () in benchmarkRun(); print (Int.toString (sum (0,0))); print "\n" end (*val _ = main ()*) ************************************************************************* ************************************************************************* ************************************************************************* FFI code : c code : ************************************************************************* ************************************************************************* ************************************************************************* //intArray.c #include <stdlib.h> #include <stdio.h> typedef struct _intArray { int size; int* arr; } intArray; intArray* createIntArray(int size){ int i; intArray* p = (intArray*) malloc (sizeof(intArray)); p->arr = (int*) malloc (size*sizeof(int)); for(i=0; i<size; i++){ p->arr[i] = 0; } p->size = size; return p; } void destroyIntArray(intArray* p){ free (p->arr); free (p); } void setIntArray(intArray* p, int elem, int val){ p->arr[elem] = val; } int getIntArray(intArray *p, int elem){ return p->arr[elem]; } int getSumIntArray(intArray* p){ int sum = 0; int i; int size = p->size; for(i=0; i<size; i++){ sum += p->arr[i]; } return sum; } ************************************************************************* ************************************************************************* ************************************************************************* ml code : ************************************************************************* ************************************************************************* ************************************************************************* open CInterface; val lib = load_lib "./intArray.so"; val get = get_sym "./intArray.so"; val PINTARR = POINTER; val c1 = call1 (get "createIntArray") INT PINTARR val c2 = call3 (get "setIntArray") (PINTARR,INT,INT) VOID val c3 = call2 (get "getIntArray") (PINTARR,INT) INT val c4 = call1 (get "getSumIntArray") (PINTARR) INT fun c_createIntArray (size) = c1 (size); fun c_setIntArray (p,elem,value) = c2 (p,elem,value); fun c_getIntArray (p,elem) = c3 (p,elem); fun c_getSumIntArray (p) = c4 (p); val size:int = 50000; val loops:int = 30; val cap:int = 50000; fun loop (pData2) = let fun loopI i = if i = size then let val _ = () in c_setIntArray(pData2,0,c_getIntArray(pData2,size-1)); () end else let val previous = c_getIntArray(pData2,i-1); val use = if previous > cap then 0 else previous in c_setIntArray(pData2,i,use+1); loopI (i+1) end in loopI 1 end fun benchmarkRun (pData2) = let fun bench i = if i = loops then () else let val _ = () in loop (pData2); bench (i+1) end in bench 1 end fun main () = let val pData = c_createIntArray(size); val final = load_sym lib "destroyIntArray"; in setFinal final pData; benchmarkRun(pData); print (Int.toString (c_getSumIntArray (pData))); print "\n" end ************************************************************************* ************************************************************************* ************************************************************************* The times are : a)for non ffi sml : 0.09s b)for ffi sml : 11.8s Is there any way I can improve the speeds on the ffi code? Thanks

3 4

Windows GUI and console
by David.Matthews＠prolingua.co.uk 15 Sep '15

15 Sep '15

The issue of the Windows console window has come up from time to time and I've had another look at the code and made a few minor changes. The first change is to provide an option to "./configure" to allow Poly/ML to be built as a "console" application rather than a "windows" application. Setting "--disable-windows-gui" passes -mconsole to the linker rather than -mwindows. This sets the appropriate bits in the EXE header. As well as affecting the linking of "poly" itself it also affects executables built with "polyc". The default remains "--enable-windows-gui" to build as a "windows" application. The second change is that when Poly is built as a Windows application, the default, it puts up a GUI window only if standard output has not been provided. Previously it put up a GUI window unless both standard input and standard output were provided. If it creates a GUI window for output it also uses it for input unless there is an explicit standard input provided. It may be helpful to provide a bit of background. I have the impression that there are two different classes of users when it comes to Poly/ML on Windows. Users from a Windows background expect the application to come with an installer, a Windows GUI and to support the standard copy-and-paste, in particular with the standard control-C/control-V key bindings. Users from a Unix background are much more used to running applications in a console window and are more likely to build applications from source. The problem is to satisfy both classes of user. Executables in Windows can be either "windows" or "console" applications depending on the "subsystem" setting in the EXE header. "console" applications are always started with a cmd.exe-style console unless they're already in a console. "windows" applications are expected to create their own GUI. My impression is that "console" applications are regarded as a legacy of DOS and not well supported. That's why I've made "windows" mode the default. Nevertheless there may be cases where someone would like to build "poly" as a console application which is the reason for adding the option. David

2 5

Fwd: Course programming language
by David.Matthews＠prolingua.co.uk 15 Sep '15

15 Sep '15

Well of course there is a Windows installer for the latest release version of Poly/ML at http://sourceforge.net/projects/polyml/files/polyml/5.5.2/ . The source for the installer is included in the source files but it needs Visual Studio and Wix ( http://wixtoolset.org/ ). David On 15/09/2015 15:00, Artella Coding wrote: > I saw your comment at > http://lists.inf.ed.ac.uk/pipermail/polyml/2015-September/001620.html > > "I have the impression that there are two different classes of users when > it comes to Poly/ML on Windows. Users from a Windows background expect the > application to come with an installer, a Windows GUI and to support the > standard copy-and-paste, in particular with the standard > control-C/control-V key bindings." > > and thought I would forward you the below, because it confirms what you say. > > ---------- Forwarded message ---------- > From: Andrej Bauer <andrej.bauer at andrej.com> > Date: Mon, Sep 14, 2015 at 7:20 PM > Subject: Re: Course programming language > To: Artella Coding <artella.coding at googlemail.com> > > > This is a completely different thing: until there is a Windows-style > installer where students just click through things it's a show > stopper. That is the reality of today's stdents (of math). > > On Mon, Sep 14, 2015 at 7:45 PM, Artella Coding > <artella.coding at googlemail.com> wrote: >> https://twitter.com/andrejbauer/status/643158821083418625 >> >> p.s. if you were also considering Standard ML you could try the > instructions >> David Matthew gave to build from source. >> >> http://lists.inf.ed.ac.uk/pipermail/polyml/2015-August/001593.html >> http://lists.inf.ed.ac.uk/pipermail/polyml/2015-August/001602.html >> >> All you need is msys2 and the rest is pretty seamless. >> >> >

1 0

← Newer
1
...
19
20
21
22
23
24
25
...
70
Older →

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

Poly/ML