Poly/ML

polyml@lists.polyml.org

720 discussions

Interpretation of the profiler output data.
by kostirya＠gmail.com 19 Aug '16

19 Aug '16

Hello. There is profiler output for ProfileTime profileMode: 10 GARBAGE COLLECTION (total) 11 servers_stream(5)c_cb(1) 12 ForeignMemory.addFree(2) 12 VectorSliceOperations().subslice(3) 13 ForeignMemory.memoise(2)(1) 14 main_handle(1) 15 Int.scan(3)read_digits(3) 17 client_stream(7)to_channel(2) 18 ForeignMemory.memoise(2)(1) 23 client_stream(7)s_cb(1)(1) 29 ThreadLib.protect(3) 30 String.concat(1) 35 CoParser.takeStr(1)(1) 41 Substring.string(1) 109 CRC32.crcstringi(2)loop(2) 329 EV.kevent(4) 1132 Socket.recvVec'(3) Where can I get to know the meaning of these numbers? Best regards, Nick.

2 2

reasonably reliably inducing a "run out of store" runtime error in OSX with 5.6 (and a fix!?)
by Michael.Norrish＠data61.csiro.au 09 Aug '16

09 Aug '16

I don't have a small reproduction of the issue, but if you use bin/Holmake --qof with HOL4 at SHA1 6bf2bfd with the following file on a quiet (without much else running at the same time) Macbook Pro (OSX 10.11.6) open HolKernel boolLib bossLib Parse val _ = new_theory"foo248" val _ = Define`foo a b = a < b` val _ = overload_on("<:",``\a b. foo b a``) val _ = export_theory() then you will almost certainly get the following error out of Poly: Run out of store - interrupting threads The file is being read into Poly through a custom use function with its own lexer (to handle the backquotes) with calls to PolyML.compiler. If you add a semicolon at the end of the second line, you don't get the error. With just a bit of load, the error is harder to get. Michael

1 0

Performance of polyml compiler
by acn1＠cam.ac.uk 16 Jul '16

16 Jul '16

Let me start with a disclaimer and explanation. I wanted to have font metrics for a set of Unicode fonts available to some SML code. The metrics are extracted from the font by a cascade of programs and I already had code to inject them into C projects by creating files that went static font_info[] = { ... ... ... }; with MANY lines of simple static data. Doing things that way puts the metric data instantly available within my program. I modified things to create the same in SML and ended up with val metrics = Vector.from List [ Vector.fromList [a,b,c,d,e,f], Vector.fromList [a,b,c,d,e,f], .. ]; with around 10000 entries in the top level list. This was simple to do and in particular simpler both now and for when/if the code gets used by people. In particular simpler than anything that has SML code that reads the metric data from a resource file. And I am only interested in the metrics I have right now and am not concerned about future expansion there. Processing the input there works, but takes around 10 minutes of a reasonably fast desktop machine. That felt pretty bad. If I change the code to go (as it were) [[x,x,x,x] @ [x,x,x,x] @ [x,x,x,x]] at the top level with say 200 "x"s in each segment and 50 segments then the code is processed in more like 10 seconds rather than 10 minutes. This feels as if it is probably a really easy case where some aspect of processing lists in the input has been coded with quadratic growth rate in a way that is probably not necessary (the fact that the version segmented using "@" gets handled faster reassures me of that). A really easy demo if this is just val l = length [ Vector.fromList [0], ... ]; with 10000 entries in the list. I understand very happily that this is pathological code that nobody would ever write by hand and that as a way of handling data can be viewed as inflexible and crude. I am also happy that I can work round it using "@" and so it is not holding me up - but it felt as if it might be worth reporting and my expectation is that a very small change to the code would address it. I had looked and the code getList in SKIPS_.ML might have been the issue, but when I recode that to build the list backwards and then reverse at the end that does not unclog things, so the issue is at least one step deeper. Arthur

3 3

Socket.connectNB
by kostirya＠gmail.com 21 Jun '16

