Poly/ML

polyml@lists.polyml.org

1 participants
698 discussions

Supporting bit shifting operations on integers
by hoelzl＠in.tum.de 03 Jun '09

03 Jun '09

Hi, I formalized floating point numbers in Isabelle using integers. From this fromalization I generate PolyML-code. A fast implementation needs bit shift operations on integers. There are shift operations available but they are not implemented very efficiently: IntInf.sml: | (* These could be implemented in the RTS although I doubt if it's | really worth it. *) | fun << (i: int, j: Word.word) = i * pow(2, Word.toInt j) | and ~>> (i: int, j: Word.word) = Int.div(i, pow(2, Word.toInt j)) How difficult is it to implement this operations efficiently in the RTS on big integers? Johannes

1 0

regular expression support?
by luzhao＠cs.utah.edu 22 Apr '09

22 Apr '09

Hi, Does PolyML support regular expression matching? I looked through the source code tree $PolyML/basis and didn't find something like Reg*. I'd like to confirm that this is true. Thanks. Lu

2 1

Binary compatibility and static linking
by rda＠lemma-one.com 09 Apr '09

09 Apr '09

I am trying to understand what level of binary compatibility I can expect if I use Poly/ML to create an executable by exporting a function which calls PolyML.rootFunction to give the users a Poly/ML interactive session. The users will then update the Poly/ML state, save it and reload it in later sessions using the functions in PolyML.SaveState. They will also load state files prebuilt for them. If I build the executable on system A and create some saved state files there, how like A does some other system B have to be for the executable and the saved state files to work on B? I am concerned both about the compatibility for the saved state files and for the shared object files libpolyml.so and libpolymain.so. I understand QinetiQ have no problems moving between systems with Intel hardware and recent-ish slackware and Fedora operating systems. Would the same files work on my Intel Mac? On a related topic: I have had no success trying to link polyml statically. I I use -Wl,-Bstatic -lpolymain -lpolyml -Wl,-Bdynamic on the command line, I get screeds of undefined reference messages. Is static linking an option to build a binary that can be run without installing Poly/ML? If so, how do I do it? Regards, Rob.

3 5

structure/signature matching regression in SVN
by fluet＠tti-c.org 09 Apr '09

09 Apr '09

>From recent SVN commit messages, I see that there has been some reorganization of structure/signature matching; apologies if the reorganization is incomplete (i.e., not ready for testing) and/or the following is a known issue. This program type checks under PolyML 5.2.1 (and SML/NJ 110.68 and MLton 20070826), but reports type errors under PolyML SVN HEAD. ===== signature UNIQUE_SET_STRUCTS = sig structure Element: sig type t end end signature UNIQUE_SET = sig include UNIQUE_SET_STRUCTS type t val toList: t -> Element.t list end structure UniqueSetRep = struct datatype 'a t = T of {elements: 'a list} end functor UniqueSet (S: UNIQUE_SET_STRUCTS): UNIQUE_SET = struct open S type elements = Element.t list structure Tree: sig structure Set: sig type t val toList: t -> elements end end = struct structure Set = struct open UniqueSetRep type t = Element.t t fun new elements = T {elements = elements} fun elements (T {elements, ...}) = elements val toList = elements end end open Tree.Set end =====

3 3

Segmentation fault when saving state
by pclayton＠taz.qinetiq.com 03 Apr '09

03 Apr '09

David, We have noticed some interesting behaviour with the state saving in Poly/ML 5.2/5.2.1--- possibly a sign that something isn't quite as intended. If poly is started and the command PolyML.SaveState.saveState "test"; is repeatedly entered, a segmentation fault eventually occurs. On my machine it always happens after 22 times. With the debug level set to 2 or 3, we get: Bad pointer 0x0d479050 found Aborted If we enter PolyML.fullGC (); just before the 22nd go, there is no segmentation fault. However, continuing to enter the original save state command results in the exception Exception- SysErr ("Out of Memory", SOME ENOMEM) raised after 8 more goes. We found this example more by chance. We have had a few other repeatable segmentation faults when saving the state but on very large examples and these are hard to reduce down. (They may be related to the above issue.) In each case, the segmentation fault could be avoided by executing PolyML.fullGC first. Generally, if we cannot create an SML script that generates an error, what is the best way to track down an issue? Thanks, Phil The information contained in this E-Mail and any subsequent correspondence is private and is intended solely for the intended recipient(s). The information in this communication may be confidential and/or legally privileged. Nothing in this e-mail is intended to conclude a contract on behalf of QinetiQ or make QinetiQ subject to any other legally binding commitments, unless the e-mail contains an express statement to the contrary or incorporates a formal Purchase Order. For those other than the recipient any disclosure, copying, distribution, or any action taken or omitted to be taken in reliance on such information is prohibited and may be unlawful. Emails and other electronic communication with QinetiQ may be monitored and recorded for business purposes including security, audit and archival purposes. Any response to this email indicates consent to this. Telephone calls to QinetiQ may be monitored or recorded for quality control, security and other business purposes. QinetiQ Limited Registered in England & Wales: Company Number:3796233 Registered office: 85 Buckingham Gate, London SW1E 6PD, United Kingdom Trading address: Cody Technology Park, Cody Building, Ively Road, Farnborough, Hampshire, GU14 0LX, United Kingdom http://www.qinetiq.com/home/notices/legal.html

