Poly/ML February 2008

polyml@lists.polyml.org

8 participants
7 discussions

REAL signature
by fluet＠tti-c.org 29 Feb '08

29 Feb '08

The implementation of the REAL signature in the Basis Library omits the "where type real = real" constraint on the Math : MATH sub-structure. Without the constraint, when writing a functor with a R : REAL argument, the body of the functor cannot "see" that R.real and R.Math.real are the same type, so the type checker does not allow R.+(R.Math.e, R.Math.pi).

2 1

a couple of how-tos
by Michael.Norrish＠nicta.com.au 27 Feb '08

27 Feb '08

I'm playing with porting HOL4 from Moscow ML to PolyML, and have found it a reasonably pleasant task so far (Moscow ML's out-of-date Basis Library is the major annoyance). However, there are a couple of things I don't quite see how to do: * how do I install a pretty-printer in my top-level loop so that my special data-types get printed nicely? Moscow ML offers Meta.installPP, and my scouring of the mailing list suggests I might use RunCall.Inner.install_pp. This is of type ((string -> unit) * (int * bool -> unit) * (int * int -> unit) * (unit -> unit) -> int -> 'a -> 'b -> unit) -> unit What do the various parameters given to the printing function mean? The first emits actual text, and the int is perhaps the linewidth, but what about the others? * Is there a way of doing a pointer-equality comparison on arbitrary values in order to give an efficient approximation of normal equality? In MoscowML there's an Obj.magic that can be used to turn 'a into an int (the underlying pointer I think). Is there something similar I can use in Poly? Many thanks, Michael.

2 1

a how-to answered already
by Michael.Norrish＠nicta.com.au 27 Feb '08

27 Feb '08

I see there is a PolyML.pointerEq.. Michael.

1 0

Re: Compiling PolyML on Windows
by David.Matthews＠prolingua.co.uk 19 Feb '08

19 Feb '08

Dave Berry wrote: > I've just downloaded PolyML to have a play about with it. What do I > need in order to compile it on Windows? I see from the docs that it > uses standard GNU tools, so do I need Cygwin plus the GNU C++ compiler? Hi Dave, I'm copying this to the Poly/ML mailing list since it may be of wider interest. You basically have three options for building Poly/ML on Windows. 1. Cygwin. You can build it in Cygwin, which essentially provides a Posix environment on Windows. In particular it supports signals which aren't a Windows concept. When built on Windows Poly/ML has to be run within a shell. 2. Mingw+Msys. Mingw contains the GNU compiler for Windows. Msys provides a shell for Mingw so that the configure script will run. This builds Poly/ML as a native Windows application which has a simple GUI. 3. Microsoft C++. The Poly/ML source includes a Visual C++ 6.0 workspace and project. This can be used to build a native Windows application. Poly/ML also requires the Microsoft assembler, MASM. I think there are versions of Microsoft C++ and MASM that can be downloaded free of charge for personal use. Which of these is easiest depends on what you already have and also what environment you are building for. David.

1 0

CPU timers in polyml
by Brian.Campbell＠ed.ac.uk 16 Feb '08

16 Feb '08

Hello everyone, I'm using the Timer structure from the basis library to measure the CPU time used during execution. Comparing the times returned by Timer.checkCPUTimes with those reported by the shell, the nongc times look suspiciously like they include the gc times as well. Shouldn't these be subtracted? Thanks, Brian Campbell

2 1

C finalizers or weak pointer mechanism?
by jstanley＠galois.com 15 Feb '08

15 Feb '08

Hello everyone, I'm currently attempting to interact with a C library via the CInterface. So far so good, but there are times when the C functions I invoke do allocation in the C heap. Is there a finalizer registration mechanism available in Poly/ML that I can use to invoke appropriate tear-down functions in the C library when Poly/ML is done with the wrapped vol? If not, is there a weak pointer mechanism available that would allow me to accomplish the same? References to some example code that does this would be ideal (and appreciated) in either of the above cases. Thanks much, Joel Stanley jstanley(a)galois.com

4 4

Re: Interrupts in Poly/ML 5.1
by David.Matthews＠prolingua.co.uk 10 Feb '08

