Poly/ML

polyml@lists.polyml.org

695 discussions

Building MS Windows applications
by rda＠lemma-one.com 19 Feb '11

19 Feb '11

I have installed Poly/ML on MS Windows using the precompiled binary. Now I want to start building my own applications. What do I need for the equivalent in MS Windows of the following command line that I would use on UNIX? cc -o hello hello.o -lpolymain -lpolyml I.e., where do I find the polymain and polyml DLLs and what developer kits can I use? E.g., will MinGW work? And which developer kits are recommended? Regards, Rob.

2 4

InternalError: jump too large raised while compiling
by andreas.lochbihler＠kit.edu 19 Feb '11

19 Feb '11

Dear all, I use Isabelle to generate ML code from my formalisation in Isabelle. When I try to load the output ML file in Poly/ML 5.4, I get the following exception: Exception- InternalError: jump too large raised while compiling Exception- Fail "Exception- InternalError: jump too large raised while compiling" raised It occurs when Poly/ML processes a structure with a large function definition (2750 lines of ML code). The same error occurs with Poly/ML 5.3. What could I do to avoid this error? Are there any options to Poly/ML that allow larger jumps? Changing the code itself is difficult as it is automatically generated. If it helps, I can provide the ML file. Regards, Andreas -- Karlsruher Institut f?r Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Geb. 50.41, Raum 023 76131 Karlsruhe Telefon: +49 721 608-48352 Fax: +49 721 608-48457 E-Mail: andreas.lochbihler(a)kit.edu http://pp.info.uni-karlsruhe.de KIT - Universit?t des Landes Baden-W?rttemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

2 1

HTTP protocol socket code
by ldixon＠inf.ed.ac.uk 17 Feb '11

17 Feb '11

[ apologies for cross-posting, the more appropriate sml-list is populated only by spam-bots :( ] Hi, Does anyone know of some HTTP code written in ML? I'd like to programmatically, in ML, do some web-queries... cheers, lucas -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

3 2

Re: On understanding Poly/ML function definition IR
by David.Matthews＠prolingua.co.uk 09 Feb '11

09 Feb '11

On 08/02/2011 00:31, Yue Li wrote: > I'm trying to get better understanding about the code tree of Poly/ML > function definition. I would appreciate if I can gain some insights from > you. > > For instance, given the following definition: > > > fun f a b = a + b; The first point to appreciate is that this is syntactic sugar for val rec f = fn a => fn b => op+ (a, b); However this general form isn't the best way of compiling the function. Frequently a curried function is applied to several or all of its arguments e.g. val x = f y z Using the general form would be inefficient. Applying f to y would result in a closure being created on the heap which would then be applied to z. Instead Poly/ML processes "fun" declarations specially. fun f a b = a + b is rewritten as val rec f' = fn <a,b> => a + b and rec f = fn_inline a => fn_inline b => f'<a,b> i.e. a pair of mutually recursive functions, because f' could contain recursive applications of f. The <> here denote multiple arguments in registers or on the stack, something that doesn't have an exact equivalent in ML since every function takes exactly one argument. > The compiler prints out 3 sections of code tree: a block, a lambda and > another block: > > BLOCK(MUTUAL(DECL #2{0 uses} = > LAMBDA( > f(2) > CL=false CR=0 LEV=0 LOCALS=0 > ARGS=G G > ARGLIVES= > RES=G CLOS=() > BLOCK(BLOCK(DECL #1{0 uses} = RECCONSTR(PARAM(0,1), PARAM(0,2)); > DECL #3{0 uses} = LOCAL(0,1); > DECL #4{0 uses} = INDIRECT(0, LOCAL(0,3)); > DECL #5{0 uses} = INDIRECT(1, LOCAL(0,3)); > GLOBAL (FUN "run_call2(1)", > LAMBDAINLINE( > run_call2(1) > CL=false CR=0 LEV=0 LOCALS=0 > ARGS=G > ARGLIVES= > RES=G CLOS=() > LOCAL(1,1) G > $(INDIRECT(0, PARAM(0,1)) G, INDIRECT(1, PARAM(0,1)) G)){LAMBDA} > ) (*GLOBAL*){early} G $(RECCONSTR(LOCAL(0,4), LOCAL(0,5)) G) > ) > )){LAMBDA} AND This is the body of "f'". The name "f(2)" represents that it takes two arguments but the name is only used for exception tracing and profiling. It has no significance to ML. > > DECL #1{0 uses} = > LAMBDAINLINE( > f(1) > CL=false CR=0 LEV=0 LOCALS=0 > ARGS=G > ARGLIVES= > RES=G CLOS=() > LAMBDAINLINE( > f(1)(1) > CL=false CR=0 LEV=0 LOCALS=0 > ARGS=G > ARGLIVES= > RES=G CLOS=() > LOCAL(2,2) G $(PARAM(0,1) G, PARAM(1,1) G)){LAMBDA}){LAMBDA} > ); This is the body of "f". It consists of two inline functions, one inside the other. > RECCONSTR(LOCAL(0,1)) > ) This is the result of a top-level declaration. The final result is a 1-tuple containing a reference to the function "f". Actually because these are all small functions it's likely that the result will be the reference to the code-tree itself so that subsequent uses of "f" at the top-level will expand the code in-line and reduce down to a use of the addition operation. Top-level declarations can be simple function declarations such as this example but just as often they involve extensive computation and return the results as multiple declarations. > I have three questions regarding this block: > > (1) First I'm wondering what do LOCAL(2, 2), and LOCAL(1, 1) refer to? > My understanding so far is that the second number of the LOCAL operator > means the number of DECL, but what does the first number refers to? This is the nesting depth. Zero means local to the function, one means local to the immediately containing function etc. So LOCAL(2,2) G $(PARAM(0,1) G, PARAM(1,1) G)) means: apply the function declared by a DECL #2 two levels out to the first or only parameter of the current function and the first or only parameter of the immediately containing function. (Oh, there's some oddity about the order of multiple parameters). I hope this answers your other questions as well but let me know if you'd like any more clarification. Regards, David

2 1

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

← Newer
1
...
39
40
41
42
43
44
45
...
70
Older →

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