Poly/ML October 2015

polyml@lists.polyml.org

8 participants
14 discussions

linking polyML modules to C
by dtopham＠gmail.com 09 Nov '18

09 Nov '18

After more experimenting with GUI in SML, I would like to now try calling an SML module from a C program. That way, the GUI could be built using traditional imperative techniques and the program logic could be written in SML. I see how to call a C function from SML, but and not so clear on how to call an SML function from a C program. I want to build code using polyc and then link with a C main program, but could anyone show me a simple example of calling that function and getting its return value? for example, I have defined: fun sum i n f = if i > n then 0.0 else f i + sum (i+1) n f ; fun int2real x = real x ; in linkToC.sml and #include <iostream> #include <fstream> std::ofstream ofs; int main() { std::cout << sum(1,10,int2real) << std::endl; ofs.open("table.dat"); for(int i = 0; i < 20; i++) ofs << i << '\t' << sum(1,i,int2real) << std::endl; } in linkToC.cpp Looking in the polyc script, I thought adding the -c option might allow me to build the object code which I could then link to the sml functions, but it complains about not having a main. Could someone point me in the right direction? Thanks, Dave On Mon, Dec 15, 2014 at 11:44 AM, David Topham <dtopham at gmail.com> wrote: > David, Thank you so much! I really appreciate your help with this. Your > sample below builds fine with polyc on my system (PolyML 5.5.2). I am using > a minimal Linux distribution named TinyCore ( > http://distro.ibiblio.org/tinycorelinux/) which comes with OpenMotif > 2.3.3 It runs in a virtual machine within another computer only taking up > a few hundred MBs! > > I am going to use it to help my students explore Discrete Math next > semester (this textbook uses SML for that purpose: > http://cs.wheaton.edu/~tvandrun/dmfp/). > > I also found a reasonably current project using PolyML and Motif here: > http://www.lemma-one.com/ProofPower/index/ > > ...however it was built on PolyML 4 and has not yet been ported to the > newer version (e.g. depends on PolyML.commit which no longer seems to be > supported). > > Happy Holidays to everyone in the PolyML community! > > -David Topham > > >> Re: GUI Interface (David Matthews) >> >> I've experimented with building a stand-alone executable with Motif and >> succeeded in getting it to work for me using polyc. (It required >> building Poly/ML with --with-x). I took the example from >> http://www.polyml.org/docs/Motif.html and wrapped it up in a function. >> I did find a problem, though. It looks as though the function has to >> suspend itself with something like Posix.Process.pause otherwise nothing >> happens. I seem to recall that the Motif stuff is handled on a separate >> thread to allow the REPL to continue to accept commands. With a >> stand-alone application there isn't a REPL so without the "pause" it >> terminates immediately. >> >> David >> >> open XWindows ; >> open Motif ; >> >> fun main() = >> let >> val shell = >> XtAppInitialise "" "xed" "Editor" [] [XmNwidth 400, XmNheight 400] ; >> >> val main = XmCreateMainWindow shell "main" [] ; >> >> val bar = XmCreateMenuBar main "bar" [] ; >> >> val fileMenu = XmCreateCascadeButton bar "file" [XmNlabelString "File"] ; >> val editMenu = XmCreateCascadeButton bar "edit" [XmNlabelString "Edit"] ; >> val viewMenu = XmCreateCascadeButton bar "view" [XmNlabelString "View"] ; >> val helpMenu = XmCreateCascadeButton bar "help" [XmNlabelString "Help"] ; >> >> val command = XmCreateText main "command" [XmNeditMode >> XmSINGLE_LINE_EDIT] ; >> >> val hscroll = XmCreateScrollBar main "hscroll" [XmNorientation >> XmHORIZONTAL] ; >> val vscroll = XmCreateScrollBar main "vscroll" [XmNorientation >> XmVERTICAL] ; >> >> val work = XmCreateDrawingArea main "work" [] ; >> in >> >> XtManageChildren [fileMenu, editMenu, viewMenu, helpMenu] ; >> XtManageChildren [bar, command, hscroll, vscroll, work] ; >> >> XmMainWindowSetAreas main bar command hscroll vscroll work ; >> >> XtManageChild main ; >> XtRealizeWidget shell; >> Posix.Process.pause() >> end; >> >> >> ------------------------------ >> >> _______________________________________________ >> polyml mailing list >> polyml at inf.ed.ac.uk >> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml >> >> End of polyml Digest, Vol 110, Issue 12 >> *************************************** >> >> -- >> The University of Edinburgh is a charitable body, registered in >> Scotland, with registration number SC005336. >> >>

2 3

Inspecting structures
by ramana.kumar＠gmail.com 27 Jan '16

27 Jan '16

