Poly/ML March 2016

polyml@lists.polyml.org

8 participants
11 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

Unhandled errors in StateLoader::LoadFile
by matthew.fernandez＠gmail.com 04 Apr '16

04 Apr '16

Hi there, In StateLoader::LoadFile one of the final blocks has the comment "If we get errors just skip the error and continue rather than leave everything in an unstable state." When the reloc is corrupted sure, but the logic in this block seems to ignore errors in some places it shouldn't. In particular, shouldn't we return false when the initial fseek fails [0] or when an fread fails [1]? It seems to me that continuing in these cases causes us to either read garbage or an uninitialised stack variable. Am I missing something here? Thanks, Matt [0]: https://github.com/polyml/polyml/blob/master/libpolyml/savestate.cpp#L1051 [1]: https://github.com/polyml/polyml/blob/master/libpolyml/savestate.cpp#L1058

2 2

random 5.6 runtime errors
by Michael.Norrish＠nicta.com.au 01 Apr '16

01 Apr '16

As per, for example, https://travis-ci.org/HOL-Theorem-Prover/HOL/jobs/118129741 we are seeing "Out of store" aborts with builds that work fine under 5.5.2. The example above is on a Linux virtual machine. We've also seen them on real (i.e., not virtualised) OSX machines. Is there something obvious we might be doing that could be causing this? We're running all our sessions with --gcthreads=1 as per discussion in http://permalink.gmane.org/gmane.comp.lang.ml.polyml.general/976 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.

2 1

Basis Library: select for file descriptors
by Michael.Norrish＠nicta.com.au 01 Apr '16

01 Apr '16

I can see there is select for socket descriptors in the Socket structure, but it doesn't appear as if there is one for file_descs in the Posix structure. Am I right? Will my multiplexing file-manipulator just have to busy loop over the descriptors I have? 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.

2 2

Reducing the size of on-disk saved state
by matthew.fernandez＠gmail.com 31 Mar '16

31 Mar '16

Hi Poly folk, I am an Isabelle/HOL user interested in reducing the on-disk size of my Isabelle/HOL heaps. These are read and written via the save state functionality in Poly/ML. Saved states compress very well via conventional algorithms. On a representative Isabelle/HOL heap I see the following: $ ls -lh -r--r--r-- 1 matthew matthew 1.7G Feb 10 11:22 MyHeap -r--r--r-- 1 matthew matthew 279M Feb 10 11:22 MyHeap.bz2 -r--r--r-- 1 matthew matthew 331M Feb 10 11:22 MyHeap.gz -r--r--r-- 1 matthew matthew 173M Feb 10 11:22 MyHeap.xz I would like to propose integrating compression into the save state functionality itself. The runtime of Bzip and XZ are probably slow enough to irritate some users, but Gzip is reasonably fast for the benefit it shows. Gzipping saved states would require linking against zlib or something similar. David Matthews has suggested the save state code detect whether a state is compressed or not on loading and act accordingly, which would provide a nice transition path for users with existing saved states. I'm interested in hearing others' opinions about this proposal. If we feel this is something reasonable to do, I'll work on implementing this. When replying to this email, please CC me directly as I'm not subscribed to the list. Thanks, Matthew

5 15

playing with Posix fork/exec/dup2 etc
by Michael.Norrish＠nicta.com.au 18 Mar '16

18 Mar '16

