Re: [polyml] Callback from a foreign thread

[Phil Clayton]

Thanks David,

I will try this out then.  The aim is to use GTask (from GLib) from ML.

Phil

On 14/11/2022 08:50, David Matthews wrote:

Phil,
It should work although I don't think I've ever actually tested it.  At 
the start of a callback the code calls PolyX86GetThreadData to get the 
ML thread data including a reference to the ML stack.  This is stored in 
thread-local storage.  If it is empty it assumes this is a new thread 
and calls CreateNewTaskData to create new ML thread data and a new stack.


David

On 13/11/2022 23:37, Phil Clayton wrote:
I am wondering whether it is possible for a new thread to be created 
in foreign code by some other library and for the new thread to call 
back into ML.  As the new thread would not be created by Poly/ML, 
presumably it would not have its own ML stack and that sounds 
problematic, given the description in the original paper [1].  On the 
other hand, perhaps an ML stack is provided by the callback closure.  
I briefly looked at the source code, and ended up at buildCallBack in 
X86ForeignCall.ML, but I would need to understand the code generation 
to make sense of that.


Phil


1.Efficient Parallel Programming in Poly/ML and Isabelle/ML

...

Like every thread that runs ML code this new thread has both
an operating-system stack that it uses when running in the RTS or
in “foreign” code through the foreign-function interface (FFI) and
an ML stack that is used when running ML code. The ML stack is
an object within the ML heap and can be scanned and updated by
the garbage-collector.

...

Because all threads are created by calls to the RTS and all
interaction with the operating system is through it the RTS is able
to maintain a table of threads and their current state. Knowing the
state of all threads is particularly important for garbage collection.

...

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

[polyml] Callback from a foreign thread

[Phil Clayton]

I am wondering whether it is possible for a new thread to be created in 
foreign code by some other library and for the new thread to call back 
into ML.  As the new thread would not be created by Poly/ML, presumably 
it would not have its own ML stack and that sounds problematic, given 
the description in the original paper [1].  On the other hand, perhaps 
an ML stack is provided by the callback closure.  I briefly looked at 
the source code, and ended up at buildCallBack in X86ForeignCall.ML, but 
I would need to understand the code generation to make sense of that.


Phil


1.Efficient Parallel Programming in Poly/ML and Isabelle/ML

...

Like every thread that runs ML code this new thread has both
an operating-system stack that it uses when running in the RTS or
in “foreign” code through the foreign-function interface (FFI) and
an ML stack that is used when running ML code. The ML stack is
an object within the ML heap and can be scanned and updated by
the garbage-collector.

...

Because all threads are created by calls to the RTS and all
interaction with the operating system is through it the RTS is able
to maintain a table of threads and their current state. Knowing the
state of all threads is particularly important for garbage collection.

...

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] 5.9 released

[Phil Clayton]

I can't help with Brew but in case it's any use, the MacPorts port has 
been updated, although there is a pending merge request to apply fixes 
for arm.


Regards,
Phil

On 07/12/21 13:25, Frank Pfenning wrote:

Would it be possible to update the Brew formula for PolyML from 5.8.2?
I couldn't easily determine who the maintainer for that is.

Thanks,
Frank

On Fri, Nov 26, 2021 at 3:18 AM David Matthews 
mailto:david.matth...@prolingua.co.uk>> 
wrote:


Poly/ML version 5.9 was officially released on Github last weekend.
There is a fixes-5.9 branch which already contains one fix, but that
just affects the interpreted version.

David

___
polyml mailing list
polyml@inf.ed.ac.uk 
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml



--
Frank Pfenning, Professor
Computer Science Department
Carnegie Mellon University
Pittsburgh, PA 15213-3891

http://www.cs.cmu.edu/~fp
+1 412 268-6343
GHC 6017



___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Size of stand-alone executables

[Phil Clayton]

These days I build Poly/ML with all combinations of yes/no for the 
following configure options for testing purposes:

--enable-shared
--enable-compact32bit
--enable-intinf-as-int

I've just built ProofPower with each such variant of Poly/ML 5.9 on my 
Linux x86_64 system and get the following sizes for pp-ml:


10485336 pp/bin/pp-ml
10572216 pp--intinf-as-int/bin/pp-ml
 8465368 pp--compact32bit/bin/pp-ml
 8547736 pp--compact32bit--intinf-as-int/bin/pp-ml
 9795648 pp--shared/bin/pp-ml
 9882528 pp--shared--intinf-as-int/bin/pp-ml
 7767840 pp--shared--compact32bit/bin/pp-ml
 7846104 pp--shared--compact32bit--intinf-as-int/bin/pp-ml

and the following sizes for a saved state (zed.polydb):

18650832 pp/db/zed.polydb
18802280 pp--intinf-as-int/db/zed.polydb
14424536 pp--compact32bit/db/zed.polydb
14610524 pp--compact32bit--intinf-as-int/db/zed.polydb
18650616 pp--shared/db/zed.polydb
18802744 pp--shared--intinf-as-int/db/zed.polydb
14424356 pp--shared--compact32bit/db/zed.polydb
14610524 pp--shared--compact32bit--intinf-as-int/db/zed.polydb

Using compact32bit gives a significant reduction in file size of both 
pp-ml and saved states.  Dynamically linking to libpolyml reduces the 
size of pp-ml by 690-700 kB versus static linking but does not affect 
the size of saved states, as you would expect.  Not using intinf-as-int 
reduces file sizes by around 1%.


So building ProofPower on a Poly/ML built using compact32bit, dynamic 
linking and not using intinf-as-int would help minimize file sizes.


Phil

On 27/11/21 00:10, Rob Arthan wrote:

David,

Thanks. That all makes sense. The ProofPower read-eval-print loop lives in this 
executable:

-rwxr-xr-x  1 rda  staff  9975056 Jul 25 14:00 /usr/local/pp/latest/bin/pp-ml

and when you add its size to the size of the saved state you get about the same 
size
as the executable. Fortunately, the size of the executable doesn’t seem
to be causing any problems in practice (and why should it? A lot of the apps on 
my phone
are much bigger than this, so Poly/ML is competitive with Java on this score 
:-)).

Regards,

Rob.


On 26 Nov 2021, at 08:38, David Matthews  wrote:

Rob,

On 25/11/2021 19:26, Rob Arthan wrote:

-rw-r--r--  1 rda  staff  44217560 Nov 25 19:06 main1.o
-rwxr-xr-x  1 rda  staff  33928480 Nov 25 19:07 main1
-rw-r--r--  1 rda  staff  24260472 Nov 25 19:10 saved_state
Here main1.o is the result of calling PolyML.export, main1 is the executable
and saved_state is the result of calling PolyML.Compiler.saveState.
He is seeing even bigger differences (possibly because he is compiling
on Windows?). The question remains though: why is the .o file much
bigger than the executable and why is the executable much bigger than
the saved state? Can we do anything to reduce the size of the executable.
(We are both calling PolyML.shareCommonData on the entry point function
beforecalling PolyML.export.)


Those figures don't surprise me.  The saved state contains data created in the 
session but because it can only be read into the same executable that created 
it, it doesn't contain anything present in the executable itself.

PolyML.export produces an object file containing everything that is reachable 
from the root.  It will almost certainly contain portions of the original 
executable so that the resulting code is self-contained.

The object file (main1.o) contains relocation information needed by the linker. 
 If the root includes ML data structures such as lists there will be a lot of 
relocation data and that could easily double the size of the file.  The size 
and format of the relocation data depend on the platform so are different in 
Windows, Linux/BSD and Mac OS.  The linker may or may not remove this in the 
final executable.  If the executable is linked to be loaded at a fixed address 
it doesn't need the relocation information.

David


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Can't build Poly/ML after introducing RunCall.rtsCallFast1

[Phil Clayton]

Ignore me: I've done something silly.  I forgot to add the functions to 
the polyFFIEPT table.


On 01/10/21 16:18, Phil Clayton wrote:
I'm adding conversions for other C types, based on the latest master 
(cf6f86a), but building fails without any error message. polyimport 
fails on my version of ForeignConstants.sml.  After experimenting, it 
seems that introducing


   RunCall.rtsCallFast1"f" ()

where f is a new function that I am also introducing, causes the failure.

Is there a different way I should be building?  I'm sure I just ran 
'make', 'make compiler' when I did this before.  I have attached the 
patch in case I've done something silly in there.




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

[polyml] Can't build Poly/ML after introducing RunCall.rtsCallFast1

[Phil Clayton]

I'm adding conversions for other C types, based on the latest master 
(cf6f86a), but building fails without any error message. polyimport 
fails on my version of ForeignConstants.sml.  After experimenting, it 
seems that introducing


  RunCall.rtsCallFast1"f" ()

where f is a new function that I am also introducing, causes the failure.

Is there a different way I should be building?  I'm sure I just ran 
'make', 'make compiler' when I did this before.  I have attached the 
patch in case I've done something silly in there.


>From 953f8dcbfec9259cc0a34819784a4742c8d616dd Mon Sep 17 00:00:00 2001
From: Phil Clayton 
Date: Fri, 1 Oct 2021 08:16:24 +0100
Subject: [PATCH] Add FFI conversions for C types

Conversions are added to the structure Foreign for C types as follows:
long long   cLonglong, cLonglongLarge
unsigned long long  cUlonglong, cUlonglongLarge
ptrdiff_t   cPtrdiff, cPtrdiffLarge
intptr_tcIntptr, cIntptrLarge
uintptr_t   cUintptr, cUintptrLarge
---
 basis/Foreign.sml  | 74 ++
 basis/ForeignConstants.sml |  8 +
 libpolyml/polyffi.cpp  | 24 +
 3 files changed, 106 insertions(+)

diff --git a/basis/Foreign.sml b/basis/Foreign.sml
index 70921620..e4d1b948 100644
--- a/basis/Foreign.sml
+++ b/basis/Foreign.sml
@@ -205,14 +205,24 @@ sig
 val cUint: int conversion
 val cLong: int conversion
 val cUlong: int conversion
+val cLonglong: int conversion
+val cUlonglong: int conversion
 val cIntLarge: LargeInt.int conversion
 val cUintLarge: LargeInt.int conversion
 val cLongLarge: LargeInt.int conversion
 val cUlongLarge: LargeInt.int conversion
+val cLonglongLarge: LargeInt.int conversion
+val cUlonglongLarge: LargeInt.int conversion
 val cSsize: int conversion
 val cSize: int conversion
+val cPtrdiff : int conversion
+val cIntptr : int conversion
+val cUintptr : int conversion
 val cSsizeLarge: LargeInt.int conversion
 val cSizeLarge: LargeInt.int conversion
+val cPtrdiffLarge : LargeInt.int conversion
+val cIntptrLarge : LargeInt.int conversion
+val cUintptrLarge : LargeInt.int conversion
 val cString: string conversion
 val cByteArray: Word8Vector.vector conversion
 val cFloat: real conversion
