Poly/ML November 2017

polyml@lists.polyml.org

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

Approaching release of 5.7.1
by David.Matthews＠prolingua.co.uk 30 Nov '17

30 Nov '17

We are approaching the point at which the current version of Git master is ready for release as Poly/ML 5.7.1. Version 5.7 introduced a number of significant changes and it has taken quite a bit of work since then to fix various bugs and sort out performance issues. I've been working with Makarius on dealing with those that affect Isabelle and we now seem to have dealt with everything. I'd like to ask everyone to try out the current version and let me know if there is anything that would stand in the way of a release. David

9 37

5.7.1 release candidate
by binghe.lisp＠gmail.com 21 Nov '17

21 Nov '17

Thanks, now I see something useful: $ echo foo | ./munge.exe The exported object file has version 5.71 but this library supports 5.70 (then it hangs) I have Poly/ML 5.7 installed in /usr/local (by Homebrew on Mac OS X 10.11), and the new 5.7.1 manually installed into $HOME. So I guess, when building `munge.exe` it must have been linked with libpolyml.a (or libpolymain.a) in /usr/local/lib because I didn?t put $HOME/lib into DYLD_LIBRARY_PATH (LD_LIBRARY_PATH on Linux). After completely removing Poly/ML 5.7 and rebuilding and installing 5.7.1 into /usr/local, the problem is resolved. Now munge.exe works correctly on my side. P. S. but multiple copies of Poly/ML actually worked well in all other cases, I normally use Poly/ML 5.6 (installed into a dedicated directory) to build HOL4 K11 release but never needed to build and run munge.exe from that version. Any way, sorry for disturbing. Regards, Chun > Il giorno 21 nov 2017, alle ore 12:18, Michael.Norrish at data61.csiro.au ha scritto: > > Those that passed are not tests of the munger per se: they are building the necessary background theories, and the munger executables. Those tests that you are trying to run are actually trying to execute the mungers. > > If you test a munger interactively with > > $ echo foo | ./munge.exe > > what do you see? > > Michael > > On 21/11/17, 19:52, "Chun Tian" <binghe.lisp at gmail.com> wrote: > > Hi, > > I rebuilt again with -t option. By default Holmake have 4 parallel threads, now all are blocked by munge tests: > > 501 60326 60299 0 9:48am ttys000 0:00.00 /bin/sh -c ./tymunge.exe < tyabb_input > tyabb_output > 501 60327 60326 0 9:48am ttys000 0:00.00 ./tymunge.exe > 501 60330 60299 0 9:48am ttys000 0:00.00 /bin/sh -c ./munge.exe < input > output > 501 60331 60330 0 9:48am ttys000 0:00.00 ./munge.exe > 501 60332 60299 0 9:48am ttys000 0:00.00 /bin/sh -c ./utymunge.exe < tyabb_input > utyabb_output > 501 60333 60332 0 9:48am ttys000 0:00.00 ./utymunge.exe > 501 60334 60299 0 9:48am ttys000 0:00.00 /bin/sh -c ./munge.exe < gh242_input > gh242_output > 501 60335 60334 0 9:48am ttys000 0:00.00 ./munge.exe > > However some munge tests indeed passed: > > Building directory src/TeX/theory_tests [21 Nov, 09:48:01] > Recursively calling Holmake in /Users/binghe/ML/HOL.stdknl/tools/cmp > Finished recursive invocation in /Users/binghe/ML/HOL.stdknl/tools/cmp > tyabbrevTheory OK > foo248Theory OK > bag248Theory OK > mdtTheory OK > untyabbrevTheory OK > pp248Theory OK > tymunge.exe OK > munge.exe OK > utymunge.exe OK > munge248.exe OK > > Regards, > > Chun Tian > >> Il giorno 21 nov 2017, alle ore 03:57, Michael.Norrish at data61.csiro.au ha scritto: >> >> Does HOL build with the -t option? >> >> This does some testing of the munging technology. >> >> Michael >> >> On 21/11/17, 10:03, "polyml on behalf of Chun Tian" <polyml-bounces at inf.ed.ac.uk on behalf of binghe.lisp at gmail.com> wrote: >> >> Hi Ramana, >> >> I found that ?munge.exe? (generated from theories) doesn?t work with this new Poly release: it simply hangs when converting *.htex to *.tex files ? and when I switched back to poly 5.6, it worked again. >> >> Can you confirm this on your side? >> >> ?Chun >> >>> Il giorno 20 nov 2017, alle ore 22:58, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> ha scritto: >>> >>> The 5.7.1 candidate appears to work for HOL4 and CakeML - I haven't done extensive tests, but normal builds seem fine. >>> >>> On 21 November 2017 at 08:41, Makarius <makarius at sketis.net> wrote: >>> On 20/11/17 14:23, David Matthews wrote: >>>> Thanks to everyone who sent in bug reports. We're almost ready to >>>> release 5.7.1. I've updated Git master ( 44b7b88 ) with pre-built >>>> compilers for 5.7.1. This is the last chance check it before the >>>> release which will probably happen at the end of the week. >>> >>> I have successfully built this version on Linux, Windows, mac OS, and >>> ran vorious manual tests of Isabelle + AFP. It all looks fine. >>> >>> Note that I will be on travel on Wed--Fri this week, so if there are any >>> last-minute issues, I cannot do any tests during these days. >>> >>> >>> Makarius >>> >>> _______________________________________________ >>> polyml mailing list >>> polyml at inf.ed.ac.uk >>> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml >>> >>> _______________________________________________ >>> polyml mailing list >>> polyml at inf.ed.ac.uk >>> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml >> >> >> > > >

