Poly/ML

polyml@lists.polyml.org

695 discussions

standard input contains a leading blank line? (5.5.2 with --enable-shared)
by michael.norrish＠nicta.com.au 28 May '14

28 May '14

If the following is foo.ML: fun doit () = let fun recurse i = case TextIO.inputLine TextIO.stdIn of NONE => () | SOME l => (print (Int.toString i ^ ": " ^ l); recurse (i + 1)) in recurse 1 end; PolyML.export("mytest", doit); and I then do $ poly < foo.ML $ cc -o mytest mytest.o -lpolymain -lpolyml $ echo "hello, world" | ./mytest I get 1: 2: hello, world as output. This is with a polyml 5.5.2 just downloaded from Sourceforge and configured with --enable-shared. I'm pretty sure this used to work (a minor feature of the HOL4 build process depended on it). Michael

2 1

Poly on MinGW
by rda＠lemma-one.com 25 May '14

25 May '14

I am trying to understand my options for using Poly/ML on MinGW for building windows applications coded in Standard ML. There is a bug reported in http://sourceforge.net/p/mingw/bugs/2043/ that you have to work around to build Poly/ML with the current MinGW. The work-around is to run configure with CXXFLAGS="-D_GLIBCXX_HAVE_FENV_H=1? in the environment. (I suspect I should also throw -O3 in there too, as I think that setting CXXFLAGS replaces its initial setting of -O3 inside the makefiles. Is that right?) Having got Poly/ML to compile, I found that polyc gives errors like the following when asked to compile a source file: gcc.exe: error: C:/DOCUME~1/rda/LOCALS~1/Temp/polyobj.2724.obj: No such file or directory If I create an object file from the Poly/ML GUI using PolyML.export, polyc will link it. If I understand what is going on correctly, the resulting program is a Windows application that brings up the Poly/ML GUI to provide the standard input, output and error channels, unless it is run with standard input and output connected to pipes, in which case it works like a pipe. I think I may end up having to package the Standard ML parts of my application as a server, with the GUI provided by clients implemented in some other language. Are there any other options? Regards, Rob.

3 7

Run out of store - interrupting threads
by David.Matthews＠prolingua.co.uk 18 May '14

18 May '14

This question arose from something on the isabelle-dev list but I think it's really of general interest. Currently Poly/ML only gives the "Run out of store - interrupting threads" message if it really cannot allocate the required memory after a full GC. This is actually rather unlikely for small cells. Instead as the amount of free space left in the heap gets smaller the GC runs more and more often. The ML code is still making progress but only very slowly. I wonder if there is a case for actually giving up at that point. Is it better to plough on in the hope that the program will complete or is it more helpful to produce a message and allow the user to try with more memory? This situation is most likely to happen if the heap space is restricted either because the address space limit has been reached in 32-bit mode or if the maximum heap has been set too low with --maxheap. David

2 3

Poly/ML 5.5.2 Released
by David.Matthews＠prolingua.co.uk 17 May '14

17 May '14

Since I haven't had any recent bug reports I've uploaded the current SVN snap-shot to SourceForge as version 5.5.2. Most of the changes are bug fixes. One major fix was to the intermediate code optimiser reported back in September. Other changes are the addition of PrettyStringWithWidth and PrettyLineBreak constructors to the PolyML.pretty datatype, Thread.Thread.numPhysicalProcessors to return the number of physical processors and printing ?.t in circumstances where t is bound to a different type. The debugger has been extended to include structures and the arguments to functors. As always, let me know if you find bugs or problems. David

3 9

polyc
by rda＠lemma-one.com 10 May '14

10 May '14

I have a couple of comments and a query about polyc (which seemed particularly attractive on Cygwin, where there seems to be quite a long list of libraries you need to know about if you are going to call the linker directly). The comment is that the help text is a bit misleading as it has more functionality than just compiling and linking a source file, e.g., you can pass it the name of an object file and it will link it with libpolymain and libpolyml. The query relates to the fact that polyc doesn?t do anything with LD_RUN_PATH (or DYLD_LIBRARY_PATH on Mac OS). Am I right in thinking that libpolyml will now always be statically linked so that you no longer to need to tell the dynamic linker where to find it? (For Poly/ML versions 5.5 and earlier the ProofPower makefiles that I am updating used to create an executable that linked libpolyml dynamically.) Regards, Rob.

4 4

Summer School on Advances in Programming Langauges
by eb120＠hw.ac.uk 14 Apr '14

14 Apr '14

Dear all, Find below the call for applications to attend the AiPL'14 Summer School. Apologies for multiple postings. =================================================== 2nd International Summer School on Advances in Programming Languages 19-22 August 2014, Heriot-Watt University, Edinburgh The 2nd International Summer School on Advances in Programming Languages offers four days of insightful lectures and lab sessions on an engaging blend of cutting-edge theoretical and practical techniques delivered by international experts. The topics include type systems and dependent types, novel programming models, and domain-specific languages, among others. The School is primarily intended for postgraduate research students and aims to foster international collaboration, and encourages a dialogue among early career researchers and renowned scientists. Important Dates: Application deadline: 30 April 2014 Notification: 15 May 2014 Speakers: Philip Wadler, University of Edinburgh Jeremy Gibbons, University of Oxford Fritz Henglein, DIKU, University of Copenhagen Rita Loogen, Philipps-Universit?t Marburg Hans Vandierendonck, Queen's University Belfast Jeremy Singer, University of Glasgow Conor McBride, University of Strathclyde Michele Weiland, Edinburgh Parallel Computing Centre Sven-Bodo Scholz, Heriot-Watt University Edinburgh Greg Michaelson, Heriot-Watt University Edinburgh Cost: 550 GBP - residential 350 GBP - no accommodation included Futher information is available at: http://www.macs.hw.ac.uk/~dsg/events/ISS-AiPL-2014/ =================================================== Evgenij on behalf of the AiPL'14 Organising Committee

