Poly/ML

polyml@lists.polyml.org

695 discussions

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

signature sharing
by ldixon＠inf.ed.ac.uk 18 May '06

18 May '06

This might be a general ML question, but perhaps you can help... I'm curious why type functions cannot be shared, but datatypes can: the following code is fine: ---- signature A = sig type T end; signature B = sig type T datatype Pair = Pair of T * T end; signature CA = sig structure a : A end; signature CB = sig structure b : B end; signature D = sig structure b : B structure cb : CB sharing cb.b = b structure ca : CA sharing ca.a = b end; ----- However, the following complains: ----- signature A = sig type T end; signature B = sig type T type Pair = T * T end; signature CA = sig structure a : A end; signature CB = sig structure b : B end; signature D = sig structure b : B structure cb : CB sharing cb.b = b structure ca : CA sharing ca.a = b end; ----- with the error message: Error: Cannot share: (D.cb.b.Pair) is a type function Found near sig structure b : B structure cb : CB sharing cb.b = b structure ca : CA sharing ca.a = b end Static errors (pass2) Is there a theoretical reason for this? (I cannot think of one) I have been thinking of things like: type tname = .... as type abbreviations to save me typing, and I'm curious why wrapping the type into a datatype should allow sharing... ? cheers, lucas

2 1

Performance of Poly/ML 4.2.0
by rda＠lemma-one.com 17 Feb '06

17 Feb '06

Poly/ML 4.2.0 seems to be a little slower building my stuff than version 4.1.3 generally and, if I'm not careful, a lot slower on Mac OS X. For a typical compilation (my SLRP parser generator), I get figures like this on a Linux PC: 4.1.3: 0.84s real 0.80s user 0.02s system 4.2.0: 0.98s real 0.93s user 0.03s system So that's about 15% slower. On Mac OS X, the figures for the same compilation are: 4.1.3: real 0m2.323s user 0m1.439s sys 0m0.122s 4.2.0: real 0m7.84s user 0m1.96s sys 0m0.14s So it's processing about 30% slower, but spending 70% of the real time doing nothing, so overall it's about 200% slower. The 70% is down to an old friend, the Mac OS X crashreporter, see: http://lists.inf.ed.ac.uk/mailman/private/polyml/2004-February/000098.html but now with version 4.2.0, you get two or three crash-reports per run and the overhead seems to be much higher. If you do "killall crashreporterd" before compiling, things look a lot better: 4.1.3: real 0m1.576s user 0m1.431s sys 0m0.112s 4.2.0: real 0m2.15s user 0m1.96s sys 0m0.13s But even with the crash-reporter overhead removed altogether, that's still more than 30% slower. Regards, Rob.

1 0

Signal Handler Persistence
by tjark.weber＠gmx.de 11 Feb '06

11 Feb '06

Hi, I've noticed some strange behavior of PolyML 4.2.0 for i386/Linux with respect to signals and signal handlers. Basically, what happens is that after installing my own signal handler for (in my case) the ALRM signal, committing the database, and restarting PolyML, further signals are apparently not delivered anymore, even though the handler itself is installed properly. Can anyone confirm this behavior, or even better yet, does anyone have an explanation? Maybe I'm just overlooking the obvious. Below is a minimal example, with relevant output included. Best regards, Tjark ,----- $./poly Poly/ML RTS version I386-4.1.3 (13:57:33 Sep 30 2002) Copyright (c) 2002 CUTS and contributors. Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%) Mapping ./ML_dbase Poly/ML 4.1.3 Release > val flag = ref false; val flag = ref false : bool ref > Signal.signal (Posix.Signal.alrm, Signal.SIG_HANDLE (fn _ => flag := true)); val it = SIG_DFL : Signal.sig_handle > Posix.Process.alarm (Time.fromSeconds 0); val it = 0.000 : Time.time > !flag; val it = true : bool > PolyML.commit(); [...] Mapping ./ML_dbase val it = true : bool > PolyML.quit(); $ ./poly Poly/ML RTS version I386-4.1.3 (13:57:33 Sep 30 2002) Copyright (c) 2002 CUTS and contributors. Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%) Mapping ./ML_dbase Poly/ML 4.1.3 Release > flag := false; val it = () : unit > Posix.Process.alarm (Time.fromSeconds 0); val it = 0.000 : Time.time > !flag; val it = false : bool So the handler appears not to be called. It is however installed properly: > val (Signal.SIG_HANDLE handler) = Signal.signal (Posix.Signal.alrm, Signal.SIG_DFL); val handler = fn : int -> unit > handler 14; val it = () : unit > !flag; val it = true : bool `-----

2 1

Poly/ML version 4.2.0
by David.Matthews＠prolingua.co.uk 08 Dec '05

08 Dec '05

I've now fully released the new version of Poly/ML. I've upped the version number to 4.2.0 for the release but it is essentially version 4.1.4 with a very few changes. This is now the official release on the Poly/ML website. I've created an installation for Windows but I haven't attempted to created binary installations for any other operating system. Since Poly/ML is now under LGPL it should be possible to package it in with the individual operating system distributions. If anyone does make a binary distribution could they let me know so that I can put a reference to it on the downloads page and if appropriate include a copy on the sourceforge site. David.

2 2

Fwd: Re: installation
by giamp＠dmi.unict.it 05 Dec '05

05 Dec '05

Hi, can you please help? Thanks! -- Giamp ----- Forwarded message from Lawrence Paulson <lp15(a)cam.ac.uk> ----- Date: Fri, 2 Dec 2005 11:48:53 +0000 From: Lawrence Paulson <lp15(a)cam.ac.uk> Reply-To: Lawrence Paulson <lp15(a)cam.ac.uk> Subject: Re: installation To: giamp(a)dmi.unict.it Try your question at polyml(a)informatics.ed.ac.uk. If they recomment Poly/ML-4.2, you need to download our Poly/ML-4.14, which is a version of that patched "backwards" to support the current Isabelle release. There's always SML/NJ, though it's slower for big proofs. Larry On 2 Dec 2005, at 11:29, giamp(a)dmi.unict.it wrote: > I'm trying to install Isabelle on an AMD Athlon 64, which is a 64 > bit x86 > architecture. > > Polyml gives a known segmentation fault, but installing its fix > produces: > > Poly/ML is not available for this architecture - x86_64 > > Ever heard about this? Do I just need to change machine? ----- End forwarded message ----- ---------------------------------------------------------------- This message was sent using IMP, the Internet Messaging Program.

3 3

segmentation fault
by ewenmaclean＠gmail.com 19 Oct '05

19 Oct '05

Skipped content of type multipart/alternative

3 4

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