Poly/ML March 2004

polyml@lists.polyml.org

7 participants
6 discussions

Poly/ML on Mac OS X 10.3
by rda＠lemma-one.com 17 Apr '04

17 Apr '04

Every time you run poly, it does a memory access that causes a memory fault, which it then handles and recovers from - a perfectly reasonable way to do its memory management, I would say. Unfortunately, on Mac OS X, the memory fault triggers a crash log to be generated, and this causes quite an overhead (about 30% of the CPU time in my ProofPower build which runs poly a few hundred times). On Mac OS X 10.2, you could turn this off with the Console utility preferences, and that claws back the lost CPU, but you can't do this on Mac OS X 10.3. Has anyone got a work-around for this? I consider it to be a bug in Mac OS X and would report it to Apple if I had a simple program to demonstrate the problem (but the technique Poly/ML is using is quite a hard one, so that's not trivial). Regards, Rob.

2 3

Licensing (was Re: [polyml] Is PolyML development dead?)
by David.Matthews＠deanvillage.com 23 Mar '04

23 Mar '04

On Wednesday, Mar 17, 2004, at 21:36 Europe/London, Rob Arthan wrote: >> On the other hand, GPL is too strong because it would appear >> to make it impossible for a company to develop software and distribute >> it with Poly/ML in such a way that they could retain their code as >> closed source. It's possible that the "Lesser GPL" that is used for >> libraries might be acceptable. > > I think the GPL is actually much less restrictive than many people > think > (ProofPower is distributed under GPL, although I did agonise over this > for a > long time). > > The relevant paragraph of the GPL is this: > > 2 b) You must cause any work that you distribute or publish, that in > whole or > in part contains or is derived from the Program or any part thereof, > to be > licensed as a whole at no charge to all third parties under the terms > of this > License. > > I don't believe that code compiled with a compiler counts as "derived > from the > compiler". The situation would, of course, be a bit less muddy if one > had > true separate compilation for ML (but even with gcc, compiled object > code > will contain compiled open source libraries, and I don't believe that > the > above paragraph means you can't sell binaries compiled with gcc). > > Regards and apologies for this long off-topic diversion, It may be slightly off-topic but this issue of the licence is really quite important and I'm keen to get a feel for what people think about it. The situation you describe is the reason that there's a difference between the GPL and the "Lesser GPL". Although I haven't read these through in detail I understand that gcc libraries are distributed under the Lesser GPL precisely because it doesn't include the clause you've quoted. If Poly/ML were distributed under the full GPL it would (as far as I can see) be impossible for a user to distribute a complete binary containing the Poly/ML run time system and database and also containing code that the user wanted to keep closed. Regards, David.

3 2

Tracing function calls
by pocm＠netvisao.pt 22 Mar '04

22 Mar '04

Hi, Is there anyway in PolyML to trace function calls? Cheers, -- Paulo J. Matos : pocm [_at_] mega . ist . utl . pt Instituto Superior Tecnico - Lisbon Computer and Software Eng. - A.I. - > http://mega.ist.utl.pt/~pocm --- -> God had a deadline... So, he wrote it all in Lisp!

2 1

Extending stack limit
by pocm＠netvisao.pt 22 Mar '04

22 Mar '04

Hi, While playing with polyml limits I executed the function squares from Paulsons Book: fun squares r = let fun between (x, y) = (* all pair between x and y*) let val diff = r - x*x fun above y = (* all pairs above y*) if y>x then [] else if y*y < diff then above (y + 1) else if y*y = diff then (x, y) :: between(x-1, y+1) else (*y*y > diff*) between(x-1, y) in above y end; val firstx = floor(Math.sqrt(real r)) in between(firstx, 0) end; And then I executed and I got: > squares 3092481270109283; Warning - Increasing stack from 147456 to 294912 bytes Warning - Increasing stack from 294912 to 589824 bytes Warning - Increasing stack from 589824 to 1179648 bytes Warning - Increasing stack from 1179648 to 2359296 bytes Warning - Increasing stack from 2359296 to 4718592 bytes Warning - Increasing stack from 4718592 to 9437184 bytes Warning - Increasing stack from 9437184 to 18874368 bytes Warning - Increasing stack from 18874368 to 37748736 bytes Warning - Increasing stack from 37748736 to 67108860 bytes Warning - Stack limit reached - interrupting process Exception- Interrupt raised I know it's a huge number, that was the idea. :D How can I increase the stack limit? Cheers, -- Paulo J. Matos : pocm [_at_] mega . ist . utl . pt Instituto Superior Tecnico - Lisbon Computer and Software Eng. - A.I. - > http://mega.ist.utl.pt/~pocm --- -> God had a deadline... So, he wrote it all in Lisp!

2 1

Is Isabelle/PolyML reentrant? (fwd)
by johnm＠cse.ogi.edu 22 Mar '04

22 Mar '04

Hi, I originally sent this post to the Isabelle theorem prover users' mailing list. Larry Paulson suggested I forward it to the Poly ML mailing list as well. In particular, does Poly ML support the ability for C functions to call ML functions, like SML/NJ does? Thanks! -john -- John Matthews Assistant Professor johnm(a)cse.ogi.edu OGI School of Science & Engineering (503) 748-1220 Oregon Health & Science University http://cse.ogi.edu/~johnm Beaverton, OR USA ---------- Forwarded message ---------- Date: Thu, 18 Mar 2004 15:58:41 -0800 (PST) From: John Matthews <johnm(a)cse.ogi.edu> To: isabelle-users(a)cl.cam.ac.uk Subject: Is Isabelle/PolyML reentrant? Tom Harke and I are interested in modifying an external oracle (verification tool) for Isabelle that is written in C. We would like the oracle to call back to selected Isabelle tactics while it is running, in order to deal with verification conditions that the external oracle can't handle itself. For this to work, the foreign function interface of the underlying SML compiler needs to allow foreign functions to call SML functions. I've found documentation for SML/NJ that indicates that this is possible, but nothing in the Poly ML documentation says that this can be done. Does this mean that I will be limited to running Isabelle on SML/NJ? If so, is support for running Isabelle on SML/NJ going to continue, or will future versions of Isabelle be limited to running only on Poly ML? Thanks, -john

2 1

Is PolyML development dead?
by pocm＠netvisao.pt 17 Mar '04

17 Mar '04

Hi all, Is PolyML development dead? Is it safe to keep developing ML programs dependent on PolyML compiler? Cheers, -- Paulo J. Matos : pocm [_at_] mega . ist . utl . pt Instituto Superior Tecnico - Lisbon Computer and Software Eng. - A.I. - > http://mega.ist.utl.pt/~pocm --- -> God had a deadline... So, he wrote it all in Lisp!

6 12

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 March 2004