Poly/ML October 2006

polyml@lists.polyml.org

4 participants
6 discussions

Poly/ML version 5 beta
by David.Matthews＠prolingua.co.uk 10 Nov '06

10 Nov '06

Thanks to some financial support from the Verisoft project and TUM I've been working through the summer on an updated version of the Poly/ML run-time system and a new code-generator for the AMD 64-bit architecture. The major new features are: Support for stand-alone binaries Support for additional platforms: AMD64, Intel Macs, Cygwin No artificial limits on size of heaps or saved image Uses standard GNU tools for building Fixed address mmap and trap-handling removed This comes at one significant cost: the persistent store system that has been a feature of Poly/ML almost since the beginning has been removed. The reason for this is that to be effective the persistent store needed to be able to reload a database at the same address every time but that could conflict with other libraries and result in seg faults. Rather than constantly adjust the location of the database with each new kernel release I decided to make the leap and change to making stand-alone binaries. This achieves much the same as the persistent store but without the complications. This version is currently only available by cvs from sourceforge and is a beta release. Full details and example code showing how to export a function and build an application can be found in http://www.polyml.org/Version5Beta.html . Makarius has been testing this with Isabelle and after some bug fixes it all seems to work. I would like to get some more feedback before making a final release but I'm aiming for a release in about a month. David.

2 3

Re: Posix.Process.alarm
by David.Matthews＠prolingua.co.uk 31 Oct '06

31 Oct '06

Tjark Weber wrote: > I'm a bit puzzled by the behavior of Posix.Process.alarm. As far as I > understand its specification, calling it with a timeout of 0 should cancel > any pending alarm request (and not raise an alarm itself). The Standard ML Basis Library book doesn't say anything about treating Posix.Process.alarm Time.zeroTime differently from any other time so by implication it ought to send an alarm signal immediately. The Posix documentation, though, says that alarm(0) cancels any pending alarm and the FreeBSD man page explicitly says that this does not send a SIGALRM. I would assume that this is the intended behaviour and I've fixed this in CVS for version 5. David.

1 0

Re: Word32 for Poly/ML version 5 beta
by David.Matthews＠prolingua.co.uk 30 Oct '06

30 Oct '06

Achim D. Brucker wrote: > I've implemented a simple Word32 structure for Poly/ML (see the > attachment file). It is a crude hack that implements the Word32 > structure (mis-) using LargeWord. I know, this is not very efficient, > but it works :-). Whereas the Word32 is not yet tested throughoutly, > it works well enough for fxp [1] (a functional XML parser for > SML). Moreover, I tested the setup by building HOL-OCL [2] with > Poly/ML and running our regression test-suite (consisting out of > several UML models that are imported into the system using the fxp > parser). All tests run successfully (which also means, that I could > successfully build Isabelle/HOL-Complex, version 2005, using the > Poly/ML 5 beta). > [1] http://www2.in.tum.de/~berlea/Fxp/ > [2] http://www.brucker.ch/projects/hol-ocl/ Thanks for submitting this, Achim. I've made a few modifications and added it to CVS. I also made a small fix to the Word8 structure while I was doing this. Can you check that this still works? In case anyone else wants to try this and isn't familiar with CVS, the commands are: cd polyml cvs update -Pd make clean make make install David.

2 1

Poly/ML version 5 beta
by dirkl＠cs.uni-sb.de 23 Oct '06

23 Oct '06

Hi David, thanks for your help. You were right, I had the mingw version of fenv.h installed because I have another programs which needs this library. After I edited config.h the compilation worked without problems. Dirk Monday, October 23, 2006, 7:22:55 PM, David Matthews wrote: > Dirk Leinenbach wrote: >> first of all, thank you very much for the new Poly/ML version which >> will hopefully be really useful in the Verisoft project. >> >> I've downloaded the new version and on linux it works very well. With >> cygwin I get compilation errors: >> >> gcc -Di386 -DLINUX -Wall -fno-strict-aliasing -g -O3 -o polyimport.exe polyimpor >> t.o libpolyml/.libs/libpolyml.a -lstdc++ -ldl >> libpolyml/.libs/libpolyml.a(reals.o): In function `_Z14Real_dispatchcP12SaveVecE >> ntryS0_': >> /cygdrive/c/temp/polyml/libpolyml/reals.cpp:432: undefined reference to `_fegetr >> ound' >> /cygdrive/c/temp/polyml/libpolyml/reals.cpp:449: undefined reference to `_fesetr >> I think the reason is that cygwin doesn't support the fenv.h library. >> In your announcement mail you highlighted the support for cygwin, so I >> think that the problem is on my side. Maybe I have to use the fenv.h >> library from mingw, or do you know any other solution? > Hi Dirk, > This works for me in Cygwin so I wonder if your setup is unusual. It > looks as though you have a version of <fenv.h> in your include path, > perhaps the mingw one, but you're not linking with a library that > contains fegetround/fesetround. The proper fix is to find out why you > are picking up the fenv.h but a work-around would be to edit config.h > and remove the line that says > #define HAVE_FENV_H 1 > David -- Dirk Leinenbach Computer Science Department Saarland University Germany Building E1 1, Room 4.06 phone: +49 - 681 / 302 - 57379 fax: +49 - 681 / 302 - 4132

1 0

Poly/ML version 5 beta
by David.Matthews＠prolingua.co.uk 23 Oct '06