1 0

5.7.1 release candidate
by David.Matthews＠prolingua.co.uk 20 Nov '17

20 Nov '17

Thanks to everyone who sent in bug reports. We're almost ready to release 5.7.1. I've updated Git master ( 44b7b88 ) with pre-built compilers for 5.7.1. This is the last chance check it before the release which will probably happen at the end of the week. David

5 4

5.7 Release
by David.Matthews＠prolingua.co.uk 11 Nov '17

11 Nov '17

I've finally got round to releasing version 5.7. The source code was actually tagged as 5.7 on Github a while ago and Github considered that a release. There are Windows installers for 32-bit and 64-bit as well as the normal source code for everything else. I'm aware that there are still some unresolved issues with this version but it seems to be stable enough for release. David

3 8

FW: Poly/ML output in LaTeX
by Michael.Norrish＠data61.csiro.au 09 Nov '17

09 Nov '17

On 9/11/17, 22:20, "Norrish, Michael (Data61, Acton)" <Michael.Norrish at data61.csiro.au> wrote: Start up with poly ?q and then emit a PolyML.print_depth 100 to get it back to printing things back to the user? Michael On 9/11/17, 20:42, "polyml on behalf of Timothy Bourke" <polyml-bounces at inf.ed.ac.uk on behalf of tim at tbrk.org> wrote: I wrote a simple LaTeX package [1,2] for exporting code snippets to validate them in an external tool and to import the resulting inferred types and error messages back into the document. Someone contacted me about supporting Poly/ML as an external tool. To do that properly, I need to resolve three issues : 1. Suppress the "Poly/ML 5.7 Release" banner on startup while still showing the inferred types (-q seems to suppress both). 2. Import a source file without showing the inferred types (PolyML.use seems always to show them). 3. Have Poly/ML terminate with a non-zero return code when an error is found (after printing the error message). Is it already possible to do such things? If not, would it be reasonable and worthwhile to add them? Tim. [1]: http://www.ctan.org/pkg/checklistings [2]: https://github.com/tbrk/checklistings

2 1

Poly/ML output in LaTeX
by tim＠tbrk.org 09 Nov '17

09 Nov '17

I wrote a simple LaTeX package [1,2] for exporting code snippets to validate them in an external tool and to import the resulting inferred types and error messages back into the document. Someone contacted me about supporting Poly/ML as an external tool. To do that properly, I need to resolve three issues : 1. Suppress the "Poly/ML 5.7 Release" banner on startup while still showing the inferred types (-q seems to suppress both). 2. Import a source file without showing the inferred types (PolyML.use seems always to show them). 3. Have Poly/ML terminate with a non-zero return code when an error is found (after printing the error message). Is it already possible to do such things? If not, would it be reasonable and worthwhile to add them? Tim. [1]: http://www.ctan.org/pkg/checklistings [2]: https://github.com/tbrk/checklistings

2 2

current git version crashes
by Michael.Norrish＠data61.csiro.au 08 Nov '17

08 Nov '17

As visible on our CI machinery at travis-ci.org, polyml?s latest git checkouts (Poly/ML 5.7 Release (Git version v5.7-283-g04d3c957)) are crashing when trying to build HOL. See for example https://travis-ci.org/HOL-Theorem-Prover/HOL/jobs/298998364 where the end of the transcript reads /home/travis/build/HOL-Theorem-Prover/HOL/bin/hol.state0 FAILED! <1> Loading /home/travis/build/HOL-Theorem-Prover/HOL/sigobj/boolLib error in quse /home/travis/build/HOL-Theorem-Prover/HOL/src/1/Prim_rec.sml : Fail "Exception- InternalError: codeToPRegRev raised while compiling" error in load $(HOLDIR)/src/1/Prim_rec : Fail "Exception- InternalError: codeToPRegRev raised while compiling" error in load /home/travis/build/HOL-Theorem-Prover/HOL/sigobj/boolLib : Fail "Exception- InternalError: codeToPRegRev raised while compiling" Loading /home/travis/build/HOL-Theorem-Prover/HOL/sigobj/boolLib: Fail "Exception- InternalError: codeToPRegRev raised while compiling" Exception- InternalError: codeToPRegRev raised while compiling Michael

1 0

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 November 2017