Poly/ML

polyml@lists.polyml.org

695 discussions

Building an executable that runs the read-eval-print loop
by rda＠lemma-one.com 27 Mar '19

27 Mar '19

I wanted to create an executable that runs the Poly/ML read-eval-print loop with some code of mine precompiled. What I found was that the print part of the read-eval-print loop doesn't work if I compile from source with polyc, but does work if I use PolyML.export to create a .o file and then link it with polyc. For example, if I have a file t.ML containing the following two lines: fun p s = (TextIO.output(TextIO.stdOut, s); s); val main = PolyML.rootFunction and compile it with: polyc -o t t.ML and then run: echo 'val x = p "Boo!\n"' | t the output I see is: Poly/ML 5.7 Release Boo! So it's executed my code, but it hasn't printed the usual report on the new value binding for x. So I copied what I do in ProofPower, which does something similar but doesn't have this problem. I appended the following line to t.ML: val _ = PolyML.export ("t", main); and compiled it with: poly < t.ML polyc -o t t.o Then when I run t as above, I see the output, I'd expected to get: Poly/ML 5.7 Release Boo! val x = "Boo!\n": string The work-around is easy, but it would be nice to be able to compile from source to executable directly (and to minimise the Poly/ML-specific code in my source). Regards, Rob.

2 1

Memory leak when FFI callback and ref value.
by kostirya＠gmail.com 14 Mar '19

14 Mar '19

Hello. I found memory leak when FFI callback and ref value. I checked Poly/ML 5.8 and 5.7. Simple code for reproduce the memory leak is attached. To prevent the memory leak I clean ref value (see comment in example). But It must do the garbage collector, is it? At least MLton have not this problem. Result of run of example code: Without clean ref value (The memory leak is) USER PID %CPU %MEM VSZ RSS TT STAT STARTED TIME COMMAND nick 19855 91,8 9,7 305016 289452 6 S+ 16:53 0:17,94 poly --script cb-po With clean ref value USER PID %CPU %MEM VSZ RSS TT STAT STARTED TIME COMMAND nick 19862 65,3 0,6 32632 17476 6 S+ 16:54 0:10,77 poly --script cb-poly Best, Nick.

2 1

Testing Poly/ML 5.8
by David.Matthews＠prolingua.co.uk 12 Mar '19

12 Mar '19

The current version of Poly/ML is approaching the point of creating a new release, 5.8. Makarius has run a lot of tests with Isabelle and various bugs have been fixed. This has mainly affected the 32-bit object ID version for 64-bits but some of the fixes will also have affected the native-address versions. This is a last chance to test the current git master before release. Don't forget to run "make compiler" at least twice after the initial "make" in order to build the up-to-date compiler and recompile all the code with it. This is particularly important if testing the --enable-compact32bit version. Some extra checking was added during testing and there is a strong chance of getting an assertion failure during the initial "make" or the first "make compiler" due to a bug in the pre-built compiler. If this happens just rerun the step. Once the compiler has been rebuilt it will incorporate a fix. David

6 12

ar cru call
by buday.gergely＠uni-eszterhazy.hu 12 Mar '19

12 Mar '19

> How can I make polyml to use "ar cr" instead of "ar cru"? The problem was only in the libffi directory. I edited the files with AR_FLAGS setting there, I guess the configure is the source of the others and then make in this directory worked, and then make in the main polyml directory went through. ar manual writes u Normally, ar r... inserts all files listed into the archive. If you would like to insert only those of the files you list that are newer than existing members of the same names, use this modifier. The u modifier is allowed only for the operation r (replace). In particular, the combination qu is not allowed, since checking the timestamps would lose any speed advantage from the operation q. So omitting the u has no real effect other than compile time. The learning is that in MobaXterm, probably due to Busybox using a limited version of ar, option u is not understood. Fixing libffi/configure to have option cr instead of cru for AR_FLAGS makes the compilation possible. Would it be possible to test with autoconf whether a system understands the u option of ar and use cr then? - Gergely

3 2

ar cru call
by buday.gergely＠uni-eszterhazy.hu 08 Mar '19

08 Mar '19