10 Feb '08

Rob, I'm copying this to Poly/ML mailing list since I think there are issues here that may affect other users. The handling of console interrupt (control-C, SIGINT) changed quite significantly in 5.1 as a result of changing from a single threaded model to multiple threads. It's complicated because there are significant differences in the way Mac OS X and Linux handle signals with multiple threads. Since there may be Isabelle users reading this it's worth pointing out that Isabelle replaces the default Poly/ML SIGINT handler with its own handler using Signal.signal. This uses Thread.Thread.broadcastInterrupt to send an Interrupt exception to all the threads, effectively the same as using the "f" option in the default handler. I removed the "s" option from the handler since ultimately this depended on the old "Process" mechanism for parallelism. The alternative top-level shell worked by having a second list of runnable processes and the effect of typing "s" in the control-C handler was to switch between these. With the current thread mechanism the run queue is handled by the kernel so this didn't really make sense and I couldn't see how to handle sub-shells with the new mechanism. The other problems are to do with the way signals are handled when there are multiple threads. Even if there is only a single ML thread and the Thread structure is not used Poly/ML is actually running at least two threads. The "main thread" is responsible primarily for garbage collection and is normally blocked waiting the ML code, which runs on a separate thread. When control-C is pressed the operating system sends the SIGINT to one of these threads. In Mac OS X, in particular, it always sends the signal to the main thread. The ML thread continues to run in parallel. While I was writing this I realised that there was a possible solution to the problems that this created and which you noticed. Previously the handler for SIGINT actually ran the loop that read from the terminal and looked at the "f", "c", "q", "t" etc codes. I've now changed this so that when SIGINT arrives it simply sets a flag. Some time later one of the ML threads (which one is indeterminate) runs the default console interrupt handler if an alternative one has not been set up. This allows the "t" (traceback) option to work since it is actually running on an ML thread. It also avoids the race conditions that arise if both the interrupt handler and the ML code are reading from the terminal at the same time, but only if the thread that runs the interrupt handler is the same as the one reading from the terminal. That will, of course, be the case if there is only one ML thread. This is still quite messy. I would prefer to get rid of the default interrupt handler that reads from the terminal altogether and switch to requiring the user to set up a handler for SIGINT using the Signal structure. Regards, David. Rob Arthan wrote: > David, > > Thanks for the prompt fix. In fact, I should confess that my current > approach in ProofPower only uses the length of the hierarchy list and > not the values of the strings in it, so I don't actually need the fix at > the moment. > > ProofPower now builds and tests on Poly/ML 5.1 on both Linux and Mac OS > X, but I have some problems with keyboard interrupts. First of all two > comments, I note that the s(witch) command is no longer available and it > seems as if the t(race) command is never able to print a trace. > > On both OSs the f(ail) and q(uit) command seem to behave differently > from 4.2.0. There is also a separate problem on Mac OS X when an > interrupt arrives while poly (or my executable with the read-eval-print > loop tailored for ProofPower) is waiting for input rather than > excecuting a function. I need to do some more investigation into the > common problem, so the rest of this e-mail is about the Mac OS > X-specific problem. (As I am using Mac OS X version 10.3.9 which is a > bit long in the tooth, I am wondering whether Poly/ML 5.1 just isn't > supported on it). > > Here is the sort of thing that happens (this is copied out of Terminal > with "\n"s added by me to show where I had to hit return to make > something happen): > > rda]- poly > Poly/ML 5.1 Release > > ^C > =>?\n > # ;\n > Error: Value or constructor (?) has not been declared Found near ? > > Static errors (pass2) > > > ^C\n > > ^D\n > =>?\n > Type q(uit - Exit from system) > c(ontinue running) > f(ail - Raise an exception) > or t(race - Get a trace of calls) > =>rda]- > > On the last line of the above, I didn't type anything: the "=>" prompt > appeared and I just waited a few seconds and then poly exited (which > would also have happened if I hadn't typed the second "?" fairly > quickly). It feels as if there are two separate threads responding to > keyboard gestures in an uncoordinated way. > > Regards, > > Rob.

2 1

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 February 2008