2 3

Compilation error on AIX
by David.Matthews＠prolingua.co.uk 24 Mar '09

24 Mar '09

nitralime wrote: > On Mon, Mar 23, 2009 at 6:55 PM, David Matthews < > I don't know how time consuming the implementation of XCOFF support would > be. > Excuse me my naive question: Is there any plan to implement it? None at the moment. It shouldn't be a great deal of work especially if it is a variant of the PE/COFF. Look at the existing XXXexport.cpp files. You'd have to get the detailed specifications of XCOFF. > I am a little bit confused about your answer. > What would it mean if you fix the bug? The bug I've fixed (in SVN) is simply to allow this file to compile. However the effect of that will be to raise an exception when you try to export in native object file format. The Poly/ML Makefile does an export as part of building the "poly" file so the normal build process won't work. There is also a portable export format which is used for the files in the "imports" directory and the "polyimport" program is used to read and execute them. You would have to adapt the "exportPoly" file which is used to compile the basis library so that after the basis library is compiled the complete Poly/ML system is written out in the portable format rather than native object file format. > Do I get after that an interpreted byte code version of PolyML? The issue of machine code or interpreted code is orthogonal to this. For example, i386 machine code may be exported as PE/COFF, ELF or MachO depending on whether the machine is running Windows, Linux or Mac OS X. Regards, David.

1 0

Compilation error on AIX
by nitralime＠googlemail.com 23 Mar '09

23 Mar '09

Hi, I am trying to compile PolyML 5.2.1 on AIX 5L. After executing configure script "./configure --prefix=/usr/local/polyml" and "gmake" I got the following error message: ---------------------------------------------------------------------------------------- .... g++ -DHAVE_CONFIG_H -I. -I.. -Wall -O3 -MT poly_specific.lo -MD -MP -MF .deps/poly_specifi mv -f .deps/poly_specific.Tpo .deps/poly_specific.Plo /bin/sh ../libtool --tag=CXX --mode=compile g++ -DHAVE_CONFIG_H -I. -I.. -Wall -O3 -M porter.cpp g++ -DHAVE_CONFIG_H -I. -I.. -Wall -O3 -MT exporter.lo -MD -MP -MF .deps/exporter.Tpo -c e exporter.cpp: In function 'SaveVecEntry* exportNative(TaskData*, SaveVecEntry*)': *exporter.cpp:429: error: 'EXC_Fail' was not declared in this scope* gmake[2]: *** [exporter.lo] Error 1 gmake[2]: Leaving directory `/tmp/polyml.5.2.1/libpolyml gmake[1]: *** [all-recursive] Error 1 gmake[1]: Leaving directory `/tmp/polyml.5.2.1' gmake: *** [all] Error 2 ---------------------------------------------------------------------------------------- I am using *gcc version 4.2.4* on *AIX 5.3*. Any help is very much appreciated! Best regards, Nik

2 1

Move to Subversion
by David.Matthews＠prolingua.co.uk 23 Mar '09

23 Mar '09

CVS is getting rather old now and most projects seem to have moved on. I've now moved Poly/ML's CVS repository to subversion and taken the opportunity to enable Trac on the SourceForge site. To download the development version you need svn co https://polyml.svn.sourceforge.net/svnroot/polyml/trunk polyml The subversion repository contains all the CVS history so I'll be disabling CVS shortly. There's quite a bit of work going on with the compiler at the moment with a view to providing much better support for development environments. There's work to make this available in Isabelle and Lucas Dixon is looking at a plug-in for jEdit. There'll be more news as we get things properly working. David.

2 2

Universal binaries
by aleks0＠gmail.com 16 Mar '09

16 Mar '09

Anyone had luck (or know where to begin for...) getting poly/ML to export mac universal binary? I guess a more general question is, can poly/ML make *.o files for a different architecture than the one it is running on?

1 0

Installing Poly/ML
by rda＠lemma-one.com 02 Mar '09

02 Mar '09

I have just learnt a few things installing Poly/ML on a Ubuntu 8.04 system freshly built from the Desktop CD: 1) Ubuntu comes out of the CD with 3/4 of a C compiler. You get gcc, but not libc, so you can compile hello-world.c but not link or run it. The configure script notices this. Installing the package libc6-dev fixes it. 2) But, the configure script doesn't seem to check that there is a C++ compiler (perhaps it should???). The output from configure looked OK, but make fell over with an error: ../libtool: line 1281: g++: command not found Installing the package g++ fixes this. 3) But, poly builds and installs but won't run, because Ubuntu is one of those systems that doesn't include /usr/local/lib on the library path, After starting again with "./configure --prefix=/usr", I have a working compiler. Regards, Rob.

2 1

← Newer
1
...
50
51
52
53
54
55
56
...
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