Poly/ML

polyml@lists.polyml.org

695 discussions

Poly/ML on Mac OS X
by David.Matthews＠prolingua.co.uk 20 Sep '02

20 Sep '02

Several people contacted me about Mac OS X 10.2 so I decided to take the plunge and buy it. I managed to track down the problem and you can find an updated version of Poly/ML in http://www.polyml.org/distrib/polyml-macosx.4.1.3.tar.gz . This contains executable and database and will only run on version 10.2 . I'll update the source in due course. For those who are interested, the problem was that the kernel included with 10.2 calls a signal handler with different parameters from previous versions. Previously it was called with a sigcontext structure containing register information, now the kernel seems to follow Solaris in providing a ucontext structure. Poly/ML needs this information because it uses a variety of signals to deal with things such as writes to database mutables, long-precision arithmetic and garbage-collection traps. Needless to say the change was not documented and the signal man page still refers to sigcontext, indeed it appears not to have changed since 1994. The only way I managed to find out what was going on was to download the Darwin kernel source and look at that. At least the source is available. The way the change was made means that it would be difficult to provide a binary that would work under 10.2 and also earlier versions of Mac OS X. It's also difficult to provide source that will automatically select the correct version when it's compiled. I'm going to assume that most people will have upgraded to 10.2 and concentrate on that. Let me know if there are any further problems. David.

1 0

PolyML om Mac OS X 10.2 (Jaguar)
by kramer＠acm.org 12 Sep '02

12 Sep '02