21 Jun '16

Hello, all. Socket.connectNB behaves oddly in Poly/ML. We get raise SysErr immediately after Socket.connectNB to a non-existent server. However, it is a nonblocking connect, so we should get information about unsuccesful connecton only after socket access. The source code is attached and here is the results for Poly/ML: > ./a.out exc in 2 socket: SysErr ("Connection refused", SOME ECONNREFUSED) exc in 3 socket: SysErr ("Connection refused", SOME ECONNREFUSED) exc in 4 socket: SysErr ("Connection refused", SOME ECONNREFUSED) . . ^C > ./a.out exc in 1 socket: SysErr ("Connection refused", SOME ECONNREFUSED) exc in 2 socket: SysErr ("Connection refused", SOME ECONNREFUSED) exc in 3 socket: SysErr ("Connection refused", SOME ECONNREFUSED) exc in 4 socket: SysErr ("Connection refused", SOME ECONNREFUSED) . . ^C We usually get errors in this situation. I've tested on Linix and FreeBSD. MLton and SML/NY don't get errors in the same situation. NIck.

2 4

not printed exception when executed file
by kostirya＠gmail.com 16 Jun '16

16 Jun '16

Hello. Why when executed file, exception is not printed? Is it OK? > cat foo.sml exception Ex fun main () = ( print "Start\n"; raise Ex; print "The End\n" ) > ( cat foo.sml ; echo 'val _ = main ()' ) | poly Poly/ML 5.6 Release Start Exception- Ex raised > polyc foo.sml && ./a.out Start > Best, Nick.

4 4

[isabelle] Opaque ascription for SML code generation
by dm＠prolingua.co.uk 13 Jun '16

13 Jun '16

Pretty-printing isn't part of the ML standard so it's not always clear how to do it properly. There have been various changes over the years. In particular, printing exception packets is difficult because the packet can contain values of types that exist only where the exception is raised. In the example below, "t" may not actually be exported from the signature. So, Poly/ML puts the print function that applies where the exception is raised into the exception packet and uses that if it needs to print the packet. There are no plans to change this. There have been some changes around the printing of types exported through opaque matching. When a structure matches a signature containing a type through opaque matching the semantics says that this creates a new type "name". Poly/ML creates a new ref to hold the pretty print function for the new type. Previously this was initialised to the pretty print function for the implementing type but this was changed in 5.6.1 to default to printing "?". It later became clear that this was too restrictive when the signature contained a datatype (e.g. "test" below) so there was a further change in commit 29985b1c in git master. So now if you install pretty printers both within the structure, (*1*) below, for the exception, and outside the signature (*2*) it will work as you expect. David On 12/06/2016 15:22, Makarius wrote: > After the Isabelle2016 release, we have discontinued SML/NJ and old > versions of Poly/ML, so there is a bit more flexibility now in canonical > patterns for Isabelle/ML. > > The example with structure A3 from above is the difficult one, notably > the situation "does not work (overrides pp for int)". Defining the pp > outside of the structure basically works, but exceptions are not printed > correctly. This is how the problem with opaque ascription was discovered > many years ago, and the abstype solution took over. > > > Here is an update of the example A3 from Stackoverflow above, using > Isabelle2016 with its bundled Poly/ML 5.6: > > ML ? > structure A :> > sig > type t > exception BAD of t > datatype test = Test of t > val a: t > val print: t -> string > end = > struct > > type t = int > > exception BAD of t > datatype test = Test of t > > val a = 42 > > fun print i = "{" ^ Int.toString i ^ "}" > > (*1*) > (*val _ = PolyML.addPrettyPrinter (fn _ => fn _ => fn x => > PolyML.PrettyString (print x))*) > end; > > (*2*) > (*val _ = PolyML.addPrettyPrinter (fn _ => fn _ => fn x => > PolyML.PrettyString (A.print x))*) > ? > > ML ?A.a; A.Test A.a; A.BAD A.a? > > > This leads to a mix of results, depending on the place where the pretty > printer is installed. > > I still don't see how to get a simple and robust pretty printer setup, > so we can't use opaque ascription ? unless David Matthews wants to > refine that again for a future release of Poly/ML. > > > Makarius > >