Hi, I try to compile polyml on MobaXterm, which is a cygwin-based distribution for Windows. Once I have a warning libtool: compile: gcc -DHAVE_CONFIG_H -I. -I. -I./include -Iinclude -I./src -O3 -fomit-frame-pointer -fstrict-aliasing -ffast-math -march=core2 -Wall -fexceptions -MT src/closures.lo -MD -MP -MF src/.deps/closures.Tpo -c src/closures.c -DDLL_EXPORT -DPIC -o src/.libs/closures.o src/closures.c: In function 'open_temp_exec_file_name': src/closures.c:273:8: warning: implicit declaration of function 'mkostemp'; did you mean 'mkstemp'? [-Wimplicit-function-declaration] fd = mkostemp (name, flags); ^~~~~~~~ mkstemp and then an error: /bin/sh ./libtool --tag=CC --mode=link gcc -O3 -fomit-frame-pointer -fstrict-aliasing -ffast-math -march=core2 -Wall -fexceptions -o libffi_convenience.la src/prep_cif.lo src/types.lo src/raw_api.lo src/java_raw_api.lo src/closures.lo src/x86/ffi.lo src/x86/win32.lo libtool: link: ar cru .libs/libffi_convenience.a src/.libs/prep_cif.o src/.libs/types.o src/.libs/raw_api.o src/.libs/java_raw_api.o src/.libs/closures.o src/x86/.libs/ffi.o src/x86/.libs/win32.o ar: unknown option -- u BusyBox v1.22.1 (2015-11-10 11:07:12 ) multi-call binary. Usage: ar [-o] [-v] [-p] [-t] [-x] ARCHIVE FILES Extract or list FILES from an ar archive -o Preserve original dates -p Extract to stdout -t List -x Extract -v Verbose ar version is 2.29.1 here. I tried this on another platform, where ar, or, better say binutils has version 2.22.52 and there is no problem. I tried to compile binutils 2.22.52 with binutils 2.29.1 but but that failed with the same error. How can I make polyml to use "ar cr" instead of "ar cru"? - Gergely

2 1

'make compiler' resulting in slow compilation
by David.Matthews＠prolingua.co.uk 06 Mar '19

06 Mar '19

Phil, Thank you for testing this and reporting the problem. It actually turned out to be a bug in the compact 32-bit version. The compilation happened to allocate an array of a particular size that was wrongly copied in the minor garbage collection resulting in a crash either in the GC itself or later on. I've pushed a fix to master and I'm copying this message to the mailing list since this represents a change that others may need to be aware of. Regards, David On 03/03/2019 00:27, Phil Clayton wrote: > David, > > I have been trying out the latest candidate for Poly/ML 5.8 (c3a630f) > with --enable-compact32bit and have not found any issues.? I was pleased > to see a space saving with saved state files, which appear to be around > 62-68% of their size compared with not using compact32bit.? I haven't > measured any other performance though. > > In one obscure respect, compact32bit fails where the full 64 bit version > does not: the exponential blow-up described in this example from a few > years ago now fails to compile code where the full 64 bit version would > take around 8 s on my machine.? Presumably some internal limit is hit > sooner with 32 bits.? I have seen two different failure messages as > shown in the following log. > > Regards, > Phil

1 0

getting the type of an identifier
by gbuday＠gmail.com 06 Mar '19

06 Mar '19

Hi, typing an identifier in the REPL gives its type: > print; val it = fn: string -> unit is there a polyml function that gives back a string of the type without the fn: prefix? I would like to use it in documentation. I have taken a look in the PolyML.NameSpace structure but did not find such a function. - Gergely

2 1

32bits addresses in 64-bit mode and other updates to master
by David.Matthews＠prolingua.co.uk 24 Jan '19

24 Jan '19

I've now merged a major piece of development work into GitHub master. This is a variant of 64-bit mode that uses 32-bit values. It was triggered by the observation that Isabelle often peformed better with the 32-bit version than the 64-bit despite the 64-bit version allowing a much larger heap and having more registers. It appears that Isabelle, at any rate, is limited more by the bandwidth between the processors and main memory than by the processors themselves. This may well be the result of the work on parallelising the application and the garbage collector. In effect there are now three versions on the X86: native 64-bit, native 32-bit and 32-bits on 64-bits. The new version can be built with the --enable-compact32bit option to configure. It allows a heap size of up to 16Gbytes by using 31-bit "object ids", essentially indexes into an array of 8-byte cells. This heap contains only the data. Code, thread stacks and other support structures are outside this. It has been extensively tested with Isabelle (thanks to Makarius) and seems to perform better than either of the native address versions. I started the development about a year ago; development of the final stages were supported by Data61 and CSIRO through Gerwin Klein. I would be interested in feedback on this and also the native address versions. Whether it well help other applications may depend on whether the limitation is processor speed or memory bandwidth. It's likely that many applications will continue to perform best with native addressing. The update also includes changes to the X86 code-generator that affect all the variants. These changes improve the way boolean values and conditionals are handled. There also other changes to the IO system. Garbage-collection of streams has been removed and overlapped IO is now used on Windows which should improve performance and responsiveness. There have been changes to the handling of floating point and Real32 has been added. Let me have any feedback. Regards, David