Under 5.5.1, and after compiling with polyc, the code below gives an assertion violation and core dump: > $ ./a.out > In parent - reading > Assertion failed: (save_vec_addr < save_vec+1000), function push, file save_vec.cpp, line 70. > Abort trap: 6 (That's the OSX wording. I get something very similar under Linux.) I may well be making a hash of my POSIX programming, but I'd still hope for an exception rather than a core dump. Michael - - - - fun mkTIO_instream fd = let open Posix.IO val (flags,_) = getfl fd val rdr = mkTextReader { fd = fd, name = "", initBlkMode = O.anySet (flags, O.nonblock) } in TextIO.mkInstream (TextIO.StreamIO.mkInstream (rdr, "")) end fun main() = let open Posix.Process Posix.IO val {infd,outfd} = pipe() in case fork () of NONE => let val () = dup2{old = outfd, new = Posix.FileSys.stdout} val () = List.app close [infd, outfd] in exec("/bin/ls", ["ls", "."]) end | SOME pid => let val _ = print "In parent - reading\n" val strm = mkTIO_instream infd fun recurse () = case TextIO.inputLine strm of NONE => () | SOME s => (print ("Child: " ^ s); recurse()) in recurse(); wait(); print "Seen child's exit\n" end end - - - - ________________________________ 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

Poly/ML Changes History
by rda＠lemma-one.com 18 Mar '16

18 Mar '16

I thought there was a changes history for Poly/ML somewhere on the Poly/ML website, but I can?t find it any more. It would be useful to have a list of changes between Poly/ML 5.5.2 and Poly/ML 5.6. Apologies if I am just being unobservant. Regards, Rob.

3 3

Reproducible Builds
by jrtc27＠jrtc27.com 09 Mar '16

09 Mar '16

Hi, I?ve been working on making Poly/ML build reproducibly (https://reproducible-builds.org), specifically the Debian package, although it should be distro-agnostic. The first step was getting timestamps to be deterministic using SOURCE_DATE_EPOCH (see https://reproducible-builds.org/docs/timestamps/), and I have done this, both for libpolyml?s different export formats, and for PolyML.make. This was sufficient when disabling native code generation. However, using x86 native code generation, ioarea is not reproducible. Specifically, for every defined entry, the first word (which I believe is the length word?) differs, with the rest of the entry zero. An example (ioarea starts at 0x01029010; sizeof(PolyWord) is 8 and IO_SPACING is 8, so 0x01029050 is entry 1): 1 Hex??dump??of??section??'.?data?: ? 1 Hex??dump??of??section??'.?data':? 2 ????0x01029000??00000000??00000000??08900201??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 2 ????0x01029000??00000000??00000000??08900201??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 3 ????0x01029010??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 3 ????0x01029010??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 4 ????0x01029020??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 4 ????0x01029020??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 5 ????0x01029030??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 5 ????0x01029030??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 6 ????0x01029040??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 6 ????0x01029040??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 7 ????0x01029050??cc495964??797f0000??00000000??00000000??.?IYdy.?.?.?.?.?.?.?.?.?.?.? 7 ????0x01029050??cc1944ae??577f0000??00000000??00000000??.?.?D.?W.?.?.?.?.?.?.?.?.?.?.? 8 ????0x01029060??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 8 ????0x01029060??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 9 ????0x01029070??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 9 ????0x01029070??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 10 ????0x01029080??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 10 ????0x01029080??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 11 ????0x01029090??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 11 ????0x01029090??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 12 ????0x010290a0??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 12 ????0x010290a0??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 13 ????0x010290b0??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 13 ????0x010290b0??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 14 ????0x010290c0??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? 14 ????0x010290c0??00000000??00000000??00000000??00000000??.?.?.?.?.?.?.?.?.?.?.?.?.?.?.?.? Where are these coming from, and do you have any ideas for how to make sure they are reproducible? Regards, James

2 2

Echo code as well as output (David Matthews)
by dtopham＠ohlone.edu 06 Mar '16

06 Mar '16

That works perfectly for what I need...thanks David On Sun, Mar 6, 2016 at 4:00 AM, <polyml-request at inf.ed.ac.uk> wrote: > Send polyml mailing list submissions to > polyml at inf.ed.ac.uk > > To subscribe or unsubscribe via the World Wide Web, visit > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > or, via email, send a message with subject or body 'help' to > polyml-request at inf.ed.ac.uk > > You can reach the person managing the list at > polyml-owner at inf.ed.ac.uk > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of polyml digest..." > > > Today's Topics: > > 1. Echo code as well as output (David Topham) > 2. Re: Echo code as well as output (David Matthews) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sat, 5 Mar 2016 09:16:05 -0800 > From: David Topham <dtopham at ohlone.edu> > To: polyml at inf.ed.ac.uk > Subject: [polyml] Echo code as well as output > Message-ID: > <CAD034BEm3Yxrgx1OeZTz-r_sQkowpw51YY8-= > ni7-qaOiTCBQQ at mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > I am looking for a way to display the code as well as the output when > running SML. > > I believe it might be called "trace" or "log"... I did find this suggestion > online: > > PolyML.startLog > > but that seems to be deprecated? > > Is there another option? > > e.g. > > fun f x = x * x; > f 4; > just displays > val it = 16: int > > and I would like something like: > > f 4 = 16 > or similar to see what code was evaluated to get the 16 >

1 0

Echo code as well as output
by dtopham＠ohlone.edu 06 Mar '16

06 Mar '16

I am looking for a way to display the code as well as the output when running SML. I believe it might be called "trace" or "log"... I did find this suggestion online: PolyML.startLog but that seems to be deprecated? Is there another option? e.g. fun f x = x * x; f 4; just displays val it = 16: int and I would like something like: f 4 = 16 or similar to see what code was evaluated to get the 16

2 1

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 March 2016