Poly/ML June 2009

polyml@lists.polyml.org

7 participants
5 discussions

Strange syntax in PolyML Code
by dathayer＠microsoft.com 30 Jun '09

30 Jun '09

I am working with the Isabell/HOL system which is hosted by default on the PolyML system. I have found a strange syntax construct in some of the source code files consisting of @{ ...some verbage ... } , examples below. I have searched the ML library pages and the PolyML docs looking for this syntactical construct and have been unable to find it. Does anyone know what this signifies? let metaSubst = @{lemma "PROP P t \<Longrightarrow> PROP prop (x \<equiv> t \<Longrightarrow> PROP P x)" by (unfold propDef)} [@{thm propDef}] Thanks David Thayer

3 3

Building on Vista x64 with VS 2008
by robertr＠rftp.com 26 Jun '09

26 Jun '09

I have recently downloaded the PolyML 5.2.1 archive and built it on my 4GB Vista x64 SP2 box, feeding the supplied Visual Studio workspace to my VS 2008 SP1 dev environment. This went quite well, with only 2 build errors and one execution problem stopping the entire bootstrapping process! :) The 2 errors are just from using the newer dev environment: the _osver variable is no longer available. So, the 2 usages (line 1434 in basicio.cpp and line 168 in process_env.cpp) need to change. As a minimal change, I would suggest if (_osver & 0x8000) => if (GetVersion() & 0x80000000) as something that will still work in older and newer environments. The execution issue happens early in the "Custom Build Step" use of PolyImport.exe: during startup, the polymain(...) function obtains the size of installed physical memory, and then defaults to using half of it. IMHO, this logic could use a new look, given modern system memory levels (4GB and up is becoming common, especially in today's dev environments)... in any case, the first actual call to VirtualAlloc is for something like 1.5 GB, and is failed. Since I was willing to believe that finding that much contiguous virtual address space could be hard - or maybe it was just that the demand to commit all of it too was the actual cause - I just forcibly cut the memory usage back to 256M and the rest of the build proceeded flawlessly, creating a functioning PolyML system. I built all 4 of the pre-defined targets - the only one that appeared seriously slow was the "IntDebug". ;) So, possibly adding some logic to (in the absence of command-line or other override) "cap" the default memory usage at 256 MB or 512 MB might be in order? Robert

3 10

Trac and CVS on SourceForge
by David.Matthews＠prolingua.co.uk 24 Jun '09

24 Jun '09

Having tried out Trac on SourceForge I've now disabled it. The problem is that SourceForge does not provide access to the configuration file necessary to add notification email addresses so it wouldn't be possible to know that a bug had been posted without checking the site. The SourceForge bug Tracker is still available and that does provide email notification. At the same time I've removed CVS since we're now using SVN. Regards, David.

1 0

PolyML Users
by ldixon＠inf.ed.ac.uk 03 Jun '09

03 Jun '09

Hello, I'm trying to find out what projects use, or can be built on PolyML, in order to write a grant application to improve PolyML and provide a continuous level of support for it. In particular, the grant would aim to provide better editing support (we have started working on this already), improvements to the module system (based on existing work by Andreas Rossberg and others), improvements to garbage collection for multi-threading programs, and perhaps improved compatibility with OCaml and Haskell (maybe based on the HLVM project). If you feel you would benefit from this, please do let me know. The more users of PolyML, the stronger our case. :) Many thanks, lucas

1 0

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

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 2009