Poly/ML

polyml@lists.polyml.org

695 discussions

Exception- Subscript unexpectedly raised while compiling
by noschinl＠in.tum.de 17 Feb '14

17 Feb '14

Hi everyone, today I stumbled upon some strange behaviour of PolyML 5.5.1 (the x86-linux version shipped with Isabelle). The behaviour also occurred with revision 1874 from the SVN (Sourceforge has problems at the moment, so I didn't test the most current version). ------------------------------------------------------ # ./poly Poly/ML 5.5.1 Release > fun f xs = (xs : ''a) val _ = (fn x => f x); Exception- Subscript unexpectedly raised while compiling Exception- Subscript unexpectedly raised while compiling ------------------------------------------------------ But: ------------------------------------------------------ # ./poly Poly/ML 5.5.1 Release > fun f xs = (xs : ''a); val _ = (fn x => f x); val f = fn: ''a -> ''a ------------------------------------------------------ But: ------------------------------------------------------ # ./poly Poly/ML 5.5.1 Release > let fun f xs = (xs : ''a); val _ = (fn x => f x) in () end; Exception- Subscript unexpectedly raised while compiling Exception- Subscript unexpectedly raised while compiling ------------------------------------------------------ So the error vanishes, if I add a semicolon before the "val", except when I am in a "let" block. Moreover, the error seems to depend on the equality type and the dummy pattern. Best regards, Lars

2 2

printInAlphabeticalOrder
by rda＠lemma-one.com 13 Feb '14

13 Feb '14

I am confused about what PolyML.Compiler.printInAlphabeticalOrder is intended to control. If I enter the following: signature S = sig val x : int val z : int val y : int end; structure S = struct val x = 1 val z = 3 val y = 2 end; the signature and the structure are both printed with the variables in reverse alphabetical order. (I was rather hoping for an option to have them in the source code order.) Regards, Rob.

2 1

Pretty-printing infix constructors
by Rda＠lemma-one.com 06 Feb '14

06 Feb '14

When I executed the following infix xxx; datatype XXX = op xxx of int * string; 1 xxx "banana"; I was rather hopping the expression at the end would print out with infix notation but it doesn't: val it = xxx (1, "banana"): XXX Is there an option in Poly/ML to have infix constructors print as infixes, or do I need to write my own pretty-printer to get that. Regards, Rob.

2 1

PolyML.pointerEq
by Brian.Campbell＠ed.ac.uk 05 Feb '14

05 Feb '14

What semantics, if any, does PolyML.pointerEq have? In particular, is it supposed to be guaranteed that if pointerEq (x,y) is true, then it will remain true after GC? My reason for asking is that I've been having trouble with assertion failures in HOL when reducing large terms. The assertions check that the left hand side of the conclusions of two theorem objects are equal according to pointerEq, because this allows a fast comparison that "should" always be true if the theorem is manipulated carefully. I'm fairly certain the assertion failures are related to GC: they are non-deterministic on code that ought to be deterministic, and vary in frequency across different machines. (I haven't seen it at all on a 4GB 32-bit machine, rarely on 4GB 64-bit, often on the 8GB I normally use and infrequently on a compute server with much more.) There's no sign of any data corruption, however. Brian

3 4

checking --enable-shared from within the REPL
by David.Matthews＠prolingua.co.uk 14 Jan '14

14 Jan '14

On 13/01/2014 22:31, Michael Norrish wrote: > I'll look at the relevant lib directories; thanks. > > The reason is that the HOL build process wants to create executables (for > mlyacc, mllex and others), and doing so without --enable-shared will fail > mysteriously. If I can cut this off at the pass, I can provide better error > messages. There was a problem that I discovered with making --disable-shared the default that I hadn't anticipated. It seems that when linking with the static library it is necessary to include some extra libraries (e.g. gmp) that are used within libpolyml. These don't seem to be needed when linking with the dynamic library so presumably they have already been linked into the dynamic library. > I confess I haven't properly looked at polyc; would this give us a uniform approach? That is the intention. "polyc" is written as part of the process of building "poly" and should include all the libraries that are needed. Regards, David

1 0

checking --enable-shared from within the REPL
by michael.norrish＠nicta.com.au 13 Jan '14

13 Jan '14

Is there any way to detect if the system has been built with --enable-shared? Something in the PolyML structure (say)? I'd like to be able to have my build script abort if the PolyML hasn't been built correctly. Or is there anything obvious my script could check in the file system to make this determination? Thanks, Michael

3 2

excessive compile times?
by Michael.Norrish＠nicta.com.au 10 Dec '13

10 Dec '13

A minimally modified version of the file at https://raw.github.com/mn200/HOL/master/src/bool/boolScript.sml takes 83 seconds to be ?used? (using PolyML.use) into an interactive PolyML session. There are a great many files that need to be used before boolScript gets to work, but none of those files need any longer than 2seconds to be used, and the vast majority take less than a second. The "minimal modifications? turn the ``?`` syntax into valid SML, such that ``p /\ q`` turns into (Term [QUOTE ?p /\\ q?]) and turns `p /\ q` into [QUOTE ?p /\\ q?] We have a timer that starts when the script file actually begins to execute, and this reports that the execution time is less than a second, so it really does seem as if the compilation time is the issue. We have many other Script files in HOL4 that are at least this long, but they don?t have slow compilation times in the same way. Also, the much smaller (30 times by LoC) https://raw.github.com/mn200/HOL/master/src/1/ConseqConvScript.sml has the same prefix as boolScript, but compiles in less than a second. Is there anything obvious (and remediable) that boolScript is doing that might be causing this problem? FWIW, Moscow ML compiles this file as quickly as all the others in the system. Thanks, 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

Flexible records and overloading
by David.Matthews＠prolingua.co.uk 01 Dec '13

01 Dec '13

The ML standard is not specific about what the "program context" should be when disambiguating flexible records and overloading. Poly/ML uses as wide a context as possible but that can mean that a program that compiles with Poly/ML won't necessarily compile with other implementations. I've added a switch PolyML.Compiler.narrowOverloadFlexRecord that defaults to false. If set to true the compiler uses a much narrower context; essentially the val binding. I've looked at a few other implementations to see what they do. The most restrictive is Hamlet which corresponds to what Poly/ML now does with narrowOverloadFlexRecord set to true. It rejects let fun f x y = x + y in f 1.0 end; which SML/NJ (110.74) accepts. Neither accept let fun f {x, ...} = x in f {x=1} end; Mlton seems to use the whole program context as Poly/ML does. David

2 2

Id like to suggest porting to Android
by monkeyrater＠hotmail.com 18 Nov '13

18 Nov '13

There are a couple of implementations for Ocaml on Android but none for SML. So Id like to suggest that you make a port for Android because mobile computing is becoming much more common and mainstream. And also the fact that Android OS is a much more stable target to port to compared to the fragmentation of Linux distros, the exclusivity of hardware costs and availability for OSX and the problems that windows 8 is bringing to user experience. -Brad Cantrell

4 4

managing compilation
by gbuday＠karolyrobert.hu 20 Oct '13

20 Oct '13

Hi, I am looking for a method of managing compilation for Poly/ML, like .cm files for SML/NJ and .mlb files for MLton. What I have found on polyml.org was PolyML.make -- is that the last word on this subject? - Gergely

2 1

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