Poly/ML

polyml@lists.polyml.org

2 participants
711 discussions

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

4.2 debs
by itz＠madbat.mine.nu 05 Sep '06

05 Sep '06

I have made debian packages for 4.2.0, to be found at http://primate.net/~itz/debian/polyml Tested only on i386. I added a bit of infrastructure to maintain the chain of child databases for libraries. I myself intend to package a couple of libraries from the net, such as FGL and FXP. Later I'll tackle either Isabelle or ProofPower, but that will be a much bigger job. -- She had a passion for anyone who could do anything really well. ... "Not for an engineer, not for a technician!" Mikhail Bulgakov, The Master & Margarita

3 3

Calling Poly/ML from foreign code
by matthews＠galois.com 31 Aug '06

31 Aug '06

Hi David et al., I'm running the Isabelle theorem prover on top of Poly/ML on a Mac OS X PowerBook G4. I would like to be able to 1. Call Isabelle's ML functions directly from external processes that have been written in C. 2. Call C code I've loaded into Isabelle's process space, and have that code call back to Poly/ML functions. Is it possible to do either of these in Poly/ML? Thanks in advance, -john

2 3

polyml on Intel based Macs
by martin＠klebermass.de 29 Jun '06

29 Jun '06

Hi, i have bought a new MacBook and i would look forward for PolyML on Intel based Macs. As i heard from Prof. Nipkow there are some problems with signaling or so on the intel based macs, so that it doesnt compile. So i have started to look a little bit on the source to about the problems and as much as i can see there are the following problems: 1. no global functions for changing the Floating Point Rounding mode needed for reals.c (im not sure if this is realy needed at the moment. 2. adding support for darwin i386 in mm.h (MM_CPU_TYPE) 3. sighandler.c SV_SAVE_REGS seems to be a ppc specific handler. At the moment im looking about solving number 1, but before i start with this, i look forward if anyone has already done more research. Thanks Martin Klebermass

3 5

line drawing in Windows
by pbrowne＠comp.dit.ie 27 Jun '06

27 Jun '06

Hi I would like to draw some lines using the MS Windows version of PolyML. I have looked at the documentation for the Windows programming interface, but I am unsure as to how to handle WM_PAINT, BeginPaint and EndPaint in PolyML. What I have in mind is something like the C code below. Thanks Pat Browne #include <windows.h> HWND g_hwndMain; LRESULT CALLBACK WndProc(HWND hWnd, UINT message, WPARAM wParam, LPARAM lParam) { int wmId, wmEvent; RECT rect; HDC hDC; PAINTSTRUCT Ps; HPEN hPen; HFONT hFont; switch (message) { case WM_PAINT: hDC = BeginPaint(hWnd, &Ps); hPen = CreatePen(PS_SOLID, 1, RGB(0, 0, 0)); SelectObject(hDC, hPen); MoveToEx(hDC, 0, 25, NULL); LineTo(hDC, 240, 25); EndPaint(hWnd, &Ps); break; case WM_KEYDOWN: if( wParam == VK_ESCAPE ) { DestroyWindow(hWnd); } break; case WM_DESTROY: PostQuitMessage(0); break; } return DefWindowProc(hWnd, message, wParam, lParam); } ATOM MyRegisterClass(HINSTANCE hInstance, LPTSTR szWindowClass) { WNDCLASS wc; wc.style = CS_HREDRAW | CS_VREDRAW; wc.lpfnWndProc = (WNDPROC) WndProc; wc.cbClsExtra = 0; wc.cbWndExtra = 0; wc.hInstance = hInstance; wc.hCursor = 0; wc.hbrBackground = (HBRUSH) GetStockObject(WHITE_BRUSH); wc.lpszMenuName = 0; wc.lpszClassName = szWindowClass; return RegisterClass(&wc); } BOOL InitInstance(HINSTANCE hInstance, int nCmdShow) { TCHAR szWindowClass[MAX_PATH]; // The window class name wcscpy(szWindowClass, TEXT("TITLE")); MyRegisterClass(hInstance, szWindowClass); g_hwndMain = CreateWindow(szWindowClass, TEXT("TITLE"), WS_EX_TOPMOST, 0, 0, 500, 500, NULL, NULL, hInstance, NULL); ShowWindow(g_hwndMain , nCmdShow); UpdateWindow(g_hwndMain); return TRUE; } int WINAPI WinMain(HINSTANCE hInstance, HINSTANCE hPrevInstance,LPTSTR lpCmdLine,int nCmdShow) { MSG msg; HACCEL hAccelTable; ZeroMemory(&msg, sizeof(MSG)); // Perform application initialization: if (!InitInstance (hInstance, nCmdShow)) { return FALSE; } // Main message loop: while(msg.message != WM_QUIT) { PeekMessage(&msg, 0, 0, 0, PM_REMOVE); TranslateMessage(&msg); DispatchMessage(&msg); } return msg.wParam; }

2 1

Fwd: [ProofPower] About Proofpower install
by rda＠lemma-one.com 22 Jun '06

22 Jun '06

The annotated and edited correspondence below gives highlights of a problem Artur Gomes is having building ProofPower. What Artur was seeing in the log fiiles from the ProofPower build script ... ... on standard error: >> > { cat /home/artur/proofpower/polyml/x86-linux/ML_dbase > >> slrpdb."polydb" || >> > exit 1; }; echo "val product_version : string = \" 2.7.6\"; val >> copyright : >> > string = \"Copyright (c) Lemma 1 Ltd. 2002\"; use\"dtd108.sml\"; >> use\" >> > imp108.sml\"; PolyML.commit();" | poly slrpdb."polydb"??| tee >> dtd108.ldd > >> > imp108.ldd >> > catchSEGV; &context = 0x807c224, in_run_time_system=1, >> context.trapno=14 >> ... on standard output: >> > root@firebird:/home/artur/proofpower/OpenProofPower-2.7.6# cat >> > src/imp108.ldd >> > Poly/ML RTS version I386-4.1.3 (19:13:05 Jun 19 2006) >> > Copyright (c) 2002 CUTS and contributors. >> > >> > Running with heap parameters >> (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%) >> > Mapping ./slrpdb.polydb >> > Poly/ML 4.1.3 Release My suggestion: >> What happens if you try to run poly interactively, e.g., using the >> following >> command line: >> >> poly /home/artur/proofpower/polyml/x86-linux/ML_dbase The results: > When I try to run poly, I got things like that: > root@firebird:/home/artur# poly > /home/artur/proofpower/polyml/x86-linux/ML_dbase > Poly/ML RTS version I386-4.1.3 (19:13:05 Jun 19 2006) > Copyright (c) 2002 CUTS and contributors. > Running with heap parameters > (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%) > segmentation fault I think we've nailed down that it's a Poly/ML > problem - poly is reporting a segmentation fault whenever he runs it, > with a bit more detail in the error report when he runs it via the > ProofPower build scripts. What should we try next? Regards, Rob.

2 3

← Newer
1
...
60
61
62
63
64
65
66
...
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