4 8

ASSERTION FAILURE: 0 at src/x86/ffi64.c:302 when --enable-debug
by kostirya＠gmail.com 11 Jan '19

11 Jan '19

Hello. I got FFI error when configure and built poly with --enable-debug *only*: ASSERTION FAILURE: 0 at src/x86/ffi64.c:302 The error happens on Linux and FreeBSD. I use PolyML from git at "Thu Jan 3 14:35:50" date (Linux) and "Fri Jun 22 13:49:32 2018" (FreeBSD): ./configure --with-gmp --enable-debug When I use PolyML *without* debugIt is all right. :-) GDB backtrace on linux: (gdb) bt #0 0x00007f53c3fca1f7 in raise () from /lib64/libc.so.6 #1 0x00007f53c3fcb8e8 in abort () from /lib64/libc.so.6 #2 0x00007f53c4c1295f in ffi_assert () from /home/nick/polyml/lib/libpolyml.so.9 #3 0x00007f53c4c1326a in ffi_prep_cif_machdep () from /home/nick/polyml/lib/libpolyml.so.9 #4 0x00007f53c4be1d31 in poly_ffi (taskData=0x7f53bc01b8c0, args=0x7f53bc01baf8, code=0x7f53bc01baf0) at polyffi.cpp:381 #5 0x00007f53c4be2986 in PolyFFIGeneral (threadId=0x7f53c4f54870, code=..., arg=...) at polyffi.cpp:587 #6 0x0000000000408aa2 in area1 () #7 0x00007f53abe429c0 in ?? () #8 0x00007f53abe42700 in ?? () #9 0x0000000000001000 in ?? () #10 0x00007f53c400f53b in new_heap () from /lib64/libc.so.6 #11 0x0000000000000000 in ?? () GDB backtrace on FreeBSD is more informative ans say "0x6f <Address 0x6f out of bounds>": (gdb) bt #0 0x000000080132a47a in thr_kill () from /lib/libc.so.7 #1 0x000000080132a444 in raise () from /lib/libc.so.7 #2 0x000000080132a3b9 in abort () from /lib/libc.so.7 #3 0x00000008009224a7 in ffi_assert () from /home/nick/polyml_new/lib/libpolyml.so.9 #4 0x0000000800923922 in classify_argument () from /home/nick/polyml_new/lib/libpolyml.so.9 #5 0x000000080092290e in examine_argument () from /home/nick/polyml_new/lib/libpolyml.so.9 #6 0x00000008009227eb in ffi_prep_cif_machdep () from /home/nick/polyml_new/lib/libpolyml.so.9 #7 0x000000080091b2d8 in ffi_prep_cif_core () from /home/nick/polyml_new/lib/libpolyml.so.9 #8 0x000000080091b54d in ffi_prep_cif () from /home/nick/polyml_new/lib/libpolyml.so.9 #9 0x00000008008e9cd8 in poly_ffi (taskData=0x802218200, args=0x80221c008, code=0x80221c000) at polyffi.cpp:379 #10 0x00000008008e8df0 in PolyFFIGeneral (threadId=0x8006b2208, code= {contents = {signedInt = 111, unsignedInt = 111, objectPtr = 0x6f, codePtr = 0x6f <Address 0x6f out of bounds>, stackAddr = 0x6f}}, arg= {contents = {signedInt = 34366811360, unsignedInt = 34366811360, objectPtr = 0x8006bece0, codePtr = 0x8006bece0 "\005", stackAddr = 0x8006bece0}}) at polyffi.cpp:585

2 2

Assertion `markCount == bitCount' failed
by gbuday＠gmail.com 04 Jan '19

04 Jan '19

Hi, in a CakeML compilation I got explorerProgTheory FAILED! <Signal 6> GC: Count error mark count 205399344, bitCount 205372170 GC: Count error mark count 205267608, bitCount 205240434 buildheap: gc.cpp:178: bool doGC(POLYUNSIGNED): Assertion `markCount == bitCount' failed. GC: Count error mark count 205267608, bitCount 205240434 What could cause this? Unsuccessful memory allocation attempt? Signal 6 is ABRT. I am using the 5.7.1 release. - Gergely

2 3

← Newer
1
...
5
6
7
8
9
10
11
...
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