@@ -594,12 +604,26 @@ struct
 { size= #size saLong, align= #align saLong, typeForm = CTypeSignedInt }
 val cTypeUlong =
 { size= #size saLong, align= #align saLong, typeForm = CTypeUnsignedInt }
+(* long long *)
+val cTypeLonglong =
+{ size= #size saLonglong, align= #align saLonglong, typeForm = CTypeSignedInt }
+val cTypeUlonglong =
+{ size= #size saLonglong, align= #align saLonglong, typeForm = CTypeUnsignedInt }
 (* ssize_t *)
 val cTypeSsize =
 { size= #size saSsize, align= #align saSsize, typeForm = CTypeSignedInt }
 (* size_t *)
 val cTypeSize =
 { size= #size saSize, align= #align saSize, typeForm = CTypeUnsignedInt }
+(* ptrdiff_t *)
+val cTypePtrdiff =
+{ size= #size saPtrdiff, align= #align saPtrdiff, typeForm = CTypeSignedInt }
+(* intptr_t *)
+val cTypeIntptr =
+{ size= #size saIntptr, align= #align saIntptr, typeForm = CTypeSignedInt }
+(* uintptr_t *)
+val cTypeUintptr =
+{ size= #size saUintptr, align= #align saUintptr, typeForm = CTypeUnsignedInt }
 (* Float: 4 on X86 *)
 val cTypeFloat =
 { size= #size saFloat, align= #align saFloat, typeForm = CTypeFloatingPt }
@@ -970,6 +994,26 @@ struct
 else if #size saLong = #size (#ctype cUint64Large) then cUint64Large
 else raise Foreign "Unable to find type for unsigned long"
 
+val cLonglong =
+if #size saLonglong = #size (#ctype cInt32) then cInt32
+else if #size saLonglong = #size (#ctype cInt64) then cInt64
+else raise Foreign "Unable to find type for long long"
+
+val cLonglongLarge =
+if #size saLonglong = #size (#ctype cInt32Large) then cInt32Large
+else if #size saLonglong = #size (#ctype cInt64Large) then cInt64Large
+else raise Foreign "Unable to find type for long long"
+
+val cUlonglong = 
+if #size saLonglong = #size (#ctype cUint32) then cUint32
+else if #size saLonglong = #size (#ctype cUint64) then cUint64
+else raise Foreign "Unable to find type for unsigned long long"
+
+val cUlonglongLarge = 
+if #size saLonglong = #size (#ctype cUint32Large) then cUint32Large
+else if #size saLonglong = #size (#ctype 

Re: [polyml] Updates in git master including major change to FFI

[Phil Clayton]

On 08/03/21 19:37, David Matthews wrote:

On 08/03/2021 17:29, Phil Clayton wrote:
I note that the binaries using the compiled FFI still have a 
dependency on libffi.  Presumably configure.ac is yet to be updated to 
make the checks on libffi conditional.  (I rebuilt with libffi 
configuration removed from 'configure' as per the attached diff and 
there was no dependence on libffi, and the tests, at least on Linux, 
were still fine.)


Thanks for that.  libffi is still needed in the interpreted version so 
I've pushed a change that only checks for libffi in that case.


That works for me as expected.

Regards,
Phil
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Updates in git master including major change to FFI

[Phil Clayton]

On 05/03/21 13:41, David Matthews wrote:

On 23/02/2021 13:00, Phil Clayton wrote:
Thanks for the updates.  I have been testing the Poly/ML variants (see 
below) and that fixes callbacks within callbacks on x86_64 provided 
compact32bit is disabled.  When compact32bit is enabled, I find that 
any use of a callback seg. faults, not just nested use.  The previous 
examples call_c_test_15 and call_c_test_16 still demonstrate this. 
(Observed on both Linux and macOS.)



The following cause callbacks to seg. fault:

--enable-shared=yes --enable-compact32bit=yes --enable-intinf-as-int=no
--enable-shared=yes --enable-compact32bit=yes --enable-intinf-as-int=yes

Thanks for reporting that.  I've pushed a fix and it looks like it works 
now.


Thanks - I have tested the fix with all variants and have not found any 
issues on Linux/macOS x86_64.


I note that the binaries using the compiled FFI still have a dependency 
on libffi.  Presumably configure.ac is yet to be updated to make the 
checks on libffi conditional.  (I rebuilt with libffi configuration 
removed from 'configure' as per the attached diff and there was no 
dependence on libffi, and the tests, at least on Linux, were still fine.)



I note that the low-level interface provided by Foreign has changed in 
a way that is not compatible with the previous version [1].  Clearly 
some break in interface is unavoidable.  Given this, could you confirm 
that the next version will be 5.8.2?  (It seems reasonable not to 
consider the low-level interface part of the stable API.)


I wanted to keep the high-level interface as stable as possible.  The 
low-level, though, needed to change.  I expect the next version will be 
5.8.2.


Good to know, thanks.

Regards,
Phil


configure.diff.gz
Description: application/gzip
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Updates in git master including major change to FFI

[Phil Clayton]

On 22/02/21 15:34, David Matthews wrote:
I've pushed some changes which should have fixed most of these issues. 
Thanks for reporting them.


Thanks for the updates.  I have been testing the Poly/ML variants (see 
below) and that fixes callbacks within callbacks on x86_64 provided 
compact32bit is disabled.  When compact32bit is enabled, I find that any 
use of a callback seg. faults, not just nested use.  The previous 
examples call_c_test_15 and call_c_test_16 still demonstrate this. 
(Observed on both Linux and macOS.)



The following cause callbacks to seg. fault:

--enable-shared=yes --enable-compact32bit=yes --enable-intinf-as-int=no
--enable-shared=yes --enable-compact32bit=yes --enable-intinf-as-int=yes


The following work fine:

--enable-shared=yes --enable-compact32bit=no  --enable-intinf-as-int=no
--enable-shared=yes --enable-compact32bit=no  --enable-intinf-as-int=yes


In both the old and new Foreign modules, the type `'a 
Foreign.closure` is abstract.  Giraffe Library uses 
`Foreign.LowLevel.cFunctionWithAbi` define its own function for 
creating a closure but there is no way to create a `'a 
Foreign.closure` value from a `Memory.voidStar` value. This is 
easily worked around by copying the type declaration and definition 
of `Foreign.cFunction` but I wondered if there could be a way to 
avoid this copying.


Can't you just use the cPointer conversion instead of cFunction?


The store of cPointer doesn't return a function that touches the 
pointer.  Although that wouldn't matter for my current uses, where there 
is always a persistent reference to a closure, I would like the 
interface to work if there isn't a persistent reference.  It's probably 
not worth changing anything though as we're talking about a few lines of 
code.



I note that the low-level interface provided by Foreign has changed in a 
way that is not compatible with the previous version [1].  Clearly some 
break in interface is unavoidable.  Given this, could you confirm that 
the next version will be 5.8.2?  (It seems reasonable not to consider 
the low-level interface part of the stable API.)


Regards,
Phil


1. The low-level interface in Foreign has the following changes:
  - type LowLevel.ctype has become LowLevel.cType
  - type LibFFI.abi has become LowLevel.abi
  - the voidStar arguments of cFunction[WithAbi] and call[WithAbi] have
 a different representation
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Updates in git master including major change to FFI

[Phil Clayton]

I hacked PolyFFICallbackException to print the exception (see attached) 
and found that it was

  Foreign "Cannot return a closure"
It's now obvious what's going wrong now in call_c_test_15.  The load 
function for a closure conversion raises the exception to prevent a
call to C returning a closure (hence the wording in the exception) but 
it also prevents a callback function taking a closure as an argument.


It would be useful if PolyFFICallbackException printed the exception 
before aborting.


On 19/02/21 16:19, Phil Clayton wrote:
In testing callbacks during callbacks, I have also tried a rather 
contrived example (attached) where the SML function closures to call 
back are passed down as arguments.  It's not something that I have 
needed to do.  I simply cannot get this to work with either 5.8.1 or the 
latest version in master.  With both versions I see the following output:


An ML function called from foreign code raised an exception.  Unable to 
continue.
call_c_test_15: diagnostics.cpp:128: void Crash(const char*, ...): 
Assertion `0' failed.


I see this even if I wrap exception handlers around the called-back 
functions to ensure that they cannot raise an exception.


I may well be doing something wrong in the example but I can't see what 
it is.  I've mentioned it in case it highlights an issue.


Regards,
Phil

On 18/02/21 23:57, Phil Clayton wrote:
I have finally tried out the new FFI with Giraffe Library with partial 
success.  For some examples, calls to C and callbacks from C are 
working but other examples result a seg. fault.  From the debug 
output, I noticed that the seg. faults occur when a callback occurs 
during a callback.  I've attached a small example that demonstrates 
the issue (call_c_test_16.tar.gz).  (Although this example uses 
dynamic loading, the same happens if dynamic linking is used.)  The 
backtrace from gdb provided no useful information so I didn't 
investigate further.


Also, I have some minor observations about the interface.  I note that 
the signature FOREIGN specifies:

 val touchClosure: 'a -> unit
I wondered whether that should be
 val touchClosure: 'a closure -> unit
(RunCall.touch is visible in the Poly/ML top-level which has the type 
of the former, so there is no loss of capability with the latter, 
which would catch cases where touchClosure is applied to the wrong 
value.)


In both the old and new Foreign modules, the type `'a Foreign.closure` 
is abstract.  Giraffe Library uses `Foreign.LowLevel.cFunctionWithAbi` 
define its own function for creating a closure but there is no way to 
create a `'a Foreign.closure` value from a `Memory.voidStar` value. 
This is easily worked around by copying the type declaration and 
definition of `Foreign.cFunction` but I wondered if there could be a 
way to avoid this copying.


In the past, I found it useful to have
 val nullClosure : 'a closure
This is easily declared with one's own closure type but if using 
Foreign.closure, it may be useful to have in Foreign.  Giraffe Library 
no longer needs this since I changed the callback mechanism to avoid 
the need to free closures, not realizing this would become available a 
month or two later!
https://github.com/giraffelibrary/giraffe/commit/2dc239946c77bdf8cb8b55223f93fcd6758439d3 



Regards,
Phil

On 19/10/20 12:12, David Matthews wrote:

Hi,
I've just pushed a collection of changes to master that have been in 
the pipeline for quite a long time.  Some of these are internal 
changes to the run-time system and some are extensions, such as the 
addition of IPv6 networking with INet6Sock and Net6HostDB structures.


The major change, though, is with the foreign function interface.  On 
X86 platforms libffi is no longer used and the version of it included 
in the libpolyml directory has been removed.  Libffi is still used in 
the interpreted version but only if the library is installed on the 
system.


Instead the foreign function interface is handled essentially as part 
of the compiler.  The high-level interface in the Foreign structure 
remains unchanged but the buildCallN functions now actually compile 
interface functions.  This results in foreign function calls being 
substantially faster than with libffi; at least 10 times faster for 
trivial calls on the X86/64.  The cost is, of course, some extra work 
when buildCallN is called, meaning that it is essential that these 
functions are only used at the top level.


The reason for the speed-up is that the interface has to place the 
arguments in the correct registers for the ABI and the rules for 
placing arguments can be quite complicated, particular on the X86/64 
on Unix. Libffi computes the placement on every call whereas the 
compiler can do this once and build code that moves the arguments 
into the right registers and returns the result.


For backwards compatibility buildClosureN functions have be

Re: [polyml] Updates in git master including major change to FFI

[Phil Clayton]

In testing callbacks during callbacks, I have also tried a rather 
contrived example (attached) where the SML function closures to call 
back are passed down as arguments.  It's not something that I have 
needed to do.  I simply cannot get this to work with either 5.8.1 or the 
latest version in master.  With both versions I see the following output:


An ML function called from foreign code raised an exception.  Unable to 
continue.
call_c_test_15: diagnostics.cpp:128: void Crash(const char*, ...): 
Assertion `0' failed.


I see this even if I wrap exception handlers around the called-back 
functions to ensure that they cannot raise an exception.


I may well be doing something wrong in the example but I can't see what 
it is.  I've mentioned it in case it highlights an issue.


Regards,
Phil

On 18/02/21 23:57, Phil Clayton wrote:
I have finally tried out the new FFI with Giraffe Library with partial 
success.  For some examples, calls to C and callbacks from C are working 
but other examples result a seg. fault.  From the debug output, I 
noticed that the seg. faults occur when a callback occurs during a 
callback.  I've attached a small example that demonstrates the issue 
(call_c_test_16.tar.gz).  (Although this example uses dynamic loading, 
the same happens if dynamic linking is used.)  The backtrace from gdb 
provided no useful information so I didn't investigate further.


Also, I have some minor observations about the interface.  I note that 
the signature FOREIGN specifies:

     val touchClosure: 'a -> unit
I wondered whether that should be
     val touchClosure: 'a closure -> unit
(RunCall.touch is visible in the Poly/ML top-level which has the type of 
the former, so there is no loss of capability with the latter, which 
would catch cases where touchClosure is applied to the wrong value.)


In both the old and new Foreign modules, the type `'a Foreign.closure` 
is abstract.  Giraffe Library uses `Foreign.LowLevel.cFunctionWithAbi` 
define its own function for creating a closure but there is no way to 
create a `'a Foreign.closure` value from a `Memory.voidStar` value. This 
is easily worked around by copying the type declaration and definition 
of `Foreign.cFunction` but I wondered if there could be a way to avoid 
this copying.


In the past, I found it useful to have
     val nullClosure : 'a closure
This is easily declared with one's own closure type but if using 
Foreign.closure, it may be useful to have in Foreign.  Giraffe Library 
no longer needs this since I changed the callback mechanism to avoid the 
need to free closures, not realizing this would become available a month 
or two later!
https://github.com/giraffelibrary/giraffe/commit/2dc239946c77bdf8cb8b55223f93fcd6758439d3 



Regards,
Phil

On 19/10/20 12:12, David Matthews wrote:

Hi,
I've just pushed a collection of changes to master that have been in 
the pipeline for quite a long time.  Some of these are internal 
changes to the run-time system and some are extensions, such as the 
addition of IPv6 networking with INet6Sock and Net6HostDB structures.


The major change, though, is with the foreign function interface.  On 
X86 platforms libffi is no longer used and the version of it included 
in the libpolyml directory has been removed.  Libffi is still used in 
the interpreted version but only if the library is installed on the 
system.


Instead the foreign function interface is handled essentially as part 
of the compiler.  The high-level interface in the Foreign structure 
remains unchanged but the buildCallN functions now actually compile 
interface functions.  This results in foreign function calls being 
substantially faster than with libffi; at least 10 times faster for 
trivial calls on the X86/64.  The cost is, of course, some extra work 
when buildCallN is called, meaning that it is essential that these 
functions are only used at the top level.


The reason for the speed-up is that the interface has to place the 
arguments in the correct registers for the ABI and the rules for 
placing arguments can be quite complicated, particular on the X86/64 
on Unix. Libffi computes the placement on every call whereas the 
compiler can do this once and build code that moves the arguments into 
the right registers and returns the result.


For backwards compatibility buildClosureN functions have been retained 
but these are wrappers around new buildCallback functions.  The 
buildCallback functions differ in two respects.  Closures created with 
buildCallback are garbage-collected which means that if they are used 
to register callbacks with a C library it may be necessary to keep a 
reference in ML.  There is a touchClosure function that should be 
called when the callback is no longer needed.  For compatibility 
closures created with buildClosure are retained in a global list to 
avoid garbage collection.


The other difference is that the buildCallba

Re: [polyml] Updates in git master including major change to FFI

[Phil Clayton]

I have finally tried out the new FFI with Giraffe Library with partial 
success.  For some examples, calls to C and callbacks from C are working 
but other examples result a seg. fault.  From the debug output, I 
noticed that the seg. faults occur when a callback occurs during a 
callback.  I've attached a small example that demonstrates the issue 
(call_c_test_16.tar.gz).  (Although this example uses dynamic loading, 
the same happens if dynamic linking is used.)  The backtrace from gdb 
provided no useful information so I didn't investigate further.


Also, I have some minor observations about the interface.  I note that 
the signature FOREIGN specifies:

val touchClosure: 'a -> unit
I wondered whether that should be
val touchClosure: 'a closure -> unit
(RunCall.touch is visible in the Poly/ML top-level which has the type of 
the former, so there is no loss of capability with the latter, which 
would catch cases where touchClosure is applied to the wrong value.)


In both the old and new Foreign modules, the type `'a Foreign.closure` 
is abstract.  Giraffe Library uses `Foreign.LowLevel.cFunctionWithAbi` 
define its own function for creating a closure but there is no way to 
create a `'a Foreign.closure` value from a `Memory.voidStar` value. 
This is easily worked around by copying the type declaration and 
definition of `Foreign.cFunction` but I wondered if there could be a way 
to avoid this copying.


In the past, I found it useful to have
val nullClosure : 'a closure
This is easily declared with one's own closure type but if using 
Foreign.closure, it may be useful to have in Foreign.  Giraffe Library 
no longer needs this since I changed the callback mechanism to avoid the 
need to free closures, not realizing this would become available a month 
or two later!

https://github.com/giraffelibrary/giraffe/commit/2dc239946c77bdf8cb8b55223f93fcd6758439d3

Regards,
Phil

On 19/10/20 12:12, David Matthews wrote:

Hi,
I've just pushed a collection of changes to master that have been in the 
pipeline for quite a long time.  Some of these are internal changes to 
the run-time system and some are extensions, such as the addition of 
IPv6 networking with INet6Sock and Net6HostDB structures.


The major change, though, is with the foreign function interface.  On 
X86 platforms libffi is no longer used and the version of it included in 
the libpolyml directory has been removed.  Libffi is still used in the 
interpreted version but only if the library is installed on the system.


Instead the foreign function interface is handled essentially as part of 
the compiler.  The high-level interface in the Foreign structure remains 
unchanged but the buildCallN functions now actually compile interface 
functions.  This results in foreign function calls being substantially 
faster than with libffi; at least 10 times faster for trivial calls on 
the X86/64.  The cost is, of course, some extra work when buildCallN is 
called, meaning that it is essential that these functions are only used 
at the top level.


The reason for the speed-up is that the interface has to place the 
arguments in the correct registers for the ABI and the rules for placing 
arguments can be quite complicated, particular on the X86/64 on Unix. 
Libffi computes the placement on every call whereas the compiler can do 
this once and build code that moves the arguments into the right 
registers and returns the result.


For backwards compatibility buildClosureN functions have been retained 
but these are wrappers around new buildCallback functions.  The 
buildCallback functions differ in two respects.  Closures created with 
buildCallback are garbage-collected which means that if they are used to 
register callbacks with a C library it may be necessary to keep a 
reference in ML.  There is a touchClosure function that should be called 
when the callback is no longer needed.  For compatibility closures 
created with buildClosure are retained in a global list to avoid garbage 
collection.


The other difference is that the buildCallback functions have a slightly 
different type from buildClosure and that reflects the underlying 
implementation.  For example,

val buildCallback1: 'a conversion * 'b conversion ->
     ('a -> 'b) ->
     ('a -> 'b) closure
The first application builds the interface code that handle the 
conversion between the ML and C ABIs.  The second application applies 
this to an ML function to build a closure value that can be passed to C. 
  This second application builds a small additional piece of code that 
simply loads the address of the ML function into a register and jumps to 
the interface code.  What this means is that while the first application 
should always be done at the top level it is possible to embed an 
application of this to a particular ML function inside ML code.  There 
is still an overhead compared with creating a closure in ML and it is 
better if possible to do the application at the top level bu

Re: [polyml] Announcement: Giraffe Library

[Phil Clayton]

That's unfortunate timing.  It's worth noting that languages using 
GObject Introspection to provide bindings should expose similarly named 
types, functions, signals and properties which eases conversion between 
those languages (which is why e.g. GTK tutorials for other languages can 
be useful for SML).


Thanks for mentioning the software directory.  I've now added it.

Phil

On 16/02/21 13:59, David Matthews wrote:
That looks really interesting.  I did some programming recently using 
GLib and it would have been good to have been able to do it in ML.


Would you like to add a reference to it to the software directory 
https://www.polyml.org/software/index.php ?  The idea of that was to 
enable users to find libraries just such as this.


Regards,
David

On 14/02/2021 13:53, Phil Clayton wrote:

[Apologies if you receive multiple copies this message]

Dear Poly/ML users,

I would like to announce the first public release of Giraffe Library, 
an SML interface to libraries that support GObject Introspection, such 
as GTK.


The latest release, 1.0.0-alpha.11, provides GTK 3 and supporting 
libraries, enabling applications with GUIs to be written entirely in 
SML.  Applications without GUIs may also find some features useful, 
for example, in GLib, sockets using UDP multicast and various 
checksums, which are not available in the current Basis Library.


For more information, download, documentation and examples, please see:

   http://giraffelibrary.org/

Regards,

Phil
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml



___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

[polyml] Announcement: Giraffe Library

[Phil Clayton]

[Apologies if you receive multiple copies this message]

Dear Poly/ML users,

I would like to announce the first public release of Giraffe Library, an 
SML interface to libraries that support GObject Introspection, such as GTK.


The latest release, 1.0.0-alpha.11, provides GTK 3 and supporting 
libraries, enabling applications with GUIs to be written entirely in 
SML.  Applications without GUIs may also find some features useful, for 
example, in GLib, sockets using UDP multicast and various checksums, 
which are not available in the current Basis Library.


For more information, download, documentation and examples, please see:

  http://giraffelibrary.org/

Regards,

Phil
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Install to users home directory

[Phil Clayton]

On 20/10/20 14:46, Jerry James wrote:

On Tue, Oct 20, 2020 at 3:14 AM Phil Clayton  wrote:

There are some instructions previously posted here:
http://lists.inf.ed.ac.uk/pipermail/polyml/2017-July/002038.html
which also show how to disable the package manager version of Poly/ML on
Fedora.


I am the current maintainer of the Fedora polyml package.  If anyone
has problems with it, please let me know.  I would like it to work
well for Fedora users.

I only build official releases, of course, so if you want to follow
development, you'll have to build your own version.  Otherwise,
though, I would like the Fedora package to be of high quality.


The package version looks good - I didn't intend to suggest otherwise. 
The issue is that updates are available for only the two most recent 
Fedora releases (I think), so older releases won't get any Poly/ML updates.


As noted in the linked message, the only reason I can see for disabling 
the package manager version is to manually install to /usr but instead I 
recommend installing in a non-conflicting location and setting up 
environment variables accordingly.  (This is all moot now we know which 
system David T. is using.)


Phil
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Run polyml in the broswer

[Phil Clayton]

Amazing!  Is there a way to copy/paste between the VM and local machine? 
 (The right-click contextual menu referred to in the FAQ isn't working 
for me.)


On 20/10/20 15:41, David Topham wrote:
Thanks to Fabrice Bellard (of QEMU fame) for his wonderful work on 
JSLinux, we can now run Alpine Linux in modern browsers using Javascript 
and Webassembly to support a virtual x86 machine.


I installed polyml in the Alpine Linux users home directory, so now 
anyone can run polyml in their browser.  Try it! (it takes a few seconds 
to boot up)


https://bellard.org/jslinux/vm.html?url=alpine-x86-xwin.cfg&mem=1024&graphic=1&guest_url=https://vfsync.org/u/polyml/pub


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Install to users home directory

[Phil Clayton]

I fired up the VM and, in the terminal, ran

  objdump -p polyml/bin/poly

and I see the output contains:

  Dynamic Section:
...
RPATH  /root/polyml/lib
...

If that RPATH were correctly set (to /home/guest/polyml/lib) I suspect 
you wouldn't need to set LD_LIBRARY_PATH in the environment.


Phil

On 20/10/20 14:54, David Topham wrote:

Thanks Phil, I found I needed to set
LD_LIBRARY_PATH as well as PATH to $HOME to use interpreter.
I really appreciate the helpful information from this community!

On Tue, Oct 20, 2020 at 4:00 AM <mailto:polyml-requ...@inf.ed.ac.uk>> wrote:


Send polyml mailing list submissions to
polyml@inf.ed.ac.uk <mailto:polyml@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-requ...@inf.ed.ac.uk <mailto:polyml-requ...@inf.ed.ac.uk>

You can reach the person managing the list at
polyml-ow...@inf.ed.ac.uk <mailto:polyml-ow...@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: Install to users home directory (Phil Clayton)
    2. Re: polyml install to Alpine Linux (David Matthews)


--

Message: 1
Date: Tue, 20 Oct 2020 10:12:37 +0100
From: Phil Clayton mailto:phil.clay...@veonix.com>>
To: polyml@inf.ed.ac.uk <mailto:polyml@inf.ed.ac.uk>
Subject: Re: [polyml] Install to users home directory
Message-ID: <090b6bb7-106a-eb9e-0732-2b00a050e...@veonix.com
<mailto:090b6bb7-106a-eb9e-0732-2b00a050e...@veonix.com>>
Content-Type: text/plain; charset=utf-8; format=flowed

On 20/10/20 05:40, David Topham wrote:
 > I know it is most efficient to install software system wide so
all users
 > share same code. But I have a situation where I want to install
only to
 > my home directory. i.e. It is Linux system where I don't have sudo
 > privilege.
 > Is that possible?
 > I am building from source, so perhaps
 > ./configure ?--prefix=$HOME
 > make
 > make install
 >
 > Or does polyml have too many dependencies on other system
libraries to
 > make that impractical?

You can specify any prefix to install to - this does not affect how
dependencies are found.  However, depending on your choice of prefix,
you may need to manually add /bin to PATH.  Depending on your
Linux distribution, it would probably be more idiomatic to do a
per-user
install to
    $HOME/.local
to avoid cluttering the home directory.  Also, if you have Poly/ML
installed system-wide via the package manager, you would need to make
sure that /bin occurs in the path before the system bin
directory, to ensure your user version is found first.

There are some instructions previously posted here:
http://lists.inf.ed.ac.uk/pipermail/polyml/2017-July/002038.html
which also show how to disable the package manager version of
Poly/ML on
Fedora.

Phil


--

Message: 2
Date: Tue, 20 Oct 2020 11:56:55 +0100
From: David Matthews mailto:david.matth...@prolingua.co.uk>>
To: polyml@inf.ed.ac.uk <mailto:polyml@inf.ed.ac.uk>
Subject: Re: [polyml] polyml install to Alpine Linux
Message-ID: <5bca1bc6-063e-b199-65f1-31e259038...@prolingua.co.uk
<mailto:5bca1bc6-063e-b199-65f1-31e259038...@prolingua.co.uk>>
Content-Type: text/plain; charset=utf-8; format=flowed

On 19/10/2020 21:08, David Matthews wrote:
 >> Yes, using .data.rel.ro <http://data.rel.ro>., i.e. relocatable
read-only data.
 >
 > Thanks, Jess.? That seems to work, at least on SELinux and Alpine.
 > OpenBSD seems to still want it to be writeable.

I've now changed the ELF exporter to write the data to .data.rel.ro
<http://data.rel.ro>.
The byte code interpreted version (--disable-native-codegeneration) now
builds without a problem on Alpine Linux and on SELinux with hardening
turned on.  That isn't a complete solution because it doesn't deal with
native code but it does show that if code could be handled everything
else will work.

I see this primarily as future-proofing Poly/ML.  It's not unlikely
that
a future release of, say Mac OS X, might outlaw TEXTRELs.

David


--

Subject: Digest Footer

___
polyml mailing list
polyml@inf.ed.ac.uk <mailto:polyml@inf.ed.ac.uk>
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Install to users home directory

[Phil Clayton]

On 20/10/20 05:40, David Topham wrote:
I know it is most efficient to install software system wide so all users 
share same code. But I have a situation where I want to install only to 
my home directory. i.e. It is Linux system where I don't have sudo 
privilege.

Is that possible?
I am building from source, so perhaps
./configure  --prefix=$HOME
make
make install

Or does polyml have too many dependencies on other system libraries to 
make that impractical?


You can specify any prefix to install to - this does not affect how 
dependencies are found.  However, depending on your choice of prefix, 
you may need to manually add /bin to PATH.  Depending on your 
Linux distribution, it would probably be more idiomatic to do a per-user 
install to

  $HOME/.local
to avoid cluttering the home directory.  Also, if you have Poly/ML 
installed system-wide via the package manager, you would need to make 
sure that /bin occurs in the path before the system bin 
directory, to ensure your user version is found first.


There are some instructions previously posted here:
http://lists.inf.ed.ac.uk/pipermail/polyml/2017-July/002038.html
which also show how to disable the package manager version of Poly/ML on 
Fedora.


Phil
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Version 5.8.1 Release

[Phil Clayton]

David,

Thanks for the release!

The release message in Github
[https://github.com/polyml/polyml/releases/tag/v5.8.1]
says
"Added Weak.touch. Including this in code that uses a weak reference 
ensures that the reference will not be garbage-collected."
I think Weak.touch was actually introduced in Poly/ML 5.6 (or even 
5.5.3).  It looks like 5.8.1 just changes its implementation.


Phil

On 20/07/20 20:57, David Matthews wrote:
After the recent bug fixes I thought it was time to produce a new 
release.  There are very few new features; it's almost all bug fixes.


Thanks to everyone for the patches and bug reports.

David

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] [ExternalEmail] Compiler (0ad5aa87) raises Option

[Phil Clayton]

I managed to produce a smallish example fairly quickly as the code 
causing it didn't have many dependencies.  I have raised 
https://github.com/polyml/polyml/issues/136


Phil

On 30/06/20 00:14, Norrish, Michael (Data61, Acton) wrote:

No, I'm afraid not.  I will try to find some time to find a MWE this week.

Michael

On 30/6/20, 02:54, "polyml on behalf of Phil Clayton" 
 wrote:

I, too, am seeing this error message with the latest master (ef44a8b).

Michael - did you make any progress with this issue?

Phil

On 22/06/20 02:18, Norrish, Michael (Data61, Acton) wrote:

Sorry to spam (will take this elsewhere after this).

The "workaround" below doesn't help in the wider context.  If I select all of 
the code without the enclosing

structure helperLib :> helperLib = struct ... end

it compiles without error, but if I have the enclosure, I again get the same 
Option error.

Michael

On 22/6/20, 11:08, "polyml on behalf of Norrish, Michael (Data61, Acton)" 
 wrote:

I get a workaround by lifting the definition of find_term_and_apply out to the 
top-level.

Michael



On 22/6/20, 10:54, "polyml on behalf of Norrish, Michael (Data61, Acton)" 
 wrote:

I don't expect this in isolation will help, but the following HOL function 
causes the compiler to emit a

Fail "Exception- Option unexpectedly raised while compiling"

message.

- - -

fun EXISTS_SEP_REWRITE_RULE rw th = let (* possibly fragile *)
val (p,q) = dest_eq (concl (SPEC_ALL rw))
val frame = genvar(type_of p)
val vs = list_dest dest_sep_exists p
val lhs = mk_star(last vs,frame)
val vs = butlast vs
fun find_exists_match lhs tm = let
  val (v,t) = dest_sep_exists tm
  val vs = list_dest dest_sep_exists tm
  in (butlast vs,last vs,generic_star_match [] lhs (last vs)) end
fun find_term_and_apply f tm = f (find_term (can f) tm)
fun foo th = let
  val (ws,tm,s) = find_term_and_apply (find_exists_match lhs) (concl th)
  val (t,t2) = (dest_eq (concl (SPEC_ALL rw)))
  val zs = list_dest dest_sep_exists t
  val (zs,z) = (butlast zs,list_dest dest_star (last zs))
  val xs = list_dest dest_star tm
  val ys = filter (fn y => not (tmem y (map (subst s) z))) xs
  val t3 = foldr mk_sep_exists (subst s (list_mk_star z (type_of frame))) 
(map (subst s) zs)
  val goal = foldr mk_sep_exists (list_mk_star (t3::ys) (type_of frame)) ws
  val goal = mk_eq(foldr mk_sep_exists tm ws,goal)
  val lemma = auto_prove "EXISTS_SEP_REWRITE_RULE" (goal,
SIMP_TAC std_ss [GSYM rw]
THEN SIMP_TAC (std_ss++sep_cond_ss) [SEP_CLAUSES]
THEN CONV_TAC (BINOP_CONV SEP_EXISTS_AC_CONV)
THEN SIMP_TAC (std_ss++star_ss) [AC CONJ_ASSOC CONJ_COMM])
  val lemma = CONV_RULE (RAND_CONV (ONCE_REWRITE_CONV [rw]
THENC SIMP_CONV std_ss [SEP_CLAUSES])) lemma
  in foo (RW1 [lemma] th) end handle HOL_ERR _ => th
in foo th end;

- - -

This comes from HOL4's examples/machine-code/hoare-triple/helperLib.sml (line 
667 onwards).

I will try to reduce it to a smaller instance.

Michael

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] [ExternalEmail] Compiler (0ad5aa87) raises Option

[Phil Clayton]

I, too, am seeing this error message with the latest master (ef44a8b).

Michael - did you make any progress with this issue?

Phil

On 22/06/20 02:18, Norrish, Michael (Data61, Acton) wrote:

Sorry to spam (will take this elsewhere after this).

The "workaround" below doesn't help in the wider context.  If I select all of 
the code without the enclosing

   structure helperLib :> helperLib = struct ... end

it compiles without error, but if I have the enclosure, I again get the same 
Option error.

Michael

On 22/6/20, 11:08, "polyml on behalf of Norrish, Michael (Data61, Acton)" 
 wrote:

I get a workaround by lifting the definition of find_term_and_apply out to the 
top-level.

Michael



On 22/6/20, 10:54, "polyml on behalf of Norrish, Michael (Data61, Acton)" 
 wrote:

I don't expect this in isolation will help, but the following HOL function 
causes the compiler to emit a

   Fail "Exception- Option unexpectedly raised while compiling"

message.

- - -

fun EXISTS_SEP_REWRITE_RULE rw th = let (* possibly fragile *)
   val (p,q) = dest_eq (concl (SPEC_ALL rw))
   val frame = genvar(type_of p)
   val vs = list_dest dest_sep_exists p
   val lhs = mk_star(last vs,frame)
   val vs = butlast vs
   fun find_exists_match lhs tm = let
 val (v,t) = dest_sep_exists tm
 val vs = list_dest dest_sep_exists tm
 in (butlast vs,last vs,generic_star_match [] lhs (last vs)) end
   fun find_term_and_apply f tm = f (find_term (can f) tm)
   fun foo th = let
 val (ws,tm,s) = find_term_and_apply (find_exists_match lhs) (concl th)
 val (t,t2) = (dest_eq (concl (SPEC_ALL rw)))
 val zs = list_dest dest_sep_exists t
 val (zs,z) = (butlast zs,list_dest dest_star (last zs))
 val xs = list_dest dest_star tm
 val ys = filter (fn y => not (tmem y (map (subst s) z))) xs
 val t3 = foldr mk_sep_exists (subst s (list_mk_star z (type_of frame))) 
(map (subst s) zs)
 val goal = foldr mk_sep_exists (list_mk_star (t3::ys) (type_of frame)) ws
 val goal = mk_eq(foldr mk_sep_exists tm ws,goal)
 val lemma = auto_prove "EXISTS_SEP_REWRITE_RULE" (goal,
   SIMP_TAC std_ss [GSYM rw]
   THEN SIMP_TAC (std_ss++sep_cond_ss) [SEP_CLAUSES]
   THEN CONV_TAC (BINOP_CONV SEP_EXISTS_AC_CONV)
   THEN SIMP_TAC (std_ss++star_ss) [AC CONJ_ASSOC CONJ_COMM])
 val lemma = CONV_RULE (RAND_CONV (ONCE_REWRITE_CONV [rw]
   THENC SIMP_CONV std_ss [SEP_CLAUSES])) lemma
 in foo (RW1 [lemma] th) end handle HOL_ERR _ => th
   in foo th end;

- - -

This comes from HOL4's examples/machine-code/hoare-triple/helperLib.sml (line 
667 onwards).

I will try to reduce it to a smaller instance.

Michael

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Horrific GC(?) behaviour in 5.8 (g44efa473)

[Phil Clayton]

I've built HOL4 with versions of Poly/ML before and after the fix 
(c355b21 and 0ad5aa8) on Linux x86_64.  I ran the miller example (with 
fixes for Poly/ML reverted) and it appears that 0ad5aa8 fixes the issue.


Under c355b21:

[pclayton@localhost miller]$ ./selftest.exe
Composite test on 91 ... 
  (0.024s)  OK
Composite test on 123 ... 
  (0.016s)  OK
Composite test on 4294967297 ... 
 [GC = 3.401] (0.394s)  OK
Composite test on 18446744073709551617 ... 
[GC = 186.871] (3.216s)  OK
Composite test on 340282366920938463463374607431768211457 ... 
^C^C


Under 0ad5aa8:

[pclayton@localhost miller]$ ./selftest.exe
Composite test on 91 ... 
[GC = 0.027] (0.023s)  OK
Composite test on 123 ... 
 (0.018s)  OK
Composite test on 4294967297 ... 
 (0.360s)  OK
Composite test on 18446744073709551617 ... 
 (2.540s)  OK
Composite test on 340282366920938463463374607431768211457 ... 
(19.700s)  OK


Chun - your Poly/ML build commands (make compiler; make install) don't 
specify "make compiler" after "make" - see

https://www.polyml.org/download.html
I wonder therefore whether the compiler was rebuilt in your test.

Phil

On 20/06/20 04:32, Chun Tian (binghe) wrote:

Hi David,

no I didn't do "make compiler" in my previous tests...  But after I did 
it (make compiler; make install) and rebuilt HOL, the "miller" selftest 
result is the same. The whole testing process still need more than 8 
minutes to finish.


Regards,

Chun


On Sat, Jun 20, 2020 at 1:23 AM David Matthews 
mailto:david.matth...@prolingua.co.uk>> 
wrote:


Hi,
You did run "make compiler" at least once after running "configure" and
"make", didn't you?
David

On 19/06/2020 18:17, Chun Tian (binghe) wrote:
 > Hi David,
 >
 > I rebuilt and installed PolyML 5.8 ('master', up to 0ad5aa8) and
ran again
 > the 'miller' selftests as Michael mentioned, but the results seem
unchanged:
 >
 > ```
 > Composite test on 91 ...
 > (0.018s)      OK
 > Composite test on 123 ...                                     [GC
= 0.037]
 > (0.013s)      OK
 > Composite test on 4294967297 ...                              [GC
= 3.487]
 > (0.376s)      OK
 > Composite test on 18446744073709551617 ...                    [GC
= 84.370]
 > (2.846s)     OK
 > Composite test on 340282366920938463463374607431768211457 ... [GC =
 > 429.267] (21.935s)   OK
 >
 > real 9m19.723s
 > user 9m7.408s
 > sys 0m12.139s
 > ```
 >
 > I'm on macOS 10.15 (catalina) with 2,3 GHz Intel Core i9 (8
core). The same
 > tests took less than 30s with PolyML 5.7.
 >
 > Hope this helps,
 >
 > Chun Tian
 >
 >
 > On Fri, Jun 19, 2020 at 6:54 PM David Matthews <
 > david.matth...@prolingua.co.uk
<mailto:david.matth...@prolingua.co.uk>> wrote:
 >
 >> Thanks, Phil, for reminding me of this.  I've committed a fix
(0ad5aa8)
 >> for that.  There was a tail-recursive function in your example that
 >> returned a tuple.  Poly/ML puts these on the stack where it can
but in
 >> this case it was causing the function to cease to be tail-recursive,
 >> eating up the stack.  The reason for the regression was a change
in the
 >> way tuples on the stack are handled in the 32-in-64 bit
version.  Your
 >> example now works as it used to.
 >>
 >> Michael, it would be worth trying your code with the latest
version to
 >> see if this has fixed it.  If it hasn't then presumably it's a
different
 >> problem and I'll have to investigate further.
 >>
 >> David
 >>
 >> On 16/06/2020 09:58, Phil Clayton wrote:
 >>> I also found that 5.8 can consume a huge amount of memory
compared to
 >>> 5.7.1.  In my case, it was a very small example doing simple
arithmetic
 >>> operations (demonstrating Fermat's method to find pairs of
factors) so
 >>> it may be related.  I have raised an issue for it:
 >>> https://github.com/polyml/polyml/issues/121
 >>>
 >>> Phil
 >>>
 >>> On 16/06/20 02:30, Norrish, Michael (Data61, Acton) wrote:
 >>>> I have some HOL code that runs to completion in ~24 seconds
user time.
 >>>>
 >>>> On 5.7.1 it runs in about that much wall clock time too.
 >>>> (Unfortunately, this test is runn

Re: [polyml] Horrific GC(?) behaviour in 5.8 (g44efa473)

[Phil Clayton]

I also found that 5.8 can consume a huge amount of memory compared to 
5.7.1.  In my case, it was a very small example doing simple arithmetic 
operations (demonstrating Fermat's method to find pairs of factors) so 
it may be related.  I have raised an issue for it:

https://github.com/polyml/polyml/issues/121

Phil

On 16/06/20 02:30, Norrish, Michael (Data61, Acton) wrote:

I have some HOL code that runs to completion in ~24 seconds user time.

On 5.7.1 it runs in about that much wall clock time too.  (Unfortunately, this 
test is running on a different machine, necessarily, but this is an old Linux 
desktop which is far less powerful than the new Macbook Pro which is running 
5.8.)

On 5.8 (updated for MacOS Catalina to the SHA above), wall clock time is 8 
minutes.

The relevant code is the selftest in examples/miller/miller which is a big 
arithmetic normalisation.

On the Mac, memory consumption (as reported by the Activity Monitor) gets as 
high as 20GB; on the Linux machine running 5.7.1, the consumption remains very 
slight (top reports 3% in its %MEM column; the machine has 16GB)

Michael



___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Building an executable that runs the read-eval-print loop

[Phil Clayton]

Rob,

Inside polyc, poly is invoked with -q to suppress output.  This flag 
sets the print depth to zero and this is being inherited by your 
application.  In your second example, you would also lose the output if 
you specified -q as follows:


  poly -q < t.ML
  polyc -o t t.o

You could add
  val () = PolyML.print_depth ...
to the end of t.ML.  If you add it before the end, polyc output will no 
longer be suppressed.  Alternatively you could add

  val () = PolyML.onEntry (fn () => PolyML.print_depth ...)
anywhere.  Unlike PolyML.export, using PolyML.print_depth avoids having 
to mention the object file name.


Regards,
Phil

On 27/03/19 18:48, Rob Arthan wrote:

I wanted to create an executable that runs the Poly/ML read-eval-print loop
with some code of mine precompiled. What I found was that the print part
of the read-eval-print loop doesn't work if I compile from source with
polyc, but does work if I use PolyML.export to create a .o file and then link it
with polyc.

For example, if I have a file t.ML containing the following two lines:

fun p s = (TextIO.output(TextIO.stdOut, s); s);
val main = PolyML.rootFunction

and compile it with:

polyc -o t t.ML

and then run:

echo 'val x = p "Boo!\n"' | t

the output I see is:

Poly/ML 5.7 Release
Boo!

So it's executed my code, but it hasn't printed the usual report
on the new value binding for x.

So I copied what I do in ProofPower, which does something similar
but doesn't have this problem. I appended the following line to t.ML:

val _ = PolyML.export ("t", main);

and compiled it with:

poly < t.ML
polyc -o t t.o

Then when I run t as above, I see the output, I'd expected to get:

Poly/ML 5.7 Release
Boo!
val x = "Boo!\n": string

The work-around is easy, but it would be nice to be able to compile
from source to executable directly (and to minimise the Poly/ML-specific
code in my source).

Regards,

Rob.

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Memory leak when FFI callback and ref value.

[Phil Clayton]

Hi Nick,

I believe that a closure created with buildClosureX is not automatically 
garbage collected because Poly/ML can't know how long a C function is 
going to hold on to the callback for.  Therefore, I suspect what's 
happening is that Poly/ML can't garbage collect the list accum because 
that is referenced by the callback function which is referenced by the 
closure.  This is desirable behaviour: accum is needed as long as there 
is a chance that the callback can be called.  If you clear out the 
contents of accum explicitly then those contents can be garbage 
collected but accum itself still won't be.  That's my guess - I haven't 
tested this hypothesis.


Phil


On 14/03/19 14:01, Kostirya wrote:

Hello.

I found memory leak when FFI callback and ref value.
I checked Poly/ML 5.8 and 5.7.
Simple code for reproduce the memory leak is attached.

To prevent the memory leak I clean ref value (see comment in example).
But It must do the garbage collector, is it? At least MLton have not
this problem.


Result of run of example code:

Without clean ref value (The memory leak is)
USER   PID %CPU %MEMVSZRSS TT  STAT STARTEDTIME COMMAND
nick 19855 91,8  9,7 305016 289452  6  S+   16:53   0:17,94 poly --script cb-po


With clean ref value
USER   PID %CPU %MEM   VSZ   RSS TT  STAT STARTEDTIME COMMAND
nick 19862 65,3  0,6 32632 17476  6  S+   16:54   0:10,77 poly --script cb-poly

Best, Nick.



___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Testing Poly/ML 5.8

[Phil Clayton]

Rob,

On 09/03/19 21:10, Rob Arthan wrote:

On 9 Mar 2019, at 16:59, David Matthews  wrote:


3) On MacOS with —disable-intinf-asint and —enable-compact32bit,
the ProofPower build fails like this:
Assertion failed: (space != 0), function ScanObjectAddress, file quick_gc.cpp, 
line 414.
4) On Fedora with —enable-intinf-asint and —enable-compact32bit,
the ProofPower build fails like this:
pp-ml: quick_gc.cpp:414: virtual PolyObject* 
QuickGCScanner::ScanObjectAddress(PolyObject*): Assertion `space != 0' failed.


This is a last chance to test the current git master before release. Don't forget to run "make compiler" at 
least twice after the initial "make" in order to build the up-to-date compiler and recompile all the code 
with it.  This is particularly important if testing the --enable-compact32bit version.  Some extra checking was added 
during testing and there is a strong chance of getting an assertion failure during the initial "make" or the 
first "make compiler" due to a bug in the pre-built compiler.  If this happens just rerun the step.  Once the 
compiler has been rebuilt it will incorporate a fix.


These are the assertion failure I mentioned.  Did this happen after running "make 
compiler"?



My script did:

make clean
make
make compiler
make compiler
make install

and it was the "make install" that failed. I also tried it with a third "make 
compiler" and that didn't make any difference.
Doing another "make install" failed in the same way.


To ensure that you have two successful runs of "make compiler", it may 
be worth adapting the script as follows:


make clean
make
while ! make compiler ; do echo "** failed, retrying make compiler **" ; 
done
while ! make compiler ; do echo "** failed, retrying make compiler **" ; 
done

make install

Still, I can't explain why "make install" would fail - I didn't think 
that invoked poly if the compiler is built.  I have built successfully 
on Fedora (25), and I'm happy to see what differs in your build if you 
send me your output log and config.status.


Regards,
Phil
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] LInkage and the Foreign structure

[Phil Clayton]

In fact `loadLibrary ""` doesn't work on Darwin, `loadExecutable ()` is 
required.


Phil

On 11/09/18 21:50, Phil Clayton wrote:
Looking at polyffi.cpp it actually looks like `loadLibrary ""` ends up 
calling

   dlopen ("", ...)
whereas `loadExecutable ()` ends up calling
   dlopen (NULL, ...)
A couple of things I have read suggest that these often give the same 
result, if not always.  So for non-Windows platforms `loadLibrary ""` 
and `loadExecutable ()` look similar.  However, the dlopen man page 
doesn't mention the empty string case, so it seems preferable to use 
`loadExecutable ()` over `loadLibrary ""`.


For Windows, I don't know what LoadLibrary("") does.  So again it seems 
preferable to use `loadExecutable ()` over `loadLibrary ""`.


Phil

On 11/09/18 04:15, Kostirya wrote:

Hello.
What is the difference between (LoadLibrary "") and (loadExecutable 
()) calls?


2018-09-10 17:53 GMT+03:00 Phil Clayton :
Slight correction: using an empty string for the library has the 
effect of
passing NULL to dlopen which means the handle passed to dlsym is the 
current

program.


On 10/09/18 15:29, Phil Clayton wrote:


Hi Mark,

  > (* symbol lookup error: /usr/lib/x86_64-linux-gnu/libgsl.so: 
undefined

  > symbol: cblas_dgemm *)

To avoid looking for the symbol "cblas_dgemm" in libgsl (which doesn't
define it), you could let the dynamic linker look for it by using an 
empty

string for the library which has the effect of passing RTLD_DEFAULT to
dlsym.

    val gsl = loadLibrary "";

To make sure these libraries are searched, you would need to start your
poly session with something like


LD_PRELOAD=/usr/lib/x86_64-linux-gnu/libgsl.so":"/usr/lib/x86_64-linux-gnu/libgslcblas.so 


\
    poly

which could be put into a wrapper script.  Or you could build an
executable (which could be a poly REPL) and link to them.

Another advantage of this approach is portability.  The SML code is 
more
portable because shared object names and their paths vary across 
systems.
Linking also avoids the problem of specifying the library names 
because you
use flags such as -lgsl and the linker works it out. Linking can be 
done in
an even more portable way using a utility like pkg-config to 
generate the

linker arguments:

    pkg-config --libs gsl

(This usual requires the -devel or -dev package for the library.)

Regards,
Phil


On 09/09/18 21:15, Mark Clements wrote:


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/x

Re: [polyml] LInkage and the Foreign structure

[Phil Clayton]

Hi David,

Thanks for the explanation and updates.  I have tested this, including 
externalDataSymbol, and all appears to work on my Linux and Darwin systems.


Initially I found that I wasn't seeing the new Foreign exception for an 
uninitalized external symbol, although there was no seg fault.  It turns 
out that was actually because the exception was occurring in a function 
registered with PolyML.onEntry.  It seems that PolyML.onEntry silently 
suppresses any exceptions from the functions it runs.  Is that intended?


I have been wondering if there is a way to have a local version of 
external(Function|Data)Symbol that falls back on

  getSymbol (loadExecutable ())
if the functions aren't available.  Could this be achieved by using one 
of two files depending on the value of PolyML.rtsVersion () ?


Thanks,
Phil

On 07/10/18 12:44, David Matthews wrote:

Hi Phil,
Thanks for that.  I've made some changes and if it all seems to work out 
I'll merge it into master.  I've added some comments below.


On 05/10/2018 09:23, Phil Clayton wrote:
I'm glad to see that Poly/ML does not include symbols in the object 
file that are referenced from ML but not required, e.g. because they 
occur in code that is never reached.  That's a useful property because 
it allows a library of ML bindings to support more functions than 
actually provided by the installed version of a binary library and 
required by the application.  Hopefully it will be possible to keep 
that property.


External symbols are ML cells that are recognised specially by 
PolyML.export and turned into linker symbols.  Since PolyML.export only 
exports reachable ML data the resulting object file will only contain 
symbols that are part of the exported code.  A consequence of this is 
that if the object file is then linked with a static library version of 
the C code the final executable will only contain the C code that is 
actually required.  An executable created using external symbols and a 
statically linked library will generally be more compact than having a 
separate dynamic library.  It also avoids the need for path 
specifications such as LD_LIBRARY_PATH.


I have run into a general issue.  After redefining a local version of 
the getSymbol function to use externalFunctionSymbol internally, I 
found that programs compiled and linked fine but seg faulted before 
entering the main ML function.  This was due to the scope in which a 
symbol was declared using externalFunctionSymbol.  The attached 
example call_c_test_13.tar.gz gives a simple example of the problem.  
The external function symbol isn't being declared until run time so 
this code is inadvertently depending on a feature of dynamic linking.  
I can see that use of externalFunctionSymbol is inherently more 
restricted that getSymbol: externalFunctionSymbol must be applied to a 
symbol name at compile time but the symbol cannot be used until run 
time, post-linking.  Are there any sort of checks that could be done 
to warn users if they get this wrong?   I can see it's not 
straightforward because run time is itself compile time for an 
exported function that is subsequently linked.  At the very least, 
could an exception be raised rather than seg faulting if there is an 
attempt to use an unresolved symbol?


I've been thinking about that.  The symbol is created with a zero 
address.  The actually address is set by the linker.  It now raises an 
exception if it tries to use a symbol when the value is zero.


Finally, is there a reason you chose the name "externalFunctionSymbol" 
rather than, say, "externalSymbol"?  It seems to work fine for 
non-functions too - see attached example call_c_test_14.tar.gz .


On the X86 and most platforms the same linker symbols are used for both 
function code and data.  There are a very few platforms that use 
different relocations for these.  See commit 76b36c9d.  I've added 
externalDataSymbol for data.


Regards,
David


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] LInkage and the Foreign structure

[Phil Clayton]

Hi David,

Thanks - this is useful.  At the very least it will point out missing 
dependencies at link time rather than run time.  That is, provided it is 
used correctly - see the issue below.


I'm glad to see that Poly/ML does not include symbols in the object file 
that are referenced from ML but not required, e.g. because they occur in 
code that is never reached.  That's a useful property because it allows 
a library of ML bindings to support more functions than actually 
provided by the installed version of a binary library and required by 
the application.  Hopefully it will be possible to keep that property.


I have run into a general issue.  After redefining a local version of 
the getSymbol function to use externalFunctionSymbol internally, I found 
that programs compiled and linked fine but seg faulted before entering 
the main ML function.  This was due to the scope in which a symbol was 
declared using externalFunctionSymbol.  The attached example 
call_c_test_13.tar.gz gives a simple example of the problem.  The 
external function symbol isn't being declared until run time so this 
code is inadvertently depending on a feature of dynamic linking.  I can 
see that use of externalFunctionSymbol is inherently more restricted 
that getSymbol: externalFunctionSymbol must be applied to a symbol name 
at compile time but the symbol cannot be used until run time, 
post-linking.  Are there any sort of checks that could be done to warn 
users if they get this wrong?   I can see it's not straightforward 
because run time is itself compile time for an exported function that is 
subsequently linked.  At the very least, could an exception be raised 
rather than seg faulting if there is an attempt to use an unresolved symbol?


Finally, is there a reason you chose the name "externalFunctionSymbol" 
rather than, say, "externalSymbol"?  It seems to work fine for 
non-functions too - see attached example call_c_test_14.tar.gz .


Phil

On 12/09/18 21:18, David Matthews wrote:
I've been thinking about adding direct external references as an 
alternative to dynamic loading of libraries.  The mechanism is all there 
now because the Poly/ML run-time library is linked to the exported code 
through external references.


I've added Foreign.externalFunctionSymbol : string -> symbol
This creates an external reference which is filled in when the code is 
exported.  The actual value is resolved by linking with the appropriate 
library.  For your example that means changing it to replace references 
to getSymbol to externalFunctionSymbol and removing the calls to 
loadLibrary.  i.e.

open Foreign;

type gsl_matrix_t = Memory.voidStar; (* for demonstration only *)
local
     val call1 =    buildCall2((externalFunctionSymbol 
"gsl_matrix_calloc"),

(cInt,cInt), cPointer)
     val call2 =    buildCall4((externalFunctionSymbol "gsl_matrix_set"),
(cPointer,cInt,cInt,cDouble), cVoid)
     val call3 =    buildCall3((externalFunctionSymbol
"gsl_linalg_exponential_ss"), (cPointer, cPointer, cDouble), cVoid)
in
fun gsl_matrix_alloc (size1,size2) = call1(size1,size2)

It seems to handle your example fine when the code is exported using 
"polyc" and then linked with the libraries.


I've committed this to a separate branch "ExternalBranch" on GitHub 
rather than "master".  I'd like some feedback on how useful this is and 
whether there are any problems before merging it.


David

On 09/09/2018 21:15, Mark Clements wrote:

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
 v

Re: [polyml] LInkage and the Foreign structure

[Phil Clayton]

Looking at polyffi.cpp it actually looks like `loadLibrary ""` ends up 
calling

  dlopen ("", ...)
whereas `loadExecutable ()` ends up calling
  dlopen (NULL, ...)
A couple of things I have read suggest that these often give the same 
result, if not always.  So for non-Windows platforms `loadLibrary ""` 
and `loadExecutable ()` look similar.  However, the dlopen man page 
doesn't mention the empty string case, so it seems preferable to use 
`loadExecutable ()` over `loadLibrary ""`.


For Windows, I don't know what LoadLibrary("") does.  So again it seems 
preferable to use `loadExecutable ()` over `loadLibrary ""`.


Phil

On 11/09/18 04:15, Kostirya wrote:

Hello.
What is the difference between (LoadLibrary "") and (loadExecutable ()) calls?

2018-09-10 17:53 GMT+03:00 Phil Clayton :

Slight correction: using an empty string for the library has the effect of
passing NULL to dlopen which means the handle passed to dlsym is the current
program.


On 10/09/18 15:29, Phil Clayton wrote:


Hi Mark,

  > (* symbol lookup error: /usr/lib/x86_64-linux-gnu/libgsl.so: undefined
  > symbol: cblas_dgemm *)

To avoid looking for the symbol "cblas_dgemm" in libgsl (which doesn't
define it), you could let the dynamic linker look for it by using an empty
string for the library which has the effect of passing RTLD_DEFAULT to
dlsym.

val gsl = loadLibrary "";

To make sure these libraries are searched, you would need to start your
poly session with something like


LD_PRELOAD=/usr/lib/x86_64-linux-gnu/libgsl.so":"/usr/lib/x86_64-linux-gnu/libgslcblas.so
\
poly

which could be put into a wrapper script.  Or you could build an
executable (which could be a poly REPL) and link to them.

Another advantage of this approach is portability.  The SML code is more
portable because shared object names and their paths vary across systems.
Linking also avoids the problem of specifying the library names because you
use flags such as -lgsl and the linker works it out. Linking can be done in
an even more portable way using a utility like pkg-config to generate the
linker arguments:

pkg-config --libs gsl

(This usual requires the -devel or -dev package for the library.)

Regards,
Phil


On 09/09/18 21:15, Mark Clements wrote:


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
___
polyml mailing list
polyml@inf.ed.ac.uk
htt

Re: [polyml] LInkage and the Foreign structure

[Phil Clayton]

Slight correction: using an empty string for the library has the effect 
of passing NULL to dlopen which means the handle passed to dlsym is the 
current program.


On 10/09/18 15:29, Phil Clayton wrote:

Hi Mark,

 > (* symbol lookup error: /usr/lib/x86_64-linux-gnu/libgsl.so: undefined
 > symbol: cblas_dgemm *)

To avoid looking for the symbol "cblas_dgemm" in libgsl (which doesn't 
define it), you could let the dynamic linker look for it by using an 
empty string for the library which has the effect of passing 
RTLD_DEFAULT to dlsym.


   val gsl = loadLibrary "";

To make sure these libraries are searched, you would need to start your 
poly session with something like


LD_PRELOAD=/usr/lib/x86_64-linux-gnu/libgsl.so":"/usr/lib/x86_64-linux-gnu/libgslcblas.so 
\

   poly

which could be put into a wrapper script.  Or you could build an 
executable (which could be a poly REPL) and link to them.


Another advantage of this approach is portability.  The SML code is more 
portable because shared object names and their paths vary across 
systems.  Linking also avoids the problem of specifying the library 
names because you use flags such as -lgsl and the linker works it out. 
Linking can be done in an even more portable way using a utility like 
pkg-config to generate the linker arguments:


   pkg-config --libs gsl

(This usual requires the -devel or -dev package for the library.)

Regards,
Phil


On 09/09/18 21:15, Mark Clements wrote:

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
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] LInkage and the Foreign structure

[Phil Clayton]

Hi Mark,

> (* symbol lookup error: /usr/lib/x86_64-linux-gnu/libgsl.so: undefined
> symbol: cblas_dgemm *)

To avoid looking for the symbol "cblas_dgemm" in libgsl (which doesn't 
define it), you could let the dynamic linker look for it by using an 
empty string for the library which has the effect of passing 
RTLD_DEFAULT to dlsym.


  val gsl = loadLibrary "";

To make sure these libraries are searched, you would need to start your 
poly session with something like


LD_PRELOAD=/usr/lib/x86_64-linux-gnu/libgsl.so":"/usr/lib/x86_64-linux-gnu/libgslcblas.so 
\

  poly

which could be put into a wrapper script.  Or you could build an 
executable (which could be a poly REPL) and link to them.


Another advantage of this approach is portability.  The SML code is more 
portable because shared object names and their paths vary across 
systems.  Linking also avoids the problem of specifying the library 
names because you use flags such as -lgsl and the linker works it out. 
Linking can be done in an even more portable way using a utility like 
pkg-config to generate the linker arguments:


  pkg-config --libs gsl

(This usual requires the -devel or -dev package for the library.)

Regards,
Phil


On 09/09/18 21:15, Mark Clements wrote:

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
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] socket from fd

[Phil Clayton]

Would it help if you could derive a path from the file descriptor?  It's 
horribly OS-specific:

https://stackoverflow.com/questions/1188757/getting-filename-from-file-descriptor-in-c

Phil

On 02/08/18 08:55, David Matthews wrote:
I don't think it's possible to create a socket from a file descriptor in 
ML.  While they are the same in Unix they are different in Windows. It's 
possible to go the other way using Socket.ioDesc.  Maybe someone else 
will have a solution.


David

On 01/08/2018 23:19, Ramana Kumar wrote:

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



___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] More portable poly compilation

[Phil Clayton]

Hi Makarius,

On 23/12/17 14:24, Makarius wrote:

Dear experts on building and linking C++ applications,

according to the blog "Creating portable Linux binaries"
http://insanecoding.blogspot.de/2012/07/creating-portable-linux-binaries.html
the following options could make the poly executable more portable
accross different Linux versions:

   CFLAGS="-static-libgcc -static-libstdc++ -Wl,-Bstatic -lgmp -Wl,-Bdynamic"

On the surface this works fine on x86_64-linux (Ubuntu 16.04 LTS), but
there is a remaining dependency on libpolyml.so, which itself depends on
dynamic gcc and stdc++ libraries.


When you build with the above CFLAGS, does
  objdump -p /bin/poly
show no NEEDED entry for libgcc and libstdc++ in the dynamic section? 
I.e. did this actually cause these libraries to be statically linked? 
(They are still present for me if I use the above -static-... options.)


"-Wl,-Bstatic -lgmp -Wl,-Bdynamic" causes configure to fail for me. 
That is not surprising because the packages for gmp only distribute 
shared object (.so) files - there is no archive (.a) file so static 
linking to gmp is not possible without building it myself.  Presumably 
you have archive/object files for all the libraries you want to 
statically link?



Including "-lpolyml" next to "-lgmp" above does not work, probably
because these options also apply to the build process of libpolyml itself.

How can I make libpolyml a static part of poly?


If you build Poly/ML with --disable-shared, libpolyml will always be 
statically linked: it has to be because no SO file is installed.


Even if Poly/ML is built with --enable-shared, the archive (.a) files 
are still installed.  Therefore, regardless of how Poly/ML was built, 
you can produce an executable that statically links libpolyml by linking 
as follows:


  gcc file.o \
-Wl,-Bstatic \
-L/lib -lpolymain -lpolyml \
-Wl,-Bdynamic \
-lpthread [-lffi] -lgmp -lm -ldl -lstdc++ -lgcc_s -lgcc

(-lffi required if --with-system-libffi was specified.)
You can't use polyc in this case though.

Phil



Alternatively, how can I make libgcc and libstdc++ a static part of
libpolyml?


Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

[polyml] FFI conversions that are portable across Poly/ML versions

[Phil Clayton]

I am trying to define LargeInt.int conversions for C integer types in 
terms of those supplied in Foreign in a way that will work with both 
Poly/ML 5.6 or 5.7.  This requires that e.g.

  - Foreign.cUint64 is used for Poly/ML = 5.6 but
  - Foreign.cUint64Large is used for Poly/ML >= 5.7
I am thinking of achieving this by having separate SML files for 
different Poly/ML versions and using the right one as follows:


  let
val version = PolyML.rtsVersion ()
  in
PolyML.use (
  if version >= 570
  then "src-5.7.sml"
  else if version = 560
  then "src-5.6.sml"
  else raise Fail "unsupported Poly/ML version"
)
  end

Is this a future-proof way to choose based on Poly/ML version?

Another option might be to copy the implementation of these conversions 
from Foreign.sml but that may not be possible - for example I couldn't 
see how to get the flag bigEndian in an application.


Is there a better way altogether with some compiler trickery?

Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] polyc and libraries

[Phil Clayton]

David,

I think I would expect `pkg-config --libs polyml` to provide the linker 
flags required to create an executable, i.e. I wouldn't expect to have 
to specify -lpolymain additionally.  I can't think of any other use 
cases of pkg-config because Poly/ML can't be used to produce a library. 
Even if it could, I don't believe adding -lpolymain would cause 
overlinking because only an archive version of libpolymain is available 
(and should always be available) and this shouldn't be included by the 
linker if there is no reference to the symbol "main".


For Poly/ML built with --disable-shared, Libs still has all the linker 
flags, as I would expect, except for -lpolymain.  If -lpolymain is 
added, it appears that it would need to be added _before_ -lpolyml 
(where it used to be), at least for my Linux distribution.


On a separate note, for Poly/ML built with --enable-shared, I believe 
that the flags recently removed to avoid overlinking should still be 
produced if `pkg-config --static ...` is used, so should appear in 
Libs.private.  However, it looks like this is only useful in the unusual 
case where all dependencies are to be statically linked.  Most 
distributions don't supply archives for all libraries so that isn't 
usually possible.  For Poly/ML built with --enable-shared, static 
linking of the Poly/ML library but not its dependencies is possible, e.g.


  gcc file.o \
-Wl,-Bstatic \
-L/tmp/polyml/lib -lpolymain -lpolyml \
-Wl,-Bdynamic \
-lpthread -lffi -lgmp -lm -ldl -lstdc++ -lgcc_s -lgcc

but `pkg-config --static ...` can't produce such commands.  Such a 
command could be produced with some shell trickery to get static-only 
dependencies, so perhaps it is worth supporting --static.


Finally, I note that libffi has its own PC file, so when Poly/ML is 
built with --with-system-libffi, instead of adding -lffi to 
Libs/Libs.private, libffi could be added to Requires/Requires.private, 
respectively.


Phil


On 18/12/17 15:47, David Matthews wrote:

Phil,
I'm not exactly clear how pkg-config is supposed to be used.  It's 
certainly possible to add -lpolymain explicitly to the libraries in 
polyml.pc.


David

On 17/12/2017 21:57, Phil Clayton wrote:

David,

On Fedora 25, polyc still appears to work for shared poly with this 
change.  However, there is an issue for pkg-config because the libs 
section in polyml.pc no longer includes the flag -lpolymain causing a 
link error:


/usr/lib/gcc/x86_64-redhat-linux/6.4.1/../../../../lib64/crt1.o: In 
function `_start':

(.text+0x20): undefined reference to `main'
collect2: error: ld returned 1 exit status

Regards,
Phil

On 12/12/17 13:14, David Matthews wrote:
The polyc script has been developed mainly to simplify the linking of 
an exported ML function and in particular to try to capture the 
libraries that need to be included.  I've been having another look at 
this because of an issue that was reported a while back.  Up till now 
the linking step has included all the libraries that were needed in 
order to link libpolyml itself.  That was extracted by the configure 
script.  It turns out that this is right if libpolyml is compiled as 
a static library but has a problem if libpolyml is a dynamic library.


Object files exported by PolyML.export make reference to external 
symbols from libpolyml but do not directly reference anything else. 
If libpolyml is a dynamic library it exports these symbols but all 
the other dependencies are satisfied by loading the appropriate 
libraries dynamically.


The issue was reported in the Fedora distribution but may also affect 
other distributions that package up Poly/ML and have separate 
packages for libraries (e.g. libgmp and libffi) and development 
packages.  They were building libpolyml as a shared library but 
because polyc included the dependencies of libpolyml itself polyc was 
including -lgmp -lffi in the link step.  This meant that it needed 
the development versions of these libraries even though they were not 
actually used.


I've now modified the configure script so that polyc only includes 
the dependent libraries if libpolyml has been built with shared 
libraries disabled and at the same time changed the default so that 
it builds a shared library unless --disable-shared is given.  
Hopefully this hasn't broken anything but I'd appreciate any reports 
of problems.



David
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Retiring CInterface?

[Phil Clayton]

I can't think of a need for CInterface.  It is probably only worth 
retaining while the FFI documentation is for CInterface.  On that note, 
it may be worth directing readers to using Foreign instead of 
CInterface: the link to the foreign function interface on the main 
documentation page

http://www.polyml.org/Doc.html
is all about CInterface.

Phil

On 12/12/17 13:16, David Matthews wrote:
Now that the Foreign structure has been around for a while I was 
wondering whether it was time to remove CInterface and the related 
structures.  Is there any specific need to keep it?


David

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] polyc and libraries

[Phil Clayton]

David,

On Fedora 25, polyc still appears to work for shared poly with this 
change.  However, there is an issue for pkg-config because the libs 
section in polyml.pc no longer includes the flag -lpolymain causing a 
link error:


/usr/lib/gcc/x86_64-redhat-linux/6.4.1/../../../../lib64/crt1.o: In 
function `_start':

(.text+0x20): undefined reference to `main'
collect2: error: ld returned 1 exit status

Regards,
Phil

On 12/12/17 13:14, David Matthews wrote:
The polyc script has been developed mainly to simplify the linking of an 
exported ML function and in particular to try to capture the libraries 
that need to be included.  I've been having another look at this because 
of an issue that was reported a while back.  Up till now the linking 
step has included all the libraries that were needed in order to link 
libpolyml itself.  That was extracted by the configure script.  It turns 
out that this is right if libpolyml is compiled as a static library but 
has a problem if libpolyml is a dynamic library.


Object files exported by PolyML.export make reference to external 
symbols from libpolyml but do not directly reference anything else.  If 
libpolyml is a dynamic library it exports these symbols but all the 
other dependencies are satisfied by loading the appropriate libraries 
dynamically.


The issue was reported in the Fedora distribution but may also affect 
other distributions that package up Poly/ML and have separate packages 
for libraries (e.g. libgmp and libffi) and development packages.  They 
were building libpolyml as a shared library but because polyc included 
the dependencies of libpolyml itself polyc was including -lgmp -lffi in 
the link step.  This meant that it needed the development versions of 
these libraries even though they were not actually used.


I've now modified the configure script so that polyc only includes the 
dependent libraries if libpolyml has been built with shared libraries 
disabled and at the same time changed the default so that it builds a 
shared library unless --disable-shared is given.  Hopefully this hasn't 
broken anything but I'd appreciate any reports of problems.



David
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Approaching release of 5.7.1

[Phil Clayton]

David,

As Rob says, I am using Linux (4.13.12-100.fc25.x86_64 from Fedora 25 
updates).


I have tried the updated version (ga24f39a) and this fixes the issue. 
ProofPower builds in the expected time.  However, I have tried a few 
more tests and find that some compiled applications are very delayed on 
exit.  In the simplest Hello World GTK application, if it is open for 
more than about 3 s before being closed, it will take at least 43 s to 
close.  (I assume that is terminated due to the crow-bar thread.) 
Oddly, another Hello World GTK demo (based on GApplication) doesn't 
exhibit this behaviour.


I agree that it is a bit late in the release cycle to address this and 
don't see the half second delay on exit being particularly problematic 
generally.


Regards,
Phil

On 25/11/17 17:44, David Matthews wrote:

Rob,
I've had a better look and I found that I was seeing this as well.  I've 
pushed a fix and it no longer seems to be doing it.  It's a very small 
change so I would be very surprised if it has broken anything but I'll 
give it a couple of days and then release 5.7.1.


Regards,
David

On 25/11/2017 16:44, Rob Arthan wrote:

David,

Knowing Phil he will be using some version of Linux, but I see similar 
results on Mac OS:

E.g., on Mac OS High Sierra 10.13.1:

rda]- echo | time /usr/local/poly/5.7-inf/bin/poly
Poly/ML 5.7 Release
 0.00 real 0.00 user 0.00 sys
rda]- echo | time /usr/local/poly/5.7.1-inf/bin/poly
Poly/ML 5.7.1 Release (Git version v5.7-290-g44b7b88e)
 0.40 real 0.00 user 0.00 sys

Over repeated experiments, I see occasional upwards blips in the real 
time for 5.7,

but 5.7.1 sticks doggedly to about 0.4 seconds.

Regards,

Rob.


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Approaching release of 5.7.1

[Phil Clayton]

I have just realized what is probably accounting for the delay below.  I 
have noticed recently that there is a slight delay when exiting the poly 
session.


  echo | time poly

gives 0.49 s elapsed time on my machine.  After a build of ProofPower 
there are 262 SML files and most are processed in separate poly sessions 
that update the saved the state.  That would give an expected delay of 
at most


  262 * 0.49 s
=
  128 s

which is not far off the 117 s extra delay below.  I think that explains it.

Phil

On 23/11/17 19:46, Phil Clayton wrote:

David,

That also fixed the issue for me.

I have been using the latest commit (g44b7b88) without issue.  My only 
observation is that there is a significant increase in the ProofPower 
build times:


Poly/ML 5.7

real    1m37.832s
user    1m33.262s
sys    0m15.108s


Poly/ML 5.7.1g44b7b88

real    3m34.839s
user    1m38.777s
sys    0m19.593s

I have kept all other things equal: the only change is the version of 
Poly/ML.  This suggests that Poly/ML is waiting for something. 
Unfortunately I haven't had time to investigate this.


Regards,
Phil

On 13/11/17 20:47, David Matthews wrote:

Rob,
Thank you for putting up with this.  We're gradually making progress. 
I've pushed a further change and this example now seems to work.  I 
didn't actually get that assertion fault but something similar.


Regards,
David

On 13/11/2017 16:32, Rob Arthan wrote:

David,

Thanks again, but I've got two ProofPower source files further on and 
then I get a different assertion failure:


Assertion failed: (val.AsAddress() > descr->originalAddress && 
val.AsAddress() <= (char*)descr->originalAddress + 
descr->segmentSize), function RelocateAddressAt, file savestate.cpp, 
line 929.


I've attached a tarball with the evidence. This time it doesn't seem 
to be deterministic, sometimes it

gets further than others.

Regards,

Rob.

On 13 Nov 2017, at 13:33, David Matthews 
 wrote:


Thanks, both of you for your contributions.  I've had another look 
at it and I've applied another fix.  The problem was really that it 
was reading beyond the end of an array which meant that whether and 
how it failed depended on the values it found.  Hopefully the latest 
fix (e968c38) will solve it but let me know if there are still 
problems.


Regards,
David

On 13/11/2017 09:12, Phil Clayton wrote:

David,
I also get a failure building ProofPower but not the same as Rob:
pp-ml: savestate.cpp:881: void 
LoadRelocate::AddTreeRange(SpaceBTree**, unsigned int, uintptr_t, 
uintptr_t): Assertion `s >= r && s <= 256' failed.
This is on a Linux x86_64 machine and occurs with commit 524fe72 (I 
haven't tested 04d3c95).  Rob's second example (20171112) should 
reproduce this but doesn't.  I modified the example as attached to 
use a single session and it gives the following error message but I 
don't know if this error is related:
pp-ml: gc_mark_phase.cpp:743: void CheckMarksOnCodeTask(GCTaskId*, 
void*, void*): Assertion `obj->ContainsNormalLengthWord()' failed.

Regards,
Phil
On 12/11/17 19:21, Rob Arthan wrote:

David,

Thanks. Unfortunately, after pulling your fix, I get the same 
assertion failure 2 files further
on in the ProofPower build. The attached tarball contains files 
similar to the ones I sent

yesterday to exhibit the problem.

Regards,

Rob.

On 12 Nov 2017, at 15:41, David Matthews 
 wrote:


Rob,
Thanks for doing that.  I've pushed a commit that seems to have 
fixed it.

Regards,
David

On 11/11/2017 18:47, Rob Arthan wrote:

David,
On 8 Nov 2017, at 14:10, David Matthews 
 wrote:


We are approaching the point at which the current version of 
Git master is ready for release as Poly/ML 5.7.1.  Version 5.7 
introduced a number of significant changes and it has taken 
quite a bit of work since then to fix various bugs and sort out 
performance issues.  I've been working with Makarius on dealing 
with those that affect Isabelle and we now seem to have dealt 
with everything.  I'd like to ask everyone to try out the 
current version and let me know if there is anything that would 
stand in the way of a release.

The ProofPower build fails with an assertion failure:
Assertion failed: (t->tree[r] == 0), function AddTreeRange, file 
savestate.cpp, line 896.
This is on Mac OS Sierra 10.12.6 with Poly/ML version 
v5.7-283-g04d3c95 .
I haven't tried any other OSs.  I presume this is happening 
where my main program calls

PolyML.SaveState.loadState.
I've attached a tarball of a cut-down set of source files that 
exhibits the problem
together with a shell script that simulates what the ProofPower 
make file does.

Regards,
Rob.

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml








___
polyml mailing list
polyml@inf.ed.ac.uk
h

Re: [polyml] Approaching release of 5.7.1

[Phil Clayton]

David,

That also fixed the issue for me.

I have been using the latest commit (g44b7b88) without issue.  My only 
observation is that there is a significant increase in the ProofPower 
build times:


Poly/ML 5.7

real1m37.832s
user1m33.262s
sys 0m15.108s


Poly/ML 5.7.1g44b7b88

real3m34.839s
user1m38.777s
sys 0m19.593s

I have kept all other things equal: the only change is the version of 
Poly/ML.  This suggests that Poly/ML is waiting for something. 
Unfortunately I haven't had time to investigate this.


Regards,
Phil

On 13/11/17 20:47, David Matthews wrote:

Rob,
Thank you for putting up with this.  We're gradually making progress. 
I've pushed a further change and this example now seems to work.  I 
didn't actually get that assertion fault but something similar.


Regards,
David

On 13/11/2017 16:32, Rob Arthan wrote:

David,

Thanks again, but I've got two ProofPower source files further on and 
then I get a different assertion failure:


Assertion failed: (val.AsAddress() > descr->originalAddress && 
val.AsAddress() <= (char*)descr->originalAddress + 
descr->segmentSize), function RelocateAddressAt, file savestate.cpp, 
line 929.


I've attached a tarball with the evidence. This time it doesn't seem 
to be deterministic, sometimes it

gets further than others.

Regards,

Rob.

On 13 Nov 2017, at 13:33, David Matthews 
 wrote:


Thanks, both of you for your contributions.  I've had another look at 
it and I've applied another fix.  The problem was really that it was 
reading beyond the end of an array which meant that whether and how 
it failed depended on the values it found.  Hopefully the latest fix 
(e968c38) will solve it but let me know if there are still problems.


Regards,
David

On 13/11/2017 09:12, Phil Clayton wrote:

David,
I also get a failure building ProofPower but not the same as Rob:
pp-ml: savestate.cpp:881: void 
LoadRelocate::AddTreeRange(SpaceBTree**, unsigned int, uintptr_t, 
uintptr_t): Assertion `s >= r && s <= 256' failed.
This is on a Linux x86_64 machine and occurs with commit 524fe72 (I 
haven't tested 04d3c95).  Rob's second example (20171112) should 
reproduce this but doesn't.  I modified the example as attached to 
use a single session and it gives the following error message but I 
don't know if this error is related:
pp-ml: gc_mark_phase.cpp:743: void CheckMarksOnCodeTask(GCTaskId*, 
void*, void*): Assertion `obj->ContainsNormalLengthWord()' failed.

Regards,
Phil
On 12/11/17 19:21, Rob Arthan wrote:

David,

Thanks. Unfortunately, after pulling your fix, I get the same 
assertion failure 2 files further
on in the ProofPower build. The attached tarball contains files 
similar to the ones I sent

yesterday to exhibit the problem.

Regards,

Rob.

On 12 Nov 2017, at 15:41, David Matthews 
 wrote:


Rob,
Thanks for doing that.  I've pushed a commit that seems to have 
fixed it.

Regards,
David

On 11/11/2017 18:47, Rob Arthan wrote:

David,
On 8 Nov 2017, at 14:10, David Matthews 
 wrote:


We are approaching the point at which the current version of Git 
master is ready for release as Poly/ML 5.7.1.  Version 5.7 
introduced a number of significant changes and it has taken 
quite a bit of work since then to fix various bugs and sort out 
performance issues.  I've been working with Makarius on dealing 
with those that affect Isabelle and we now seem to have dealt 
with everything.  I'd like to ask everyone to try out the 
current version and let me know if there is anything that would 
stand in the way of a release.

The ProofPower build fails with an assertion failure:
Assertion failed: (t->tree[r] == 0), function AddTreeRange, file 
savestate.cpp, line 896.
This is on Mac OS Sierra 10.12.6 with Poly/ML version 
v5.7-283-g04d3c95 .
I haven't tried any other OSs.  I presume this is happening where 
my main program calls

PolyML.SaveState.loadState.
I've attached a tarball of a cut-down set of source files that 
exhibits the problem
together with a shell script that simulates what the ProofPower 
make file does.

Regards,
Rob.

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml








___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml









___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
pol

Re: [polyml] Approaching release of 5.7.1

[Phil Clayton]

David,

I also get a failure building ProofPower but not the same as Rob:

pp-ml: savestate.cpp:881: void LoadRelocate::AddTreeRange(SpaceBTree**, 
unsigned int, uintptr_t, uintptr_t): Assertion `s >= r && s <= 256' failed.


This is on a Linux x86_64 machine and occurs with commit 524fe72 (I 
haven't tested 04d3c95).  Rob's second example (20171112) should 
reproduce this but doesn't.  I modified the example as attached to use a 
single session and it gives the following error message but I don't know 
if this error is related:


pp-ml: gc_mark_phase.cpp:743: void CheckMarksOnCodeTask(GCTaskId*, 
void*, void*): Assertion `obj->ContainsNormalLengthWord()' failed.


Regards,
Phil

On 12/11/17 19:21, Rob Arthan wrote:

David,

Thanks. Unfortunately, after pulling your fix, I get the same assertion failure 
2 files further
on in the ProofPower build. The attached tarball contains files similar to the 
ones I sent
yesterday to exhibit the problem.

Regards,

Rob.


On 12 Nov 2017, at 15:41, David Matthews  wrote:

Rob,
Thanks for doing that.  I've pushed a commit that seems to have fixed it.
Regards,
David

On 11/11/2017 18:47, Rob Arthan wrote:

David,

On 8 Nov 2017, at 14:10, David Matthews  wrote:

We are approaching the point at which the current version of Git master is 
ready for release as Poly/ML 5.7.1.  Version 5.7 introduced a number of 
significant changes and it has taken quite a bit of work since then to fix 
various bugs and sort out performance issues.  I've been working with Makarius 
on dealing with those that affect Isabelle and we now seem to have dealt with 
everything.  I'd like to ask everyone to try out the current version and let me 
know if there is anything that would stand in the way of a release.

The ProofPower build fails with an assertion failure:
Assertion failed: (t->tree[r] == 0), function AddTreeRange, file savestate.cpp, 
line 896.
This is on Mac OS Sierra 10.12.6 with Poly/ML version v5.7-283-g04d3c95 .
I haven't tried any other OSs.  I presume this is happening where my main 
program calls
PolyML.SaveState.loadState.
I've attached a tarball of a cut-down set of source files that exhibits the 
problem
together with a shell script that simulates what the ProofPower make file does.
Regards,
Rob.

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml








___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml



load-state-problem-pbc1.tar.gz
Description: application/gzip
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] semantics of SaveState.loadState

[Phil Clayton]

You are loading the state into the new executable a.out which is not the 
same as the executable poly used to save the state.  If you save the 
state from a.out, you should be ok, e.g


bar.ML

fun die s = (TextIO.output(TextIO.stdErr, s ^ "\n");
 OS.Process.exit OS.Process.failure)

datatype cmd = Save | Load

fun main() =
  let
val (cmd, s,file) = case CommandLine.arguments() of
   ["save",s,file] => (Save,s,file)
 | ["load",s,file] => (Load,s,file)
 | _ => die ("Usage:\n  "^CommandLine.name() ^
 " [save|load] state file")
  in
case cmd of
  Save => (
PolyML.use file;
PolyML.SaveState.saveState s;
print "Saved state successfully\n"
  )
| Load => (
PolyML.SaveState.loadState s;
print "Loaded state successfully\n";
PolyML.use file
  )
  end


$ polyc bar.ML
$ echo "val x = ref 10;" > file1.sml
$ echo 'print ("!x = " ^ Int.toString (!x) ^ "\n");' > file2.sml
$ ./a.out save foo file1.sml
$ ./a.out load foo file2.sml

Phil
On 31/08/17 00:32, michael.norr...@data61.csiro.au wrote:

The state is being saved from “bare” poly, and being reloaded into the same 
environment (no complicated chains of states in my example).  “Silently crash” 
means exits without any output, even though the … section of my code includes 
calls to print.

Here is a simple example:

First:

 $ echo "val x = ref 10; PolyML.SaveState.saveState \"foo\";" | poly

generating my state file “foo”.

Then I write bar.ML:


fun die s = (TextIO.output(TextIO.stdErr, s ^ "\n");
  OS.Process.exit OS.Process.failure)

fun write_to_file f =
   let
 val ostrm = TextIO.openOut f
   in
 TextIO.output(ostrm, "(* this is a file *)\n");
 TextIO.closeOut ostrm
   end

fun main() =
   let
 val (s,file) = case CommandLine.arguments() of
[s,file] => (s,file)
  | _ => die ("Usage:\n  "^CommandLine.name() ^
  " state file")
   in
 PolyML.SaveState.loadState s;
 print "Switched state successfully\n";
 write_to_file file;
 PolyML.use file
   end


Then I compile with polyc:

$ polyc bar.ML

Then I try running a.out

$ ./a.out foo usefile

I get no output, an exit code of 1 and usefile hasn’t been created.

This is on macos (uname says “Darwin Kernel Version 16.7.0”), and with Poly/ML 
5.6 Release.

Michael


On 30/8/17, 22:33, "David Matthews"  wrote:

 How exactly are you saving the state you want to load?  The problem is
 that you can only load a saved state into the same executable as you
 used to save it.  The ultimate reason for this restriction is that the
 saved state does not save any heap cells that are present in the
 executable but instead saves their (relative) addresses.  loadState will
 raise an exception if the saved state does not match the executable.
 
 By "silently crash" do you mean that it raises an exception that you are

 not handling or is this something else?
 
 David
 
 On 30/08/2017 13:10, michael.norr...@data61.csiro.au wrote:

 > If I have a program I’d like to compile with polyc that looks like
 >
 >
 > fun main () =
 >   let
 > val _ = PolyML.SaveState.loadState (hd (CommandLine.arguments()))
 >   in
 > …
 >   end
 >
 > what, if anything can I put in the … and have it work?
 >
 > All I really want is what is effectively a sequence of calls to “use” in 
that slot, but there seem to be many ways of generating executables that silently 
crash.
 >
 > Michael
 >
 > ___
 > polyml mailing list
 > polyml@inf.ed.ac.uk
 > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
 >
 


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Different behaviors between SML/NJ and Poly/ML in a code from 'The Little MLer'

[Phil Clayton]

On 05/07/17 19:27, Makarius wrote:

On 05/07/17 18:57, Roní Gonçalves wrote:


In Fedora 25 I am stuck with Poly/ML 5.6 as well as in Ubuntu 16.04.
Fortunately, in Fedora 26, there will be Poly/ML 5.7


It is actually quite easy to compile Poly/ML from sources.

I do this routinely for anything that is sufficiently important for me
and not one of the big standard packages that are used by millions of
users and properly maintained.


You are in no way stuck with Poly/ML 5.6 on Fedora 25...  To install 
your own version, you would remove the package:


  dnf erase polyml

Then prevent the package from returning by adding 'polyml' to the line 
starting 'exclude=' in /etc/dnf/dnf.conf .  For example, mine says:


  exclude=polyml,mlton,ocaml

You could do the same for the package polyml-libs but I wouldn't on 
principle because another package could depend on that.  Instead, I 
would install to a non-default location (e.g. /opt/polyml/polyml-5.7) to 
avoid clashing with the polyml-libs package as follows:


  ./configure --prefix=/opt/polyml/polyml-5.7
  make
  su -c 'make install'

In ~/.bash_profile add the following line to make this version of 
Poly/ML available in your shell (after subsequent login):


  PATH=$PATH:/opt/polyml/polyml-5.7/bin

Phil

P.S. If you are using the linker directly you may also want to add the 
following lines to ~/.bash_profile :


  LD_LIBRARY_PATH=/opt/polyml/polyml-5.7/lib:$LD_LIBRARY_PATH
  PKG_CONFIG_PATH=/opt/polyml/polyml-5.7/lib/pkgconfig:$PKG_CONFIG_PATH

but you won't need those if you just use polyc to build executables.
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] interfacing object oriented libraries

[Phil Clayton]

For GTK+ the problem is constrained - not surprisingly - because the 
library was designed to make it easy to write bindings for: the library 
is written in C and all the OO machinery is provided in the library. 
So, given an OO library, one approach might be to introduce top-level 
wrapper functions for a class's constructors and methods, and top-level 
accessor functions for a class's members and export those top-level 
functions.  Then you could create bindings like mGTK does.  Hopefully.


Or perhaps you were asking about OO representation on the ML side of the 
binding?


Phil


On 16/02/2017 11:49, Gergely Buday wrote:

Hi,

there are known theoretical difficulties bridging SML code to object
oriented interfaces.

What can be done practically?

mGTK has a description here

https://www.usenix.org/legacy/event/usenix04/tech/freenix/full_papers/larsen
/larsen.pdf

Is there any other way?

- Gergely

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml



___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Can't unify int (*In Basis*) with LargeInt.int ...

[Phil Clayton]

For the MLton FFI, there are ML structures that implement INTEGER/WORD 
for each of the platform-dependent signed/unsigned C types.  The ML int 
can be set by the compiler option -default-type (to Int32, Int64 or 
IntInf) so may not match the platform's C int type.


With Poly/ML conversions, LargeInt variants seem reasonable.

To maximize portability across compilers and platforms, I think a C 
interface would want to use LargeInt.int for numeric parameters on the 
ML side.


Phil

On 10/10/2016 18:45, David Matthews wrote:

I think Mlton uses the same precision for C int and ML int so there
won't be the issue of an overflow exception when passing values from C
to ML.  That's easier to do with a full program compiler than the
incremental compilation of Poly/ML.

David

On 10/10/2016 15:40, Kostirya wrote:

I think it should "to turn these conversions back to use FixedInt.int and
raise an exception".
It's important to preserve full compatibility with MLton, SML/NY, SML#
...

MLton:
val plus = _import "plus": (int * int) -> int;
val r = 0 + plus(1, 2)
val _ = print ( (Int.toString(r) ^ "\n" ) )

New Poly/ML:
val plus = buildCall2 ((getSymbol mylib "plus"), (cInt, cInt), cInt)
val r = 0 + plus(1, 2)
val _ = print ( (LargeInt.toString(r) ^ "\n" ) )

The difference in SML code has already appeared in:

MLton:  val _ = print ( (Int.toString(r) ^ "\n" ) )
PolyML: val _ = print ( (LargeInt.toString(r) ^ "\n" ) )


2016-10-10 16:02 GMT+03:00 David Matthews
:


I noticed this and thought I'd committed a fix but it seems not.  The
issue is that the C "int" type may have, depending on the platform, one
more bit of precision than FixedInt.int in Poly/ML.

Now that the default int in Poly/ML is FixedInt.int that raises a
question
about how to deal with the various conversions (e.g. cInt) that could
return a value that would overflow.  Currently, c(U)Int8 and 16 have
type
"int conversion" and the rest, c(U)Int32/64 and c(U)Int have type
"LargeInt.int conversion".  While this ensures that there will never
be an
overflow when converting C values to ML it does mean there's a mismatch
between C "int" and ML "int".  I'm wondering whether to turn these
conversions back to use FixedInt.int and raise an exception when a value
will not fit and perhaps introduce new conversions (e.g. cIntLarge) to
handle the full range of values.

Does anyone have any comments?
David


On 10/10/2016 13:18, Kostirya wrote:


Hello.
I updated Poly/ML from git (commit
aa7bea141f227ea5d7feaa849763ad53fb4147d3) and found that
mlsource/extra/CInterface/Examples/NewForeignTest.sml is broken:

env LD_LIBRARY_PATH=. poly --script NewForeignTest.sml



(4, 4)
(5, 5)
(12345, ...)
NewForeignTest.sml:133: error: Type error in function application.
   Function: buildClosure1 :
  (int -> unit) * int conversion * unit conversion ->
(int -> unit) closure
   Argument: (fn i => print (Int.toString i), cInt, cVoid) :
  (int -> unit) * LargeInt.int conversion * unit conversion
   Reason:
  Can't unify int (*In Basis*) with LargeInt.int (*In Basis*)
 (Different type constructors)
Found near buildClosure1 (fn i => print (... ...), cInt, cVoid)

Is LargeInt.int a default int type for FFI now?

Nick.



___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

___

polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml



___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Some questions about Foreign

[Phil Clayton]

Hi Kostirya,

On 24/05/2016 09:07, Kostirya wrote:

Hello.

I have some questions about Foreign.

1. How to convert OS.IO.iodesc (from socket) into cUint (uintptr_t)?


The Basis Library docs explain about converting iodesc values and 
portability issues:

http://sml-family.org/Basis/os-io.html#SIG:OS_IO.iodesc:TY

With Poly/ML, if you want to pass an iodesc value to/from a C function 
you probably want to create your own conversion by building on cUint. 
See (untested) code below that creates cIoDescConv.  Note that valOf may 
raise an exception.




2. C function is need 'const struct timespec *timeout' argument.
Where struct timespec is:

struct timespec {
 time_t  tv_sec;
 long tv_nsec;
};

Do I understand correctly that this is
cOptionPtr (cStruct2 (cInt32, cLong))
?

But how can I call this from polyml?
I call as SAME (3, 0) and got error: Exception- Foreign "cOptionPtr must
be applied to a pointer type" raised


You need to use cStar or cConstStar for the dereferencing.  It looks 
like you want

  cConstStar (cStruct2 (cInt32, cLong))
Whether you use cOptionPtr around that depends on whether you want to be 
able to pass a null/non-null pointer for an optional value.


Phil


fun convMap (fromC, toC) conv =
  let
open Foreign
val {ctype, load, store} = breakConversion conv
  in
 makeConversion {
  ctype = ctype,
  load  = fromC o load,
  store = fn (p, x) => store (p, toC x)
}
  end

val cFileDescConv =
  convMap
(
  Posix.FileSys.wordToFD o SysWord.fromInt,
  SysWord.toInt o Posix.FileSys.fdToWord
)
Foreign.cUint

val cIoDescConv =
  convMap
(Posix.FileSys.fdToIOD, valOf o Posix.FileSys.iodToFD)
cFileDescConv

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Assertion `costMin > userGCRatio' failed

[Phil Clayton]

The values were indeed equal and the change to
  ASSERT(costMin >= userGCRatio);
avoids the failure.  I added code to print the values if they are equal 
and we get:

costMin = 0.04943205418749
userGCRatio = 0.04943205418749
which is the nearest value to 1/9 for a double.

In case you're wondering which commit introduces the regression, it was 
d0815825.  The previous commit 3ca17b4b does not show this problem.  I 
looked at the log for just libpolyml/heapsizing.cpp and this change 
seemed the best candidate and got lucky.


Phil


On 28/01/2016 12:02, David Matthews wrote:

Phil,

On 27/01/2016 19:52, Phil Clayton wrote:

I am getting the following assertion failure with Poly/ML 5.6:

eg_test: heapsizing.cpp:602: bool
HeapSizeParameters::getCostAndSize(POLYUNSIGNED&, double&, bool):
Assertion `costMin > userGCRatio' failed.

To get some timing stats, I was running a test application repeatedly to
take an average time.  It would appear that the sooner I re-run the
application after the previous run has terminated, the more likely the
above failure is to occur.  There is no failure when I run the test once
per second manually.  Running the test application in quick succession
using the command
   ./eg_test ; ./eg_test
gives the failure every 3 to 4 invocations.  Is there more information I
can provide?

Poly/ML 5.5.2 doesn't exhibit this issue.


This is very strange.  The only thing I can think of is that the system
is taking time to free up memory released when the previous run completes.

I've looked at the code and there haven't been any real changes in that
area.  It would be helpful to have some sort of idea which commit starts
to show the problem.  Could you check whether it fails if you change the
assertion to:
ASSERT(costMin >= userGCRatio);
The test before is "cost < userGCRatio" so it is possible that it's
exactly equal.  These are doubles so the chances are low.

Regards,
David
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

[polyml] Assertion `costMin > userGCRatio' failed

[Phil Clayton]

I am getting the following assertion failure with Poly/ML 5.6:

eg_test: heapsizing.cpp:602: bool 
HeapSizeParameters::getCostAndSize(POLYUNSIGNED&, double&, bool): 
Assertion `costMin > userGCRatio' failed.


To get some timing stats, I was running a test application repeatedly to 
take an average time.  It would appear that the sooner I re-run the 
application after the previous run has terminated, the more likely the 
above failure is to occur.  There is no failure when I run the test once 
per second manually.  Running the test application in quick succession 
using the command

  ./eg_test ; ./eg_test
gives the failure every 3 to 4 invocations.  Is there more information I 
can provide?


Poly/ML 5.5.2 doesn't exhibit this issue.

Phil
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Changes to Foreign structure

[Phil Clayton]

On 13/01/2016 14:25, Phil Clayton wrote:

I've started using the Foreign structure and it seems to be working well
in tests.  (It will probably be a week until I can test it with larger
applications though.)


I've replaced all use of the old CInterface structure by Foreign in a 
large library and so far test applications are all working as before. 
I'm glad to see the back of vols.  I don't have any timing measurements, 
so can't comment on improvements there.


Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Foreign calls not working after loadState in new session

[Phil Clayton]

David,

On 19/01/2016 19:14, David Matthews wrote:

Phil,

On 19/01/2016 18:38, Phil Clayton wrote:

After loading an existing state in a fresh session, I find that
previously defined calls to C functions (saved in the state) crash the
session if (and only if) the foreign call was called in an earlier
session before the state was saved.  I can supply an example if
necessary.

After investigating, it is actually malloc that is failing in the calls.
  Surprisingly, the very first malloc in the session finds an existing
address.  As freeList is emptied by PolyML.onEntry presumably freeList
is being restored by loadState.  Does that sound like an issue?  I would
expect that the freeList state is untouched by loadState.


I think you're right.  It looks as though freeList is an ordinary ref.
It should be a special ref that isn't set by loading the state.  These
are used in the basis library particular for IO streams.  I've just
pushed that change to a new branch - No-overwrite-test.  Could you check
if that fixes the problem?


Thanks for the quick patch - that fixes it.  Also, I modified my version 
with diagnostic messages and now see the expected messages from malloc.


Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

[polyml] Foreign calls not working after loadState in new session

[Phil Clayton]

After loading an existing state in a fresh session, I find that 
previously defined calls to C functions (saved in the state) crash the 
session if (and only if) the foreign call was called in an earlier 
session before the state was saved.  I can supply an example if necessary.


After investigating, it is actually malloc that is failing in the calls. 
 Surprisingly, the very first malloc in the session finds an existing 
address.  As freeList is emptied by PolyML.onEntry presumably freeList 
is being restored by loadState.  Does that sound like an issue?  I would 
expect that the freeList state is untouched by loadState.


Phil
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Negative offset for getX and setX functions in Foreign.Memory

[Phil Clayton]

On 16/01/2016 08:51, David Matthews wrote:

On 15/01/2016 16:13, Phil Clayton wrote:

The functions getX and setX in Foreign.Memory take an offset as a
Word.word.  I'm finding that it is possible to have a negative offset by
negating the word offset, e.g.
   get8 (p, ~ 0w1)
Is that guaranteed work generally?

Given that
   Word.wordSize = 63
   SysWord.wordSize = 64
I wouldn't have expected this to work for get8/set8 but it does.

Phil

P.S. My efforts to inspect the source didn't get far as these functions
go straight to run-time calls and I'm not familiar with internal
representations in Poly/ML...


The intention is that they should work correctly for negative offsets.
It seemed more useful that way.  Word.toIntX does imply that the basis
library understands signed word values.


Yes - the getX/setX operations are more useful by allowing negative 
offsets.  Unfortunately, the word offset can be viewed in an unsigned 
way.  I would suggest e.g.

  getX : voidStar * int -> Word8.word
unless use of an int introduces more overhead.

Certainly the Basis Library understands sign extension of words.  If the 
Word.word offset is signed extended to a SysWord.word (the underlying 
pointer representation) then I see no problem.




Currently these functions end up in the assembly code, in the case of
getX as cmem_load_asm_8, where it uses an arithmetic shift to detag. I'm
currently working on incorporating them into the code-generator which
will much improve efficiency but that will have to wait for the next
release.


Good to know, thanks.

Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

[polyml] Negative offset for getX and setX functions in Foreign.Memory

[Phil Clayton]

The functions getX and setX in Foreign.Memory take an offset as a 
Word.word.  I'm finding that it is possible to have a negative offset by 
negating the word offset, e.g.

  get8 (p, ~ 0w1)
Is that guaranteed work generally?

Given that
  Word.wordSize = 63
  SysWord.wordSize = 64
I wouldn't have expected this to work for get8/set8 but it does.

Phil

P.S. My efforts to inspect the source didn't get far as these functions 
go straight to run-time calls and I'm not familiar with internal 
representations in Poly/ML...

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Changes to Foreign structure

[Phil Clayton]

I've started using the Foreign structure and it seems to be working well 
in tests.  (It will probably be a week until I can test it with larger 
applications though.)  My comments below are just for interest, nothing 
significant to report.


I have a minor comment about the type of the store function in conversions:
  Memory.voidStar * 'a -> unit -> unit
Every time I used a store function, I found that it would be more 
convenient to have

  'a -> Memory.voidStar -> unit -> unit
There were two reasons:
 1. To easily compose store functions, e.g.
  val cX : x conversion =
makeConversion {
  load  = toX o load,
  store = store o fromX,  <--- not valid
  ctype = ctype
}
 2. To apply just the value being stored to get a type that contains no 
type variables, e.g.

  storeInt 3 : Memory.voidStar -> unit -> unit

I'm not actually using Foreign directly but via a module PolyMLFFI to 
provide a suitable interface.  This gives a type-safe interface for 
creating calls, callback closures and struct conversions without using 
an infinite family of functions for each, e.g.

  open PolyMLFFI
  val aCall = call aSym (cInt &&> cInt --> cDouble)
The "price to pay" for this is that arguments or struct fields are 
joined using an infix pair constructor in ML, e.g.

  aCall (2 & 3)
(This would be nicer if SML allowed user-defined infix type constructors...)
This module also provides a low-level interface that is slightly 
higher-level than Foreign.LowLevel because it takes care of storing the 
arguments in memory.  This can be used with the ctype, load and store 
components of a conversion, e.g.

  fun f m n =
LowLevel.call fSym
  [cTypeInt,   cTypeInt]   cTypeInt
  [storeInt m, storeInt n] loadInt

I've attached this interface module, PolyMLFFI, in case it is useful to 
anyone.  Also, I am interested in any comments, particularly regarding 
efficiency.  (Currently it doesn't support cStar because updateC and 
updateML fields are not exposed by Foreign.  It could be updated but I 
didn't need those.)


Phil


On 16/12/2015 12:35, David Matthews wrote:

There have been a few changes to the Foreign structure.  The callN
functions have been renamed as buildCallN and the way functions are
passed as arguments has been changed.

The reason for the changes is to make clear that the expensive
operations are creating the C functions and closures and that calling a
C function or passing a constructed closure are comparatively cheap.

It is important to call the buildXXX functions at the top-level e.g. in
a structure, so that the C function is created once.  The old callN
functions were curried and it wasn't apparent that the partial
application to the conversions was quite different to the application of
this to the arguments.  For that reason the buildXXX take a tuple.

David

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml






PolyMLFFI.tar.gz
Description: GNU Zip compressed data
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Using a common CIF for callbacks

[Phil Clayton]

On 11/01/2016 12:10, David Matthews wrote:

On 11/01/2016 08:34, Phil Clayton wrote:

I notice that the buildClosurewithAbi functions take the SML function
to call back to in the same tuple as the type of the callback arguments
and return value.  Consequently the interface for constructing closures
using doesn't allow the same CIF to be used for multiple callbacks to
different SML functions (of the same type).  Is that deliberate or could
there be some advantage in allowing that?


For the X86 at least; I can't say for the other architectures; the CIF
is very simple, consisting really of the types and a few flags.  I had
expected that there would be some code there but there isn't.  The
complicated part is when the closure is actually built and this involves
allocating memory with mmap so that it can be executable and building
the code that is passed as the C function.  There's little to be gained
from reusing the CIF.


I looked at the code for FFI runtime call 55 (create a CIF) and there's 
not a huge amount in there so it's not much overhead.  I couldn't see 
where the memory allocated for a CIF is freed though.  (Probably not an 
issue as the number of callback functions in an application is likely to 
bounded, assuming that they are built only once by correct use of 
buildClosure.)


I have an interface where the CIF can be reused and was concerned that 
doing so would be problematic, given that Foreign doesn't allow this. 
It sounds like that isn't a problem though.




More importantly I wanted to steer users away from trying to create
closures on-the-fly because of the cost.  Before the recent change to
use "buildClosureN" the calling mechanism implied that it was possible
to define a function that took, say an integer and an ML function, and
that the cost of passing the integer and the function were similar.  In
practice that's not the case.  They're only similar if the ML function
has already been wrapped as a C closure.


Yes, I see, hence the type 'a closure to represent a function whose 
closure has been constructed.




I have a long-term plan to turn the buildCallN and buildClosureN
functions into something that is almost a mini-compiler that will
produce an interface function when it is applied.  It may only be
possible to do that in certain cases and fall back to libffi in the
other cases.  It's complicated because there are different ABIs for the
various combinations of X86-32/X86-64 and Unix/Windows.


Interesting - is that to make the FFI faster?  I wonder if the 
experiences of MLton would be useful for creating such an interface.


Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

[polyml] Type inference issue using signature constraint

[Phil Clayton]

I have an example where a module is type checking fine even though I 
have introduced a type error into it!  I've reduced it down to a small 
example.  It looks like there is a problem using type constraints from a 
signature where the signature is also required to resolve record 
components.  See attached example for details.


Phil


polyml_compiler_issue-20160112-1.sml.gz
Description: GNU Zip compressed data
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

[polyml] Using a common CIF for callbacks

[Phil Clayton]

I notice that the buildClosurewithAbi functions take the SML function 
to call back to in the same tuple as the type of the callback arguments 
and return value.  Consequently the interface for constructing closures 
using doesn't allow the same CIF to be used for multiple callbacks to 
different SML functions (of the same type).  Is that deliberate or could 
there be some advantage in allowing that?


For example, we could have:

val buildClosure2withAbi:
  LibFFI.abi * ('a conversion * 'b conversion) * 'c conversion ->
  ('a * 'b -> 'c) ->
  ('a * 'b -> 'c) closure

fun buildClosure2withAbi
  (
abi: abi,
(arg1Conv: 'a conversion, arg2Conv: 'b conversion),
resConv: 'c conversion
  )
: ('a * 'b -> 'c) -> ('a * 'b -> 'c) closure =
let
fun callback f (args, res) = ...

val argTypes = [#ctype arg1Conv, #ctype arg2Conv]
and resType = #ctype resConv

val makeCallback = cFunctionWithAbi abi argTypes resType
in
fn f => Memory.memoise (fn () => makeCallback(callback f)) ()
end

Then, at the top-level, an application could define e.g.

  val binOpClosure = buildClosure2 ((cDouble, cDouble), cDouble)
  val addClosure  = binOpClosure Real.+
  val subtractClosure = binOpClosure Real.-
  ...

I don't know enough about libffi to know whether that is useful or would 
be problematic.


Phil


On 16/12/2015 12:35, David Matthews wrote:

There have been a few changes to the Foreign structure.  The callN
functions have been renamed as buildCallN and the way functions are
passed as arguments has been changed.

The reason for the changes is to make clear that the expensive
operations are creating the C functions and closures and that calling a
C function or passing a constructed closure are comparatively cheap.

It is important to call the buildXXX functions at the top-level e.g. in
a structure, so that the C function is created once.  The old callN
functions were curried and it wasn't apparent that the partial
application to the conversions was quite different to the application of
this to the arguments.  For that reason the buildXXX take a tuple.

David

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Changes to Foreign structure

[Phil Clayton]

On 04/01/2016 21:51, David Matthews wrote:

On 04/01/2016 20:39, Phil Clayton wrote:

I've been looking at the new Foreign structure.  It is good to see that
the family of callNretM functions has been eliminated by introducing
cStar.  I've updated a few examples to use the buildCall functions
and they appear to work.

With CInterface, I was avoiding the family of call functions by
implementing a single call function based on call_sym or
call_sym_and_convert.  I am trying to do something equivalent using
Foreign.LowLevel based on the implementation in buildCallwithAbi.
There is a problem: the field "updateML" is not accessible because
   'a conversion
is abstract.  Am I right in thinking "updateML" is required for
conversions involving cStar?  If so, is there a way I can implement my
own variant of a buildCall function?


My thinking was that anyone programming at the level of Foreign.LowLevel
would want to build their own conversions.  I can see it's a problem if
you want to make use of the existing higher level conversions.


In case you're interested in an example of using the conversions, see 
the attached code.  This defines a single 'call' function that avoids a 
family of 'call' functions by taking a function signature that is 
constructed using existing conversions.  For example:


   open Foreign Call
   val f1 = call sym1 (cInt && cInt --> cInt) : (int, int) pair -> int
   val f2 = call sym2 (cFloat --> cInt)   : real -> int
   ...
   ... f1 (2 & 3) : int
   ... f2 Math.e : int

Here, the existing conversions are convenient for capturing the 
characteristics of a C type even when not using the existing 
buildCall functions.  I don't have any objection to creating my own 
conversions - easily done by wrapping existing ones - it would just be 
nice if all the existing ones worked with the above.




Originally "conversion" was completely transparent but it meant that
constructing any new "conversion" required all the functions to be
provided even though most of the time the "update" functions aren't
needed.  I did think about having extended versions of "makeConversion"
and "breakConversion" which would allow the "update" functions to be
included or extracted.  I'd like to keep "conversion" abstract because I
can see that in the future it might be helpful to include extra
functions or fields and having it completely transparent makes it
difficult to provide backwards compatibility.


It take your point about abstraction.  "updateML" and "updateC" seem 
reasonable in concept - they are variants of load and store that are 
applied to the arguments after a call - but perhaps their names could be 
more meaningful.


Hiding the "updateX" functions is not a problem for me.  To avoid the 
family of callNretM functions in CInterface, I already have a framework 
in place for dealing with arguments passed by reference so I don't need 
to use "cStar", though it would have allowed a little more code to be 
shared with MLton.  I could prevent "cStar" from being used accidentally 
by making my own conversion type.




Also - just an observation - in the functions buildCallwithAbi,
couldn't the argument offsets (and the amount of memory to malloc) be
calculated once, rather than for each foreign call?  E.g. in
buildCall2withAbi:

let
 val callF = callwithAbi abi [arg1Type, arg2Type] resType fnAddr
 val arg1Offset = alignUp(#size resType, #align arg1Type)
 val arg2Offset = alignUp(arg1Offset + #size arg1Type, #align
arg2Type)
 val argSize = arg2Offset + #size arg2Type
in
 fn (a, b) =>
 let
 val rMem = malloc argSize
 ...


True.  The idea is that these functions should all be inlined in which
case all these would be compile-time constants.  Making them inlined
means setting maxInlineSize to a very large value while compiling
"basis/Foreign.sml".  The way the basis library is compiled that wasn't
possible until the 5.6 compilers were built.

I'm trying to avoid making any changes in git "master" until the release
is complete but it would certainly be worth doing in the development
version.


Another observation for future consideration: there is no conversion for 
the boolean type.  I believe that the existing CInterface.BOOL is a 
convenience for an int treated as a boolean (indicating a non-zero 
value) and can easily be created as a derived conversion.  It's worth 
noting that C99 has a type "_Bool" (with a macro to refer to it as 
"bool") that "is large enough to store the values 0 and 1".  Depending 
on the platform, I believe that sizeof(_Bool) could be larger than one 
byte, so it could be useful to have a conversion for the _Bool type.


Phil


call.sml.gz
Description: GNU Zip compressed data
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Changes to Foreign structure

[Phil Clayton]

I've been looking at the new Foreign structure.  It is good to see that 
the family of callNretM functions has been eliminated by introducing 
cStar.  I've updated a few examples to use the buildCall functions 
and they appear to work.


With CInterface, I was avoiding the family of call functions by 
implementing a single call function based on call_sym or 
call_sym_and_convert.  I am trying to do something equivalent using 
Foreign.LowLevel based on the implementation in buildCallwithAbi. 
There is a problem: the field "updateML" is not accessible because

  'a conversion
is abstract.  Am I right in thinking "updateML" is required for 
conversions involving cStar?  If so, is there a way I can implement my 
own variant of a buildCall function?


Also - just an observation - in the functions buildCallwithAbi, 
couldn't the argument offsets (and the amount of memory to malloc) be 
calculated once, rather than for each foreign call?  E.g. in 
buildCall2withAbi:


let
val callF = callwithAbi abi [arg1Type, arg2Type] resType fnAddr
val arg1Offset = alignUp(#size resType, #align arg1Type)
val arg2Offset = alignUp(arg1Offset + #size arg1Type, #align arg2Type)
val argSize = arg2Offset + #size arg2Type
in
fn (a, b) =>
let
val rMem = malloc argSize
...

Phil

On 16/12/2015 12:35, David Matthews wrote:

There have been a few changes to the Foreign structure.  The callN
functions have been renamed as buildCallN and the way functions are
passed as arguments has been changed.

The reason for the changes is to make clear that the expensive
operations are creating the C functions and closures and that calling a
C function or passing a constructed closure are comparatively cheap.

It is important to call the buildXXX functions at the top-level e.g. in
a structure, so that the C function is created once.  The old callN
functions were curried and it wasn't apparent that the partial
application to the conversions was quite different to the application of
this to the arguments.  For that reason the buildXXX take a tuple.




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] InternalError: AllocStore found but last allocation not complete

[Phil Clayton]

24/09/15 08:44, David Matthews wrote:

On 22/09/2015 19:00, Phil Clayton wrote:

After integrating the new Finalizable module in a library, I am getting
an internal error from the compiler:

   Exception- InternalError: AllocStore found but last allocation not
complete raised while compiling


Thanks for reporting this and cutting it down to a suitable example.
I've tracked down the problem and committed a fix.


Thanks - this works with the latest commit.



As a shameless plug for the newly updated debugger, I used that to set a
breakpoint on the exception and then it was easy to see what was going
on.  The new debugger is a great deal faster than the old version so
it's perfectly feasible to build the whole compiler with debugging enabled.


I tried the debugger many years ago but it couldn't cope with large 
examples.  I seem to recall that compiling with PolyML.Compiler.debug 
set to true sometimes failed.  I'll give it another go sometime.


I just had a quick look at the tutorial.  How do you exit from the debug 
prompt?  (Ctrl+C didn't work.)




One other point, when trying to cut examples down to the smallest case
that demonstrates a bug, it's worth playing with
PolyML.Compiler.maxInlineSize.  It's often the case that a bug only
shows up when an example is large enough that it isn't inlined so
setting this to something small, e.g. 1, may allow more of the
surrounding code to be pruned away.


That's useful to know.  I checked the latest commit with maxInlineSize 
set to 1 and it still compiles.


I was hopeful that increasing maxInlineSize would provide a work-around 
for 5.5.2.  It does, by setting maxInlineSize to 175, but at the expense 
of much longer compilation times - see the tables below.  Also, the 
executable size of the example is much larger with 5.5.3.  Is that expected?


Phil


The columns below show
 1. PolyML.Compiler.maxInlineSize
 2. real|user|sys times
 3. helloworld executable size


5.5.2

160 fails
170 fails
175 1m14.032s|1m22.092s|0m3.807s290122
180 1m13.523s|1m21.813s|0m3.728s290122
200 1m14.671s|1m23.267s|0m3.684s290122
240 1m15.493s|1m22.855s|0m3.736s290944
320 1m20.699s|1m30.642s|0m4.133s283650


5.5.3 (5dc43ce8e8eaaae7...)

1   0m11.476s|0m13.651s|0m1.470s912681
80  0m18.673s|0m22.754s|0m2.071s882459
120 0m16.855s|0m19.518s|0m1.770s893577
160 0m30.113s|0m39.925s|0m3.004s923681
170 0m30.687s|0m40.661s|0m2.948s923575
175 1m20.665s|1m41.830s|0m5.302s923589
180 1m18.039s|1m34.776s|0m4.183s923589

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] polyc with different base executable

[Phil Clayton]

23/09/15 03:11, Michael Norrish wrote:

Or is there another way of getting what I need?  I'd like to dispense with 
explicit calls in our own code to PolyML.export, and then needing to call the 
linker, but we do want to be able to build heaps in this way, layer by layer.


Have you looked at PolyML.SaveState ?
http://www.polyml.org/documentation/Reference/PolyMLSaveState.html

Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

[polyml] InternalError: AllocStore found but last allocation not complete

[Phil Clayton]

After integrating the new Finalizable module in a library, I am getting 
an internal error from the compiler:


  Exception- InternalError: AllocStore found but last allocation not 
complete raised while compiling


This affects Poly/ML 5.5.2 and the very latest commit with the compiler 
rebuilt (twice).  An example is attached showing this.  I have reduced 
this as far as I can but still a few small library files are required. 
The file 'polyml.sml' is the top-level file that uses the other files.


Regards,
Phil


polyml_compiler_issue-20150922-1.tar.gz
Description: GNU Zip compressed data
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Using a finalizer with multiple arguments

[Phil Clayton]

21/09/15 18:41, David Matthews wrote:

On 21/09/2015 16:08, Phil Clayton wrote:

What I am actually observing is that finalizers are not run on exit for
finalizable values that are in scope in the top-level environment.  On
exit, the REPL has finished, so shouldn't such values be garbage
collected and therefore finalized?


I noticed that but it's very difficult to fix.  The problem is that the
top level environment is an array contained in the executable.  It is
treated as "initialised data" by the linker and loader.  The garbage
collector treats mutable data in the executable as roots for garbage
collection which means it never has to look at the immutable data in the
executable.  The only way I can see of fixing the problem is to copy all
the data, both mutable and immutable, from the executable into the heap.


I see what you mean.  I was thinking only about an interactive/batch 
session.  For an executable, it's not clear that it makes sense to have 
a finalizable value at the top-level.  Already something odd is 
happening: in the attached example toplevel_eg1.sml, the executable has 
a finalizer depending on whether PolyML.fullGC was called when building.




As I wrote that it occurred to me that there might be some way of
processing the current finaliser list during the shut-down process so
that only weak refs that were referenced by other finalisers were
preserved.  This would allow the detection of dependencies, which is
what is really needed at that point.  This would be much cheaper and
could be done instead of the current call to PolyML.fullGC.


This reminded me of a similar discussion a while ago:
http://lists.inf.ed.ac.uk/pipermail/polyml/2012-August/001050.html

Matthew Fluet suggested that just working through finalizers, ignoring 
garbage collection, could break certain invariants.  I think I was only 
in favour of ignoring garbage collection given the limitations of 
setFinal, which don't apply here.  My inclination is to see how we get 
on with iterating PolyML.fullGC on exit.




I've merged the current Finalizer branch into master on github.


I've been testing Finalizable and found a few things.

1.  A finalizer that raises an exception causes the cleaning thread to 
terminate.  Attached patch 0001 handles exceptions from finalizers and 
reports them.


2.  I have an FFI-related test suite for checking finalization that 
produces an output log.  Now that finalizers are called asynchronously, 
the log entries are out of place and the order is not deterministic. 
Even carefully ordering text output and always flushing does not 
entirely solve the problem: writing to stdOut from different threads 
seems to lead to some corruption.  What I needed was a function to 
synchronously run all finalizers (like on exit) in the main thread.  I 
have added a function doGCAndFinalize in the attached patch 0002.  I'm 
not convinced by this patch but it resolves this issue.


3.  For 5.5.2, when finalizeBefore is used, it appears that not all 
finalizers are run by repeatedly calling PolyML.fullGC.  This occurs on 
exit and, with patch 0002 applied, when doGCAndFinalize is called.  See 
attached example test1.sml.gz.  It appears that this has been fixed in 
the current development by commit

  d9ca031dd99161c93ba03c42af396dafbf8c8482
so I mention that just for information.  I have no immediate need for 
finalizeBefore, so this should not hold me up.


Please feel free to mangle/ignore patches as you see fit.

Phil

>From e099235870b48353d3f5b154a70244bc7eafa21a Mon Sep 17 00:00:00 2001
From: Phil Clayton 
Date: Mon, 21 Sep 2015 18:15:34 +0100
Subject: [PATCH 1/2] Handle exceptions from finalizer functions

---
 basis/Finalizable.sml |   14 --
 1 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/basis/Finalizable.sml b/basis/Finalizable.sml
index 8b29794..4d5b1f4 100644
--- a/basis/Finalizable.sml
+++ b/basis/Finalizable.sml
@@ -81,11 +81,21 @@ structure Finalizable :> FINALIZABLE =
 fun swap (a, b) = (b, a)
 
 
+fun reportExn e = (
+  TextIO.output (
+TextIO.stdErr,
+concat["Warning: finalizer raised exception ", exnMessage e, "\n"]
+  );
+  TextIO.flushOut TextIO.stdErr
+) handle _ => ()
+
+fun run f = f () handle e => reportExn e
+
 local
   fun threadFn () = (
 Thread.Mutex.lock Weak.weakLock;
 while true do (
-  app (fn f => f ()) (updatePendingList clean ());
+  app run (updatePendingList clean ());
   Thread.ConditionVar.wait (Weak.weakSignal, Weak.weakLock)
 )
   )
@@ -98,7 +108,7 @@ structure Finalizable :> FINALIZABLE =
 val () = PolyML.fullGC ()  (* PolyML.fullGC is synchronous *)
 val (runNowFns, ps') = clean ((), ps)
   in
-app (fn f => f ()) runNowFns;
+app run runNowFns;
 

Re: [polyml] Using a finalizer with multiple arguments

[Phil Clayton]

19/09/15 13:11, David Matthews wrote:

On 19/09/2015 12:30, Phil Clayton wrote:

Much appreciated.  For now I'd like to get a version working on top of
5.5.2, and I assume assignment will suffice there.  Is there a way to
create a non-overwritable ref in a normal session?  I don't seem to be
able to access LibrarySupport.noOverwriteRef (and these seem to be
needed for cleanAtExit to work).


Are you sure that LibrarySupport.noOverwriteRef is actually required for
the finalisers to be run on exit?  It should only make a difference if
you're saving state.  I've just tried editing basis/Finalizable.sml so
that will compile under 5.5.2-fixes and tested it with a simple example
and it does what I'd expect.


My mistake - it seems I was testing the two versions on slightly 
different examples.


What I am actually observing is that finalizers are not run on exit for 
finalizable values that are in scope in the top-level environment.  On 
exit, the REPL has finished, so shouldn't such values be garbage 
collected and therefore finalized?


Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] FFI overhead

[Phil Clayton]

Poly/ML is using libffi to call C functions.  To determine the FFI 
overhead, you could create an example that just makes the same number of 
calls to empty C functions with the same number of arguments.


To see what happens when a C function is called, look at call_sym 
function in foreign.cpp:

https://github.com/polyml/polyml/blob/master/libpolyml/foreign.cpp#L874
For a C function to improve efficiency, the C function needs to be 
faster by more than the FFI overhead.  I strongly suspect that SML 
functions like IntArray.update take less time than the FFI overhead, so 
no improvement is possible by using C functions.  (I suspect such simple 
SML functions take much less time, so I would expect use of C functions 
to be much slower.)


Phil

P.S. I think that there is scope for efficiency improvement in Poly/ML 
but with some upheaval.  For example, if call_sym first took parameters 
that indicate the types of arguments and the return value, then, for 
each call site, arg_values and arg_types could be created once and the 
call to ffi_prep_cif made once.  Still, the arguments have to be filled 
in on each call:

PolyWord p = arg_list;
for (POLYUNSIGNED i=0; iGet(1));
arg_types[i] = ctypeToFfiType(taskData, 
Head(p).AsObjPtr()->Get(0));

}


19/09/15 16:17, Artella Coding wrote:

Hi, I thought that I would try to speed up the SML code at
http://stackoverflow.com/questions/32425267/how-to-improving-array-benchmark-performance-in-polyml
by using the FFI, but this results in significant slowdown.

Non ffi code :

*
*
*

val size:int = 5;
val loops:int = 30;
val cap:int = 5;

val data = IntArray.array(size,0);

fun loop () =
   let
 fun loopI i =
   if i = size then
 let val _ = () in
   IntArray.update(data,0,IntArray.sub(data,size-1));
   ()
 end
   else
 let val previous = IntArray.sub(data,i-1)
 val use = if previous > cap then 0 else previous in
   IntArray.update(data,i,use+1);
   loopI (i+1)
   end
   in loopI 1 end

fun benchmarkRun () =
   let
 fun bench i =
   if i = loops then ()
   else let val _ = () in
  loop ();
  bench (i+1)
end
   in bench 1 end

fun sum (i,value) =
   if i = size then value
   else sum(i+1,value+Array.sub(data,i))

fun main () = let val _ = () in
   benchmarkRun();
   print (Int.toString (sum (0,0)));
   print "\n"
   end

(*val _ = main ()*)

*
*
*

FFI code :

c code :

*
*
*

//intArray.c
#include 
#include 

typedef struct _intArray {
   int size;
   int* arr;
} intArray;

intArray* createIntArray(int size){
   int i;
   intArray* p = (intArray*) malloc (sizeof(intArray));
   p->arr = (int*) malloc (size*sizeof(int));
   for(i=0; iarr[i] = 0;
   }
   p->size = size;
   return p;
}

void destroyIntArray(intArray* p){
   free (p->arr);
   free (p);
}

void setIntArray(intArray* p, int elem, int val){
   p->arr[elem] = val;
}

int getIntArray(intArray *p, int elem){
   return p->arr[elem];
}

int getSumIntArray(intArray* p){
   int sum = 0;
   int i;
   int size = p->size;
   for(i=0; iarr[i];
   }
   return sum;
}

*
*
*

ml code :

*
*
*

open CInterface;

val lib = load_lib "./intArray.so";
val get = get_sym "./intArray.so";

val PINTARR = POINTER;

val c1 = call1 (get "createIntArray") INT PINTARR
val c2 = call3 (get "setIntArray") (PINTARR,INT,INT) VOID
val c3 = call2 (get "getIntArray") (PINTARR,INT) INT
val c4 = call1 (get "getSumIntArray") (PINTARR) INT

fun c_createIntArray (size) = c1 (size);
fun c_setIntArray (p,elem,value) = c2 (p,elem,value);
fun c_getIntArray (p,elem) = c3 (p,elem);
fun c_getSumIntArray (p) = c4 (p);


val size:int = 5;
val loops:int = 30;
val cap:int = 5;

fun loop (pData2) =
   let
 fun loopI i =
   if i = size then
 let val _ = () in
   c_setIntArray(pData2,0,c_getIntArray(pData2,size-1));
  

Re: [polyml] Using a finalizer with multiple arguments

[Phil Clayton]

18/09/15 17:38, David Matthews wrote:

On 18/09/2015 13:50, Phil Clayton wrote:

The only other changes I'm thinking about are:
1.  Introducing a "touch" primitive for long-term security in case a
future update to the optimiser means that the current "touch" becomes a
no-op.


I think that would be a very good idea.


I've done that now.  It's a new run-time system call which just returns
0.  RTS calls are used for all built-in functions and it's possible for
the code-generator to process simple ones directly inline.  I haven't
done that at the moment so it goes as far as a piece of assembly code.


Much appreciated.  For now I'd like to get a version working on top of 
5.5.2, and I assume assignment will suffice there.  Is there a way to 
create a non-overwritable ref in a normal session?  I don't seem to be 
able to access LibrarySupport.noOverwriteRef (and these seem to be 
needed for cleanAtExit to work).




Also, is there any point in Weak.weak taking an optional value?  (Would
anyone ever call it with NONE?)  Presumably weak could add the required
SOME to give
   val weak : 'a ref -> 'a ref option ref


My thinking was that you might have a finite set of resources, such as
file descriptors, and a list of weak references or a weak array with an
entry for each resource.  When a resource was allocated a SOME entry
would be made in the weak ref/array.  If the resource was no longer
reachable the corresponding entry would be set to NONE and the resource
could be reclaimed and later reallocated.


I see now.  I had overlooked the possibility of reusing one of these 
weak refs after it is NONE.


Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Using a finalizer with multiple arguments

[Phil Clayton]

18/09/15 11:53, David Matthews wrote:

Thanks for your patch.  I've integrated it and pushed it to github.


I was wondering how finalisation should this interact with saving state?
  Should the state of the finalizers be restored when loadState is
called?  That is what will happen with the code as it currently is but
it is possible to change that so that the state is not affected by
loadState by using "non-overwritable" references.


That's an interesting question.  If there is a case for using a
finalizable value on resources whose state is entirely captured in the
mutable and immutable store, then the finalizable state should probably
be restored.  Most uses I've seen are for C pointers which wouldn't be
available in a new session but this is already a limitation of vols.  At
the moment I can't think of a reason to use non-overwritable refs.


I thought some more about this and ran some tests.  I've now made it an
non-overwritable reference.  I would expect that finalisation would only
make sense for external state so it is better to have the finaliser list
unaffected by SaveState.loadState.  The following examples now do what I
would expect:
Session 1:
let
 open Finalizable
 val z = new ()
in
 addFinalizer(z, fn () => print "Saver final\n");
 PolyML.SaveState.saveState "saved";
 touch z
end;
Prints "Saver final" on exit.

Session 2:
let
 open Finalizable
 val z = new ()
in
 addFinalizer(z, fn () => print "Loader final\n");
 PolyML.SaveState.loadState "saved";
 touch z
end;
Prints "Loader final" on exit.


That makes sense to me.  The function cleanAtExit seems to be working 
now too.  Was it the use of non-overwritable refs that fixed that?




The only other changes I'm thinking about are:
1.  Introducing a "touch" primitive for long-term security in case a
future update to the optimiser means that the current "touch" becomes a
no-op.


I think that would be a very good idea.



2.  Simplifying the Weak structure by removing everything except the
"weak" function.  weakSignal and weakLock were really intended to allow
users to write their own finalisation code but if we have finalisers
provided they're probably unnecessary.  There would obviously have to be
a way to wake up the finaliser thread.  Currently it's integrated with
the signal handler thread in a non-obvious way.


Also, is there any point in Weak.weak taking an optional value?  (Would 
anyone ever call it with NONE?)  Presumably weak could add the required 
SOME to give

  val weak : 'a ref -> 'a ref option ref

weakSignal and weakLock could be avoided by adding Signal.onWeakMark to 
allow functions to be called when weak references are marked as NONE. 
An on-weak-mark handler thread could be started by Signal.  I really 
don't understand the overall architecture though.


Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Using a finalizer with multiple arguments

[Phil Clayton]

17/09/15 16:12, David Matthews wrote:

On 17/09/2015 11:50, Phil Clayton wrote:

Thanks for the example - it was a useful to see how to use the Thread
structure.  And to see how easy it was.  That's a nice library.

Attached is a first stab at implementing the FINALIZABLE signature shown
below, which is identical to MLTON_FINALIZABLE.  The code is based on
the MLton implementation but with a number of differences.  As mentioned
in the other email, there seems to be an issue with finalizers not being
run when exiting via OS.Process.exit.


Phil,
I've begun by adding your code to a Finalizable branch in the github
repository.  The Finalizable structure and signature are included in the
basis library when "poly" is built.  It looks good and there's just a
few points.


Great!



Your definition of "touch" should be fine.  I think I now understand
what's happening.  At the moment at any rate the Poly/ML optimiser views
the "store" as a single entity so it won't try to reorder or remove
assignments just because they occur to locations that a more
sophisticated analysis might show to be independent.  By the way, I
think perhaps the reason you had that rather bizarre behaviour with your
previous definition of "touch" was that the address of the token was
still in a register.  Calling "print" before calling PolyML.fullGC will
have replaced the address with something else.

I was wondering how finalisation should this interact with saving state?
  Should the state of the finalizers be restored when loadState is
called?  That is what will happen with the code as it currently is but
it is possible to change that so that the state is not affected by
loadState by using "non-overwritable" references.


That's an interesting question.  If there is a case for using a 
finalizable value on resources whose state is entirely captured in the 
mutable and immutable store, then the finalizable state should probably 
be restored.  Most uses I've seen are for C pointers which wouldn't be 
available in a new session but this is already a limitation of vols.  At 
the moment I can't think of a reason to use non-overwritable refs.




I've altered the initialisation code slightly.  It now uses
PolyML.onEntry to start the thread and install the atExit handler.  This
ensures that these are run on every run. Have a look at
basis/BasicStreamIO.sml which also contains a "non-overwritable"
reference for the list of streams that must be closed when Poly/ML exits.


I spotted this too after building a test case as a stand-alone 
executable and nothing happened...




I wonder if the finalizers should be called outside updatePendingList
i.e. after "mutex" has been released?  The problem at the moment is that
if a finalizer calls "new" it will deadlock.  A finalizer should
probably not be creating a new finalizer but equally we don't want
deadlock.


Good point.  That was easily fixed by making the function clean return a 
list of functions to run instead of a flag.  See attached patch (created 
with git format-patch).  (I can't do pull requests at the moment because 
Github no longer works properly with Firefox 16.)


Regards,
Phil

>From d0f11c79944826be3a26780634ad2227793da612 Mon Sep 17 00:00:00 2001
From: Phil Clayton 
Date: Thu, 17 Sep 2015 18:31:31 +0100
Subject: [PATCH] Avoid deadlock due to Finalizable.new in finalizer

Finalizers must be run after the lock on pendingList is released because
Finalizable.new needs to acquire the lock to add to pendingList.
---
 basis/Finalizable.sml |   15 ---
 1 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/basis/Finalizable.sml b/basis/Finalizable.sml
index 057743a..3e2a1d1 100644
--- a/basis/Finalizable.sml
+++ b/basis/Finalizable.sml
@@ -70,12 +70,12 @@ structure Finalizable :> FINALIZABLE =
 fun clean ((), ps) =
   foldl
 (
-  fn (p as {isAlive, runFinalizers}, (changed, ps)) =>
+  fn (p as {isAlive, runFinalizers}, (runNowFns, ps)) =>
 if isAlive ()
-then (changed, p :: ps)
-else (runFinalizers (); (true, ps))
+then (runNowFns, p :: ps)
+else (runFinalizers :: runNowFns, ps)
 )
-(false, [])
+([], [])
 ps
 
 fun swap (a, b) = (b, a)
@@ -85,7 +85,7 @@ structure Finalizable :> FINALIZABLE =
   fun threadFn () = (
 Thread.Mutex.lock Weak.weakLock;
 while true do (
-  ignore (updatePendingList clean ());
+  app (fn f => f ()) (updatePendingList clean ());
   Thread.ConditionVar.wait (Weak.weakSignal, Weak.weakLock)
 )
   )
@@ -96,9 +96,10 @@ structure Finalizable :> FINALIZABLE =
 fun loop ps =
   let
 val () = PolyML.fullGC ()  (* PolyML.fullGC is synchronous *)
- 

Re: [polyml] Using a finalizer with multiple arguments

[Phil Clayton]

Thanks for the example - it was a useful to see how to use the Thread 
structure.  And to see how easy it was.  That's a nice library.


Attached is a first stab at implementing the FINALIZABLE signature shown 
below, which is identical to MLTON_FINALIZABLE.  The code is based on 
the MLton implementation but with a number of differences.  As mentioned 
in the other email, there seems to be an issue with finalizers not being 
run when exiting via OS.Process.exit.


Phil


signature FINALIZABLE =
  sig
type 'a t
val new : 'a -> 'a t
val addFinalizer : 'a t * ('a -> unit) -> unit
val finalizeBefore : 'a t * 'b t -> unit
val touch : 'a t -> unit
val withValue : 'a t * ('a -> 'b) -> 'b
  end


16/09/15 11:56, David Matthews wrote:

On 15/09/2015 23:06, Phil Clayton wrote:

In MLton, creating a finalizable value from the pointer and size is
simple.  Roughly as follows:

   fun fromNewPtr p n =
 let
   val array = Finalizable.new p
 in
   Finalizable.addFinalizer (t, fn p => free_ (p, n));
   array
 end

where free_ is the C free function.  If Poly/ML can use the same or
similar code, that would be much easier!


This is my quick attempt to create something similar.  As long as the
result of the call to makeFinal is reachable the finalisation function
will not be called.  Once it becomes unreachable the finalisation
function will be called soon after the GC.  I've only tested it with
explicit calls to PolyML.fullGC but it should work equally when the GC
is activated automatically.  However it does require a full GC and that
can occur relatively infrequently.
David

local
 open Weak
 val finals = ref []

 fun threadFn () =
 let
 val () = Thread.Mutex.lock weakLock
 fun doFilter (ref (SOME _), _) = true
 |   doFilter (ref NONE, f) = (f(); false)
 in
 while true do
 (
 finals := List.filter doFilter (!finals);
 Thread.ConditionVar.wait(weakSignal, weakLock)
 )
 end

 val _ = Thread.Thread.fork(threadFn, [])
in
 fun makeFinal (f : unit -> unit) =
 let
 val r = ref ()
 val () =
 ThreadLib.protect weakLock
 (fn () => finals := (weak(SOME r), f) :: ! finals) ()
 in
 r
 end
end;
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml






finalizable-1.sml.gz
Description: GNU Zip compressed data
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Using a finalizer with multiple arguments

[Phil Clayton]

16/09/15 12:40, David Matthews wrote:

On 15/09/2015 22:18, Phil Clayton wrote:

I think weak references could do the job.  Better still, I may be able
to adapt (shamelessly copy) MLtonFinalizable:
https://github.com/MLton/mlton/blob/master/basis-library/mlton/finalizable.sig


https://github.com/MLton/mlton/blob/master/basis-library/mlton/finalizable.sml


This would have the added bonus of a common interface for finalizable
values between the compilers.

The main question is when to check the weak references.  Is there some
way to register a function to be called immediately after a GC?  I'll
investigate using a separate thread and the mutex which may be better
anyway.


There's no way to register a function.  Because of the way the thread
system works I think the only way to do the finalisation is through a
separate thread.


Understood.  I think a separate thread is better anyway.



Finalizers should also be called when the ML session exits.  It appears
that functions registered with OS.Process.atExit are always run before
Poly/ML exits (whether or not there is an explicit call to
OS.Process.exit).  Can you confirm that?


The intention is that that should be the case.  If OS.Process.terminate
is called the functions aren't run.  I have just done a test and it
appears that exiting by calling Thread.Thread.exit() doesn't run the
atExit functions either.


I think the desirable behaviour is for finalizers to be run whenever 
Poly/ML is ending its own process.  For example, if SIGTERM causes 
Poly/ML to exit, finalizers should be run because they are typically 
performing clean-up operations.  Is there a way to do that?


Also, even using OS.Process.atExit and exiting via OS.Process.exit, I am 
finding that remaining finalizers aren't being run.  After a call to 
fullGC in the at-exit function, the weakly referenced values haven't 
been garbage-collected, so their finalizers aren't run.  Has the 
lifespan of those values has not ended at that that point?  (See my 
other email for the example code.)




I was wondering how to implement the 'touch' function of
MLTON_FINALIZABLE that forces a weak reference to stay alive.  The
expression
   ignore (PolyML.pointerEq (x, x) orelse raise Fail "touch"; print "");
seems to prevent Poly/ML optimizing the dependence on x away and works
for any type x.  Bizarrely, I found that without print "", the weak
reference stayed alive.  Can you think of something simpler?


I looked at the MLton documentation and couldn't understand what "touch"
was trying to achieve.  Could you explain it?


"touch t" prevents finalization of t until the call has been evaluated. 
 "touch t" an operation that uses t to do nothing, so t cannot be 
garbage-collected until the operation has finished.




My idea with weak variables in Poly was that the "token" and the item to
be finalised would be linked in such a way that they would have the same
lifetime e.g. the "token" would be paired with the item.


With these finalizable values, no "item" is required, there is only a 
"token".  The token can be a reference to anything so we make it a 
reference to the value that finalizers will be run on.  All access to 
the finalizable value is by dereferencing the token, so the token is 
referenced as long as the finalizable value is used.  This is ensured by 
having an abstract type requiring Finalizable.withValue to be used to 
access the value.




Is the issue
that a global optimising compiler such as MLton could work out that the
token was not referenced even though the item was and remove it from the
pair at the last reference?


I don't think that is the issue here (as we don't have an item).



Poly/ML only does that in very limited
circumstances.  Is the idea of "touch" that this counts as a reference
to the token and that you add a call to it after each reference to the
item so that the lifetime of the token is no less than the lifetime of
the item?


Yes, but as there is no item, the purpose of touch is to delay 
finalization until some other event has occurred.  One example use of 
touch is in the implementation of Finalizable.finalizeBefore.  The 
'other event' is finalization of another finalizable value.




Since the token is a reference either assigning or
dereferencing it should work.  Even if the result is always () that
should still count as a reference.


I find that
  ignore (!value)
doesn't keep the value alive whereas
  value := !value
does.  That was a useful suggestion - much more preferable to my earlier 
idea.  The assignment is doing work whose effect isn't required but is 
that an overhead worth worrying about?


Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Using a finalizer with multiple arguments

[Phil Clayton]

Hi Artella,

Thanks - I wondered about that but it is quite a bit of effort by 
comparison because I am creating a framework for automatically 
generating bindings rather than writing some bindings by hand.  When 
calling a C function that takes the array pointer, the struct pointer 
would be passed from ML, so it would be necessary to wrap the C function 
to dereference the struct pointer to get the array pointer.  I would 
want to do that dereferencing on the ML side (by manipulating vols) to 
avoid having to generate C function wrappers.  That's not too much 
effort.  Also, as you say, a free function would be needed but that 
would need to be generated I don't really want to extend the framework 
to do that - currently I don't generate any C code.


In MLton, creating a finalizable value from the pointer and size is 
simple.  Roughly as follows:


  fun fromNewPtr p n =
let
  val array = Finalizable.new p
in
  Finalizable.addFinalizer (t, fn p => free_ (p, n));
  array
end

where free_ is the C free function.  If Poly/ML can use the same or 
similar code, that would be much easier!


Regards,
Phil

15/09/15 15:27, Artella Coding wrote:

Hi Phil,

Can't you wrap the array and size in a struct. For example in
https://github.com/polyml/polyml/tree/cb1b36caa242fc6ea9f74b015158466efac68d66/mlsource/extra/CInterface/Examples
we have :

-
//ForeignTest.c
typedef struct _tree {
struct _tree *left, *right;
intnValue;
} *tree;

int SumTree(tree t)
{
if (t == NULL) return 0;
else return t->nValue + SumTree(t->left) + SumTree(t->right);
}
-

and

-
(*ForeignTest.sml*)
val sumTree = CInterface.call1 ( CInterface.load_sym mylib "SumTree")
TREE INT;

-

So you just write a FreeTree function, which is modelled after the
FreeIt function in ForeignTest.c :

void FreeIt(void *p)
{
 printf("Freed object at %p\n", p);
 fflush(stdout);
 free(p);
}

, which then reads nValue and passes it on to the relevant gtk function?

On Mon, Sep 14, 2015 at 10:36 PM, Phil Clayton mailto:phil.clay...@lineone.net>> wrote:

I am trying to create an SML binding to a C function that returns an
array that the caller must free.  Usually, there is a free function
that takes just the array (as a pointer) which can be attached as a
finalizer with CInterface.setFinal.  I have encountered a case [1]
where the caller must also pass the size of the array, returned when
the array is created, to the free function.

Simplifying the example, we have, for some C type Elem:

   Elem *new (..., int *n_elems);  /* n_elems is an 'out' parameter */
   void free (Elem *elems, int n_elems);

and want an SML function like

   val new : ... -> elem vector

Unfortunately, the function given to CInterface.setFinal is called
with only one argument, the vol that is being finalized.  Therefore
this free function cannot be used.  Does the current FFI
architecture allow a variant of setFinal that passes extra arguments
to the finalization function?  For example:

   val setFinal1 : sym -> 'a Conversion -> vol -> 'a -> unit

This isn't particularly common so is probably not a show-stopper.
Another benefit could be enabling use of functions g_slice_alloc and
g_slice_free1 that needs the number of bytes to free:
https://developer.gnome.org/glib/stable/glib-Memory-Slices.html

Thanks,
Phil


1.  The C function in question is gtk_target_table_new_from_list
that returns an array and its size.  The array should be freed with
gtk_target_table_free which should be passed the size.  See:
   -

https://developer.gnome.org/gtk3/stable/gtk3-Selections.html#gtk-target-table-new-from-list
   -

https://developer.gnome.org/gtk3/stable/gtk3-Selections.html#gtk-target-table-free
___
polyml mailing list
polyml@inf.ed.ac.uk <mailto:polyml@inf.ed.ac.uk>
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Using a finalizer with multiple arguments

[Phil Clayton]

David,

I think weak references could do the job.  Better still, I may be able 
to adapt (shamelessly copy) MLtonFinalizable:

https://github.com/MLton/mlton/blob/master/basis-library/mlton/finalizable.sig
https://github.com/MLton/mlton/blob/master/basis-library/mlton/finalizable.sml
This would have the added bonus of a common interface for finalizable 
values between the compilers.


The main question is when to check the weak references.  Is there some 
way to register a function to be called immediately after a GC?  I'll 
investigate using a separate thread and the mutex which may be better 
anyway.


Finalizers should also be called when the ML session exits.  It appears 
that functions registered with OS.Process.atExit are always run before 
Poly/ML exits (whether or not there is an explicit call to 
OS.Process.exit).  Can you confirm that?


I was wondering how to implement the 'touch' function of 
MLTON_FINALIZABLE that forces a weak reference to stay alive.  The 
expression

  ignore (PolyML.pointerEq (x, x) orelse raise Fail "touch"; print "");
seems to prevent Poly/ML optimizing the dependence on x away and works 
for any type x.  Bizarrely, I found that without print "", the weak 
reference stayed alive.  Can you think of something simpler?


Finally, a couple of general issues:

1. I was getting some unexpected behaviour with weak references using 
Poly/ML 5.5.0 - see the following example.  Poly/ML 5.5.2 behaved as 
expected though.  Does that mean 5.5.0 should be avoided?


  local
val w = Weak.weak (SOME (ref ()))
  in
fun check () = isSome (!w)
  end
  ;
  check ();
  val () = PolyML.fullGC ();
  check ();  (* false for 5.5.2, ok; true for 5.5.0 - issue? *)

2. The function weakArray confuses me although I doubt I will need to 
use it.  It's not clear why it would be called with a reference, i.e. 
non-NONE argument because that is duplicated for every array element. 
Furthermore, if it is called with a non-NONE argument and the array size 
is more than 1, then this can crash Poly/ML.  For example, entering the 
following in the top-level:


  val wa = Weak.weakArray (2, SOME (ref ()));
  PolyML.fullGC ();
  wa; (* seg fault *)

Regards,
Phil

15/09/15 13:21, David Matthews wrote:

On 14/09/2015 22:36, Phil Clayton wrote:

I am trying to create an SML binding to a C function that returns an
array that the caller must free.  Usually, there is a free function that
takes just the array (as a pointer) which can be attached as a finalizer
with CInterface.setFinal.  I have encountered a case [1] where the
caller must also pass the size of the array, returned when the array is
created, to the free function.


Phil,
I wonder if this is a case for the use of a weak reference (
http://www.polyml.org/documentation/Reference/Weak.html ) ?  Have a look
at this link and see whether it would work for you.

Essentially, what weak references do is allow you to run finalisers in
"ML space".  CInterface.setFinal sets up a C function to be run as a
finaliser and the GC runs these immediately when it detects an
unreferenced "vol".  It can't run an ML function at that point because
the ML heap is still being collected.  Changes to weak references are
notified at some point after ML is resumed after the GC.

If you've got any questions please ask.  I'd also be interested to know
if it solves your problem.

Regards,
David




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

[polyml] Using a finalizer with multiple arguments

[Phil Clayton]

I am trying to create an SML binding to a C function that returns an 
array that the caller must free.  Usually, there is a free function that 
takes just the array (as a pointer) which can be attached as a finalizer 
with CInterface.setFinal.  I have encountered a case [1] where the 
caller must also pass the size of the array, returned when the array is 
created, to the free function.


Simplifying the example, we have, for some C type Elem:

  Elem *new (..., int *n_elems);  /* n_elems is an 'out' parameter */
  void free (Elem *elems, int n_elems);

and want an SML function like

  val new : ... -> elem vector

Unfortunately, the function given to CInterface.setFinal is called with 
only one argument, the vol that is being finalized.  Therefore this free 
function cannot be used.  Does the current FFI architecture allow a 
variant of setFinal that passes extra arguments to the finalization 
function?  For example:


  val setFinal1 : sym -> 'a Conversion -> vol -> 'a -> unit

This isn't particularly common so is probably not a show-stopper. 
Another benefit could be enabling use of functions g_slice_alloc and 
g_slice_free1 that needs the number of bytes to free:

https://developer.gnome.org/glib/stable/glib-Memory-Slices.html

Thanks,
Phil


1.  The C function in question is gtk_target_table_new_from_list that 
returns an array and its size.  The array should be freed with 
gtk_target_table_free which should be passed the size.  See:
  - 
https://developer.gnome.org/gtk3/stable/gtk3-Selections.html#gtk-target-table-new-from-list
  - 
https://developer.gnome.org/gtk3/stable/gtk3-Selections.html#gtk-target-table-free

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] polyc and poly --script

[Phil Clayton]

Hi David,

Thanks - I've tried building an application with r1985 in the following 
configurations and pkg-config is working now:

  static, non-system libffi
  static, system libffi
  shared, non-system libffi
  shared, system libffi

Phil

24/03/15 12:01, David Matthews wrote:

Hi Phil,
I've changed configure so that FFI_LIBS gets added to LIBS within the
configure script.  This should avoid the need to add it explicitly in
other places.  Let me know if there are problems.

David

On 23/03/2015 23:45, Phil Clayton wrote:

Hi David,

15/10/13 17:50, David Matthews wrote:

On 15/10/2013 17:38, René Neumann wrote:

@David: Have you seen my other issue in the original email?


Was this the --with-system-ffi issue?  I've fixed it in SVN trunk.  It
may be something to port to the fixed branch.


It looks like r1871 didn't update polyml.pc.in similarly.

pkg-config is not producing -lffi when Poly/ML is built with
   --with-system-ffi

Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] polyc and poly --script

[Phil Clayton]

Hi David,

15/10/13 17:50, David Matthews wrote:

On 15/10/2013 17:38, René Neumann wrote:

@David: Have you seen my other issue in the original email?


Was this the --with-system-ffi issue?  I've fixed it in SVN trunk.  It
may be something to port to the fixed branch.


It looks like r1871 didn't update polyml.pc.in similarly.

pkg-config is not producing -lffi when Poly/ML is built with
  --with-system-ffi

Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] emacs SML mode

[Phil Clayton]

My Makefiles contain something like the following:

@set -o pipefail ; \
 poly --use load.sml \
  | tee polyml.log \
  | (grep -E -e "^(Warning-|Error-|Exception-)" || true)

The primary purpose is to print any warnings in the terminal as they are 
produced whilst redirecting the full log to a file for reference.  (I 
don't like this because it's necessary to use the Bash-specific option 
"pipefail" to prevent piping  losing the exit status and this doesn't 
work with other shells like Dash.)


Is there a way to tell Poly/ML to print warning/error message to stderr 
as well as stdout?  That would avoid needing to match on the


I don't have any objection to the patch however - the above is easily 
changed.


Phil

15/03/15 14:38, David Matthews wrote:

Peter,
Thanks for that.  I've applied it to SVN so unless someone objects that
it has messed up their error message parsing it will be in the next
release.
Regards,
David

On 14/03/2015 20:39, Peter Gammie wrote:

David,

On 14 Dec 2014, at 9:23, David Matthews
 wrote:


I seem to recall that the current format of error messages was
designed to be parsed by emacs but probably as long ago as the
1980s.  I have no objection at all to changing the format to
something more appropriate. It probably needs no more than a change
to the bit of code around line 443 in basis/FinalPolyML.sml that
assembles a text error message from the location information.  If you
want to experiment and send me a patch that works for you I’m happy
to look at it.


Here’s a very minor patch to generate Emacs-compatible errors and
warnings. See below. It’s an SVN diff - hope that works for you.

cheers,
peter

Index: basis/FinalPolyML.sml
===
--- basis/FinalPolyML.sml(revision 1980)
+++ basis/FinalPolyML.sml(working copy)
@@ -441,10 +441,14 @@
  else (* Plain text form. *)
  (
  printString(concat
-   ( (if hard then ["Error-"] else ["Warning-"]) @
+   ( (if file = "" then ["poly: "] else [file, ":"]) @
+ (if startLine = 0 then [] else [Int.toString
startLine]) @
+ (if startPosition = 0 then [": "] else [".",
Int.toString startPosition, "-", Int.toString endPosition, ": "]) @
+ (if hard then ["error: "] else ["warning: "]) ));
+(*   ( (if hard then ["Error-"] else ["Warning-"]) @
   (if file = "" then [] else [" in '", file,
"',"]) @
   (if startLine = 0 then [] else [" line ",
Int.toString startLine]) @
- (if startLine = 0 andalso file = "" then [] else
[".\n"])));
+ (if startLine = 0 andalso file = "" then [] else
[".\n"]))); *)
  PolyML.prettyPrint(printString, !lineLength)
fullMessage
  )
  end
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml



___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] linking polyML modules to C

[Phil Clayton]

19/01/15 12:19, David Matthews wrote:

On 19/01/2015 04:34, David Topham wrote:

Thanks David for your response.

While searching I found this comment you made earlier:

"The foreign-function interface allows for call-back functions so
there is
the mechanism to produce a C function that when called calls an ML
function."

in
http://stackoverflow.com/questions/17580386/shared-libraries-in-poly-ml

Doesn't this indicate a mechanism that allows an SML function to be
called
from C?


Yes, but the "main program" still has to be in ML.  You can call C
library functions and pass an ML function as an argument.


Or the ML functions can be passed via global variables that are 
initialized from the ML side - see attached example.  That may be easier 
if there are a large number of ML functions.




Actually, I did wonder whether this could be used as a way of exporting
ML functions to create a library that could be called from a C main
program and came to the conclusion that it was going to be too
complicated.  Poly/ML uses libffi to interface with C.  libffi can build
closures that wrap around ML functions so that these can be passed into
C.  The format of the closure it constructs differs markedly depending
on the particular architecture since different architectures have
different calling conventions for C.  The closure is a data structure
with pointers in it.  Exporting it would require turning the pointers
into relocations that the linker/loader will understand.  libffi simply
doesn't provide that information.  It's there by implication in the
source code but not explicitly.

David
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml





call_c_test_10.tar.gz
Description: GNU Zip compressed data
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Poly/ML and UI toolkits [Was: Poly/ML]

[Phil Clayton]

12/12/14 18:15, Ian Zimmerman wrote:

On Fri, 12 Dec 2014 14:17:27 +0100 (CET),
Makarius  wrote:

Makarius> Back to the original question: a public version of the
Makarius> aforementioned GTK C bindings for Poly/ML would be great.

Agreed, so could someone ping Phil Clayton about it?  I am too shy
(having been given access to an early version privately, and not having
done anything with it).


Thanks for mentioning this Ian.  Unfortunately I've only just caught up 
with this discussion.


GTK+ bindings do exist for Poly/ML as part of Giraffe Library, which I 
am developing.  See below for a brief overview.  The same bindings are 
also provided for MLton, allowing the same application code to compile 
with either compiler.


Giraffe Library is not publicly available yet because there are a couple 
of little loose ends that I want to tie up.  However, I would be very 
happy to provide a copy to anyone wanting to try it out and feedback 
would be welcome.  Giraffe Library is LGPL simply to have the same 
licence as GTK+ and company.


There are quite a few omissions in the library.  Despite this, a lot can 
be done.  To get a flavour of things, the ubiquitous Hello World example 
from the GTK+ tutorial is attached!


Regards,
Phil


 ---  1.  Overview  ---

Giraffe Library is a Standard ML library that provides an interface to
GObject-based libraries, such as GTK+.  The interface introduces some
abstraction of the libraries to provide expected features of
Standard ML such as:

  - automatic memory management (garbage collection)
  - type-safety
  - no uninitialized values
  - portable source code

For the most part, Giraffe Library is generated automatically from the
GIR data of the libraries.  At present, interfaces to parts of the
following libraries are available:

  - GTK+
  - Pango
  - GtkSourceView
  - VTE (Virtual Terminal Emulator)

val msg = "Hello world!"
fun printMsg () = app print [msg, "\n"]

fun deleteEvent _ = false
fun destroy () = Gtk.mainQuit ()

fun setup () =
  let
open Gtk
val window = Window.new WindowType.TOPLEVEL
val button = Button.newWithLabel msg
  in
Window.setTitle window msg;
Window.setDefaultSize window 200 75;

Signal.connect window Widget.deleteEventSig deleteEvent;
Signal.connect window Widget.destroySig destroy;

Signal.connect button Button.clickedSig printMsg;

Container.add window button;

Widget.showAll window
  end


fun error msg =
  let
  open TextIO OS.Process
  fun printErr s = output (stdErr, s)
  in
  app printErr msg;
  flushOut stdErr;
  exit failure
  end


fun main () =
  let
val _ = Gtk.init (CommandLine.name () :: CommandLine.arguments ())
  in
setup ();
Gtk.main ()
  end
handle e => error ["Uncaught exception\n", exnMessage e, "\n"]
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] address type in Poly/ML interface to C (FFI)

[Phil Clayton]

I'm fairly sure that whatever integer type you use to hold a pointer, 
it's going to get converted to a vol at the C interface anyway - inside 
a conversion are functions to convert from/to vols.  Also, the supplied 
conversions for integer types work with IntInf.int, e.g.


> LONG : IntInf.int Conversion;
val it = ?: int Conversion

so IntInf.int will be involved too, which may not be optimized out.

Probably most efficient to use vol for a pointer and the conversion 
POINTER.  This would avoid the creation of a new vol when passing a 
pointer to a C function whereas passing an ML integer may require a new 
vol to be created each time.


04/10/14 18:19, m...@beroal.in.ua wrote:

The interface is generated from C prototypes, and every pointer is
wrapped in an ML type for every C "typedef", so safety is not of concern
here. As I said, the library requires to free objects explicitly.

BTW,
$ uname -a
Linux [skipped] 3.16.1-1-ARCH #1 SMP PREEMPT [skipped] x86_64 GNU/Linux
 > SysWord.wordSize;
val it = 64: int


Appears that this changed in 5.5.1:

Poly/ML 5.5.0 Release
> SysWord.wordSize;
val it = 126: int

Poly/ML 5.5.1 Release
> SysWord.wordSize;
val it = 64: int



On 04.10.14 16:14, Phil Clayton wrote:

I would suggest that you don't actually want an ML integer type to
hold your C pointers.  The main reason is that you would lose some
type-safety because type checking would not detect accidental use of
an integer as a pointer (and vice-versa).

What you should want in ML is an abstract type for a pointer, say,
Pointer.t that has the required operations.  Creating a simple
signature/structure to provide a pointer type (defined internally as a
vol) would go some way to removing the confusion about using vol
directly.

In ML, the types SysWord.word and IntInf.int would be wide enough to
hold pointer types.  With Poly/ML, I'm sure it would be much more
efficient to use a vol.  (On my x86_64 system, SysWord.wordSize =
126.)  Also, if you're going to use the garbage collector to free
memory when a pointer is no longer referenced, your pointer types must
be based on a vol.

Phil

26/09/14 09:59, m...@beroal.in.ua wrote:

Hello.

As I can see, there is no address type. The suggested conversion for C
pointers (POINTER : vol Conversion) converts a C pointer to "vol".

As follows from
http://www.polyml.org/docs/CInterface.html#17%20Volatile%20Implementation

, "vol" contains an address of a heap object. If its boolean field
"owns" is true, it garbage-collects its heap object.

If a C library requires that freeing a heap object be done explicitely,
managing an address to that heap object by "vol" is inefficient and
confusing. A "vol" value contains an index of the element of the "vols"
array which contains an address of a memory block which contains an
address of the heap object. What I really need is an ML integer type
that is wide enough to hold a C pointer; I called it "address type".

I'm trying to create a binding to the XCB library (
http://xcb.freedesktop.org/ ). Some functions from XCB don't manage
memory (so the Poly/ML garbage collector may be used); some functions
are allocating objects, and those objects must be freed by the function
"free" or "xcb_disconnect".
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml








___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] address type in Poly/ML interface to C (FFI)

[Phil Clayton]

I would suggest that you don't actually want an ML integer type to hold 
your C pointers.  The main reason is that you would lose some 
type-safety because type checking would not detect accidental use of an 
integer as a pointer (and vice-versa).


What you should want in ML is an abstract type for a pointer, say, 
Pointer.t that has the required operations.  Creating a simple 
signature/structure to provide a pointer type (defined internally as a 
vol) would go some way to removing the confusion about using vol directly.


In ML, the types SysWord.word and IntInf.int would be wide enough to 
hold pointer types.  With Poly/ML, I'm sure it would be much more 
efficient to use a vol.  (On my x86_64 system, SysWord.wordSize = 126.) 
 Also, if you're going to use the garbage collector to free memory when 
a pointer is no longer referenced, your pointer types must be based on a 
vol.


Phil

26/09/14 09:59, m...@beroal.in.ua wrote:

Hello.

As I can see, there is no address type. The suggested conversion for C
pointers (POINTER : vol Conversion) converts a C pointer to "vol".

As follows from
http://www.polyml.org/docs/CInterface.html#17%20Volatile%20Implementation
, "vol" contains an address of a heap object. If its boolean field
"owns" is true, it garbage-collects its heap object.

If a C library requires that freeing a heap object be done explicitely,
managing an address to that heap object by "vol" is inefficient and
confusing. A "vol" value contains an index of the element of the "vols"
array which contains an address of a memory block which contains an
address of the heap object. What I really need is an ML integer type
that is wide enough to hold a C pointer; I called it "address type".

I'm trying to create a binding to the XCB library (
http://xcb.freedesktop.org/ ). Some functions from XCB don't manage
memory (so the Poly/ML garbage collector may be used); some functions
are allocating objects, and those objects must be freed by the function
"free" or "xcb_disconnect".
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] polyc

[Phil Clayton]

Hi Rob,

23/04/14 17:13, Rob Arthan wrote:

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.)


I believe that, by default, Gcc default would not link libpolyml 
statically if a shared version of the library exists.  Whether the 
shared version exists depends on the particular Poly/ML installation. 
Supplying the argument --enable-shared to 'configure' when building 
creates the SO file.


If Poly/ML is built with a shared library and is not installed to a 
system location (so the libpolyml SO file is not automatically found), 
then executables from polyc require LD_LIBRARY_PATH to be set.  Setting 
the linker path in polyc came up in discussion before, in a thread 
starting here:

http://lists.inf.ed.ac.uk/pipermail/polyml/2013-April/001216.html
(due to the comment in item 3)
The current position seems to be that anyone installing (a shared 
version) to a non-system location needs to set LD_LIBRARY_PATH, just as 
they will need to set PATH.


I believe that LD_RUN_PATH can be specified in the environment for polyc 
to achieve the required effect.  However, its value would have to be 
determined, which is unfortunate given that polyc has this information 
internally (libdir).  The PC file for use with pkg-config is an 
alternative that is useful for Makefiles, e.g.


POLYMLLIB  := `pkg-config polyml --variable=libdir`

$(NAME)-polyml : $(NAME)-polyml.o
	@LD_RUN_PATH=$(POLYMLLIB):$(LD_RUN_PATH) $(CC) -ggdb -o $@ `pkg-config 
--libs polyml` $<


but you may not want a dependency on that utility.

Regards,
Phil

P.S. I think there have been a few updates/fixes to polyc since the 
5.5.1 release.


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] checking --enable-shared from within the REPL

[Phil Clayton]

I would have thought that it's enough to check to see whether the LIBDIR 
directory defined in the polyc script contains an SO file.  Or perhaps 
just look at

  ldd `which poly`
The shared version is installed iff the output contains something like
  libpolyml.so.5 => ...

Phil

13/01/14 12:28, David Matthews wrote:

There's nothing within the Poly/ML environment that will tell you.  You
might be able to find a .so/.dll/.dylib file corresponding to libpolyml
in /usr/local/lib but it could be elsewhere.

Why exactly do you need to know whether it was compiled with
--enable-shared or --disable-shared?

David

On 13/01/2014 05:00, Michael Norrish wrote:

Is there any way to detect if the system has been built with
--enable-shared?
Something in the PolyML structure (say)?  I'd like to be able to have
my build
script abort if the PolyML hasn't been built correctly.  Or is there
anything
obvious my script could check in the file system to make this
determination?

Thanks,
Michael



___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Flexible records and overloading

[Phil Clayton]

29/11/13 13:47, David Matthews wrote:

The ML standard is not specific about what the "program context" should
be when disambiguating flexible records and overloading.  Poly/ML uses
as wide a context as possible but that can mean that a program that
compiles with Poly/ML won't necessarily compile with other
implementations.  I've added a switch
PolyML.Compiler.narrowOverloadFlexRecord that defaults to false.  If set
to true the compiler uses a much narrower context; essentially the val
binding.

I've looked at a few other implementations to see what they do.  The
most restrictive is Hamlet which corresponds to what Poly/ML now does
with narrowOverloadFlexRecord set to true.  It rejects
let fun f x y = x + y in f 1.0 end;
which SML/NJ (110.74) accepts.  Neither accept
let fun f {x, ...} = x in f {x=1} end;
Mlton seems to use the whole program context as Poly/ML does.


There was a discussion about this on the MLton mailing list while ago 
and MLton now has an annotation to control the context used:

http://thread.gmane.org/gmane.comp.lang.ml.mlton.user/1335/focus=6086
http://sourceforge.net/p/mlton/code/7618/

I thought MLton's default value for this annotation (equivalent to its 
previous behaviour) caused a narrower context than PolyML, so I have 
been using

  -default-ann 'resolveScope topdec'
to get (nearly) equivalent behaviour between the compilers.

Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] managing compilation

[Phil Clayton]

19/10/13 12:58, Buday Gergely wrote:

Hi,

I am looking for a method of managing compilation for Poly/ML, like .cm files 
for SML/NJ and .mlb files for MLton. What I have found on polyml.org was 
PolyML.make -- is that the last word on this subject?


With Poly/ML, I find it easiest to have source files of the form
  use "";
  use "";
  ...
solely for the purpose of processing other source files.

This question came up a while ago, and I posted an answer here:
http://lists.inf.ed.ac.uk/pipermail/polyml/2012-August/001059.html
(about half way down)

Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] pkg-config for Poly/ML

[Phil Clayton]

David,

26/09/13 18:31, David Matthews wrote:

I've just committed support for pkg-config with Poly/ML.  Would you like
to have a look at it and see if it works as you expect?  Let me know if
there are any changes needed.  You had separate versions for the shared
and static libraries.  I can see why you did that but it looks like it
would be a lot more work.


Thanks for the update.  The polyml.pc file appears to be generated as 
expected.  Using one set of linking flags for shared and static 
libraries does not appear to matter actually: although unnecessary 
linker flags can create unnecessary library dependencies, ldd shows that 
there isn't any additional dependency when linking to the shared library 
using the static flags.


I couldn't actually do a complete stand-alone test with r1862 because it 
wouldn't build on my machine - see output below.  (My guess is that 
r1859 is causing the problem.  Maybe the shift left is overflowing on 
x86_64 giving zero?)


Regards,
Phil


./polyimport -H 50 polytemp.txt -I . < ./exportPoly.sml

Value of -H option is too large
-H 
--minheap 
--maxheap 
--gcpercent 
--stackspace 
--gcthreads 
--debug 
--logfile 
Debug options:
checkmem 
gc 
gcdetail 
memmgr 
threads 
gctasks 
heapsize 
x 
sharing 
locks 
rts 
make[2]: *** [polyexport.o] Error 1
make[2]: Leaving directory `/home/pclayton/SML/PolyML/svn/trunk/polyml'
make[1]: *** [all-recursive] Error 1
make[1]: Leaving directory `/home/pclayton/SML/PolyML/svn/trunk/polyml'
make: *** [all] Error 2

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] pkg-config for Poly/ML

[Phil Clayton]

19/09/13 16:05, Ramūnas Gutkovas wrote:

On 9/19/13 4:47 PM, Alex Merry wrote:

On 19/09/13 15:14, David Matthews wrote:

I don't know how useful it will be in general, though.  I've done a
quick look and pkg-config doesn't seem to be installed on several
set-ups I looked at including Mac OS X and Solaris.


I didn't really have a feel for its general prevalence outside the Linux 
world and agree that it may not be useful for all applications.  A quick 
search suggests it should be straightforward to build though, e.g.

https://github.com/LearnBoost/node-canvas/wiki/Installation---OSX
(though --with-internal-glib may be needed if glib is not present).
Possibly even a single-command install, e.g.
http://cduu.wordpress.com/2011/11/26/install-pkg-config-on-mac-os-x/
However, I doubt applications such as HOL4 would want to force this on 
those building them.




The other problem
is that it is going to require the PC files to be written into
/usr/lib/pkgconfig or some other non-user-writable directory.  One of
the problems I was trying to work round was the fact that many users of
Poly/ML are running on systems that are managed centrally and they don't
have root access.  It's this that makes shared libraries a problem
because libpolyml can't be installed to /usr/lib or /usr/local/lib.  All
this means that anyone distributing code, such as HOL4 or Metit that are
intended to be built with poly, can't rely on pkg-config.


It should just be installed to $PREFIX/lib/pkgconfig; users can then
export the environment variable
PKG_CONFIG_PATH=$PREFIX/lib/pkgconfig:$PKG_CONFIG_PATH
before building the tool that uses Poly/ML, in much the same way that
they have to set
PATH=$PREFIX/bin:$PATH
(or supply an absolute path to poly).  pkg-config will then find the .pc
file.


Yes, and more generally, once a build system has determined the location 
of poly it could set PKG_CONFIG_PATH within the build process.


Possibly $PREFIX/share/pkgconfig would be better installation location. 
 One would want the property that when $PREFIX is /usr, the PC file is 
located in the default pkg-config path.  This is

  $libdir/pkgconfig:$datadir/pkgconfig
where libdir and datadir are determined by the installation location of 
pkg-config.  pkg-config can report these:


  [pclayton@rizzo ~]$ pkg-config --variable=pc_path pkg-config
  /usr/lib64/pkgconfig:/usr/share/pkgconfig

libdir is either .../lib or .../lib64 depending on the platform so 
datadir, which is .../share, avoids the difference.




On 9/19/13 4:47 PM, Alex Merry wrote:

pkg-config is mostly a Linux thing (although I suspect it's easily found
on *BSD systems), so it's not so useful for Windows or the proprietary
unices like OS X and Solaris.


pkg-config seems to have support for these platforms (mingw in the case 
of Windows).  It would be useful to know how readily available it is via 
a package management system on those platforms.



19/09/13 16:05, Ramūnas Gutkovas wrote:

A possible option would also be to generate a shell script, say
poly-config, and install on the same path as poly which would accept the
same options as pkg-config. The script could be generated in case the
pkg-config is not available. This would solve the portability issue for
non linux systems.


Yes, or even a subset of the behaviour.

Standing back, there appear to be (at least) two levels here:
1. Indicating to a build system whether Poly/ML SO files are available 
so it can select suitable linker flags

2. Providing the required linker flags for any Poly/ML installation
The first would suffice but the second would be nice.

Regards,
Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

[polyml] pkg-config for Poly/ML

[Phil Clayton]

18/09/13 12:51, David Matthews wrote:

The complication is that exactly which libraries have to be included
depend on how libpolyml was built.  The configure script detects the
libraries that are needed to build "poly" and builds a linker command
line from that.  In particular, -lgmp is included only if GMP is
present.  This all makes it difficult for a build script such as that
used by HOL4 to have a standard linker command line.

The idea of "polyc" is to capture the linker command line that was used
to build "poly" on the particular platform and make it available for
other applications.  ...


One well-established aid for constructing suitable command-line options 
is pkg-config.  This may be more useful for use in Makefiles due to 
greater flexibility than polyc.  For pkg-config, a library installs a PC 
file.  (There are quite a few examples in /usr/lib64/pkgconfig/ on my 
system.)  This tells pkg-config which command line options are required 
for building with that library.


A while ago, I experimented with this, creating the attached PC file for 
polyml and adapting a Makefile to use pkg-config to construct the polyml 
linker command-line options.  This seems to work.  For example, the 
Makefile rule (for Poly/ML built with --enable-shared)


$(NAME)-polyml : $(NAME)-polyml.o
$(CC) -o $@ -L$(POLYMLLIB) -lpolymain -lpolyml $<

was changed to

$(CC) -o $@ `pkg-config --libs polyml` $<

given the attached polyml.pc in the pkg-config path.  For static 
linking, this would be


$(CC) -o $@ -static `pkg-config --libs --static polyml` $<

however this requires all dependencies to be static: given that 
pkg-config generates command-line options for all dependencies, it is 
not possible to switch back and forth between -static and -dynamic.


For Poly/ML built with --disable-shared (now default) the same commands 
also work by using a slightly different polyml.pc where certain 
dependencies are moved from

  Libs.private
to
  Libs
as they are always required for linking.  This is shown in 
polyml.pc-disable-shared, also attached.


With pkg-config, other variables can be extracted too.  For example, the 
Makefile lines


  POLYML := $(shell which poly 2> /dev/null)
  POLYMLBIN  := $(patsubst %/,%,$(dir $(POLYML)))
  POLYMLHOME := $(patsubst %/,%,$(dir $(POLYMLBIN)))
  POLYMLLIB  := $(POLYMLHOME)/lib

were replaced by

  POLYMLBIN  := `pkg-config --variable=bindir polyml`
  POLYMLLIB  := `pkg-config --variable=libdir polyml`
  POLYML := $(POLYMLBIN)/poly
  POLYMLROOT := `pkg-config --variable=prefix polyml`

Furthermore, should any future enhancements to the FFI want to allow 
C-side code to reference symbols from Poly/ML H files, pkg-config can 
produce command-line options for C include directories too.  I seem to 
recall that I once wanted to include a MLton H file in code on the 
C-side of the MLton FFI.


There is a default pkg-config path which can be overridden with the 
environment variable PKG_CONFIG_PATH.  That seems as good a way as any 
to indicate which version of Poly/ML should be used when building an 
application.


Regards,
Phil

prefix=/opt/polyml/polyml-r1848d
exec_prefix=${prefix}
bindir=${exec_prefix}/bin
libdir=${exec_prefix}/lib
includedir=${prefix}/include

Name: Poly/ML
Description: Poly/ML Standard ML Compiler
URL: http://www.polyml.org/
Version: 5.5.1
Requires: 
Libs: -L${libdir} -lpolymain -lpolyml
Libs.private: -lpthread -lgmp -lm -ldl -lstdc++ -lgcc_s -lgcc
Cflags: -I${includedir}
prefix=/opt/polyml/polyml-r1848
exec_prefix=${prefix}
bindir=${exec_prefix}/bin
libdir=${exec_prefix}/lib
includedir=${prefix}/include

Name: Poly/ML
Description: Poly/ML Standard ML Compiler
URL: http://www.polyml.org/
Version: 5.5.1
Requires: 
Libs: -L${libdir} -lpolymain -lpolyml -lpthread -lgmp -lm -ldl -lstdc++ -lgcc_s 
-lgcc
Libs.private:
Cflags: -I${includedir}
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Compiler in SVN

[Phil Clayton]

01/09/13 13:56, Rob Arthan wrote:


On 2 Aug 2013, at 13:21, David Matthews  wrote:


….
Please try out the SVN version and let me know how it goes.
…


I am grateful to Phil Clayton for pointing out a surprising performance issue 
that he noticed while building ProofPower. He found that the elapsed time for 
the build was over 3 minutes with the latest development version and less than 
1.5 minutes with version 5.5, even though the user and system times were about 
the same. I repeated the experiments and got similar results.

The problem is easy to reproduce. E.g., construct a source file perftest.ML 
containing the following:

structure PerfTest = struct
fun f x = x;
end;

Then run

time echo 'use"perftest.ML"' | poly

WIth 5.5, I get:

real0m0.016s
user0m0.003s
sys 0m0.010s

With the latest version (SVN rev 1838), I get:

real0m0.416s
user0m0.003s
sys 0m0.010s

The ProofPower build runs Poly/ML about 180 times. The results I am seeing are 
compatible with an overhead of about 400ms on each of these runs.


I think this delay is actually when exiting Poly/ML.  I have just this 
moment hit Ctrl+D to exit poly in a terminal but, as nothing happened 
immediately, I hit it again.  In fact, both key strokes registered and I 
zapped the terminal.  (It seems I really am that impatient!)


The delay can still be seen with just

  time echo | poly

Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Compiler in SVN

[Phil Clayton]

02/08/13 13:21, David Matthews wrote:

There's been quite a lot of work on the intermediate code optimiser
since the last release and it's largely been rewritten.  The main aim
has been to reduce the number of cases where heap storage was allocated
for argument tuples or closures.

There were a number of bugs that appeared during testing but I'm not
aware of anything outstanding.  Isabelle2013 and HOL4 both seem to build
successfully and there does seem to be some speed-up.  I'd like to
release this version in the next month or so but I'd like to fix any
other bugs that have been introduced.  Please try out the SVN version
and let me know how it goes.  Don't forget that after the configure and
make steps you need to run "make compiler" at least once and preferably
twice.  Otherwise you will still be using the 5.5 compiler.


I'm trying the latest revision in SVN (1838) and have found that after

  open PolyML;

entering either of the following causes a seg fault:

  stackTrace ();
  PolyML.stackTrace ();

The previous version that I tried - 1738 - didn't do this.

Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Incorrect floating point conversion

[Phil Clayton]

I can confirm that 1838 appears to fix this.  I now see the following 
responses, for x and y as before:


y < x; (* false *)
x < y; (* false *)

Phil


25/08/13 22:57, Phil Clayton wrote:

Interesting.  Things looked all right when I double-checked this:

val a = 0.999722444243843710864894092082977294921874
val m = 0.999722444243843710864894092082977294921875
val b = 0.999722444243843710864894092082977294921876
;
a < b; (* true *)
a < m; (* true *)
b < m; (* false *)
m < b; (* false *)

(* So we have a < m = b *)

However, when I tried your value for a, it doesn't work.  I think the
problem can be reduced to:

val x = 0.99972244424384371086489409208297729492187
val y = 0.999722444243843710864894092082977294921874
;
y < x; (* true *)

Phil


25/08/13 19:50, Florian Weimer wrote:

I noticed this:

Poly/ML 5.5.1 Development

val a = 0.99972244424384371086489409208297729492187;;

val a = 1.0: real

val b = 0.999722444243843710864894092082977294921876;;

val b = 1.0: real

a < b;;

val it = false: bool

a > b;;

val it = false: bool

So both values are equal according to Poly/ML.  But the correct
conversion for the first one is (in hexadecimal floating point
notation) 0x1.dp-1, and for the second
0x1.ep-1, so the values should be different.
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Incorrect floating point conversion

[Phil Clayton]

Interesting.  Things looked all right when I double-checked this:

val a = 0.999722444243843710864894092082977294921874
val m = 0.999722444243843710864894092082977294921875
val b = 0.999722444243843710864894092082977294921876
;
a < b; (* true *)
a < m; (* true *)
b < m; (* false *)
m < b; (* false *)

(* So we have a < m = b *)

However, when I tried your value for a, it doesn't work.  I think the 
problem can be reduced to:


val x = 0.99972244424384371086489409208297729492187
val y = 0.999722444243843710864894092082977294921874
;
y < x; (* true *)

Phil


25/08/13 19:50, Florian Weimer wrote:

I noticed this:

Poly/ML 5.5.1 Development

val a = 0.99972244424384371086489409208297729492187;;

val a = 1.0: real

val b = 0.999722444243843710864894092082977294921876;;

val b = 1.0: real

a < b;;

val it = false: bool

a > b;;

val it = false: bool

So both values are equal according to Poly/ML.  But the correct
conversion for the first one is (in hexadecimal floating point
notation) 0x1.dp-1, and for the second
0x1.ep-1, so the values should be different.
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] suppressing compiler output

[Phil Clayton]

David,

Thanks for the explanation in your previous message.  I was wrong to 
think that the linking method used to build Poly/ML fixes the way 
Poly/ML-based applications are linked.  I must have been getting the gcc 
flags wrong when I was trying this a few years ago.  Most likely, it was 
just the absence/presence of the dynamic libraries due to Poly/ML 
configure flags that actually caused what I saw.


On 15/04/13 12:17, David Matthews wrote:

On 12/04/2013 12:54, David Matthews wrote:

Based on this, I think there would be a case for setting the default for
Poly/ML to be --disable-shared so that producing the dynamic version
requires an explicit option.


I've now committed this change.  The default is now not to build the
shared library but that can be overridden with --enable-shared.  Like
any change in SVN it's always provisional so it can be reverted if
necessary.  I'd like feedback either for or against.


The main downside that I can see with this approach is that the SO files 
are not built or installed.  Therefore, with a standard installation, it 
would not be possible for a Poly/ML-based application to choose whether 
to link dynamically or statically to the Poly/ML libs.


Now that I have had a chance to play around, dropping the SO files seems 
a little drastic to get polyc to link statically, so avoid the 
LD_LIBRARY_PATH issue.  I found that replacing (both occurrences of)


  -L${LIBDIR} -lpolymain -lpolyml

in polyc with

  ${LIBDIR}/libpolymain.a ${LIBDIR}/libpolyml.a

effected static linking even when Poly/ML was built with 
--enable-shared.  In fact only libpolyml needs changing, i.e.


  -L${LIBDIR} -lpolymain ${LIBDIR}/libpolyml.a

suffices, because libpolymain has only a static library.

Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] suppressing compiler output

[Phil Clayton]

On 11/04/13 16:11, David Matthews wrote:

On 11/04/2013 11:44, Makarius wrote:

On Thu, 11 Apr 2013, David Matthews wrote:


I misunderstood the motivation for polyc.  I thought that it was to
allow those without compiling/linking knowledge to easily build
executables, i.e. to de-skill the process.  Whilst such users may
realize that

   ./configure --prefix 

requires

   PATH=${PATH}:${bindir}

they would not realize that they need (assuming no super-user
privileges)

   LD_LIBRARY_PATH=${LD_LIBRARY_PATH}:${libdir}


I just wonder how common that case is.


Perhaps I'm wrong.  I guess if there was a simple, portable way of
sorting out the paths I'd consider it.


Maybe this is just something to be prominently documented in 
installation instructions!


I am also wondering whether libtool helps.  I know very little about it 
though.




 From some of the comments on this thread I had the idea that there were
potential users of Poly/ML out there who were put off by the
read-eval-print-loop.  After all, that isn't the way most other
programming languages/implementations work.  Having the --script option
allows those used to scripting to code something up quickly so that's
one group catered for.  Another group of potential users are those used
to the compile-link-execute model and that was the group I was trying to
target with the polyc script.


Understand.  I think I probably came up with a different group based on 
what I thought a Python programmer may typically know.  I don't have any 
experience with Python though nor any Python compilers (if such things 
exists).




The most elementary wrapper script for standalone ("portable") Poly/ML
directories is included in the attachment.  The real one for Isabelle is
more advanced.  Next time I will consider "./configure
--disable-shared", which I did not know before.


I wonder if --disable-shared should be the default with ./configure.  It
would solve a lot of these problems.  I can see that packagers who are
going to build a package to install to the standard location would want
to build the shared library but users building a stand-alone system
probably don't want it.  If you're only building "poly" anyway there's
no saving by having libpolyml as a separate library.


If, in future, people are building Poly/ML-based applications, I think 
it would be preferable for the default to be dynamic.  For example, I 
have just tried building the (SML!) GTK+ Hello World demo: the 
executable is much larger with static linking (768k with -ggdb, 560k 
stripped) than with dynamic linking (160k, 148k).


The default linking method is quite a significant decision because, if I 
understand correctly, it fixes the way Poly/ML-based applications are 
linked, i.e. it is not possible to choose the linking method (to 
Poly/ML) when building a Poly/ML-based application.  Is that correct? 
(I am intrigued to know why.)


Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] suppressing compiler output

[Phil Clayton]

On 09/04/13 11:28, David Matthews wrote:

On 08/04/2013 21:22, Phil Clayton wrote:

On 08/04/13 12:21, David Matthews wrote:
I have found something called config.rpath which seems to be part of the
GNU portability library.  This appears to calculate potentially useful
values for passing rpath to linkers.  acl_cv_hardcode_libdir_flag_spec
may of use - I don't know.  Nor do I know how you would go about using
it!

Alternatively, LD_RUN_PATH could be set for the link command.  Although
probably benign if unsupported, I don't know how portable it is to other
platforms.

Presumably I am experiencing this linker path issue because I have
installed Poly/ML to a non-standard location(?)  In such a set up, maybe
it is reasonable to require LD_LIBRARY_PATH to be set for executables
from polyc.  Perhaps it is worth considering what would users expect if
the compiled executables are copied to different systems.


I found some references to rpath in the porting guidelines for Debian.
The general recommendation was to avoid it because while it would work
for one library it might have an adverse effect if an application used
other shared libraries.


Yes, it appears people feel quite strongly about that, so probably best 
avoided!




Is there a reason you're installing to a "non-standard location"?


I install to /opt/polyml/polyml-${version} to allow multiple versions to 
coexist, for at least two reasons:
1. To quickly allow (performance) regression tests to be performed 
between versions of Poly/ML.
2. I have needed a pre-release due to an enhancement not yet available 
in the main release.  (For example, a while ago I was making use of an 
FFI enhancement before 5.5 was released.)

Other people may have other reasons for multiple versions.



In
Linux that basically means "not listed in /etc/ld.so.conf" so the
simplest solution is to add your location there.


You're right, I should really do that.  In fact, on Fedora, I would add 
the file

  /etc/ld.so.conf.d/polyml-${version}.conf
that contains the libdir.



Another solution is to
use static linking so you don't have to worry about it.  Use ./configure
--disable-shared.

>

My idea with the polyc script was to try to make it easy for people
familiar with C to be able to try out Poly/ML.  Of course it may evolve
beyond that but for the moment I want to keep it simple.


I misunderstood the motivation for polyc.  I thought that it was to 
allow those without compiling/linking knowledge to easily build 
executables, i.e. to de-skill the process.  Whilst such users may 
realize that


  ./configure --prefix 

requires

  PATH=${PATH}:${bindir}

they would not realize that they need (assuming no super-user privileges)

  LD_LIBRARY_PATH=${LD_LIBRARY_PATH}:${libdir}

Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] suppressing compiler output

[Phil Clayton]

On 08/04/13 12:21, David Matthews wrote:

3. In the polyc that was built, I see
   EXTRA=" "
As it stands, the Poly/ML lib directory is not added to the linker path
so I presume (for Linux) that this was meant to contain something like
   -Wl,-rpath ${LIBDIR}
so that it is not necessary to set LD_LIBRARY_PATH before running the
executable.


I really had in mind the Windows build which needs a few extra options.
  I hadn't thought of "rpath".  My only concern would be if there are
linkers around that don't support it.  There doesn't seem to be a simple
way in autoconf to find out if the linker supports it.


I have found something called config.rpath which seems to be part of the 
GNU portability library.  This appears to calculate potentially useful 
values for passing rpath to linkers.  acl_cv_hardcode_libdir_flag_spec 
may of use - I don't know.  Nor do I know how you would go about using it!


Alternatively, LD_RUN_PATH could be set for the link command.  Although 
probably benign if unsupported, I don't know how portable it is to other 
platforms.


Presumably I am experiencing this linker path issue because I have 
installed Poly/ML to a non-standard location(?)  In such a set up, maybe 
it is reasonable to require LD_LIBRARY_PATH to be set for executables 
from polyc.  Perhaps it is worth considering what would users expect if 
the compiled executables are copied to different systems.


Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] suppressing compiler output

[Phil Clayton]

polyc looks very useful.  I just tried it out for 1723 and noticed a few 
things:


1. -L${LIBDIR} is missing in the case when -o is not specified, causing 
the error:

  /usr/bin/ld: cannot find -lpolymain
  /usr/bin/ld: cannot find -lpolyml
  collect2: ld returned 1 exit status

2. The Makefile.am has
  EXTRA=\"$(EXTRALDFLAGS)\"
which should, perhaps, be
  EXTRALDFLAGS=\"$(EXTRALDFLAGS)\"
as EXTRALDFLAGS is used inside the script.

3. In the polyc that was built, I see
  EXTRA=" "
As it stands, the Poly/ML lib directory is not added to the linker path 
so I presume (for Linux) that this was meant to contain something like

  -Wl,-rpath ${LIBDIR}
so that it is not necessary to set LD_LIBRARY_PATH before running the 
executable.


Phil


On 05/04/13 13:24, David Matthews wrote:

I've added a "polyc" script that is generated from the build process.
The idea of this is to provide the similar sort of functionality that
users of C expect from the "cc" command.  It's very simple at the moment
and is limited to a few options.  It compiles an ML source file and
exports the "main" function.  The -o option specifies where the
executable is to be placed, defaulting to a.out on Unix.

david@dunedin:~$ cat hello.ML
fun main() = print "Hello World\n";
david@dunedin:~$ polyc hello.ML -o hello
david@dunedin:~$ ./hello
Hello World

The script includes the path names to where the poly binary and the
libraries will be installed so it's not possible to run it within the
build directory.
David
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml



___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] suppressing compiler output

[Phil Clayton]

I'm not sure what your exact requirements are but a possible solution 
may be to create an executable.  Then compile-time output would not be 
mixed with run-time output.  It's straightforward: wrap everything into 
a toplevel function and export that, e.g.


[pclayton@rizzo ~]$ cat hello.sml
fun main () = print "Hello World!\n";
PolyML.export ("hello", main);

Compile:
  cat hello.sml | poly

Link:
  POLYHOME=/opt/polyml/polyml-5.5  # your Poly/ML installation
  POLYLIB=${POLYHOME}/lib
  LD_RUN_PATH=${POLYLIB}:${LD_RUN_PATH} cc -ggdb -o hello -L${POLYLIB} 
-lpolymain -lpolyml hello.o


Run:
  ./hello


Phil


On 28/03/13 20:49, Gergely Buday wrote:

Hi,

I would like to feed an sml program into poly from standard input:

$ cat hello.sml |poly
Poly/ML 5.4.1 Release

# Hello World!val it = (): unit


Is it possible to use this so that the compiler itself does not print
anything? I have found poly -q which does not print the release
message but that still prints all the rest.

- Gergely
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] use depth

[Phil Clayton]

On 24/02/13 02:40, Lucas Dixon wrote:

How about:

val use_depth = ref 0;
fun use s= (use_depth := (!use_depth) + 1; PolyML.use s; use_depth :=
(!use_depth) - 1);


Presumably you'd want to handle any exceptions raised by PolyML.use too 
(and reraise them after decrementing use_depth).


Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Type inference issue with phantom types

[Phil Clayton]

On 06/09/12 11:19, David Matthews wrote:

On 05/09/2012 18:07, David Matthews wrote:

On 05/09/2012 14:27, Phil Clayton wrote:

I probably spoke a bit too soon here.  After more interactive use, it
appears that records and tuples can be expanded one level in the types
printed back.  This can make types much harder to read which may be an
issue for those using an interactive session to e.g. inspect expression
types by evaluating fragments of code.  With the example at the end, 5.4
prints back

   val nearest = fn: point -> point list1 -> real * point

which is fairly self-explanatory, whereas r1581 prints back

   val nearest = fn:
  real * real -> (real * real) * (real * real) list -> real * (real
* real)

I can't see a way to fix the bug and still keep the old printing of
types with abbreviations.  The problem is that the language definition
does not consider printing at all.


Well, after thinking some more about it overnight I did realise there
was an alternative fix for the bug that kept the old printing.  I've
committed this and now the old printing has been restored.


Thanks for this.  I have to say the old printing makes interactive work 
easier.  Also, this update reduces time to compile the auto-generated 
libraries of function bindings - 7.2s vs 8.6s.




I was actually on the point of releasing 5.5 and I've already rebuilt
the compilers.  I can see that it would be preferable to include this
latest change in the 5.5 release especially if you are processing the
output automatically.  I might just hold off a little bit longer.


And even if output isn't being processed automatically, the more 
succinct compiler output generally makes life easier.  I'll continue 
with r1592 and see how it goes.  I haven't found it to be worse than 
r1591 in any respect yet.


Phil

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml