Poly/ML

polyml@lists.polyml.org

698 discussions

MLTEMP files
by buday.gergely＠uni-eszterhazy.hu 13 Nov '18

13 Nov '18

Hi there, running a CakeML bootstrapping process I got an error no space left on device Actually, the disk was not full but consumed all possible inodes: $ sudo df -i / [sudo] password for gbuday: Filesystem Inodes IUsed IFree IUse% Mounted on /dev/sda1 512064 512064 0 100% / That was because of 361391 MLTEMPXXXX files in /tmp. Is that a Poly/ML thing? - Gergely

3 2

polyml Digest, Vol 152, Issue 3
by dtopham＠gmail.com 11 Nov '18

11 Nov '18

Thank you David, That is very helpful information and maybe good to add to the Debugger tutorial to help others. If I explicitly add type information to variables the debugger works. On Sat, Nov 10, 2018 at 4:00 AM <polyml-request at inf.ed.ac.uk> wrote: > Send polyml mailing list submissions to > polyml at inf.ed.ac.uk > > To subscribe or unsubscribe via the World Wide Web, visit > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > or, via email, send a message with subject or body 'help' to > polyml-request at inf.ed.ac.uk > > You can reach the person managing the list at > polyml-owner at inf.ed.ac.uk > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of polyml digest..." > > > Today's Topics: > > 1. Re: Debugger (David Matthews) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 9 Nov 2018 13:13:17 +0000 > From: David Matthews <David.Matthews at prolingua.co.uk> > To: polyml at inf.ed.ac.uk > Subject: Re: [polyml] Debugger > Message-ID: <ab525449-d652-c995-211a-675dc359063b at prolingua.co.uk> > Content-Type: text/plain; charset=utf-8; format=flowed > > Dave, > It seems to be a bug with printing the value of a polymorphic equality > type variable. "s" has type ''a and that upsets the debugger. It works > either if there is a type constraint to force the type of "s" to be int > list or if "member" is changed so that the equality function is passed > as an argument and the functions are fully polymorphic. I need to find > out why equality types cause problems. > > David > > On 09/11/2018 05:29, David Topham wrote: > > I am trying to use the debugger in PolyML but always get errors. Here is > > my code: > > > > PolyML.Compiler.debug := true; > > open PolyML.Debug; > > fun member(x,[]) = false > > | member(x,(y::ys)) = if x = y then true else member(x,(ys)); > > member(2,[2,3,4]); (* expect true *) > > member(5,[2,3,4]); (* expect false *) > > fun subset([],s) = true > > | subset((x::xs),s) = member(x,s) andalso subset(xs,s); > > fun equals(s1,s2) = subset(s1,s2) andalso subset(s2,s1); > > breakIn "subset"; > > > > subset([],[1,2,3]); (* expect true *) > > subset([2],[1,2,3]); (* expect true *) > > > > It does break at the debug prompt, but when typing > > > > dump(); > > > > it crashes with: Function subset:Exception- Cast "toAddress" raised > > > > Do you have any suggestions? > > > > I am using Debian 9 64-bit and installed using apt-get > > > > "polyml is already the newest version (5.6-8)" > > > > -Dave > > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > polyml mailing list > polyml at inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > > ------------------------------ > > End of polyml Digest, Vol 152, Issue 3 > ************************************** > > -- > The University of Edinburgh is a charitable body, registered in > Scotland, with registration number SC005336. > > -- -Dave

1 0

linking polyML modules to C
by dtopham＠gmail.com 09 Nov '18

09 Nov '18

After more experimenting with GUI in SML, I would like to now try calling an SML module from a C program. That way, the GUI could be built using traditional imperative techniques and the program logic could be written in SML. I see how to call a C function from SML, but and not so clear on how to call an SML function from a C program. I want to build code using polyc and then link with a C main program, but could anyone show me a simple example of calling that function and getting its return value? for example, I have defined: fun sum i n f = if i > n then 0.0 else f i + sum (i+1) n f ; fun int2real x = real x ; in linkToC.sml and #include <iostream> #include <fstream> std::ofstream ofs; int main() { std::cout << sum(1,10,int2real) << std::endl; ofs.open("table.dat"); for(int i = 0; i < 20; i++) ofs << i << '\t' << sum(1,i,int2real) << std::endl; } in linkToC.cpp Looking in the polyc script, I thought adding the -c option might allow me to build the object code which I could then link to the sml functions, but it complains about not having a main. Could someone point me in the right direction? Thanks, Dave On Mon, Dec 15, 2014 at 11:44 AM, David Topham <dtopham at gmail.com> wrote: > David, Thank you so much! I really appreciate your help with this. Your > sample below builds fine with polyc on my system (PolyML 5.5.2). I am using > a minimal Linux distribution named TinyCore ( > http://distro.ibiblio.org/tinycorelinux/) which comes with OpenMotif > 2.3.3 It runs in a virtual machine within another computer only taking up > a few hundred MBs! > > I am going to use it to help my students explore Discrete Math next > semester (this textbook uses SML for that purpose: > http://cs.wheaton.edu/~tvandrun/dmfp/). > > I also found a reasonably current project using PolyML and Motif here: > http://www.lemma-one.com/ProofPower/index/ > > ...however it was built on PolyML 4 and has not yet been ported to the > newer version (e.g. depends on PolyML.commit which no longer seems to be > supported). > > Happy Holidays to everyone in the PolyML community! > > -David Topham > > >> Re: GUI Interface (David Matthews) >> >> I've experimented with building a stand-alone executable with Motif and >> succeeded in getting it to work for me using polyc. (It required >> building Poly/ML with --with-x). I took the example from >> http://www.polyml.org/docs/Motif.html and wrapped it up in a function. >> I did find a problem, though. It looks as though the function has to >> suspend itself with something like Posix.Process.pause otherwise nothing >> happens. I seem to recall that the Motif stuff is handled on a separate >> thread to allow the REPL to continue to accept commands. With a >> stand-alone application there isn't a REPL so without the "pause" it >> terminates immediately. >> >> David >> >> open XWindows ; >> open Motif ; >> >> fun main() = >> let >> val shell = >> XtAppInitialise "" "xed" "Editor" [] [XmNwidth 400, XmNheight 400] ; >> >> val main = XmCreateMainWindow shell "main" [] ; >> >> val bar = XmCreateMenuBar main "bar" [] ; >> >> val fileMenu = XmCreateCascadeButton bar "file" [XmNlabelString "File"] ; >> val editMenu = XmCreateCascadeButton bar "edit" [XmNlabelString "Edit"] ; >> val viewMenu = XmCreateCascadeButton bar "view" [XmNlabelString "View"] ; >> val helpMenu = XmCreateCascadeButton bar "help" [XmNlabelString "Help"] ; >> >> val command = XmCreateText main "command" [XmNeditMode >> XmSINGLE_LINE_EDIT] ; >> >> val hscroll = XmCreateScrollBar main "hscroll" [XmNorientation >> XmHORIZONTAL] ; >> val vscroll = XmCreateScrollBar main "vscroll" [XmNorientation >> XmVERTICAL] ; >> >> val work = XmCreateDrawingArea main "work" [] ; >> in >> >> XtManageChildren [fileMenu, editMenu, viewMenu, helpMenu] ; >> XtManageChildren [bar, command, hscroll, vscroll, work] ; >> >> XmMainWindowSetAreas main bar command hscroll vscroll work ; >> >> XtManageChild main ; >> XtRealizeWidget shell; >> Posix.Process.pause() >> end; >> >> >> ------------------------------ >> >> _______________________________________________ >> polyml mailing list >> polyml at inf.ed.ac.uk >> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml >> >> End of polyml Digest, Vol 110, Issue 12 >> *************************************** >> >> -- >> The University of Edinburgh is a charitable body, registered in >> Scotland, with registration number SC005336. >> >>

2 3

make problem
by buday.gergely＠uni-eszterhazy.hu 06 Nov '18

06 Nov '18

Hi there, cloning polyml from github I did configure --prefix=/home/gbuday/polyml Running make I get the following error: make[2]: Entering directory `/home/gbuday/polyml' /bin/sh ./libtool --tag=CC --mode=link gcc -O3 -Ilibffi/include -o polyimport polyimport.o libpolyml/libpolyml.la -lrt -lm -ldl -lgcc_s -lgcc libtool: link: gcc -O3 -Ilibffi/include -o .libs/polyimport polyimport.o libpolyml/.libs/libpolyml.so -lrt -lm -ldl -lgcc_s -lgcc -Wl,-rpath -Wl,/home/gbuday/polyml/lib gcc: libpolyml/.libs/libpolyml.so: No such file or directory It exists as a symbolic link: $ ls -l libpolyml/.libs/libpolyml.so lrwxrwxrwx. 1 gbuday gbuday 18 nov 6 15.08 libpolyml/.libs/libpolyml.so -> libpolyml.so.9.0.0 but the versioned libpolyml.so.9.0.0 does not. Is this a bug or I haven't managed something well? - Gergely

2 1

[RFC]: Modules to support C FFIs -- a proposal and a minor patch
by domagoj.stolfa＠gmail.com 23 Oct '18

23 Oct '18

Hi all: I've only been using Poly for a few days and haven't done too much SML before a project I'm working on now -- but I've noticed a couple of things that seemed a little tedious while implementing some modules as a part of that project. I may have missed something, and if that's the case please do point it out to me. However, in case what I've observed is in fact the current state of the world, I've written a small proposal and a patch to eliminate these little annoyances (suggested to me by DGASAU on freenode). In essence, I've been building an FFI in the past few days and noticed an absence of a number of things. Namely, there seems to be a lack of support for standard C types such as uint16_t, int16_t, int8_t, int64_t and float (not sure about int64_t). This can make building FFIs a bit of a hassle sometimes, as it requires explicit checks of what value the integer/word in SML might contain before deciding to try and write it. An example of such a workaround would be: ??? ??? if (#NOFFS a) > 0w65535 orelse (#NENOFFS a) > 0w65535 ??? ??? then raise RunCall.Conversion "Invalid Word16 constant" ??? ??? else (...) where #NOFFS a and #NENOFFS a are otherwise manipulated as Word32.words. Moreover, this seems to sometimes cause people developing software or extracting executable specifications from proof assistants such as Isabelle that depend on things like Word16 to discard or impose a limitation on SML used with PolyML as it simply does not support these types out of the box [1, 2] Would it make sense to support these types in PolyML, namely through Word16.word, Int16.int, Int8.int and Int64.int, where Word16 would be of WORD signature, while Int16, Int8 and Int64 would be of INTEGER signature. I've attached a sample patch for supporting Word16, very heavily based on David Matthews' work on Word8 in order to demonstrate what a very crude implementation of the proposal would look like. Is this a real problem, and if so, is implementing these things a sensible way forward? Thanks! [1]: http://rohandrape.net/?t=smlsc3&e=README [2]: https://www.isa-afp.org/browser_info/current/AFP/Native_Word/outline.pdf -- Domagoj

2 2

LInkage and the Foreign structure
by mark.clements＠ki.se 17 Oct '18

17 Oct '18

I am enjoying using polyml's Foreign structure. However, in using the GNU Scientific Library (GSL), I have run into a problem with linkage. The GSL library (libgsl.so) calls standard cBLAS matrix functions with unknown symbols to allow the user to link with different cBLAS implementations (NB: GSL provides an unoptimised cBLAS implementation named libgslcblas.so). When I call a GSL function that depends on the cBLAS functions, I get a symbol not defined error. I have tried unsuccessfully (a) loading the libgslcblas library either before or after loading libgsl, (b) changing the loadLibrary implementation to use dlopen with RTLD_LAZY | RTLD_GLOBAL, and (c) compiling the SML code to an object file and then linking against the libraries. How could this be made to work? Sincerely, Mark. PS test code for (a) is: open Foreign; val gsl = loadLibrary "/usr/lib/x86_64-linux-gnu/libgsl.so"; val gslcblas = loadLibrary "/usr/lib/x86_64-linux-gnu/libgslcblas.so"; type gsl_matrix_t = Memory.voidStar; (* for demonstration only *) local val call1 = buildCall2((getSymbol gsl "gsl_matrix_calloc"), (cInt,cInt), cPointer) val call2 = buildCall4((getSymbol gsl "gsl_matrix_set"), (cPointer,cInt,cInt,cDouble), cVoid) val call3 = buildCall3((getSymbol gsl "gsl_linalg_exponential_ss"), (cPointer, cPointer, cDouble), cVoid) in fun gsl_matrix_alloc (size1,size2) = call1(size1,size2) fun gsl_matrix_set (ptr : gsl_matrix_t, i, j, x) = call2(ptr, i, j, x) fun gsl_matrix (arr : real Array2.array) = let val size1 = Array2.nRows arr val size2 = Array2.nCols arr val ptr = gsl_matrix_alloc(size1, size2) val _ = Array2.tabulate Array2.RowMajor (size1, size2, fn (i,j) => gsl_matrix_set(ptr, i, j, Array2.sub(arr, i, j))) in ptr end fun gsl_mexp (arr : real Array2.array) = let val size1 = Array2.nRows arr val size2 = Array2.nCols arr val ptr = gsl_matrix arr val ptr2 = gsl_matrix_alloc(size1, size2) val _ = call3(ptr, ptr2, 0.01) in ptr2 end end; fun main() = let val a = Array2.fromList [[1.0,2.0],[3.0,4.0]]; val ptr = gsl_matrix(a); val m = gsl_mexp(a) (* fails *) in () end; (* symbol lookup error: /usr/lib/x86_64-linux-gnu/libgsl.so: undefined symbol: cblas_dgemm *) For (c): polyc -c test.sml g++ test.o -L/usr/lib/x86_64-linux-gnu -lgsl -lgslcblas `pkg-config --libs polyml` ./a.out # same error

4 12

"Exception- InternalError: asGenReg raised while compiling"
by mark.clements＠ki.se 13 Sep '18

13 Sep '18

Does anyone know why the following will not compile? I am using Poly/ML 5.7.1 Release (Git version v5.7.1-88-g04ba183) on Ubuntu 16.04LTS. fun invDet2(M) = let val a = Array2.sub(M,0,0) val b = Array2.sub(M,0,1) val c = Array2.sub(M,1,0) val d = Array2.sub(M,1,1) val det = (a*d - b*c) val x = 1.0/det val inv = Array2.fromList [[d*x, ~b*x], [~c*x, a*x]] in (inv,det) end; (* see http://www.cs.cmu.edu/afs/cs/project/pscico/pscico/src/matrix/RealMatrix.sml *) Note that the following is okay: fun invDet2(M) = let val a = Array2.sub(M,0,0) val b = Array2.sub(M,0,1) val c = Array2.sub(M,1,0) val d = Array2.sub(M,1,1) val det = (a*d - b*c) val inv = Array2.fromList [[d/det, ~b/det], [~c/det, a/det]] in (inv,det) end; --- Mark

2 3

socket from fd
by Ramana.Kumar＠cl.cam.ac.uk 03 Aug '18

03 Aug '18

Hi Poly/ML, Is it possible to retrieve a socket from a file descriptor in Standard ML or Poly/ML? E.g., if Posix.FileSys.ST.isSock (Posix.FileSys.fstat fd) is true, then what can I do to fd to use functions in the Socket structure on it? Cheers, Ramana

4 3

Error with poly_smlnj-lib.sml
by mark.clements＠ki.se 31 Jul '18

31 Jul '18

Dear all, This is my first post. I am trying to use poly_smlnj-lib.sml (with a plan to see whether mlnffigen can be ported from MLton to Poly/ML). Following instructions from http://www.tbrk.org/software/poly_smlnj-lib.html (see also https://github.com/standardml/smackage/blob/master/src/poly_smlnj-lib.sml), I called: $ poly > use "poly_mlyacc.sml"; (* ok *) > use "poly_smlnj-lib.sml"; with the latter giving an error: /usr/local/lib/mlton/sml/smlnj-lib/Util/bit-array.sml:781: error: Structure (Word8Array) has not been declared in structure Unsafe Found near Unsafe.Word8Array.create (Word8Array.length bits) I am using Poly/ML 5.7.1 Release and MLton 20180207. Any suggestions would be welcomed. Kindly, Mark.

2 2

PolyML and paths for load files.
by kostirya＠gmail.com 05 Jul '18

05 Jul '18

Hello. Let's take into account Env to load files in use function? > diff -u FinalPolyML.sml_orig FinalPolyML.sml --- FinalPolyML.sml_orig 2018-07-05 11:17:32.489398000 +0300 +++ FinalPolyML.sml 2018-07-05 11:20:20.012445000 +0300 @@ -674,6 +674,7 @@ end val suffixes = ref ["", ".ML", ".sml"] + val paths = ref ["POLYML_LIB", "SMACKAGE_HOME", "SMACKAGE"] (*****************************************************************************) @@ -689,15 +690,20 @@ (* We use the functional layer and a reference here rather than TextIO.input1 because that requires locking round every read to make it thread-safe. We know there's only one thread accessing the stream so we don't need it here. *) - fun trySuffixes [] = + fun trySuffixes name [] = (* Not found - attempt to open the original and pass back the exception. *) (TextIO.getInstream(TextIO.openIn originalName), originalName) - | trySuffixes (s::l) = + | trySuffixes name (s::l) = (TextIO.getInstream(TextIO.openIn (originalName ^ s)), originalName ^ s) - handle IO.Io _ => trySuffixes l + handle IO.Io _ => trySuffixes name l + (* First in list is the name with no suffix. *) - val (inStream, fileName) = trySuffixes("" :: ! suffixes) + fun tryPath name [] = trySuffixes name ("" :: ! suffixes) + | tryPath name (p::ps) = trySuffixes (p ^ name) ("" :: ! suffixes) handle IO.Io _ => tryPath name ps + + val (inStream, fileName) = tryPath originalName (rev (foldl (fn (p, r) => case OS.Process.getEnv p of NONE => r | SOME p => p ^ "/"::r) [""] (!paths))) + val stream = ref inStream (* Record the file name. This allows nested calls to "use" to set the correct path. *) >

1 1

← Newer
1
...
7
8
9
10
11
12
13
...
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