Poly/ML June 2006

polyml@lists.polyml.org

5 participants
3 discussions

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

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