1 0

Incorrect floating point conversion
by fw＠deneb.enyo.de 24 Mar '14

24 Mar '14

I noticed this: Poly/ML 5.5.1 Development > val a = 0.99999999999999972244424384371086489409208297729492187;; val a = 1.0: real > val b = 0.999999999999999722444243843710864894092082977294921876;; val b = 1.0: real > a < b;; val it = false: bool > a > b;; val it = false: bool So both values are equal according to Poly/ML. But the correct conversion for the first one is (in hexadecimal floating point notation) 0x1.ffffffffffffdp-1, and for the second 0x1.ffffffffffffep-1, so the values should be different.

4 4

[isabelle-dev] PolyML crashes
by michael.norrish＠nicta.com.au 03 Mar '14

03 Mar '14

I seem to be able to pretty reliably produce the following: Exception- InternalError: indirect - invalid constant address raised while compiling Exception- InternalError: indirect - invalid constant address raised while compiling Unfortunately, it takes hours to get there... Switching to --gcthreads=1 may have fixed another error we were having, relating to unwarranted pointer-equality tests. Michael On 21/02/14 22:30, David Matthews wrote: > Hi, > I'm aware of a number of assertion failures that seem to occur intermittently. > This is one of the ones on my list. I suspect they are all symptoms of the same > bug but I have never been able to narrow it down or reproduce it. It does seem > to occur when the memory management is under heavy load. > > Thanks for reporting it and if anyone manages to reproduce it more consistently > I would be very interested. > > Regards, > David > > On 20/02/2014 14:21, Ond?ej Kun?ar wrote: >> Hi! >> In the past couple of months I've gotten a crash of PolyML always with >> the same error message. I cannot reproduce the problem reliably but >> because it has already happened, let say, six times in the past three >> months, I am reporting the problem here: >> >> Unofficial version of Isabelle/HOL (unidentified repository version) >> poly: gc_mark_phase.cpp:432: virtual void >> MTGCProcessMarkPointers::ScanAddressesInObject(PolyObject*, >> POLYUNSIGNED): Assertion `baseAddr > (PolyWord*)obj && baseAddr < >> ((PolyWord*)obj)+length' failed. >> >> >> This refers to any changeset in the past three months. >> >> Best, >> Ondrej >> _______________________________________________ >> isabelle-dev mailing list >> isabelle-dev at in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ > isabelle-dev mailing list > isabelle-dev at in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

3 3

(Pseudo) static linking with C
by list.2006＠nul.jp 19 Feb '14

19 Feb '14

Hi, Although Poly/ML has nice interface for calling C functions, it only supports dynamic linking. <http://www.polyml.org/docs/CInterface.html> This is not pleasant if you want to distribute a program as a simple stand-alone executable. (setting the library path might be crumsy for the user) A solution would be 'linking statically but loading dynamically.' Actually, dlopen seems to support this if the filename argument is NULL. The following experiment (on Ubuntu 13.04 x86_64) seems to have succeeded, but needs a little modification to Poly/ML. How do you think? Any chance for Poly/ML to incorporate something similar? Best regards, -- KOBAYASHI, Tomoyas ===== patch ===== --- foreign.cpp.orig 2014-02-15 00:29:32.334802335 +0900 +++ foreign.cpp 2014-02-15 00:35:58.362818505 +0900 @@ -742,7 +742,7 @@ return res; #else /* UNIX version */ - void *lib = dlopen(name,DLOPENFLAGS); + void *lib = dlopen(*name == 0 ? NULL : name,DLOPENFLAGS); if (!lib) { char buf[256]; ===== experiment session ===== $ cat difference.c int difference (int x, int y) { return x > y ? x - y : y - x; } $ gcc -c difference.c -fPIC -o difference.o $ cat diff.sml local open CInterface in fun diff (n, m) = let val lib = load_lib "" val sym = load_sym lib "difference" val diff' = call2 sym (INT, INT) INT in diff' (n, m) end fun main () = print (Int.toString (diff (13, 50)) ^ "\n"); end $ poly Poly/ML 5.5.2 Testing > use "diff.sml"; val diff = fn: int * int -> int val main = fn: unit -> unit val it = (): unit > PolyML.export("diff.o", main); val it = (): unit > $ gcc -L ~/poly/lib -rdynamic diff.o difference.o -lpolymain -lpolyml -lstdc++ -lm -ldl -lpthread -lgmp $ ./a.out 37 $

2 2

Subsecond time in stat structures
by loganjerry＠gmail.com 18 Feb '14

18 Feb '14

I would like to propose a patch to PolyML (attached) that uses subsecond time fields in stat structures, when they are available. I think the patch is fairly straightforward. When I changed configure.ac by adding the AC_CHECK_MEMBERS macro, autoconf started whining at me about AC_CANONICAL_HOST being obsolete. Then it turned out that its replacement, AC_CANONICAL_TARGET, must appear before AM_INIT_AUTOMAKE, hence the slight rearrangement of macro calls there. Ignore that part if you like AC_CANONICAL_HOST. I am not sure of the best place to put the STAT_SECS and STAT_USECS macros. They seemed to me to be somewhat related to other definitions in io_internal.h, but perhaps there is a better place to put them. Anyway, this is more a proof of concept than a finished product. Feel free to mangle it to your heart's content. I won't be offended. :-) Regards, -- Jerry James http://www.jamezone.org/

2 2

← Newer
1
...
25
26
27
28
29
30
31
...
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