Poly/ML

polyml@lists.polyml.org

720 discussions

time measurement
by p.clayton＠eris.qinetiq.com 08 Apr '04

08 Apr '04

All, I have a few questions about timing... 1. Are the times printed by PolyML.timing `user' times or elapsed times? (I suspect the first but would like to check...) 2. Do any of these times include garbage collection? 3. Is there any way for an ML program to access these times, i.e. can they be bound (perhaps as a record) to an ML name? (Either at the top-level only or even within a program for time so far.) 4. If the utime component of Posix.ProcEnv.times () was used to measure sections of code within a program would this time include interludes for garbage collection? (Is the garbage collector a different process and therefore not counted in this `user' time?) Thanks for any help, Phil.

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

Trying to work through the C FFI document
by pocm＠netvisao.pt 19 Dec '03

19 Dec '03

Hi all, I've created sample.c file with: int difference (int x, int y) { return x > y ? x - y: y - x; } Run gcc and ld: pmatos@euler sml_c_scheme $ gcc -c sample.c -o sample.o pmatos@euler sml_c_scheme $ ld -o sample.so sample.o ld: warning: cannot find entry symbol _start; defaulting to 0000000008048094 pmatos@euler sml_c_scheme $ Created an sml file with: fun get_sym lib sym = load_sym (load_lib lib) sym; Ran poly and evaluated the file and I got: Error: in '/tmp/sml6042nwv', line 1. Value or constructor (load_sym) has not been declared Found near load_sym(load_lib(lib))(sym) Error: in '/tmp/sml6042nwv', line 1. Value or constructor (load_lib) has not been declared Found near load_sym(load_lib(lib))(sym) Exception- Fail "Static errors (pass2)" raised Do I need to import something? What's wrong? Best regards, A Merry Christmas and a Happy New Year, -- 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

Building PolyML from scratch
by pocm＠netvisao.pt 12 Dec '03

12 Dec '03

Hi all, I'm trying to build PolyML from scratch so I got the basis, driver and mlsource tarballs and unpacked driver, then unpacked basis and mlsource into driver, did the symlink for CodeCons and in the drive dir I ran: pmatos@euler driver $ ./poly ML_dbase < mlsource/BuildAll.sml Poly/ML RTS version I386-4.1.3 (15:24:34 Dec 10 2003) Copyright (c) 2002 CUTS and contributors. Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%) Unable to open ML_dbase Can anybody please explain me what's the problem? I'm just trying to follow the instructions at: http://www.polyml.org/download.html Best regards, -- 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

Printable Documentation
by pocm＠netvisao.pt 10 Dec '03

10 Dec '03

Hi all, Where can I find printable documentation (PS, PDF, DVI) for the Poly/ML compiler? Best regards, -- 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

InternalError
by skalberg＠in.tum.de 06 Oct '03

06 Oct '03

Hi, I'm writing an interface between a proprietary model checker and the theorem prover Isabelle. For this, I need to parse some XML and I've been carrying around a record with different data I need for this. After trying to exend this record, I get InternalError: addFieldToGeneric: Not a labelled record raised while compiling when trying to load my XML parser. Unfortunately, I'm somewhat restrained when it comes to posting my code, but maybe someone can help me locate the problem anyway. The working version of the program had the functions fun update_typs {typs,thy} typs' = {typs=typs',thy=thy } fun update_thy {typs,thy} thy' = {typs=typs ,thy=thy'} and the main function was just fun import_file filename thy = let val body = body_of (parse_file filename) val typs = Symtab.update_new(("t",Free("t",timeT)),Symtab.empty) in #thy (parse_itl body {typs=typs,thy=thy}) end all code reachable from the function parse_itl only accesses/manipulates the record through functions #thy, #typs, update_typs, and update_thy, and this worked fine. I then needed an extra field, and thefore extended the record: fun update_typs {macs,typs,thy} typs' = {macs=macs,typs=typs',thy=thy } fun update_thy {macs,typs,thy} thy' = {macs=macs,typs=typs ,thy=thy'} fun import_file filename thy = let val body = body_of (parse_file filename) val typs = Symtab.update_new(("t",Free("t",timeT)),Symtab.empty) in #thy (parse_itl body {macs=Symtab.empty,typs=typs,thy=thy}) end with the rest of the program unchanged; This provokes the aforementioned "internal error". I've tried to isolate the problem, but so far without success. Any ideas? Best, - Sebastian -- http://www.mangust.dk/skalberg/

1 0

Jump to page:

2026

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