Poly/ML February 2014

polyml@lists.polyml.org

7 participants
12 discussions

Inspecting structures
by ramana.kumar＠gmail.com 27 Jan '16

27 Jan '16

Is there a way to look at the contents (i.e. signature) of a structure without opening it? (I suppose you could just open it then call a lot of PolyML.Compiler.forgetXXX, but that's quite tedious) Also, is it possible to retrieve the long path of an identifier in scope? Something that will, for example, take the rev in scope and say that it came from List. Finally, what about searching for an identifier that would come into scope if you opened some structures?

3 5

polyc and poly --script
by rene.neumann＠in.tum.de 24 Mar '15

24 Mar '15

Hi, two completely orthogonal questions/remarks for PolyML 5.5.1: 1.) When building PolyML with '--with-system-libffi' the '-lffi' part is missing in the linker line in polyc. 2.) Is it somehow possible to see if an ML file is run via 'poly --script' or as a standalone executable? Because for the one the logic has to be wrapped in 'fun main ()', and for the other it should not :). (Ie, what I want: if is_script then main() else () ) Thanks, Ren? -- Ren? Neumann Institut f?r Informatik (I7) Technische Universit?t M?nchen Boltzmannstr. 3 85748 Garching b. M?nchen Tel: +49-89-289-17232 Office: MI 03.11.055

4 9

[Fwd: Re: [polyml] Building Poly/ML on MacOS X 10.6]
by rda＠lemma-one.com 29 Dec '14

29 Dec '14

I wrote: > I am completely baffled. I thought I hada solved all my problems on > MacOS X > 10.6 and was just tidying up, when I had to recompile a 32 bit > version of > Poly/ML to test a tidied up make file. This failed because > PolyML.Compiler.printTypesWithStructureName no longer exists. The same > problem happened when i rebuild a 64 bit version. What has happened? but it was a false alarm: my make file was wrong for other reasons and the absence of PolyML.Compiler.printTypesWithStructureName was not relevant. No doubt there are good reasons why this variable has been withdrawn. Regards, Rob.

3 6

Isabelle/ML IDE
by makarius＠sketis.net 29 Sep '14

29 Sep '14

Dear friends of Poly/ML, or Standard ML in general, Isabelle2013-2 is now available from the usual mirror sites: Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Munich (Germany) http://isabelle.in.tum.de/ Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/ It is mainly an environment for interactive and automated theorem proving, but the integration of Isabelle/ML into the Prover IDE makes it suitable for general Standard ML development (potentially in teaching scenarios). After downloading / unpacking / running the main application of Isabelle/jEdit, the Documentation panel on the right-hand side gives quick access to Examples, notably src/HOL/ex/ML.thy for some Isabelle/ML basics. The manual on Isabelle/jEdit in the same panel provides further details on the IDE, which is based on the jEdit text editor. Makarius

1 1

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

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

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 February 2014