1 0

Foreign and cShort
by kostirya＠gmail.com 25 May '16

25 May '16

is it error? > cat foo.c short foo (short x) { return x+1; } > clang -shared -o foo.so foo.c > cat foo.sml open Foreign; val mylib = loadLibrary "foo.so" fun foo x = buildCall1 ((getSymbol mylib "foo"), cShort, cShort) x val r = foo ~5 val _ = print ( (Int.toString r) ^ "\n" ) > env LD_LIBRARY_PATH=. poly --script foo.sml 65532 P.S. Polyml is from git 5 days ago.

2 2

Some questions about Foreign
by kostirya＠gmail.com 25 May '16

25 May '16

Hello. I have some questions about Foreign. 1. How to convert OS.IO.iodesc (from socket) into cUint (uintptr_t)? 2. C function is need 'const struct timespec *timeout' argument. Where struct timespec is: struct timespec { time_t tv_sec; long tv_nsec; }; Do I understand correctly that this is cOptionPtr (cStruct2 (cInt32, cLong)) ? But how can I call this from polyml? I call as SAME (3, 0) and got error: Exception- Foreign "cOptionPtr must be applied to a pointer type" raised Best regard.

2 2

NetHostDB.fromString
by kostirya＠gmail.com 24 May '16

24 May '16

Hello. NetHostDB.fromString have error: > poly Poly/ML 5.6 Release > NetHostDB.toString (valOf(NetHostDB.fromString "127.0.0.1")); val it = "0.0.0.127": string > NetHostDB.toString (valOf(NetHostDB.fromString "10.0.0.34")); val it = "0.0.0.10": string > NetHostDB.toString (valOf(NetHostDB.fromString "10.1.1.34")); val it = "10.1.1.34": string MLton: > cat 1.sml val _ = print (NetHostDB.toString (valOf(NetHostDB.fromString "127.0.0.1"))) > mlton 1.sml > ./1 127.0.0.1>

2 2

Stack trace : condensed form
by artella.coding＠googlemail.com 15 May '16

15 May '16

Hi, is it possible to get a condensed stack trace where recursive calls are collapsed into one line in the printout of the stack trace? For example suppose that I have : *************************************************************** (* test.ml *) PolyML.Compiler.debug := true; open PolyML.Debug; breakAt("test.ml",12); fun is_divisible(n : int, currentDivisor : int) = if currentDivisor <= n - 1 then n mod currentDivisor = 0 orelse is_divisible(n, currentDivisor + 1) else false; (* This is line 12 *) fun is_prime(n : int) : bool = if n = 2 then true else not(is_divisible(n, 2)); fun main() = is_prime(11); *************************************************************** Then upon running as follows : > poly > use "test.ml"; > main(); test.ml line:12 function:is_divisible false; (* This is line 12 *) > stack(); > test.ml line:12 function:is_divisible test.ml line:8 function:is_divisible test.ml line:8 function:is_divisible test.ml line:8 function:is_divisible test.ml line:8 function:is_divisible test.ml line:8 function:is_divisible test.ml line:8 function:is_divisible test.ml line:8 function:is_divisible test.ml line:8 function:is_divisible test.ml line:8 function:is_divisible test.ml line:18 function:is_prime test.ml line:21 function:main test.ml line:4 function:? val it = (): unit debug > The recursive call to "is_divisible" takes up most of the space of the printout of the stack trace. Is it a possible to get a condensed form of this printout, for example something like : test.ml line:12 function:is_divisible test.ml line:8 function:is_divisible [***repeated 9 times***] test.ml line:18 function:is_prime test.ml line:21 function:main test.ml line:4 function:? Thanks

1 0

← Newer
1
...
16
17
18
19
20
21
22
...
72
Older →

Jump to page:

2026

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