Is there a way to look at the contents (i.e. signature) of a structure without opening it? (I suppose you could just open it then call a lot of PolyML.Compiler.forgetXXX, but that's quite tedious) Also, is it possible to retrieve the long path of an identifier in scope? Something that will, for example, take the rev in scope and say that it came from List. Finally, what about searching for an identifier that would come into scope if you opened some structures?

3 5

compressing heap images
by Japheth.Lim＠nicta.com.au 02 Nov '15

02 Nov '15

On 21/10/15, Gerwin Klein wrote: > It turns out that with our collection of large Isabelle sessions that we > run regularly, polyml heap image space is becoming a noticeable problem > for us. > We found another way to solve this problem. Isabelle uses saveState to save heaps. If we use saveChild instead, we get a substantial reduction in heap sizes. However, this makes the saved states less portable because they contain the pathname of the parent. Then loading will fail if the heaps are moved to a different path. Here it would be nice if Poly/ML could use relative paths for the parent, and look them up relative to the child. There are other ways to fix this (e.g. chdir before loadState) but I'd rather get the above behaviour from Poly/ML directly. Any thoughts? Japheth ________________________________ 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.

2 4

type real in polyml
by immler＠in.tum.de 30 Oct '15

30 Oct '15

Hi David, Thanks for your answer, I should have subscribed to the polyml mailing list earlier. Using the SSE2 instructions and/or setting the intermediate precision to 64 bit would give a nice and clear semantics to floating point expressions in Poly/ML, so I would be very much looking forward to such a change. Best regards, Fabian > Am 07.10.2015 um 15:56 schrieb David Matthews <David.Matthews at prolingua.co.uk>: > > 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 >>> >>> >>>

2 1

Nested use
by David.Matthews＠prolingua.co.uk 21 Oct '15

21 Oct '15

There's long been an issue with "use" when trying to compile and run files which themselves contain "use". For example if ROOT.ML contains: use "first.ML"; use "second.ML"; The inner calls to "use" are taken relative to whatever the original working directory was set to, which means that ROOT.ML always has to be called with the right directory. It's not possible to call use "/home/david/mydirectory/ROOT.ML"; from an arbitrary directory. I've committed a change to the NestedUse branch which is one possible solution to this. The version of "use" in there records the full path to the parent directory of the file name when a file is "used". If that file then contains a nested call to "use" the file is first checked as previously using the original working directory but if that fails it looks for the name by appending the parent directory to the name given. So in the example above, it would first look for "./first.ML" and only if that does not exist would it look for "/home/david/mydirectory/first.ML". This seems as though it should achieve the desired effect with the minimum change to existing programs but there are other alternatives. For example, should it look first relative to the parent directory? David

3 4

compressing heap images
by Gerwin.Klein＠nicta.com.au 21 Oct '15

21 Oct '15

It turns out that with our collection of large Isabelle sessions that we run regularly, polyml heap image space is becoming a noticeable problem for us. To give an impression, we are now daily generating hundreds of gigabytes of polyml heap images. We do this on SSDs, because they reduce build times significantly. For SSDs, hundreds of gigabytes is still a large percentage of total capacity. Raf noticed recently that simple fast compression such as LZO/liblzo works really well for disk heap images. We?re getting a size reduction to about 27% at speeds of about 400MB/s. Initially I thought we might write a little wrapper that compresses/decompresses as polyml writes/reads these images, but it?s awkward, duplicates path logic etc. Would this be something worthwhile to include directly in the polyml heap dumping process instead? That way it would not just benefit us, but everyone who uses Isabelle and other polyml-based sessions on SSDs. Cheers, Gerwin ________________________________ 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.

1 0

Profiling
by David.Matthews＠prolingua.co.uk 15 Oct '15

15 Oct '15

There has been some sort of profiling support in Poly/ML almost since the beginning. I have a feeling that the numbering system used in PolyML.profiling dates back to the old Poly language. There have been some recent changes to add support for yet another profiling mode, an option that profiles the time spent in a function but only for the calling thread, giving a way of separating out the work done in a multi-threaded application. It seemed like a good opportunity to revisit the whole thing. I've moved all aspects of profiling into a new structure PolyML.Profiling and removed the PolyML.profiling switch. The various options are now controlled by a datatype and there is a function "profile" that takes a mode, a function and an argument, runs the function by applying it the argument and prints the profile at the end. datatype profileMode = ProfileTime | ProfileAllocations | ProfileLongIntEmulation | ProfileTimeThisThread val profile = fn: profileMode -> ('a -> 'b) -> 'a -> 'b There are a couple of profiling modes that are a bit different since they print information about the state of the heap as the result of the previous computation. They are intended for use with PolyML.Compiler.allocationProfiling which causes the compiler to add extra information about where cells have been allocated. datatype profileDataMode = ProfileLiveData | ProfileLiveMutableData val profileData = fn: profileDataMode -> unit Finally there are additional versions of the functions that take an extra argument to enable an application (e.g. Isabelle) to capture the output from profiling. They take a function that is called with the unsorted list of counts and names. val profileDataStream = fn: ((int * string) list -> unit) -> profileDataMode -> unit val profileStream = fn: ((int * string) list -> unit) -> profileMode -> ('a -> 'b) -> 'a -> 'b David

1 0

incorrect canonical paths
by ramana＠member.fsf.org 15 Oct '15

15 Oct '15

Hi all, I just built Poly/ML fixes-5.2.2 (687b32704fdaffe013427962238482b786b666a4) fresh on a new machine with the following setup: uname -a Linux lemma 4.0.0-2-amd64 #1 SMP Debian 4.0.8-1 (2015-07-11) x86_64 GNU/Linux Now, if I go to a directory with non-lowercase name, I get a bad result: ramana at lemma:~$ mkdir TEST ramana at lemma:~$ cd TEST ramana at lemma:~/TEST$ poly Poly/ML 5.5.3 Testing > OS.Path.mkCanonical(OS.FileSys.getDir()); val it = "/home/ramana/test": string Why does Poly/ML think it is OK to lowercase filenames on this platform? Cheers, Ramana

2 2

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

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 October 2015