Poly/ML December 2009

polyml@lists.polyml.org

6 participants
6 discussions

[Fwd: Re: [polyml] Building Poly/ML on MacOS X 10.6]
by rda＠lemma-one.com 29 Dec '14

29 Dec '14

I wrote: > I am completely baffled. I thought I hada solved all my problems on > MacOS X > 10.6 and was just tidying up, when I had to recompile a 32 bit > version of > Poly/ML to test a tidied up make file. This failed because > PolyML.Compiler.printTypesWithStructureName no longer exists. The same > problem happened when i rebuild a 64 bit version. What has happened? but it was a false alarm: my make file was wrong for other reasons and the absence of PolyML.Compiler.printTypesWithStructureName was not relevant. No doubt there are good reasons why this variable has been withdrawn. Regards, Rob.

3 6

IDE for PolyML 5.3
by peter.bader＠gmx.de 26 Dec '09

26 Dec '09

Hello all, I saw that there is an IDE communication protocol support in 5.3. Is there an IDE for Windows or LINUX? Best regards, Peter Bader

2 1

Windows Command Line Version
by peter.bader＠gmx.de 26 Dec '09

26 Dec '09

Hello all, under Windows PolyML (I am using 5.3) starts its own window. Is there a Windows Command Line version? Why would I want it? I am using emacs with SML mode. This allows very convenient syntax oriented editing of the source code and running an ML "interpreter" in an extra emacs window/buffer, to which I can send fragments of my source code. I would love to switch to PolyML but keep my environment. I would appreciate any help. (I searched through the whole mailing list archive (polyml.mbox), but could not find an answer). Best regards Peter Bader (enthusiastic PolyML novice)

2 1

problem with polyml on ubuntu on virtualbox
by jjduan＠cs.utah.edu 24 Dec '09

24 Dec '09

I have a Virtualbox set up on Windows 7 64 bit. On top of it I run Ubuntu. My intention is to build HOL on Ubuntu. However I ran into some issue which is weird. It appears on Ubuntu 9.10/9.04, 32 or 64 bit, Polyml 5.3 or 5.2.1. Seems to be a universal issue. I know someone who runs 64bit Ubuntu 9.10 with Polyml 5.3 and HOL on a real machine and he doesn't have problems. Below is a trace. Any help? Error- in '/tmp/MLTEMPSab29r', line 586. Structure (Polyhash) has not been declared Found near open Polyhash Error- in '/tmp/MLTEMPSab29r', line 587. Value or constructor (mkPolyTable) has not been declared Found near mkPolyTable (length vlist, Fail "varmap") Error- in '/tmp/MLTEMPSab29r', line 589. Type error in function application. Function: insert varmap : ''a list -> ''a list Argument: (h, i) : 'a * 'b Reason: Can't unify ''a list to 'a * 'b (Incompatible types) Found near (insert varmap (h, i); enum t (i - 1) (h :: A)) Error- in '/tmp/MLTEMPSab29r', line 591. Value or constructor (peek) has not been declared Found near case peek vmap v of NONE => v | SOME i => Bv i Error- in '/tmp/MLTEMPSab29r', line 592. Value or constructor (transform) has not been declared Found near transform (fn x => x + 1) vmap Error- in '/tmp/MLTEMPSab29r', line 670. Structure (Polyhash) has not been declared Found near open Polyhash Error- in '/tmp/MLTEMPSab29r', line 671. Value or constructor (mkPolyTable) has not been declared Found near mkPolyTable (Array.length prefix, Fail "AV") Error- in '/tmp/MLTEMPSab29r', line 675. Value or constructor (peekInsert) has not been declared Found near case peekInsert AV (n, PREFIX i) of NONE => insertl rst (i + 1) dupls | SOME _ => ... ... (... + ...) ((...) :: dupls) Error- in '/tmp/MLTEMPSab29r', line 680. Type error in function application. Function: insert AV : ''a list -> ''a list Argument: (s, BODY) : 'a * occtype Reason: Can't unify ''a list to 'a * occtype (Incompatible types) Found near ( (fn s => insert AV (s, ...)), (fn (s, ...) => ... ... (...)), peek AV, dupls ) Error- in '/tmp/MLTEMPSab29r', line 681. Type error in function application. Function: insert AV : ''a list -> ''a list Argument: (s, PREFIX i) : 'a * occtype Reason: Can't unify ''a list to 'a * occtype (Incompatible types) Found near ( (fn s => insert AV (s, ...)), (fn (s, ...) => ... ... (...)), peek AV, dupls ) Error- in '/tmp/MLTEMPSab29r', line 682. Value or constructor (peek) has not been declared Found near let open Polyhash; val AV = mkPolyTable (...); fun insertl ... = ... | ...; val ... = ... in ((fn s => ... ... (...)), (fn (...) => ... ...), peek AV, dupls) end Static Errors Thanks, Jianjun

2 1

Pretty-printing in version 5.3
by rda＠lemma-one.com 14 Dec '09

14 Dec '09

I can't find any documentation for the new approach to pretty-printing in version 5.3 of Poly/ML. For ProofPower, I am using the PolyML.install_pp interface that is provided for backwards compatibility. but it doesn't seem to give the same results. I find that many things that used to print nicely spread over several lines now print as one long thin column with only one or two symbols in each column. The problem seems to be with the interpretation of the boolean part of the parameter to the function that begins a block. The attached code shows a difference between 5.2 and 5.3. On 5.2 both times the value of t t is pretty-printed you get the same results, which is one symbol per line until what is left will fit all on one line. On 5.3, the first time you get a sqaureish block and the second time you get one symbol per line. I can't find any documentation for the install_pp interface either so I don't really know which behaviour is right. Regards, Rob. datatype TERM = Num of int | Plus of TERM * TERM; fun term_pp (funs as ( adds : string -> unit, beginb : int * bool -> unit, space : int * int -> unit, endb : unit -> unit)) (t : TERM) = ( case t of Num n => adds (Int.toString n) | Plus (t1, t2) => ( beginb(0, true); term_pp funs t1; space(1, 0); adds "+"; space(1, 0); term_pp funs t2; endb() ) ); fun pp flag (funs as (adds, beginb, space, endb)) _ _ t = ( beginb(0, flag); beginb(0, false); (* removing this and the matching end makes no difference *) term_pp funs t; endb(); endb() ); fun interval m n = ( let fun aux acc i = ( if i < m then acc else aux (i::acc) (i-1) ); in aux [] n end ); PolyML.Compiler.lineLength := 40; val _ = PolyML.install_pp (pp false); val t = foldr Plus (Num 0) (map Num (interval 1 40)); val _ = PolyML.install_pp (pp true); t;

3 7

Fixes to 5.3
by David.Matthews＠prolingua.co.uk 05 Dec '09

05 Dec '09

I've set up a branch in SVN to contain fixes to the current release. I'm intending to limit this to problems that have been found since the release which actually affect people. Other problems will be fixed in trunk and included in the next release. So far I've applied the fix to the problem with X-Windows that Rob reported and a fix that Aleksej Saushev sent for the Makefiles under BSD. The branch can be found using svn co https://polyml.svn.sourceforge.net/svnroot/polyml/fixes-5.3 Depending on what else comes up I may produce a 5.3.1 release. Meanwhile there's ongoing work towards 5.4. Regards, David

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 December 2009