Poly/ML

polyml@lists.polyml.org

2 participants
711 discussions

Isabelle/ML IDE based on jEdit
by makarius＠sketis.net 09 Feb '11

09 Feb '11

The following might be interesting to people working with Standard ML on the Poly/ML platform. The Isabelle2011 release includes an experimental Prover IDE based on Scala and jEdit that can be also used as one for Standard ML, thanks to the tight integration of Poly/ML into the prover environment. Thus semantic annotations produced by the Poly/ML compiler are presented as tool tips and hyperlinks in the source. This is a simple corollary of much more involved prover infrastructure, and David Matthews has provided some functionality to connect to that quite some time ago. See http://isabelle.in.tum.de/download.html for the regular Isabelle download and installation instructions. An editor session can be started like this (from the shell): Isabelle2011/bin/isabelle jedit -l Pure Test.thy Then Test.thy file can be populated like this: theory Test imports Pure begin ML {* fun fact 0 = 1 | fact n = n * fact (n - 1); *} ML {* fact 42 *} end Now it is possible to hover over the ML text while holding CONTROL (or COMMAND on Mac OS X) to see some of the content produced by the Poly/ML IDE support, rendered as tooltips and hyperlinks. Here is another example: ML {* length *} Hovering with CONTROL/COMMAND will expose a hyperlink pointing to the Poly/ML library sources. For non-prover people it might look a bit odd to embed ML text like that into a formal theory file. At a later stage there will be also management for individual ML files. The document model is stateless as far as ML bindings are concerned. Global side-effects via reference variables are an exception to that. (In the Isabelle context mutable state is never used in application code.) Anybody interested in the augmented Isabelle/ML itself should take a look at chapter 0 of http://isabelle.in.tum.de/dist/Isabelle2011/doc/implementation.pdf There is also some support for parallel functional programming using futures, which did not make it into the manual yet. See http://www4.in.tum.de/~wenzelm/papers/parallel-ml.pdf for some overview. Makarius

1 0

CInterface problem on SPARC/Solaris
by mmoel＠t-online.de 27 Jan '11

27 Jan '11

An HTML attachment was scrubbed... URL: http://lists.inf.ed.ac.uk/mailman/private/polyml/attachments/20110126/948a2…

2 3

Poly/ML 32-bit and memory usage
by noschinl＠in.tum.de 18 Jan '11

18 Jan '11

Hi all, I'm trying to build JinjaThreads, a massive Isabelle theory, using the 32-bit linux version of Poly/ML 5.4.0. The machine is equipped with 6 GiB of RAM and runs a 64-bit linux kernel. After a while, Poly/ML aborts with "Run out of store - interrupting threads". But at this time, the poly process only has allocated around 2.7GiB of memory (VIRT). Why does Poly/ML does not try to allocate more memory? I tried to request a bigger initial heap size with "-H 3500", but this seemed to result in a heap size of 2GiB. As I tested with a small C program, a 32-bit process can allocate (and use) 4070MiB on this machine. Greetings, Lars

1 0

exit code 89 with r1259
by ramana.kumar＠gmail.com 17 Jan '11

17 Jan '11

When I try to build HOL4 using polyml svn 1259 the builder consistently exits with exit code 89 and I think it is running out of memory. I'm sorry I don't have anything more helpful to add - I'm switching back to svn 1243 (which I happen to have and which works), but I'm happy to follow instructions to retrieve information that might lead to finding the problem. I am on x86_64.

2 1

Release Announcement of PolyChrome 0.3
by ldixon＠inf.ed.ac.uk 13 Jan '11

13 Jan '11

Dear ML enthusiasts, We are pleased to announce the first release of PolyChrome (version 0.3). This is an extension for the Firefox web browser that runs Standard ML programs embedded in HTML documents, and lets those programs manipulate the webpage much like JavaScript does. PolyChrome uses PolyML (http://www.polyml.org/, use svn version on Mac, and that or 5.4-fixes on linux) and provides a cute way to quickly develop interfaces for Standard ML programs using HTML. The extension also provides a simple foreign function interface to JavaScript. As a result, JavaScript libraries and interfaces provided by the browser, such as DOM and Canvas, can be used from Standard ML programs. For more information, documentation, download links, etc see: http://kidkarolis.github.com/PolyChrome/ PolyChrome still has many rougher edges, but we feel it's now ready for a first release into the wild; we'd welcome contributions, bug-reports, and other feedback. Best wishes, Karolis Narkevi?ius and Lucas Dixon -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

1 0

Socket.accept on MacOS causes 100% processor usage
by ldixon＠inf.ed.ac.uk 12 Jan '11

12 Jan '11

Hi, Below is a little ML code that prints out everything that gets sent to port 8080. On linux this behaves much as expected, but on MacOS, as soon as the Socket.accept call is made, it uses 100% of processor. The code: (* Reproducable on Mac OS X 10.6.5 PolyML 5.4 Not reproducable on Linux :) After calling main() the CPU usage becomes 100%. After connecting to this server socket by doing telnet localhost 8080 the CPU usage is still 100%. *) fun mkServerSocket () = let val server = INetSock.TCP.socket(); val _ = Socket.bind(server, INetSock.any 8080); val _ = Socket.Ctl.setREUSEADDR(server,true); val saddr = INetSock.fromAddr(Socket.Ctl.getSockName server); val _ = Socket.listen(server,128); in (saddr,server) end; fun readLoop active_socket = let val s = Byte.bytesToString(Socket.recvVec(active_socket,80)); val _ = PolyML.print s; (* print to output *) in (PolyML.print "about to read...\n"; readLoop active_socket) end; fun main() = let val (saddr, server_socket) = mkServerSocket () val (active_socket, active_socket_addr) = Socket.accept server_socket in readLoop active_socket end; -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