23 Oct '06

Dirk Leinenbach wrote: > first of all, thank you very much for the new Poly/ML version which > will hopefully be really useful in the Verisoft project. > > I've downloaded the new version and on linux it works very well. With > cygwin I get compilation errors: > > gcc -Di386 -DLINUX -Wall -fno-strict-aliasing -g -O3 -o polyimport.exe polyimpor > t.o libpolyml/.libs/libpolyml.a -lstdc++ -ldl > libpolyml/.libs/libpolyml.a(reals.o): In function `_Z14Real_dispatchcP12SaveVecE > ntryS0_': > /cygdrive/c/temp/polyml/libpolyml/reals.cpp:432: undefined reference to `_fegetr > ound' > /cygdrive/c/temp/polyml/libpolyml/reals.cpp:449: undefined reference to `_fesetr > I think the reason is that cygwin doesn't support the fenv.h library. > In your announcement mail you highlighted the support for cygwin, so I > think that the problem is on my side. Maybe I have to use the fenv.h > library from mingw, or do you know any other solution? Hi Dirk, This works for me in Cygwin so I wonder if your setup is unusual. It looks as though you have a version of <fenv.h> in your include path, perhaps the mingw one, but you're not linking with a library that contains fegetround/fesetround. The proper fix is to find out why you are picking up the fenv.h but a work-around would be to edit config.h and remove the line that says #define HAVE_FENV_H 1 David

1 0

PolyML Segmentation Faults or MMAP failures.
by C.Kaliszyk＠cs.ru.nl 10 Oct '06

10 Oct '06

Hello, I am trying to run PolyML on i386 linux, and I can't get it to work. I get segmentation faults with some kernel versions, and mmap failures with other versions. I first tried with kernel 2.6.14 and with 2.6.17.2 (current one in debian-sid). On both setups PolyML segfaults. When run with GDB it shows: c@cek:/tmp$ gdb ./poly-driver GNU gdb 6.4.90-debian Copyright (C) 2006 Free Software Foundation, Inc. GDB is free software, covered by the GNU General Public License, and you are welcome to change it and/or distribute copies of it under certain conditions. Type "show copying" to see the conditions. There is absolutely no warranty for GDB. Type "show warranty" for details. This GDB was configured as "i486-linux-gnu"...Using host libthread_db library +"/lib/tls/i686/cmov/libthread_db.so.1". (gdb) run Starting program: /tmp/poly-driver Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005) Copyright (c) 2002-5 CUTS and contributors. Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%) Program received signal SIGSEGV, Segmentation fault. 0xa7e84bd8 in mmap () from /lib/tls/i686/cmov/libc.so.6 PolyML 4.2 also segfaults, on the same mmap, on both above kernel versions. After upgrading the kernel to 2.6.18 I no longer get the segfault, but a proper error message. PolyML 4.2.0 compiled with EXTRA_DEBUG sais: c@cek:~/isa/driver420$ ./poly Poly/ML RTS version I386-4.2.0 (07:41:26 Oct 6 2006) Copyright (c) 2002-5 CUTS and contributors. Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%) Mapping ./ML_dbase Reading in header: 00002000 bytes MMAP; addr=0x20000000, len=00002000, prot=00000007, flags=00000032, fd=-1, off=00000000 Mapping in H->i_space Reading page table; page: 1, length: 00000004 MMAP; addr=0x20002000, len=00008000, prot=00000007, flags=00000032, fd=-1, off=00000000 Mapping in pages MMAP; addr=0x2070c000, len=00502000, prot=00000005, flags=00000012, fd=3, off=0000c000 Mapping in H->m_space Reading page table; page: 5, length: 00000001 MMAP; addr=0x2000a000, len=00002000, prot=00000007, flags=00000032, fd=-1, off=00000000 Mapping in pages MMAP; addr=0x2000c000, len=000e6000, prot=00000005, flags=00000012, fd=3, off=0050e000 allocating H->m_space.bitmap MMAP; addr=0x3f002000, len=00007300, prot=00000007, flags=00000022, fd=-1, off=00000000 allocating H->i_space.bitmap MMAP; addr=0x3f002000, len=00028100, prot=00000007, flags=00000022, fd=-1, off=00000000 MMAP; addr=0x3f002000, pa=0x6fe38000 MMAP; addr=0x3f000000, len=00002000, prot=00000007, flags=00000032, fd=-1, off=00000000 entry no 13, at address 3f0001a0 is a jumpentry to 80755c8 entry no 14, at address 3f0001c0 is a jumpentry to 807550e entry no 84, at address 3f000a80 is a jumpentry to 8074dbf MMAP; addr=0x97e00000, len=00200000, prot=00000007, flags=00000032, fd=-1, off=00000000 ** MMAP: Unable to map file: 0 to address 0x97e00000 ** errno=12: Cannot allocate memory ** This may be due to insufficient swap space, will retry in 2 seconds ... And it never succeeds, but goes in an infinite loop. PolyML 4.1.3 also fails, just the addresses in the error are different, the mmap that fails shows: ** MMAP: Unable to map file: 0 to address 0xa7e00000 PolyML seems to use only the kernel and glibc, so let me mention that my glibc version is 2.3.6.ds1-5 (latest one on debian-sid). Any suggestions on how to get PolyML to run? Cezary Kaliszyk

1 0

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 October 2006