--Apple-Mail-7--233804249 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=US-ASCII; format=flowed I've tried the binary download for Max OS X on 10.2 (Jaguar) and found PolyML to "hang". It starts, but there's no input prompt. It chews cpu cycles though. Then I tried to compile the sources and ran into the problem below. ? Does anyone have a patch to make PolyML work on OS X 10.2? Thanks, - Reto $ cd driver; ./configure; make [...] cc -DGCC -DPOWER2 -DMACOSX -g -O2 -Wall -DDEFAULT_POLYPATH='".:/usr/lib/poly:/usr/local/lib/poly"' -c -o run_time.o run_time.c run_time.c: In function `init_run_time_system': run_time.c:1249: warning: implicit declaration of function `sigaltstack' cc -E -DPOWER2 -DMACOSX -DGCC power_assembly.S | tr ';' '\012' > powtemp.s cc -x assembler-with-cpp -o power_assembly.o -c powtemp.s power_assembly.S:673:Parameter syntax error (parameter 3) power_assembly.S:723:Parameter syntax error (parameter 3) make[1]: *** [power_assembly.o] Error 1 make: *** [none] Error 2 --Apple-Mail-7--233804249 Content-Transfer-Encoding: 7bit Content-Type: text/enriched; charset=US-ASCII I've tried the binary download for Max OS X on 10.2 (Jaguar) and found PolyML to "hang". It starts, but there's no input prompt. It chews cpu cycles though. Then I tried to compile the sources and ran into the problem below. ? Does anyone have a patch to make PolyML work on OS X 10.2? Thanks, - Reto $ cd driver; ./configure; make [...] cc -DGCC -DPOWER2 -DMACOSX -g -O2 -Wall -DDEFAULT_POLYPATH='".:/usr/lib/poly:/usr/local/lib/poly"' -c -o run_time.o run_time.c run_time.c: In function `init_run_time_system': run_time.c:1249: warning: implicit declaration of function `sigaltstack' cc -E -DPOWER2 -DMACOSX -DGCC power_assembly.S | tr ';' '\012' > powtemp.s cc -x assembler-with-cpp -o power_assembly.o -c powtemp.s <bold>power_assembly.S:673:Parameter syntax error (parameter 3) power_assembly.S:723:Parameter syntax error (parameter 3) </bold>make[1]: *** [power_assembly.o] Error 1 make: *** [none] Error 2 --Apple-Mail-7--233804249--

2 2

Problems interacting using stdin/stdout
by bart.jacobs＠cs.kuleuven.ac.be 26 Aug '02

26 Aug '02

Hi, I'm writing a program that runs Poly/ML as a child process, redirecting standard input and output. I'm working on the Windows XP platform. Poly/ML behaves suboptimally in this setting. I'm experiencing two problems. One problem is fatal, the other is very annoying. The fatal problem is that Poly/ML simply hangs at some point during the interaction. I suppose it's some kind of deadlock. The problem is reproducible in that it happens at the exact same point, every time I run the program with the same input. But the entire environment in which the program runs is so big (it's Isabelle) that I'm not going to try to describe it. I'm just hoping that someone out there already knows about this. I don't have a debugger now, but when I get hold of one, I will try to hunt down the bug myself. The annoying problem is that Poly/ML goes to sleep for 0.5 seconds after every command. My program feeds hundreds of commands at a time to Poly/ML, so this means a *huge* slowdown. Putting all commands on a single line is not an option, since I need to stop feeding commands as soon as a command prints an error message. I think I found the cause of this sleeping problem: it's the MsgWaitForMultipleObjects call in processes.c. In the comments in the source code, David Matthews explains that it's just too hard to avoid this. I'm sure that's true in the general case, when you're running many lightweight processes, all of which are reading, writing, doing GUI stuff, etc., but in my case, Poly/ML is really just a simple sequential single-threaded read-eval-print loop. So, what I'm saying is, would it be possible to do some special-casing for the one-lightweight-process case on the Windows platform, so that you could just do blocking I/O calls? (This would probably also solve the fatal problem described above.) And I also don't really need the DDE functionality, so that we could do away with the message pump. These problems would have caused me to defect to another ML implementation, if it wasn't that Poly/ML is simply by far the best implementation out there. Many thanks to David Matthews for this great piece of software! But again, I hope there is some way to fix these problems. Bart

1 0

problem installing polyml on linux
by baxter＠math.umn.edu 17 Jul '02

17 Jul '02

Hello all, after using polyml on my windows machine I decided to install it on our dept linux system, and seem to be doing something wrong (as usual!). I downloaded the gzipped tarred archive. When I try to start it I type poly ML_dbase Then I get the following message: Poly/ML RTS version I386-4.1.2 (14:43:27 Jan 15 2002) Copyright (c) 2002 CUTS and contributors. Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%) Segmentation fault I also downloaded the driver source and built poly with gcc 2.95.4 and glibc 2.2.5. I downloaded the i386 database by itself. Using these files gives the same result. Can anyone suggest what I should be doing here? Thanks, John

1 0

multiple "where type"
by itz＠speakeasy.org 03 Jul '02

03 Jul '02

Hi, does PolyML support the syntax <sig> where type t = foo and t' = bar ? I am getting parse errors at the "and" when I try to use it. OTOH, <sig> where type t = foo where type t' = bar parses fine, but my sigs are already verbose enough :( -- Ian Zimmerman, Oakland, California, U.S.A. GPG: 433BA087 9C0F 194F 203A 63F7 B1B8 6E5A 8CA3 27DB 433B A087 EngSoc adopts market economy: cheap is wasteful, efficient is expensive.

3 4

Poly/ML as a component?
by bart.jacobs＠student.kuleuven.ac.be 01 Jul '02

01 Jul '02

Hi. It would be great if it were possible to use Poly/ML from other programming languages. There would be a polyml.so or polyml.dll file, that could be linked with, for example, the following C program: #include "polyml.h" main() { Poly_LoadDatabase("mydb.pmd"); int result = Poly_InvokeFunction_Int_Int("add_one", 5); printf("%d plus one is %d\n", 5, result); } It would of course be better still if there could be a Poly/ML COM component or Poly/ML .NET component (unmanaged and non-verifiable, of course). The problem with these scenarios is that Poly/ML would have to live together with other modules in the same process. This probably causes multithreading issues and address space issues. Poly/ML uses memory mapping to load the database. It uses fixed addresses for this. What if the address range is being used by other modules? Poly/ML uses certain operating system functionality to implement multithreading. Could this interfere with other modules? We have a design space here: one extreme is Poly/ML, which is very efficient, but has rather poor interoperability. The other extreme is SML.NET (see www.research.microsoft.com) (I'm talking about the concept, since it has not (yet?) been released): this would provide great interoperability, but most probably at the expense of efficiency in time and space. Of course, Poly/ML is the greatest programming language ever and all other languages are superfluous :-), but we cannot avoid the fact that some people use other languages, and, as a result, useful libraries get written in other languages. My problem is that I want to combine the Isabelle theorem proving system (isabelle.in.tum.de), written in SML, with the .NET Framework's user interface components. As an approximation to the DLL approach I discussed above, I'm looking into writing some simple remote procedure call code to connect the Poly/ML process and the .NET process. That way, Poly/ML would be a kind of "server" accepting remote procedure calls through a socket. (See also my previous mail.) Is it possible to run Poly/ML on Windows without the user interface? This would allow me to invisibly launch Poly/ML from the .NET program, with a database that contains an "onEntry" function that listens on a TCP port and accepts remote procedure calls. Any thoughts on this?

3 2

Socket.accept doesn't seem to work.
by bart.jacobs＠student.kuleuven.ac.be 01 Jul '02

01 Jul '02

Hi. When I use Socket.accept in Poly/ML 4.1.2 on Windows, I get SysErr("accept failed", SOME EFAULT). Also, I think I found a bug in the driver source code, but I'm not sure that the latter causes the former. Specifically, in the code for Socket.Ctl.setNBIO (POLY_SYS_net number 43), it says ioBits |= ~NON_BLOCKING_IO instead of ioBits |= NON_BLOCKING_IO I want to thank David Matthews for giving us Poly/ML.

2 1

compilation problem - am I going mad?
by itz＠speakeasy.org 26 Jun '02

26 Jun '02

Sorry for sending this to the request address :( Hi, trying to compile these two files: (* BITSET.sml *) signature BITSET = sig exception Not_found; (* raised by [choose] *) type ty; (* type of bitsets*) val make_bitset : int -> ty ; (* [make_bitset size] creates a new empty bitset containing [size] bits.*) val copy : ty -> ty ; (* [copy v] returns a fresh exact copy of bitset [v].*) val copy_negated : ty -> ty ; (* [copy_negated v] returns a fresh bit vector that is the complement of [v].*) val set : ty -> int -> unit ; (* [set v i] sets the [i]th bit of vector [v].*) val clear : ty -> int -> unit ; (* [clear v i] clears the [i]th bit of vector [v].*) val test : ty -> int -> bool ; (* [test v i] tests the [i]th bit of vector [v].*) val neg : ty -> unit ; (* [neg v] complements the vector [v] in place.*) val band : ty -> ty -> unit ; (* [band v_to v_from] performs a [land] of [v_to] and [v_from], changing [v_to] in place.*) val bor : ty -> ty -> unit ; (* [bor v_to v_from] performs a [lor] of [v_to] and [v_from], changing [v_to] in place.*) val bxor : ty -> ty -> unit ; (* [bxor v_to v_from] performs a [lxor] of [v_to] and [v_from], changing [v_to] in place.*) val bsub : ty -> ty -> unit ; (* [bsub v_to v_from] computes the set difference [v_to - v_from], storing the result in [v_to].*) val is_sub : ty -> ty -> bool ; (* [is_sub v1 v2] tests if vector [v1] is a subset of [v2].*) val is_equal : ty -> ty -> bool ; (* [is_equal v1 v2] tests if vector [v1] is structurally equal to [v2].*) val choose : ty -> int ; (* [choose v] returns an arbitary integer [i] such that [v[i] = true], if there is one, otherwise raises [Not_found]. Equal integers are returned for structurally equal vectors.*) end; (* BITSET.sml ends here *) (* Bitset.sml *) structure Bitset :> BITSET = struct exception Not_found; (* raised by [choose] *) exception Size_mismatch; (* import selected stuff from LargeWord and Array *) val wordSize = LargeWord.wordSize; type word = LargeWord.word; val notb = LargeWord.notb; val << = LargeWord.<< ; val fromLargeInt = LargeWord.fromLargeInt; val andb = LargeWord.andb; val orb = LargeWord.orb; val xorb = LargeWord.xorb; val length = Array.length; val sub = Array.sub; val tabulate = Array.tabulate; val update = Array.update; val modifyi = Array.modifyi; val foldli = Array.foldli; val appi = Array.appi; type ty = { size : int , last_mask : word , bits : word Array.array }; fun make_mask (i: int) = notb (<< (notb (fromLargeInt 0), Word.fromInt i)); fun word_size (s: int) = (s div wordSize) + 1; fun make_bitset s = if s < 0 then raise Size else let val bits = Array.array (word_size s, fromLargeInt 0); val mask = make_mask (s mod wordSize) in { size = size, last_mask = mask, bits = bits } end ; fun copy v = let val s = #size v ; val ws = word_size s ; fun f i = sub (#bits v, i) in { size = s, last_mask = #last_mask v, bits = Array.tabulate (ws, f) } end ; fun copy_negated v = let val last = length (#bits v) - 1; fun f i = if i <> last then notb (sub (#bits v, i)) else andb (#last_mask v, notb (sub (#bits v, i))) in { size = #size v, last_mask = #last_mask v, bits = Array.tabulate (last+1, f) } end ; fun set v i = let val idx = i div wordSize; val bit = i mod wordSize; val mask = << (fromLargeInt 1, Word.fromInt bit) in update (#bits v, idx, orb (sub (#bits v, idx), mask)) end; fun clear v i = let val idx = i div wordSize; val bit = i mod wordSize; val mask = notb (<< (fromLargeInt 1, Word.fromInt bit)) in update (#bits v, idx, andb (sub (#bits v, idx), mask)) end; fun test v i = let val idx = i div wordSize; val bit = i mod wordSize; val mask = << (fromLargeInt 1, Word.fromInt bit) in andb (sub (#bits v, idx), mask) <> fromLargeInt 0 end; fun neg v = let val last = length (#bits v) - 1; fun f (i, x) = if i <> last then notb x else andb (#last_mask v, notb x) in modifyi f (#bits v, 0, SOME(last+1)) end; fun band to from = if #size from <> #size to then raise Size_mismatch else let fun f (i, x) = andb (sub (#bits from, i), x) in modifyi f (#bits to, 0, SOME(length (#bits to))) end; fun bor to from = if #size from <> #size to then raise Size_mismatch else let fun f (i, x) = orb (sub (#bits from, i), x) in modifyi f (#bits to, 0, SOME(length (#bits to))) end; fun bxor to from = if #size from <> #size to then raise Size_mismatch else let fun f (i, x) = xorb (sub (#bits from, i), x) in modifyi f (#bits to, 0, SOME(length (#bits to))) end; fun bsub to from = if #size from <> #size to then raise Size_mismatch else let fun f (i, x) = andb (notb (sub (#bits from, i)), x) in modifyi f (#bits to, 0, SOME(length (#bits to))) end; fun is_sub v1 v2 = if #size v1 <> #size v2 then raise Size_mismatch else let fun p (i, x, b) = b andalso andb (x, notb (sub (#bits v2, i))) = fromLargeInt 0 in foldli p true (#bits v1, 0, SOME(length (#bits v1))) end; fun is_equal v1 v2 = if #size v1 <> #size v2 then raise Size_mismatch else let fun p (i, x, b) = b andalso x = sub (#bits v2, i) in foldli p true (#bits v1, 0, SOME(length (#bits v1))) end; fun find_bit (w: word) = let fun fb1 i mask = if andb (mask, w) <> fromLargeInt 0 then i else fb1 (i+1) (<< (mask, Word.fromInt 1)) in fb1 0 (fromLargeInt 1) end ; fun choose v = let val ridx = ref ~1; fun f (i, x) = if !ridx = ~1 andalso x <> 0 then ridx := i else () in (appi f (#bits v, 0, SOME(length (#bits v))); if !ridx = ~1 then raise Not_found else let val idx = !ridx; val bit = find_bit (sub (#bits v, idx)) in !ridx * wordSize + bit end) end; end; (* Bitset.sml ends here *) I am getting these errors: > Making Bitset Error: in 'Bitset.sml', line 133. Can't unify Words.LargeWord.word with int (Different type constructors) Found near find_bit(sub( (#bits)(v), idx)) Error: in 'Bitset.sml', line 20. Can't match int to Words.LargeWord.word (Different type constructors) While checking (choose) near structure Bitset :> BITSET = struct exception Not_found exception Size_mismatch val ... = ... type ... ... ... end Error: in 'Bitset.sml', line 20. Can't match int to string -> int (Incompatible types) While checking (make_bitset) near structure Bitset :> BITSET = struct exception Not_found exception Size_mismatch val ... = ... type ... ... ... end Bitset was not declared Exception- Fail "Static errors (pass2)" raised I look at the code forward and backward and really think it is correct. Here's the typing as I see it: bit = find_bit (sub (#bits v, idx)) ^^^ ^^^^^^^^ ^^^ ^^^^^^^ ^^^ int word->int (word array, int)->word word array int !ridx * wordSize + bit ^^^^^ ^^^^^^^^ ^^^ int int int And what in the world has STRING to do with it ?!? February 2002 release of PolyML. -- Ian Zimmerman, Oakland, California, U.S.A. GPG: 433BA087 9C0F 194F 203A 63F7 B1B8 6E5A 8CA3 27DB 433B A087 EngSoc adopts market economy: cheap is wasteful, efficient is expensive.

1 1

PolyML on cygwin?
by Tomas.Juknevicius＠nomagic.com 20 May '02

20 May '02

Hello guys/girls, I'm new to this list, also new to polyML :). I have a question: i'm trying to launch the linux version of polyml on CygWin (under win2000) with little success. The executable 'poly' just answers with: ./poly: 1: Syntax error: "(" unexpected when trying to launch it ... Maybe someone knows the solution or has encountered similar situation? PS why i'm trying the linux version on cygwin under win200 and not polyml for win32? Well, actualy, i'm trying to launch the Isabelle system, (which uses polyML) and it has no win32 version. So i'm stuck with Isabelle on cygwin. When I tried to couple Isabelle/cygwin with win32 version of polyML, win32 executable of polyML could not crunch linux style file paths, supplied by Isabelle under cygwin. Hence i'm stuck with the only combination left - run both Isabelle & linux version of polyML under cygwin. Unfortunately, when linux version of polyML is launched under cygwin, it just seems to complain '1: Syntax error: "(" unexpected'. This output apears no matter what parameters i supply for the poly executable :( -- Tomas Juknevicius

2 1

stack trace
by frittinger＠acm.org 14 May '02

14 May '02

Hello, I'm new to PolyML and have some questions concerning debugging and erro= r messages. The function PolyML.exception_trace prints a number behind each functio= n name in the stack trace. Could someone please tell me what this number indicat= es? Is there a way to get the line number of the input file (like njml does= ) where a Match exception is thrown? Thanks in advance, Frank ***********************************************************************= Frank Rittinger Albert-Ludwigs Universit=E4t Freiburg, Institut f=FCr Informatik Georges-Koehler-Allee, Geb. 52 (Room 00-021), 79110 Freiburg, Germany Phone: +49 761 203 8245 Fax: +49 761 203 8242 URL: http://www.informatik.uni-freiburg.de/~rittinge ***********************************************************************=

2 1

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