Poly/ML May 2014

polyml@lists.polyml.org

6 participants
9 discussions

Inspecting structures
by ramana.kumar＠gmail.com 27 Jan '16

27 Jan '16

Is there a way to look at the contents (i.e. signature) of a structure without opening it? (I suppose you could just open it then call a lot of PolyML.Compiler.forgetXXX, but that's quite tedious) Also, is it possible to retrieve the long path of an identifier in scope? Something that will, for example, take the rev in scope and say that it came from List. Finally, what about searching for an identifier that would come into scope if you opened some structures?

3 5

polyc and poly --script
by rene.neumann＠in.tum.de 24 Mar '15

24 Mar '15

Hi, two completely orthogonal questions/remarks for PolyML 5.5.1: 1.) When building PolyML with '--with-system-libffi' the '-lffi' part is missing in the linker line in polyc. 2.) Is it somehow possible to see if an ML file is run via 'poly --script' or as a standalone executable? Because for the one the logic has to be wrapped in 'fun main ()', and for the other it should not :). (Ie, what I want: if is_script then main() else () ) Thanks, Ren? -- Ren? Neumann Institut f?r Informatik (I7) Technische Universit?t M?nchen Boltzmannstr. 3 85748 Garching b. M?nchen Tel: +49-89-289-17232 Office: MI 03.11.055

4 9

[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

Isabelle/ML IDE
by makarius＠sketis.net 29 Sep '14

29 Sep '14

Dear friends of Poly/ML, or Standard ML in general, Isabelle2013-2 is now available from the usual mirror sites: Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Munich (Germany) http://isabelle.in.tum.de/ Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/ It is mainly an environment for interactive and automated theorem proving, but the integration of Isabelle/ML into the Prover IDE makes it suitable for general Standard ML development (potentially in teaching scenarios). After downloading / unpacking / running the main application of Isabelle/jEdit, the Documentation panel on the right-hand side gives quick access to Examples, notably src/HOL/ex/ML.thy for some Isabelle/ML basics. The manual on Isabelle/jEdit in the same panel provides further details on the IDE, which is based on the jEdit text editor. Makarius

1 1

standard input contains a leading blank line? (5.5.2 with --enable-shared)
by michael.norrish＠nicta.com.au 28 May '14

28 May '14

If the following is foo.ML: fun doit () = let fun recurse i = case TextIO.inputLine TextIO.stdIn of NONE => () | SOME l => (print (Int.toString i ^ ": " ^ l); recurse (i + 1)) in recurse 1 end; PolyML.export("mytest", doit); and I then do $ poly < foo.ML $ cc -o mytest mytest.o -lpolymain -lpolyml $ echo "hello, world" | ./mytest I get 1: 2: hello, world as output. This is with a polyml 5.5.2 just downloaded from Sourceforge and configured with --enable-shared. I'm pretty sure this used to work (a minor feature of the HOL4 build process depended on it). Michael

2 1

Poly on MinGW
by rda＠lemma-one.com 25 May '14

25 May '14

I am trying to understand my options for using Poly/ML on MinGW for building windows applications coded in Standard ML. There is a bug reported in http://sourceforge.net/p/mingw/bugs/2043/ that you have to work around to build Poly/ML with the current MinGW. The work-around is to run configure with CXXFLAGS="-D_GLIBCXX_HAVE_FENV_H=1? in the environment. (I suspect I should also throw -O3 in there too, as I think that setting CXXFLAGS replaces its initial setting of -O3 inside the makefiles. Is that right?) Having got Poly/ML to compile, I found that polyc gives errors like the following when asked to compile a source file: gcc.exe: error: C:/DOCUME~1/rda/LOCALS~1/Temp/polyobj.2724.obj: No such file or directory If I create an object file from the Poly/ML GUI using PolyML.export, polyc will link it. If I understand what is going on correctly, the resulting program is a Windows application that brings up the Poly/ML GUI to provide the standard input, output and error channels, unless it is run with standard input and output connected to pipes, in which case it works like a pipe. I think I may end up having to package the Standard ML parts of my application as a server, with the GUI provided by clients implemented in some other language. Are there any other options? Regards, Rob.

3 7

Run out of store - interrupting threads
by David.Matthews＠prolingua.co.uk 18 May '14

18 May '14

This question arose from something on the isabelle-dev list but I think it's really of general interest. Currently Poly/ML only gives the "Run out of store - interrupting threads" message if it really cannot allocate the required memory after a full GC. This is actually rather unlikely for small cells. Instead as the amount of free space left in the heap gets smaller the GC runs more and more often. The ML code is still making progress but only very slowly. I wonder if there is a case for actually giving up at that point. Is it better to plough on in the hope that the program will complete or is it more helpful to produce a message and allow the user to try with more memory? This situation is most likely to happen if the heap space is restricted either because the address space limit has been reached in 32-bit mode or if the maximum heap has been set too low with --maxheap. David

2 3

Poly/ML 5.5.2 Released
by David.Matthews＠prolingua.co.uk 17 May '14

17 May '14

Since I haven't had any recent bug reports I've uploaded the current SVN snap-shot to SourceForge as version 5.5.2. Most of the changes are bug fixes. One major fix was to the intermediate code optimiser reported back in September. Other changes are the addition of PrettyStringWithWidth and PrettyLineBreak constructors to the PolyML.pretty datatype, Thread.Thread.numPhysicalProcessors to return the number of physical processors and printing ?.t in circumstances where t is bound to a different type. The debugger has been extended to include structures and the arguments to functors. As always, let me know if you find bugs or problems. David

3 9

polyc
by rda＠lemma-one.com 10 May '14

10 May '14

I have a couple of comments and a query about polyc (which seemed particularly attractive on Cygwin, where there seems to be quite a long list of libraries you need to know about if you are going to call the linker directly). The comment is that the help text is a bit misleading as it has more functionality than just compiling and linking a source file, e.g., you can pass it the name of an object file and it will link it with libpolymain and libpolyml. The query relates to the fact that polyc doesn?t do anything with LD_RUN_PATH (or DYLD_LIBRARY_PATH on Mac OS). Am I right in thinking that libpolyml will now always be statically linked so that you no longer to need to tell the dynamic linker where to find it? (For Poly/ML versions 5.5 and earlier the ProofPower makefiles that I am updating used to create an executable that linked libpolyml dynamically.) Regards, Rob.

4 4

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 May 2014