Poly/ML April 2016

polyml@lists.polyml.org

6 participants
6 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

Posix implementation raising Fail exception
by Michael.Norrish＠nicta.com.au 25 Apr '16

25 Apr '16

As can be seen in https://travis-ci.org/HOL-Theorem-Prover/HOL/jobs/124717527 our use of Posix waiting is occasionally causing a Fail exception to be raised from inside the Posix implementation (there's no Fail exception with that message in our source code, and our code *is* doing a wait at that point). I'm afraid this doesn't seem easy to reproduce. 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 6

reliably crashing 5.6 on OSX 10.11.4
by Michael.Norrish＠nicta.com.au 25 Apr '16

25 Apr '16

The attached tarball (derived from a prefix of the HOL4 sources) reliably (every one of the tens of attempts I've made so far) crashes PolyML 5.6 on my Macbook Pro with Assertion failed: (save_vec_addr < save_vec+1000), function push, file save_vec.cpp, line 70. Abort trap: 6 Just change into the crashpoly directory and do poly --use usethis.ML If the call to Posix.Process.sleep in multiLib.sml is made for a much shorter length of time (pass 15 instead of 15000 to the genthms call, say), it works as expected. I also got 3/3 crashes with the time delay at 5000. I have tried to remove extraneous material from the tarball, but I'd be very surprised if it was minimal. 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

Assertion failure in scanaddrs.cpp
by lars＠hupel.info 15 Apr '16

15 Apr '16

Hi, I'm afraid I don't have a reproducible test case, but Gerwin Klein encouraged me to post and document this problem anyway. Using "polyml-5.6-1" bundled with Isabelle, we got the following assertion failure*: poly: scanaddrs.cpp:338: void ScanAddress::ScanRuntimeWord(PolyWord*): Assertion `w->IsDataPtr()' failed. $ uname -a Linux vm-10-155-208-88 3.16.0-4-amd64 #1 SMP Debian 3.16.7-ckt20-1+deb8u3 (2016-01-17) x86_64 GNU/Linux ML_OPTIONS="-H 8000" Cheers Lars * <https://ci.isabelle.systems/jenkins/job/isabelle-repo-makeall/131/console>

1 0

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

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