2 2

redirecting stdout elsewhere
by ldixon＠inf.ed.ac.uk 20 Nov '10

20 Nov '10

Hi, I was recently wondering if it is possible to redirect std-out to go to a different output stream in ML. Has anyone done anything similar? I was having trouble seeing how to do this with the Standard-ML basis... any suggestions on directions to look at? I can see how to effectively to it by hacking the compiler... but was wondering if there is a better way... (surely!?) ? cheers, lucas -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

4 5

Strange error message on declaration of datatypes
by florian.haftmann＠informatik.tu-muenchen.de 12 Nov '10

12 Nov '10

Hi, the two datatype declarations in sequence datatype 'a T = T of ('a * 'a T) list; datatype 'a S = S of 'a T; give a strange error message haftmann@macbroy15:/home/nfs_data$ /opt/polyml/polyml-5.3.0/x86-linux/polyml Poly/ML 5.3 Release > datatype 'a T = T of ('a * 'a T) list; datatype 'a S = S of 'a T; datatype 'a T = T of ('a * 'a T) list > Exception- InternalError: changeL: Unknown code raised while compiling Exception- InternalError: changeL: Unknown code raised while compiling Apparently I'm using polyml 5.3.0 un x86-linux. Thanks for any hints, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_info…

1 1

St9bad_alloc with Memory Limits near 2^n GB
by tjark.weber＠gmx.de 25 Oct '10

25 Oct '10

Running Poly/ML 5.4 on a 64-bit Linux machine with 16 GB of physical RAM, I see unexpected St9bad_alloc exceptions when I use ulimit -v with limits near 8 GB/4 GB/2 GB/1 GB. For instance, $ uname -a Linux weber 2.6.34.6-54.fc13.x86_64 #1 SMP Sun Sep 5 17:16:27 UTC 2010 x86_64 x86_64 x86_64 GNU/Linux $ poly -v Poly/ML 5.4 Release RTS version: X86_64-5.4.0 $ ulimit -v 8388608 $ poly terminate called after throwing an instance of 'St9bad_alloc' what(): std::bad_alloc Aborted (core dumped) $ ulimit -v 4321280 $ poly terminate called after throwing an instance of 'St9bad_alloc' what(): std::bad_alloc Aborted (core dumped) $ ulimit -v 2170880 $ poly terminate called after throwing an instance of 'St9bad_alloc' what(): std::bad_alloc Aborted (core dumped) $ ulimit -v 1146880 $ poly terminate called after throwing an instance of 'St9bad_alloc' what(): std::bad_alloc Aborted (core dumped) The same problem is present in Poly/ML 5.3. Any help would be appreciated. Regards, Tjark

2 3

polyml error
by jlcaadawson＠netspeed.com.au 24 Oct '10

24 Oct '10

Trying to run polyml I get the following error: [jeremy@home2006 ~]$ poly poly: error while loading shared libraries: libstdc++.so.5: cannot open shared object file: No such file or directory This is in Fedora 13 running the package [jeremy@home2006 ~]$ rpm -q -i polyml Name : polyml Relocations: (not relocatable) Version : 5.2.1 Vendor: Fedora Project Release : 3.fc12 Build Date: Tue 28 Jul 2009 02:18:46 PM EST But the package allegedly requires libstdc++.so.6 [jeremy@home2006 ~]$ rpm -q -R polyml libc.so.6 libc.so.6(GLIBC_2.0) libdl.so.2 libgcc_s.so.1 libm.so.6 libpolyml.so.1 libpthread.so.0 libstdc++.so.6 rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 rtld(GNU_HASH) rpmlib(PayloadIsXz) <= 5.2-1 and that file is there [jeremy@home2006 ~]$ ls -l /usr/lib/libstdc++* lrwxrwxrwx. 1 root root 19 May 13 11:19 /usr/lib/libstdc++.so.6 -> libstdc++.so.6.0.13 -rwxr-xr-x. 1 root root 942040 May 4 07:14 /usr/lib/libstdc++.so.6.0.13 Is this a problem with polyml or with Fedora ? (BTW, polyml-4.1.4 works fine) Grateful for any help., Jeremy

3 4

← Newer
1
...
41
42
43
44
45
46
47
...
72
Older →

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