Re: [polyml] Size of stand-alone executables

[Rob Arthan]

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] Problem linking .o file

[Rob Arthan]

I am trying to reproduce an issue reported by a ProofPower user.
I am not getting as far as he did. I am seeing the following,
when I try to produce an executable from a .o file created
using PolyML.export.

rda]- polyc -o main1 main1.o
Undefined symbols for architecture x86_64:
  "_PolyFFIGeneral", referenced from:
  anon in main1.o
  "_PolyNetworkGeneral", referenced from:
  anon in main1.o
  "_PolyNetworkGetHostByAddr", referenced from:
  anon in main1.o
  "_PolyNetworkGetHostByName", referenced from:
  anon in main1.o
  "_PolyTimingGeneral", referenced from:
  anon in main1.o
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)

This is with Poly/ML 5.8.2 running on MacOS Catalina 10.15.7.
polyc successfully builds an executable when I create a toy example,
but not for this .o file which contains most of a fairly large application.

Where am I going wrong?

Regards,

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

Re: [polyml] Problem with compact32bit

[Rob Arthan]

David,

Apologies! This was all down to a simple misunderstanding on my part. I hadn't
appreciated that --enable-compact32bit gives you 31-bit ints. My proof search
explores in excess of 2^32 blind alleys and it tries to count them. 

The confusion about Mac OS versions and lldb was caused by me doing the tests
with the compiler built with --enable-intinf-as-int as well as 
--enable-compact32bit.

Regards,

Rob.

> On 3 Apr 2019, at 18:41, Rob Arthan  wrote:
> 
> David,
> 
> 
>> On 2 Apr 2019, at 11:34, David Matthews  
>> wrote:
>> 
>> Rob,
>> Have you tried using the Poly debugger?
>> PolyML.Compiler.debug := true;
>> open PolyML.Debug;
>> breakEx Overflow;
>> then compile your code.
>> 
>> This won't help if the problem is a code-generator bug because adding the 
>> debugging code may well change the code and avoid the bug but if it's a 
>> library function this may narrow it down.
>> 
> It ran to completion after about 6 hours. So compiling for debugging does 
> avoid the bug. Is there anything
> I can do with gdb? I’ll have a think about instrumenting my code with 
> exception handlers to try to pinpoint
> the problem.
> 
> Regards,
> 
> Rob.
> 
>> Regards,
>> David
>> 
>> On 31/03/2019 13:31, Rob Arthan wrote:
>>> I have done some further experiments. I can reproduce the problem on
>>> Mac OS Mojave 10.14.4
>>> Fedora 24
>>> Kubuntu 18.10
>>> The above were all run an iMac using VirtualBox VMs for the Linux
>>> distros.
>>> I also tried running poly under a debugger and found that the problem
>>> doesn’t occur when run under lldb on Mac OS Mojave. It does occur
>>> when run under gdb on the two Linux distros.
>>> Regards,
>>> Rob
>>>> On 31 Mar 2019, at 00:04, Rob Arthan  wrote:
>>>> 
>>>> The tarball did survive the mailing list and I've just unpacked it and 
>>>> tried
>>>> the test on my MacBook. The problem does not occur on a MacBook
>>>> running Mac OS High Sierra 10.13.6 but does occur on an iMac
>>>> running Mac OS Mojave 10.14.4.
>>>> 
>>>> I'll try it on some Linux VMs tomorrow.
>>>> 
>>>> Regards,
>>>> 
>>>> Rob.
>>>> 
>>>>> On 30 Mar 2019, at 16:50, Rob Arthan  wrote:
>>>>> 
>>>>> I was doing some performance comparisons and found what looks like a bug 
>>>>> in Poly/ML
>>>>> when compiled with —enable-compact32bit. The problem is that ML code that
>>>>> runs to completion when compiled to use native 64 bit addresses, raises 
>>>>> Overflow
>>>>> when compiled to 32 bit addressing. The code is a lengthy proof search
>>>>> that explores in excess of 4,000,000,000 blind alleys. It takes about
>>>>> 10 to 20 minutes to find the proof when using 64 bit addressing
>>>>> and it takes 2 or 3 minutes before it raises Overflow when using 32 bit 
>>>>> addressing.
>>>>> 
>>>>> I don’t really know where to start with narrowing the problem down. I’ve 
>>>>> attached a tarball
>>>>> containing cutdown source that demonstrates the problem, but the mailing 
>>>>> list
>>>>> software will likely strip it off, hence CC to David.
>>>>> 
>>>>> 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

Re: [polyml] Problem with compact32bit

[Rob Arthan]

I have done some further experiments. I can reproduce the problem on

Mac OS Mojave 10.14.4
Fedora 24
Kubuntu 18.10

The above were all run an iMac using VirtualBox VMs for the Linux
distros.

I also tried running poly under a debugger and found that the problem
doesn’t occur when run under lldb on Mac OS Mojave. It does occur
when run under gdb on the two Linux distros.

Regards,

Rob

> On 31 Mar 2019, at 00:04, Rob Arthan  wrote:
> 
> The tarball did survive the mailing list and I've just unpacked it and tried
> the test on my MacBook. The problem does not occur on a MacBook
> running Mac OS High Sierra 10.13.6 but does occur on an iMac
> running Mac OS Mojave 10.14.4.
> 
> I'll try it on some Linux VMs tomorrow.
> 
> Regards,
> 
> Rob.
> 
>> On 30 Mar 2019, at 16:50, Rob Arthan  wrote:
>> 
>> I was doing some performance comparisons and found what looks like a bug in 
>> Poly/ML
>> when compiled with —enable-compact32bit. The problem is that ML code that
>> runs to completion when compiled to use native 64 bit addresses, raises 
>> Overflow
>> when compiled to 32 bit addressing. The code is a lengthy proof search
>> that explores in excess of 4,000,000,000 blind alleys. It takes about
>> 10 to 20 minutes to find the proof when using 64 bit addressing
>> and it takes 2 or 3 minutes before it raises Overflow when using 32 bit 
>> addressing.
>> 
>> I don’t really know where to start with narrowing the problem down. I’ve 
>> attached a tarball
>> containing cutdown source that demonstrates the problem, but the mailing list
>> software will likely strip it off, hence CC to David.
>> 
>> 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

Re: [polyml] Problem with compact32bit

[Rob Arthan]

The tarball did survive the mailing list and I've just unpacked it and tried
the test on my MacBook. The problem does not occur on a MacBook
running Mac OS High Sierra 10.13.6 but does occur on an iMac
running Mac OS Mojave 10.14.4.

I'll try it on some Linux VMs tomorrow.

Regards,

Rob.

> On 30 Mar 2019, at 16:50, Rob Arthan  wrote:
> 
> I was doing some performance comparisons and found what looks like a bug in 
> Poly/ML
> when compiled with —enable-compact32bit. The problem is that ML code that
> runs to completion when compiled to use native 64 bit addresses, raises 
> Overflow
> when compiled to 32 bit addressing. The code is a lengthy proof search
> that explores in excess of 4,000,000,000 blind alleys. It takes about
> 10 to 20 minutes to find the proof when using 64 bit addressing
> and it takes 2 or 3 minutes before it raises Overflow when using 32 bit 
> addressing.
> 
> I don’t really know where to start with narrowing the problem down. I’ve 
> attached a tarball
> containing cutdown source that demonstrates the problem, but the mailing list
> software will likely strip it off, hence CC to David.
> 
> 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] Building an executable that runs the read-eval-print loop

[Rob Arthan]

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

Re: [polyml] Testing Poly/ML 5.8

[Rob Arthan]

David,

After the "git pull", I've rebuilt Poly/ML and ProofPower and had no problems 
with any
combination of --enable-intinf-asint, --enable-compact32bit and MacOS v. Fedora.

Poly/ML compiled with --enable-compact32bit gives me  5-8% improvement in 
execution times
and 30-40% improvement in the size of saved states on some typical ProofPower 
examples.
So that's a worthwhile improvement - many thanks to you and Makarius!

Regards,

Rob.


> On 10 Mar 2019, at 16:30, David Matthews  
> wrote:
> 
> Rob, Phil and everyone else,
> 
> I'm in the process of putting together the 5.8 release and as part of that 
> I've pushed an updated pre-built compiler for X64/32 for Linux, Mac OS etc.  
> That means that for that platform only, for the moment, it is no longer 
> necessary to run "make compiler", although it won't hurt.  It should no 
> longer produce the assertion fault, so if it does this is a different bug.  
> To be absolutely sure please run "make distclean" before trying "git pull".
> 
> The pre-built compilers (in the "imports" directory) are essentially binary 
> blobs although they are encoded as text.  Since they are large and any update 
> results in a major change to the text I try to avoid updating them more often 
> than once for each release.
> 
> 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] Testing Poly/ML 5.8

[Rob Arthan]

David,

Thanks. I've interleaved my replies below.

> On 9 Mar 2019, at 16:59, David Matthews  
> wrote:
> 
> Rob,
> Thanks for testing this and your comments.  I'm replying to your individual 
> comments below.
> 
> On 09/03/2019 16:11, Rob Arthan wrote:
>> 1) The configure script doesn’t validate an option beginning "—enable-“.
>> So I didn’t notice that I’d mistyped —enable-compact32bit until I realised 
>> that
>> I was getting executables and saved states with almost identical sizes.
>> (I appreciate that this may be an autoconfig thing that you can’t control.)
> 
> Yes, I seem to remember that it is and that it wasn't possible to avoid it 
> because there is a separate "configure" for libffi.

OK. Is there a way of telling whether poly has been built with 
--enable-compact32bit? (So you can check whether
you got what you wanted.)

> 
>> 2) If you build Poly/ML with —disable-compact32bit and then try to build it
>> with —enable-compact32 without doing “make clean", it will fail during the 
>> “make install” step like this:
>> Making install in .
>> ./polyimport  polytemp.txt -I . < ./exportPoly.sml
>> Assertion failed: (j >= -(((POLYSIGNED)0x80 << 
>> (POLYSIGNED)(8*(sizeof(PolyWord)-1) -1)) -1)-1 && j <= (((POLYSIGNED)0x80 << 
>> (POLYSIGNED)(8*(sizeof(PolyWord)-1) -1)) -1)), function GetValue, file 
>> pexport.cpp, line 461.
>> /bin/sh: line 1: 46725 Abort trap: 6   ./polyimport polytemp.txt -I 
>> . < ./exportPoly.sml
>> make[1]: *** [polyexport.o] Error 134
>> make: *** [install-recursive] Error 1
>> Doing “make clean” solves this problem.
> 
> I would always run "make distclean" before rerunning configure. Basically, 
> what is happening is that it is picking up the wrong pre-built compiler.

I'll remember to do that in future.
 
> 
>> 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.

Regards,

Rob.

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

Re: [polyml] Testing Poly/ML 5.8

[Rob Arthan]

David,

I’ve been trying building and testing ProofPower on the various combinations of
MacOS Mojave v. Linux Fedora 24, —enable-compact32bit v. —disable-compact32bit
and —enable-intinf-asint and —disable-intinf-asint and have a few observations.

1) The configure script doesn’t validate an option beginning "—enable-“.
So I didn’t notice that I’d mistyped —enable-compact32bit until I realised that
I was getting executables and saved states with almost identical sizes.
(I appreciate that this may be an autoconfig thing that you can’t control.)

2) If you build Poly/ML with —disable-compact32bit and then try to build it
with —enable-compact32 without doing “make clean", it will fail during the 
“make install” step like this:

Making install in .
./polyimport  polytemp.txt -I . < ./exportPoly.sml
Assertion failed: (j >= -(((POLYSIGNED)0x80 << 
(POLYSIGNED)(8*(sizeof(PolyWord)-1) -1)) -1)-1 && j <= (((POLYSIGNED)0x80 << 
(POLYSIGNED)(8*(sizeof(PolyWord)-1) -1)) -1)), function GetValue, file 
pexport.cpp, line 461.
/bin/sh: line 1: 46725 Abort trap: 6   ./polyimport polytemp.txt -I . < 
./exportPoly.sml
make[1]: *** [polyexport.o] Error 134
make: *** [install-recursive] Error 1

Doing “make clean” solves this problem.

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.

I can attempt to give you cut-down code to reproduce (3) and (4) if the above
error messages don’t give you enough of a clue.

Regards,

Rob.


> On 21 Feb 2019, at 12:44, David Matthews  
> wrote:
> 
> The current version of Poly/ML is approaching the point of creating a new 
> release, 5.8.  Makarius has run a lot of tests with Isabelle and various bugs 
> have been fixed.  This has mainly affected the 32-bit object ID version for 
> 64-bits but some of the fixes will also have affected the native-address 
> versions.
> 
> 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.
> 
> 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

[Rob Arthan]

David,

> On 26 Nov 2017, at 09:14, David Matthews  
> wrote:
> 
> I don't see that myself but it's certainly possible.  A delay followed by 
> Error 1 suggests that it is relying on the crow-bar thread to stop. The fact 
> that this only happens on some platforms suggests a race condition.
> 
> In view of this I'm inclined to release the version without this change 
> (44b7b88) as 5.7.1 and investigate the problem later.

i’ve no objection to that as far as ProofPower is concerned, because the 
situation in the ProofPower build process where there a lots of little runs of 
Poly/ML is completely untypical of normal use of ProofPower. In normal use, a 
typical session is either an interactive session lasting hours or even days or 
a batch replay of a proof script that will take 10 seconds or more.

Regards,

Rob.
___
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

[Rob Arthan]

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.

> On 25 Nov 2017, at 13:08, David Matthews <david.matth...@prolingua.co.uk> 
> wrote:
> 
> That's odd.  When I run it it exits immediately.  Exactly what platform are 
> you running it on?
> 
> When a thread calls OS.Process.exit, which is what happens when end-of-stream 
> is detected by the compiler, it marks all the other threads to exit and then 
> starts a "crow-bar" thread.  That waits for 40s (it was 20s in 5.7 and 
> earlier) which forces an process exit if the other threads haven't finished 
> in that time.  There were issues with race conditions in earlier versions of 
> Poly/ML which meant that sometimes the main thread would not correctly detect 
> that the threads had exited but I thought all that had been fixed.
> 
> Regards,
> David
> 
> On 25/11/2017 09:24, Phil Clayton wrote:
>> 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
>>> 
>>> real1m37.832s
>>> user1m33.262s
>>> sys0m15.108s
>>> 
>>> 
>>> Poly/ML 5.7.1g44b7b88
>>> 
>>> real3m34.839s
>>> user1m38.777s
>>> sys0m19.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 
>>>>>> <david.matth...@prolingua.co.uk> 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.

Re: [polyml] Approaching release of 5.7.1

[Rob Arthan]

David,

I've done my other tests and it's working fine. I have just a couple of 
observations.

1) On Mac OS (and presumably any system with clang as the C compiler), the
configure script gives a warning. (I just let this go by and nothing seems to 
have gone wrong.)

checking for C compiler vendor... clang


* WARNING: Don't know the best CFLAGS for this system  *
* Use ./configure CFLAGS=... to specify your own flags *
* (otherwise, a default of CFLAGS=-O3 will be used)*


2) The configure script doesn't complain about unrecognised options beginning
with --enable. E.g,

configure --enable-garbage

just carries on. This fooled me when I managed to misspell 
--enable-intinf-as-int.
If this is forced upon you by autoconfig, then so be it.

Many thanks for your rapid turnround with the earlier problems.
Your great work on Poly/ML is very much appreciated.

Regards,

Rob.

___
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'

[Rob Arthan]

Roní,

If you don’t want to upgrade to version 5.7, you can work around the problem 
like this:

val oldMaxInlineSize = !PolyML.Compiler.maxInlineSize;
val _ = PolyML.Compiler.maxInlineSize := 1;
fun ints(n) = Link(n + 1, ints);
val _ = PolyML.Compiler.maxInlineSize := oldMaxInlineSize;

Aside to David: it can take quite a while for new releases to Poly/ML to make 
it into the
various package managers that people like to use. E.g., MacPorts is still on 
version 5.5.2.

Regards,

Rob.

> On 5 Jul 2017, at 08:37, David Matthews  
> wrote:
> 
> I think you must be using an older version of Poly/ML.  There was a bug in 
> 5.6 and earlier versions that caused the optimiser to loop but that has been 
> fixed in the current version, 5.7.
> 
> Regards,
> David
> 
> On 04/07/2017 17:40, Roní Gonçalves wrote:
>> Actually, I have mistyped the definition of chain before. I am sorry. The
>> definitions are:
>> datatype chain = Link of int * (int -> chain);
>> fun ints(n) = Link(n + 1, ints);
>> And for these definitions, Poly/ML does not work, but SML/NJ does.
>> Best regards,
>> Roní Gonçalves.
>> 2017-07-04 13:37 GMT-03:00 Roní Gonçalves :
>>> Hello, everyone!
>>> 
>>> I am reading The Little MLer from Matthias Felleisen and Daniel Friedman
>>> using Poly/ML interpreter.
>>> 
>>> In chapter 7, whe have some sort of stream implementation:
>>> 
>>> datatype chain = Link of datatype chain = Link of int * (int -> chain);
>>> fun ints(n) = Link(n + 1, ints);
>>> 
>>> When I try to define the function ints in Poly/ML 5.6 interpreter, it does
>>> not work, it runs forever. But when I write the same code in SML/NJ v110.78
>>> interpreter, things work. Is this difference in their behaviors a bug or is
>>> it normal or expected?
>>> 
>>> Best regards,
>>> 
>>> Roní Gonçalves.
>>> 
>> ___
>> 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] Update to code-generator and run-time system interface

[Rob Arthan]

> On 20 Oct 2016, at 18:01, David Matthews <david.matth...@prolingua.co.uk> 
> wrote:
> 
> On 20/10/2016 12:14, Rob Arthan wrote:
>> During interactive development of a proof script it is usual to try
>> things out repeatedly with frequent evaluations of minor variants of
>> an attempted proof step until you find one that works. It is ls also
>> perfectly possible for a user to develop a ProofPower database the
>> way people develop spreadsheets and SQL databases, incrementally
>> adding things over a prolonged period of time. It is not clear to me
>> how bad the impact would be in these use cases.  Is there a way to
>> find out how much memory is occupied by compiled code? If so, then I
>> could try some experiments to quantify the impact.
>> 
>>> On 19 Oct 2016, at 12:34, David Matthews
>>> <david.matth...@prolingua.co.uk> wrote: The new mechanism for
>>> handling pieces of code deals with most of the issues apart from
>>> the question of garbage collection.  I was really trying to get a
>>> feeling for how serious this was.  From the comments on the mailing
>>> list it looks as though this is something that is wanted so I'll
>>> try and see if I can find a solution.
>> 
>> 
>> And thank you for thinking of us!
>> 
>> If it makes the solution easier, I don’t think there is any need to
>> include garbage collection for code in the on-the-fly garbage
>> collection. I think it would be fine to implement it either as an ML
>> function on its own or built into PolyML.SaveState.saveChild (and
>> friends) and PolyML.export.
>> 
> 
> Just one point.  There is only a leak for redefinitions of functions while 
> they are in local memory.  If you load a saved state, redefine a function in 
> it and then save a new state then the old code will be replaced with the new 
> code, just as before.
> 

That sounds very promising.  Is it also the case that space for code that was 
only generated
to calculate the value of a top level binding will be reclaimed when you save 
state or
export an object file? E.g., the code generated for the right-hand side of the 
following binding.

val fact10 = let fun f i = if i <= 0 then 1 else i * f(i-1) in f 10 end;

If so, then the only one of my use cases that might have a problem is
interactive development.  I strongly suspect this is not going to be significant
in practice. As I said, if there is a way to see how much memory is occupied
by compiled code, I could do some experiments to see if my suspicion is correct.

Regards,

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

Re: [polyml] Update to code-generator and run-time system interface

[Rob Arthan]

> On 17 Oct 2016, at 20:38, Makarius  wrote:
> 
> On 20/09/16 14:15, David Matthews wrote:
>> ...
>> Currently, there is a leak because each top-level expression is compiled
>> down to machine code even though the code is only executed once.  My
>> plan is to avoid that by interpreting the top-level rather than fully
>> compiling it.
> 
> ...
> I do wonder how the classic LCF-style proof assistants would cope with
> that, notably ProofPower and HOL4.

Thanks for thinking of us!

The ProofPower model is of incremental development of a database
containing both data and functions to process it held in a persistent object 
store
as provided in Poly/ML by the PolyML.SaveState structure.  A great deal of
the data will comprise syntax trees (proved theorems) that have each been 
calculated
by evaluating a large ML expression (a proof) that is executed just once.

Most users will keep all the source files they used to build a database and will
be prepared to rebuild from scratch quite frequently. I suspect that this use 
case won’t
be badly affected by the leak - presumably the leak will be roughly 
proportional to
the size of the proof scripts (and so it will be megabytes rather than 
gigabytes).

During interactive development of a proof script it is usual to try things out
repeatedly with frequent evaluations of minor variants of an attempted proof
step until you find one that works. It is ls also perfectly possible for a user 
to develop
a ProofPower database the way people develop spreadsheets and SQL databases,
incrementally adding things over a prolonged period of time. It is not clear to 
me
how bad the impact would be in these use cases.  Is there a way to find out how 
much
memory is occupied by compiled code? If so, then I could try some experiments 
to quantify the impact.

> On 19 Oct 2016, at 12:34, David Matthews  
> wrote:
> The new mechanism for handling pieces of code deals with most of the issues 
> apart from the question of garbage collection.  I was really trying to get a 
> feeling for how serious this was.  From the comments on the mailing list it 
> looks as though this is something that is wanted so I'll try and see if I can 
> find a solution.


And thank you for thinking of us!

If it makes the solution easier, I don’t think there is any need to include 
garbage
collection for code in the on-the-fly garbage collection. I think it would be 
fine
to implement it either as an ML function on its own or built into
PolyML.SaveState.saveChild (and friends) and PolyML.export.

Regards,

Rob.

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

Re: [polyml] Update to code-generator and run-time system interface

[Rob Arthan]

David,


> On 20 Sep 2016, at 19:00, David Matthews <david.matth...@prolingua.co.uk> 
> wrote:
> 
> Rob,
> The complication is that the pretty print datatype is essentially shared 
> between the compiler and the compiled code.  If the compiler has been 
> compiled with a different length of int from the user code there's the 
> potential for confusion.  The compiler builds default print functions for 
> types and I was trying to ensure that both sides had the same understanding.
> 
> It may be that it isn't a problem.  I'll think about this some more.

I have now tried a ProofPower build with a work-around for this and everything 
is working.
It would be nice not to have to work around this. As things stand, the PolyML 
structure contains
a rather odd mixture of int and FixedInt.int when you compile with 
—enable-intinf-as-int.
E.g., compare prettyPrint with addPrettyPrinter.

> 
> The "datatype" definition in PRETTYSIG.sml is commented out.  The 
> "constructors" actually use FixedInt.int.
> 

I didn’t notice that!

Regards,

Rob.

> Regards,
> David
> 
> On 20/09/2016 16:40, Rob Arthan wrote:
>> David,
>> 
>> After using the patch in my last post to enable me to build poly, ProofPower 
>> now builds
>> and behaves as I would expect it to when compiled without 
>> —enable-intinf-as-int.
>> When I compile with —enable-intinf-as-int I get a problem because the type of
>> PolyML.PrettyBlock has a FixedInt in it where it had just in in version 5.6.
>> 
>>> PolyML.PrettyBlock;
>> val it = fn:
>>   FixedInt.int * bool * PolyML.context list * PolyML.pretty list ->
>> PolyML.pretty
>> 
>> Is that intended? I can’t understand why it has happening because the 
>> datatype
>> declaration in PRETTYSIG.sml uses int. If this is intended then I can work 
>> round
>> it, but it would be nice not to have to.
>> 
>> 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] Update to code-generator and run-time system interface

[Rob Arthan]

Makarius,

> On 20 Sep 2016, at 16:42, Makarius <makar...@sketis.net> wrote:
> 
> On 20/09/16 16:50, Rob Arthan wrote:
>> 
>> I think this patch fixes it:
>> 
>> diff --git a/libpolyml/pexport.cpp b/libpolyml/pexport.cpp
>> index b03b1da..a9ebd2e 100644
>> --- a/libpolyml/pexport.cpp
>> +++ b/libpolyml/pexport.cpp
>> @@ -158,7 +158,7 @@ void PExport::printObject(PolyObject *p)
>> for (unsigned i = 0; i < ps->length; i++)
>> {
>> char ch = ps->chars[i];
>> -fprintf(exportFile, "%02x", ch);
>> +fprintf(exportFile, "%02x", ch & 0xff);
>> }
>> }
>> else
> 
> It seems to work, but it is unclear to me why.
> 
> A few lines before there is the following text:
> 
>/* See if the first word is a possible length.  The length
>   cannot be one because single character strings are
>   represented by the character. */
>/* This is not infallible but it seems to be good enough
>   to detect the strings. */
>POLYUNSIGNED bytes = length * sizeof(PolyWord);
>if (length >= 2 && ...)
> 
> It looks like it requires further update.
> 

I think length is the length of the PolyObject representing the string
while ps->length is the length of the string and will have been 1 in
the call that caused the problem. I suspect the comments
and possibly the test on length are redundant.

Regards,

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

Re: [polyml] Update to code-generator and run-time system interface

[Rob Arthan]

David,

After using the patch in my last post to enable me to build poly, ProofPower 
now builds
and behaves as I would expect it to when compiled without —enable-intinf-as-int.
When I compile with —enable-intinf-as-int I get a problem because the type of
PolyML.PrettyBlock has a FixedInt in it where it had just in in version 5.6.

> PolyML.PrettyBlock;
val it = fn:
   FixedInt.int * bool * PolyML.context list * PolyML.pretty list ->
 PolyML.pretty

Is that intended? I can’t understand why it has happening because the datatype
declaration in PRETTYSIG.sml uses int. If this is intended then I can work round
it, but it would be nice not to have to.

Regards,

Rob.

> On 20 Sep 2016, at 15:50, Rob Arthan <r...@lemma-one.com> wrote:
> 
> David, Makarius,
> 
> I think this patch fixes it:
> 
> diff --git a/libpolyml/pexport.cpp b/libpolyml/pexport.cpp
> index b03b1da..a9ebd2e 100644
> --- a/libpolyml/pexport.cpp
> +++ b/libpolyml/pexport.cpp
> @@ -158,7 +158,7 @@ void PExport::printObject(PolyObject *p)
> for (unsigned i = 0; i < ps->length; i++)
> {
> char ch = ps->chars[i];
> -fprintf(exportFile, "%02x", ch);
> +fprintf(exportFile, "%02x", ch & 0xff);
> }
> }
> else
> 
> Regards,
> 
> Rob.
> 
>> On 20 Sep 2016, at 15:04, Makarius <makar...@sketis.net> wrote:
>> 
>> On 20/09/16 14:16, David Matthews wrote:
>>>> 
>>>> Instead of creating a new singleton string each time, it would refer to
>>>> a vector of 256 pre-allocated values.
>>> 
>>> That seems a very good idea.  I've implemented it.
>> 
>> I've tried to compile this version d7b9234f2793 using configure
>> --enable-intinf-as-int, but it fails towards the end as follows:
>> 
>> ./polyimport --intIsIntInf polytemp.txt -I . < ./exportPoly.sml
>> polyimport: pexport.cpp:728: bool PImport::DoImport(): Assertion `ch ==
>> '\n'' failed.
>> /bin/bash: line 1:   515 Aborted (core dumped)
>> ./polyimport --intIsIntInf
>> 
>> 
>>  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 mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Update to code-generator and run-time system interface

[Rob Arthan]

David, Makarius,

I think this patch fixes it:

diff --git a/libpolyml/pexport.cpp b/libpolyml/pexport.cpp
index b03b1da..a9ebd2e 100644
--- a/libpolyml/pexport.cpp
+++ b/libpolyml/pexport.cpp
@@ -158,7 +158,7 @@ void PExport::printObject(PolyObject *p)
 for (unsigned i = 0; i < ps->length; i++)
 {
 char ch = ps->chars[i];
-fprintf(exportFile, "%02x", ch);
+fprintf(exportFile, "%02x", ch & 0xff);
 }
 }
 else

Regards,

Rob.

> On 20 Sep 2016, at 15:04, Makarius  wrote:
> 
> On 20/09/16 14:16, David Matthews wrote:
>>> 
>>> Instead of creating a new singleton string each time, it would refer to
>>> a vector of 256 pre-allocated values.
>> 
>> That seems a very good idea.  I've implemented it.
> 
> I've tried to compile this version d7b9234f2793 using configure
> --enable-intinf-as-int, but it fails towards the end as follows:
> 
> ./polyimport --intIsIntInf polytemp.txt -I . < ./exportPoly.sml
> polyimport: pexport.cpp:728: bool PImport::DoImport(): Assertion `ch ==
> '\n'' failed.
> /bin/bash: line 1:   515 Aborted (core dumped)
> ./polyimport --intIsIntInf
> 
> 
>   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

Re: [polyml] Update to code-generator and run-time system interface

[Rob Arthan]

David,

I have just pulled get rev d7b9234f2793aef14b984ad808bbdfc6e1c59403 and get the 
following
when I do make compiler (after configure with no options other than 
—prefix=/usr/local/poly/dev):

Making all in libpolymain
make[3]: Nothing to be done for `all'.
Making all in .
./polyimport  polytemp.txt -I . < ./exportPoly.sml
Assertion failed: (ch == '\n'), function DoImport, file pexport.cpp, line 728.
/bin/sh: line 1: 98398 Abort trap: 6   ./polyimport polytemp.txt -I . < 
./exportPoly.sml
make[3]: *** [polyexport.o] Error 134
make[2]: *** [all-recursive] Error 1
make[1]: *** [all] Error 2
make: *** [compiler] Error 2

Regards,

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

Re: [polyml] Update to code-generator and run-time system interface

[Rob Arthan]

David,

Many thanks for the quick turn round on these issues. I have got quite a bit 
further.
The ProofPower build is now failing as a result of the following issue:

5) In string comparisons, the leading character is being treated as negative
if it has character code greater than 127:

E.g.,

> "\128" < "\000";
val it = true: bool
> "\128a" < "\000a";
val it = true: bool

Character comparisons are OK:

> #"\128" < #"\000";
val it = false: bool

(This is on Mac OS X after building Poly/ML with Apple's Xcode tool chain.)

Regards,

Rob.

> On 18 Sep 2016, at 16:36, David Matthews <david.matth...@prolingua.co.uk> 
> wrote:
> 
> Rob,
> Thanks for that and for cutting it down to something manageable.  As a result 
> I've been able to track down and fix the problem.  Let me know as and when 
> you find anything else.
> 
> Regards,
> David
> 
> On 17/09/2016 16:20, Rob Arthan wrote:
>> David,
>> 
>> 
>>> On 17 Sep 2016, at 14:49, Rob Arthan <r...@lemma-one.com> wrote:
>> …
>>> … I am getting a segfault somewhere in the
>>> ProofPower parser generator. I will report again when I have
>>> isolated that.
>> 
>> To the list of three issues in my previous e-mail, I can now add:
>> 
>> 4) In some circumstances a function call can lead to a segfault.
>> 
>> I’ve attached a short extract from the parser generator code that 
>> demonstrates the problem.
>> If you execute the body of the function empty_non_terminals interactively
>> with the parameter bound to the test data, then nothing goes wrong.
>> If you call the function with the test data as parameter (as on the last 
>> line of the
>> attached file) you get a segfault.
>> 
>> 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] Update to code-generator and run-time system interface

[Rob Arthan]

David,


> On 17 Sep 2016, at 14:49, Rob Arthan <r...@lemma-one.com> wrote:
…
> … I am getting a segfault somewhere in the
> ProofPower parser generator. I will report again when I have
> isolated that.

To the list of three issues in my previous e-mail, I can now add:

4) In some circumstances a function call can lead to a segfault.

I’ve attached a short extract from the parser generator code that demonstrates 
the problem. 
If you execute the body of the function empty_non_terminals interactively
with the parameter bound to the test data, then nothing goes wrong.
If you call the function with the test data as parameter (as on the last line 
of the
attached file) you get a segfault.

Regards,

Rob.



slrp-bug-cutdown.ML
Description: Binary data
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Update to code-generator and run-time system interface

[Rob Arthan]

David,

I have been having a go at building ProofPower with the latest updates.
Here is some miscellaneous feedback:

1) Are these two errors in the configure output harmless? (This is on
Mac OS X using Apple’s Xcode tools.)

checking for __attribute__((visibility("hidden")))... no
clang: error: unsupported option '-print-multi-os-directory'
clang: error: no input files
checking that generated files are newer than configure… done

2) SML90.explode crashes. The following patch fixes this:

--- a/basis/SML90.sml
+++ b/basis/SML90.sml
@@ -81,9 +81,8 @@ struct
 fun ord "" = raise Ord | ord s = Char.ord(String.sub(s, 0))
 
 fun chr i = str(Char.chr i)
-(* Because single character strings are represented by the characters
-   themselves we just need to coerce String.explode. *)
-val explode: string -> string list = RunCall.unsafeCast(String.explode)
+
+val explode: string -> string list = map str o String.explode
 val implode = String.concat
 
 type instream = TextIO.instream and outstream = TextIO.outstream

3) If I configure with —enable-intinf-as-int, make compiler fails:

Use: basis/IMPERATIVE_IO.sml
Use: basis/ImperativeIO.sml
Use: basis/TextIO.sml
Exception- InternalError: findEntry - not found raised while compiling

make[3]: *** [polyexport.o] Error 1
make[2]: *** [all-recursive] Error 1
make[1]: *** [all] Error 2
make: *** [compiler] Error 2

Not being able to build with —enable-intinf-as-int  isn’t a stopper for me,
but when I press on, I am getting a segfault somewhere in the
ProofPower parser generator. I will report again when I have
isolated that.

Regards,

Rob.

> On 16 Sep 2016, at 13:24, David Matthews  
> wrote:
> 
> I have now pushed a major update to git master which is the result of work 
> going back to the beginning of the year.  It covers a number of areas but 
> largely the code-generator and the run-time system interface.
> 
> The basic design of much of the low-level parts of Poly/ML dated back to the 
> early days.  While it has changed a lot in detail the overall structure has 
> remained the same.  The idea was to bring the whole thing up to date.
> 
> The run-time system interface has been redesigned and instead of a vector of 
> entries to the run-time system the ML code now uses a form of 
> foreign-function interface to call individual functions.  The advantage is 
> that it is much easier to add new functions.  In addition when building an 
> executable it is possible for the linker to select only the parts of 
> libpolyml that are actually required for the application, at least if the 
> static library version is used.  It should be possible to adapt the 
> foreign-function interface it uses to speed up calls made using the Foreign 
> structure, although that's not done at the moment.
> 
> The code-generator has been rewritten particularly the register assignment.  
> The previous version had been the result of a series of adaptations to new 
> architectures over the years.  The new version focusses solely on the X86.  
> I'm still working on this.  Doing this has needed a temporary, slow, 
> code-generator which is why it has taken until now to push this to git master.
> 
> The representation of strings has been simplified.  Previously, single 
> character strings were represented by the character itself as a tagged value. 
>  This was largely a relic of SML 90 which didn't have a separate char type.  
> That has been removed and all strings are now represented as a vector of 
> bytes.  This speeds up string operations since the code no longer has to 
> consider the special case.
> 
> SSE2 instructions are now used for floating point on the X86/64. Floating 
> point support in the new code-generator is rudimentary at the moment and not 
> to the same extent as the previous code-generator.
> 
> The handling of return addresses from functions has been simplified.  A 
> consequence of this is that when pieces of code are compiled they are stored 
> in a separate area of memory rather than in the general heap and not 
> garbage-collected.  It is no longer possible to get an exception trace so 
> PolyML.exception_trace has no effect.  The debugger handles this much better 
> anyway.
> 
> Although the focus has been on the X86 the portable byte-code interpreter has 
> been improved and is significantly faster.
> 
> The system has had some basic testing but there are bound to be bugs in 
> something as complex as this.  I'm also continuing to work on improvements.  
> When testing this it is essential to run "make compiler" at least once and 
> generally twice to build the new compiler and then build the compiler itself 
> with the new compiler.
> 
> 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

Re: [polyml] Equality Type Parameter in Datatype Declaration

[Rob Arthan]

> On 16 Sep 2016, at 20:59, Bernard Berthomieu  
> wrote:
> 
> ...
> I like the treatment of polyML :-), but I guess it is not standard:
> 
> The "definition" (http://sml-family.org/sml97-defn.pdf) says, page 19:
>  "... In particular, the equality attribute has no significance in a bound
>   variable of a type function; for example ... "
> 
> So, unless I'm mistaken, sml-nj is right.
> 

That's interesting. The text you quote is pretty clear, but how is it 
consistent with the static semantics of constructor bindings on p29,
which I read as saying that in Tjark's example: datatype ''a t = C of ''a,
C gets type ''a -> ''a t?

Regards,

Rob.

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

Re: [polyml] Equality Type Parameter in Datatype Declaration

[Rob Arthan]

David,

> On 16 Sep 2016, at 19:19, David Matthews  
> wrote:
> 
> I've checked hamlet and mlton and they both reject it so I think in this case 
> Poly/ML is right and SML/NJ is wrong.  I can't point to the bit of the 
> definition that says that, though.

It's in Appendix C:  "Of [the type names listed in the initial static basis] 
all except exn and real admit equality".

Regards,

Rob.


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

Re: [polyml] not printed exception when executed file

[Rob Arthan]

Kostriya,


Gergely’s answer is right. When you build a stand-alone executable,
your ML code has to do all the input and output. If you want to report 
exceptions you need to handle them and take appropriate action. E.g.,

fun main () = ( print "Start\n"; raise Ex; print "The End\n" )
handle exc => (
print ("function main raised an exception: " ^ exnMessage exc ^ 
"\n"
)
);

Regards,

Rob.


> On 15 Jun 2016, at 18:33, Gergely Buday  wrote:
> 
> The compiled code will not display uncaught exceptions but the execution 
> stops.
> 
> - Gergely
> 
> On Wednesday, 15 June 2016, Kostirya  > wrote:
> Hello.
> Why when executed file, exception is not printed? Is it OK?
> 
> > cat foo.sml 
> exception Ex 
> fun main () = ( print "Start\n"; raise Ex; print "The End\n" )
> 
> > ( cat foo.sml ; echo 'val _ = main ()' ) | poly
> Poly/ML 5.6 Release
> Start
> Exception- Ex raised
> 
> > polyc foo.sml && ./a.out
> Start
> >
> 
> 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

[polyml] Poly/ML changes history

[Rob Arthan]

I have a recollection of a list somewhere on the Poly/ML website giving a brief 
description of what had changed in each version of Poly/ML, but I can’t find it 
any more. Am I just being unobservant or was I imagining things? The specific 
question I wanted to answer was: which version introduced polyc?

Regards,

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

Re: [polyml] determining if an outstream is a tty

[Rob Arthan]

PS:

In fairness to the Standard ML Basis library, the behaviour is documented
and does make sense. The description of getReader and getWriter say that they
flush the stream and mark it as terminated, which is what you’d probably
want if you were going to use setInstream or setOutstream to associate
the reader or writer with a different  stream. Here you have to reassociate the
reader or writer with the original stream to get it working again.

Regards,

Rob.


> On 7 May 2016, at 11:56, Rob Arthan <r...@lemma-one.com> wrote:
> 
> Michael,
> 
> I adapted this from an analogous function is_term_in that we have in 
> ProofPower
> and it seems to work.
> 
>   fun is_term_out (outstream : TextIO.outstream) = (
>   let val (wr as TextPrimIO.WR{ioDesc,...},buf) =
>   TextIO.StreamIO.getWriter(TextIO.getOutstream 
> outstream);
>   val _ = TextIO.setOutstream
>   (outstream, TextIO.StreamIO.mkOutstream(wr, 
> buf));
>   in  case ioDesc of
>   NONE => false
>   |   SOME desc => (OS.IO.kind desc = OS.IO.Kind.tty)
>   end
>   );
> 
> For reasons that I don’t claim to understand, the stream behaves as if it is 
> closed
> after the call to getWriter. You have to use setOutstream (or setInstream in 
> is_term_in)
> to fix that before anything (e.g., the read-eval-print loop) attempts to do 
> I/O on the stream.
> 
> Regards,
> 
> Rob.
> 
> 
>> On 7 May 2016, at 06:01, Michael Norrish <michael.norr...@nicta.com.au> 
>> wrote:
>> 
>> The Basis library documentation for OS.IO suggests that it should be 
>> possible to get one's hand on a primitive reader or writer iodesc by pulling 
>> things apart to get PrimIO values.
>> 
>> Doing type-directed programming, I thought I might do this for a 
>> TextIO.outstream with
>> 
>>> val getIOD = (fn TextPrimIO.WR r => #ioDesc r) o #1 o 
>>> TextIO.StreamIO.getWriter o TextIO.getOutstream;
>>  val getIOD = fn: TextIO.outstream -> OS.IO.iodesc option
>> 
>> This has the right type (and I couldn't see any other way of getting the 
>> right type).  Unfortunately, I can't run it:
>> 
>>> getIOD TextIO.stdOut;
>>  Exception Io raised while writing to stdOut.
>> 
>> terminating the session.
>> 
>> If this had worked, I then hoped to be able to call Posix.FileSys.iodToFD on 
>> the value, if there was one, and to then eventually call 
>> Posix.ProcEnv.isatty on the result of that, if present.
>> 
>> Is there a right way to do this?
>> 
>> Many thanks,
>> Michael
>> 
>> 
>> 
>> 
>> 
>> The information in this e-mail may be confidential and subject to legal 
>> professional privilege and/or copyright. National ICT Australia Limited 
>> accepts no liability for any damage caused by this email or its attachments.
>> ___
>> 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] determining if an outstream is a tty

[Rob Arthan]

Michael,

I adapted this from an analogous function is_term_in that we have in ProofPower
and it seems to work.

fun is_term_out (outstream : TextIO.outstream) = (
let val (wr as TextPrimIO.WR{ioDesc,...},buf) =
TextIO.StreamIO.getWriter(TextIO.getOutstream 
outstream);
val _ = TextIO.setOutstream
(outstream, TextIO.StreamIO.mkOutstream(wr, 
buf));
in  case ioDesc of
NONE => false
|   SOME desc => (OS.IO.kind desc = OS.IO.Kind.tty)
end
);

For reasons that I don’t claim to understand, the stream behaves as if it is 
closed
after the call to getWriter. You have to use setOutstream (or setInstream in 
is_term_in)
to fix that before anything (e.g., the read-eval-print loop) attempts to do I/O 
on the stream.

Regards,

Rob.


> On 7 May 2016, at 06:01, Michael Norrish  wrote:
> 
> The Basis library documentation for OS.IO suggests that it should be possible 
> to get one's hand on a primitive reader or writer iodesc by pulling things 
> apart to get PrimIO values.
> 
> Doing type-directed programming, I thought I might do this for a 
> TextIO.outstream with
> 
>> val getIOD = (fn TextPrimIO.WR r => #ioDesc r) o #1 o 
>> TextIO.StreamIO.getWriter o TextIO.getOutstream;
>   val getIOD = fn: TextIO.outstream -> OS.IO.iodesc option
> 
> This has the right type (and I couldn't see any other way of getting the 
> right type).  Unfortunately, I can't run it:
> 
>> getIOD TextIO.stdOut;
>   Exception Io raised while writing to stdOut.
> 
> terminating the session.
> 
> If this had worked, I then hoped to be able to call Posix.FileSys.iodToFD on 
> the value, if there was one, and to then eventually call Posix.ProcEnv.isatty 
> on the result of that, if present.
> 
> Is there a right way to do this?
> 
> Many thanks,
> Michael
> 
> 
> 
> 
> 
> The information in this e-mail may be confidential and subject to legal 
> professional privilege and/or copyright. National ICT Australia Limited 
> accepts no liability for any damage caused by this email or its attachments.
> ___
> 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] Poly/ML Changes History

[Rob Arthan]

Phil,

Thanks. That’s useful although it doesn’t mention the change that prompted my
question: namely the replacement of PolyML.profiling by the new features
in the structure PolyML.Profiling.

Regards,

Rob.

> On 17 Mar 2016, at 14:02, Phil Eaton <philneato...@gmail.com> wrote:
> 
> As a side note, there is a list of changes on the release page on Github here 
> <https://github.com/polyml/polyml/releases>.
> 
> On Thu, Mar 17, 2016 at 8:53 AM, Rob Arthan <r...@lemma-one.com 
> <mailto:r...@lemma-one.com>> wrote:
> I thought there was a changes history for Poly/ML somewhere on the
> Poly/ML website, but I can’t find it any more. It would be useful to have
> a list of changes between Poly/ML 5.5.2 and Poly/ML 5.6. Apologies
> if I am just being unobservant.
> 
> Regards,
> 
> Rob.
> ___
> polyml mailing list
> polyml@inf.ed.ac.uk <mailto:polyml@inf.ed.ac.uk>
> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml 
> <http://lists.inf.ed.ac.uk/mailman/listinfo/polyml>
> 
> -- 
> Phil Eaton
> ___
> 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] Poly/ML Changes History

[Rob Arthan]

I thought there was a changes history for Poly/ML somewhere on the
Poly/ML website, but I can’t find it any more. It would be useful to have
a list of changes between Poly/ML 5.5.2 and Poly/ML 5.6. Apologies
if I am just being unobservant.

Regards,

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

Re: [polyml] playing with Posix fork/exec/dup2 etc

[Rob Arthan]

> On 18 Mar 2016, at 13:13, David Matthews  
> wrote:
> 
> On 18/03/2016 02:40, Michael Norrish wrote:
>> Under 5.5.1, and after compiling with polyc, the code below gives an 
>> assertion violation and core dump:
> 
> This was a bug that has been fixed in the current version, 5.6.
> 
> Exceptions are raised in the run-time system when it detects errors such as 
> invalid parameters.  Assertions are used for errors in the run-time system 
> itself.  The idea is to be slightly more helpful than just a segfault with no 
> other information.
> 
I tried Michael’s example on 5.6. It didn’t raise an exception, but it also 
didn’t terminate:
it hangs in the call to TextIO.inputLine in the parent process, so I think 
there is something
else wrong (as the call is reading from a pipe whose writer has exited, so I'd 
expect
it to return NONE).

Regards,

Rob.

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

Re: [polyml] Reducing the size of on-disk saved state

[Rob Arthan]

> On 17 Feb 2016, at 18:34, David Matthews  
> wrote:
> ...
> Of more concern is that LZO is licensed under GPL rather than LGPL. Poly/ML 
> is licensed under LGPL and that means that it cannot include or even link to 
> LZO without coming under GPL.  That doesn't preclude experimenting with it 
> but for distribution I'd prefer a library that didn't have these problems.

It would cause me significant problems if the Poly/ML licence changed to GPL.
I can't understand why the LZO developers chose GPL rather than LGPL unless
they hope that decision would force people to buy their commercial offering 
(which
I believe is a doomed business plan).

Regards,

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

Re: [polyml] Fixed precision int

[Rob Arthan]

> On 10 Feb 2016, at 17:01, Makarius  wrote:
> 
> On Wed, 10 Feb 2016, David Matthews wrote:
> 
> This reminds me of the situation in SML/NJ, before I spent some efforts to 
> force int = IntInf.int on it.  It includes a somewhat "patched" basis library 
> like this: 
> http://isabelle.in.tum.de/repos/isabelle/file/9343649abb09/src/Pure/RAW/proper_int.ML

ProofPower takes a different approach to this: it uses the compiler's native 
integers
except where logical soundness requires an IntInf, where it uses a type it 
defines
called INTEGER, which has its own operations @+, @-, @* etc. implemented
using  the operators of Int or IntInf as appropriate (selected at compile-time 
by
using a conditional compilation feature that is built into the way ProofPower
packages ML code into documents).

ProofPower builds and tests fine using poly built from the FixedPrecisionInt
branch after tweaking the conditionally compiled bits of code so that Poly/ML
is treated just like Standard ML of New Jersey in the definition of the type
INTEGER. (And tweaking a few tests that accidentally forgot that INTEGER
and int are not necessarily the same.)

>> I'm inclined to think that having a "configure" option would be the answer.
> 

I think that's a good idea, but it gives me a bit of problem as my conditial 
compilation
is based on the compiler and not how the compiler has been configured.

> That would greatly simplify the Isabelle setup, because we always provide a 
> separately compiled version of Poly/ML.

I can see why you do that, but I don't want to do it for ProofPower. So if we 
have
a "configure" option, then it would be good for me if there some well-defined 
way, e.g., using
"poly -v", for a build script to find out how a pre-installed Poly/ML 
installation has
been configured.

> 
> Since we are about to discontinue SML/NJ altogether, it would allow to remove 
> the above tricks, and not move them over to Poly/ML.

I can unerstand why you are doing that too, but in this case I'm really glad I 
tried
to maintain compatibility, as it meant I already had almost everything I needed 
to
accommodate the proposed change :-).

All that said, I would be surprised if the change made any significant 
performance
improvement on any of my code, because anything that is computationally 
intensive
in the theorem prover tends to be dealing with object language data, and, if
that data is numeric, it will be arbitrary precision. 

Regards,

Rob.

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

Re: [polyml] Towards Poly/ML 5.6

[Rob Arthan]

David,

> On 7 Jan 2016, at 19:19, David Matthews <david.matth...@prolingua.co.uk> 
> wrote:
> 
> Rob,
> 
> On 07/01/2016 17:50, Rob Arthan wrote:
>> ... I can  roll my own implementation of it using
>> PolyML.addPrettyPrinter. Is that going to be an easy exercise?
> 
> The compatibility code for install_pp was removed with a commit on 19th 
> October.  See
> https://github.com/polyml/polyml/commit/075bda98965195f522cf1de02aaf9a6f23d0b050
> 
> It should give you an idea of what to do but it's very simple because there's 
> a close approximation between the old addString/beginBlock/break/endBlock and 
> PrettyString, PrettyBlock and PrettyBreak.  Essentially what it does is 
> create a stack of pending beginBlocks and then adds the breaks and strings to 
> the top of the stack, popping the stack when it finds an endBlock.
> 
> You'll have to convert each occurrence of install_pp individually because 
> addPrettyPrinter and the old install_pp are type-dependent functions rather 
> than polymorphic (like PolyML.print).

That's great, thanks. I am in business with Poly/ML 5.6 now.

You can actually package the conversion (of the argument you pass to install_pp 
into the argument you pass to addPrettyPrinter) as a polymorphic function, say 
called make_pp. So the conversion simply involves replacing calls of install_pp 
with calls of (addPrettyPrinter o make_pp).

Regards,

Rob.

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

[polyml] addPrettyPrinter type security

[Rob Arthan]

PolyML.addPrettyPrinter checks its printArgTypes parameter carefully
when you are installing a pretty-printer for a polymorphic type.
As far as I can see it guarantees type security for polymorphic types.

However, when you install a pretty-printer for a monomorphic type,
the parameter isn't checked at all. E.g., the following code doesn't
result in any error messages and ends by crashing poly.

datatype MONO = Mono of int;

fun pp_mono1 _ (i : int) (Mono j) = (
PolyML.PrettyString (Int.toString (i + j))
);

PolyML.addPrettyPrinter pp_mono1;

Mono 42; (* Prints "val it = 42: MONO" - apparently i was 0 *)

fun pp_mono2 _ (r : int ref) (Mono _) = (
PolyML.PrettyString (Int.toString (!r))
);

PolyML.addPrettyPrinter pp_mono2;

Mono 42; (* Crashes *)

Shouldn't processArgTypes be required to have type unit when
defining a pretty-printer for a monotype? The patch below
implements this check and tries to improve the error message
(which is already a bit misleading if you get something wrong
for a type with more than one parameter).

Regards,

Rob.

diff --git a/mlsource/MLCompiler/VALUE_OPS.ML b/mlsource/MLCompiler/VALUE_OPS.ML
index 1535d4f..9e00f0d 100644
--- a/mlsource/MLCompiler/VALUE_OPS.ML
+++ b/mlsource/MLCompiler/VALUE_OPS.ML
@@ -958,8 +958,8 @@ struct
 val typeVars = List.tabulate(arity, fn _ => mkTypeVar 
(0, false, true, false))
 val tupleType =
 case typeVars of
-[] => (* No arg so we can have anything here. 
*)
-mkTypeVar (generalisable, false, false, 
false)
+[] => (* No arg so must have unit. *)
+   unitType
 |   [arg] => mkFn arg (* Just a single function. *)
 |   args => mkProductType(List.map mkFn args)
 val addPPType = mkFunctionType(argPrints, 
mkFunctionType(installType, pretty))
@@ -970,7 +970,7 @@ struct
 in
 checkPPType(addPPType, testType, "addPrettyPrint", 
lex, loc,
 fn () =>
-PrettyString "addPrettyPrint element functions 
must have type 'a * int -> pretty")
+PrettyString "addPrettyPrint element functions 
must have type 'a * int -> pretty, 'b * int -> pretty, ... with one function 
for each type parameter")
 end;
 
 (* Only report the error when the function is run.  Because 
addPrettyPrint is


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

Re: [polyml] Towards Poly/ML 5.6

[Rob Arthan]

> On 3 Jan 2016, at 18:33, James Clarke <jrt...@jrtc27.com> wrote:
> 
> Hi Rob,
> install_pp has been deprecated for a while[1], with addPrettyPrinter[2] being 
> its replacement. Is there a reason you can't use that?
> 
Thanks for the reminder. (I’m glad to see the documentation doesn’t actually 
say “deprecated”, a word that I deprecate as a substitute for “not recommended” 
:-).) I was actually testing on an oldish release of ProofPower. Later releases 
use addPrettyPrinter.

Note that the the PolyMLStructure documentation will be out-of-date for version 
5.6.

Regards,

Rob.

> Regards,
> James
> 
> [1] 
> http://www.polyml.org/documentation/Reference/PolyMLStructure.html#install_pp
> [2] 
> http://www.polyml.org/documentation/Reference/PolyMLStructure.html#addPrettyPrinter
> 
>> On 3 Jan 2016, at 17:27, Rob Arthan <r...@lemma-one.com> wrote:
>> 
>> David,
>> 
>> 
>>> On 2 Jan 2016, at 09:08, David Matthews <david.matth...@prolingua.co.uk> 
>>> wrote:
>>> 
>>> I've updated the github repository with pre-built compilers for 5.6 
>>> Release.  This is now the release candidate.  Unless there are any 
>>> significant problems this will be released in the next few weeks.
>> 
>> The ProofPower build expects to install pretty-printers using 
>> PolyML.install_pp. That doesn’t seem to be there any more in the 5.6 release 
>> candidate.
>> 
>>> Best wishes for 2016,
>> 
>> Happy New Year to you and the Poly/ML user community!
>> 
>> 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

Re: [polyml] Towards Poly/ML 5.6

[Rob Arthan]

David,


> On 2 Jan 2016, at 09:08, David Matthews  
> wrote:
> 
> I've updated the github repository with pre-built compilers for 5.6 Release.  
> This is now the release candidate.  Unless there are any significant problems 
> this will be released in the next few weeks.
> 

The ProofPower build expects to install pretty-printers using 
PolyML.install_pp. That doesn’t seem to be there any more in the 5.6 release 
candidate.

> Best wishes for 2016,

Happy New Year to you and the Poly/ML user community!

Regards,

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

[polyml] Lexical analyser bug?

[Rob Arthan]

I mistyped a word constant and was a bit surprised by the error message.

rda]- poly
Poly/ML 5.5.2 Release
 0xw9;
Error-malformed integer constant: 0w
Static Errors

Contrast this with SML/NJ:

rda]- sml
Standard ML of New Jersey v110.76 [built: Mon Mar  3 16:26:20 2014]
- 0xw9;
stdIn:3.2-3.5 Error: unbound variable or constructor: xw9
stdIn:3.1-3.5 Error: operator is not a function [literal]
  operator: int
  in expression:
0 errorvar

With the following contrived example:

fun f x y = print Boo!
val xw9 = xw9;
f 0xw9;

Poly/ML reports a syntax error while SML/NJ and mlton both print Boo!

I am not sure who is right about this.

Regards,

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

[polyml] C Interface documentation

[Rob Arthan]

I am trying to help with porting some code that uses the C foreign function
interface from Linux to Mac OS X and have been trying a toy example
on both systems. I have actually been very impressed by how easy it
was to get started with the interface, but I did note some small issues
with the documentation.

The first point is with the release notes, which do say that the C Interface
was not supported on Mac OS X once upon a time, but don’t say that
it is supported now. (Aside: do time profiling and polling work now too?)

The web page about the C Interface says that load_lib will raise
an exception if the dynamic library cannot be found.
My experience on both OSes is that load_lib and load_sym don’t raise any 
exceptions.
You get the exception when you try to call a C function. The documentation
also says that it will kill your ML session if the file exists but has the 
wrong format,
but that seems to have been fixed now.

It says that if load_lib is called with a relative path name,
then it will be interpreted with respect to the directory in which the ML
session was started from. I don’t think this can be right. Surely you will get
whatever behaviour dlopen gives you (and typically that will be a search
involving environment variables like LD_LIBRARY_PATH and some
OS-specific standard places like /lib). So, for example, if mylib.so
is in the current directory and I pass “mylib.so” to load_lib, on Fedora, I get

load_lib mylib.so : mylib.so: cannot open shared object file: No such file or 
directory

If I change “mylib.so” on the call to load_lib to “./mylib.so” or run with
LD_LIBRARY_PATH=. or copy mylib.so into /usr/lib64, it works.
On Mac OS X, on the other hand, if have “mylib.dylib” in my current directory,
load_lib will find it given the relative pathname, because dlopen on Mac OS X
includes the current directory as one of the standard places.

Regards,

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

Re: [polyml] regarding problem with PolyML debugging prompt

[Rob Arthan]

On 27 Sep 2014, at 16:10, saroj sarojanaray...@gmail.com wrote:

 Hi, 
 I am using PolyML in windows XP sp3 . I tried to run through example 
 on how to use  source level debugger, which is provided on you website 
 .http://www.polyml.org/docs/Debugging.html
 
 I am able to open debugging prompt using open PolyML.Debug option.
 But I am unable to exit debug prompt. I tried control C  option . But it is 
 only interrupting compilation,  without breakIn  option as shown in your 
 website. I set breakIn f option 
 as mentioned. 
 
 Please let me the solution.

The documentation is out of date. PolyML no longer implements the dialogue 
asking you
what to do after a keyboard interrrupt (Control C). In the example in the 
documentation,
the program loops, so if you just call “continue()” you will be stuck in the 
debugger.
One way out is to call continueWithEx with an exception that the
program doesn’t handle. E.g., (in the documented example) do:

continueWithEx Div;

Maybe David might like to consider adding a function to the debugger that will
abandon the thread being debugged.

Regards

Rob.

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

Re: [polyml] can't quit sessions

[Rob Arthan]

On 31 Jul 2014, at 06:13, Tom Meumann u5028...@anu.edu.au wrote:

 Hi all,
 
 I'm using PolyML 5.5.0 to run some tests as a batch job and I can't
 figure out how to quit without using ^D (which I can't feed in
 automatically when batching things).
 
 I've tried using PolyML.quit (); and PolyML.exit 0; but neither of
 these work.
 
 I'm opening the PolyML structure first (open PolyML;) but I'm still
 getting errors saying that the commands haven't been declared.  I can
 use some other functions defined in PolyML such as PolyML.use, but not
 all (for instance cd isn't available).
 
 Seems the documentation is incorrect?
 http://www.polyml.org/docs/Intro1.html

I think that part of the documentation must be out of date.

 
 Can anyone help me out on this one?
 

There is a Standard Basis Library function that does what you want. Try:

   OS.Process.exit OS.Process.success;

Regards,

Rob.

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

Re: [polyml] .polyml and poly-stats

[Rob Arthan]

David,

On 2 Jul 2014, at 11:42, David Matthews david.matth...@prolingua.co.uk wrote:

 On 29/06/2014 11:41, Rob Arthan wrote:
 
 The files are only 4096 bytes so it is not much of an overhead, but
 it is a bit messy. Would it make sense to provide a function in
 PolyML.Statistics allowing a process to opt into making its
 statistics available? (Or conversely, is there a requirement to
 access statistics from a program that has not been designed with that
 in mind?)
 
 The idea was to make the statistics available for another poly or a different 
 program.  The difficulty is finding a way to make them available.  In Windows 
 it is possible to have a named shared memory segment which is created by the 
 poly process and can be opened, read-only, by another process.  When the 
 creating process finishes the memory segment is deleted unless another 
 process is currently reading it.  There's no equivalent, as far as I can 
 tell, in Unix.  The only way to make a shared memory segment available to 
 another process is to map a file and the file will remain after the creating 
 process exits unless it is explicitly deleted.
 
 My preference would be for a way to have the equivalent of named shared 
 memory segments.

Have you looked at System V shared memory (shmget/shmat etc.)?  This seems to 
be available on most flavours of UN*X these days. However, it is a long while 
since I have used these interfaces and they may just move the problem from the 
world of ls and rm to the world of ipcs and ipcrm.

 If there is no alternative to the present scheme of creating a mapped file in 
 the file system then it would probably be better to only create it if the 
 creating process explicitly requests it.  That could be a flag somewhere in 
 PolyML.Statistics or, probably easier, a command line option.  Any ideas?

If you stick with mmap, then control via the command line looks good to me.

Regards,

Rob.



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

Re: [polyml] .polyml and poly-stats

[Rob Arthan]

David,

On 2 Jul 2014, at 13:41, David Matthews david.matth...@prolingua.co.uk wrote:

 On 02/07/2014 13:20, Rob Arthan wrote:
 Have you looked at System V shared memory (shmget/shmat etc.)?  This
 seems to be available on most flavours of UN*X these days. However,
 it is a long while since I have used these interfaces and they may
 just move the problem from the world of ls and rm to the world of
 ipcs and ipcrm.
 
 Thanks for suggesting this.  I was hoping someone might be able to suggest 
 something.  However, looking a bit more closely, I can see a problem.  shmget 
 uses a key which has to be derived from an existing file via ftok.  That 
 looks as though it would require a file to be created in the file system for 
 each process.  It could be zero size but I think it leads to the problem 
 you've identified.

I don’t think you have to use ftok (in fact, I have never used it). However you 
do need some scheme for allocating the numbers. I don’t know if you can arrange 
to have shared memory segments automatically disappear when all related 
processes die (which is why I thought you might just be moving the problem into 
a different namespace).

Regards,

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

Re: [polyml] .polyml and poly-stats

[Rob Arthan]

On 27 Jun 2014, at 17:53, David Matthews david.matth...@prolingua.co.uk wrote:

 On 27/06/2014 12:03, Makarius wrote:
 What are the conditions under which Poly/ML 5.5.2 creates a directory
 $HOME/.polyml and puts poly-stats files there?
 Poly/ML always creates a .polyml directory and a poly-stats file.  The 
 poly-stats file will be deleted when the Poly/ML process finishes normally.  
 If it crashes, though, the file will remain.
 
 I am also using PolyML.Statistics.getLocalStats, but shouldn't the
 shared-memory file be for global stats only?
 The Poly/ML process does not know when another process wants to read the 
 statistics so they are always made available as a memory-mapped file.
 
I discovered the same problem with ProofPower where users run via a GUI which 
just kills the ProofPower executable when the user quits or asks to restart the 
ProofPower session. It is a bit surprising that running a stand-alone program 
(like Joe Hurd’s opentheory or my slrp parser generator) creates $HOME/.polyml 
and that aborting a run with Ctrl+C leaves a stats file in that directory. 

The files are only 4096 bytes so it is not much of an overhead, but it is a bit 
messy. Would it make sense to provide a function in PolyML.Statistics allowing 
a process to opt into making its statistics available? (Or conversely, is there 
a requirement to access statistics from a program that has not been designed 
with that in mind?)

Regards,

Rob.

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

Re: [polyml] Poly on MinGW

[Rob Arthan]

David,

On 20 May 2014, at 13:07, David Matthews david.matth...@prolingua.co.uk wrote:

 Rob,
 
 On 20/05/2014 06:57, Rob Arthan wrote:
 I agree that it wasn’t very clear whether this was thought to be a
 bug in the MinGW header files or not.
 
 I may have a look and see if this is something I can fix easily but there's 
 no point if they are going to fix in Mingw anyway.  Last time I used Mingw I 
 didn't have this problem.

As the work-around just involves setting an environment variable when you run 
configure, I don’t think it is worth spending much time on.

 
 I would actually have expected the “GUI” to be a command prompt
 window. I.e., I would have expected poly to be a console application.
 This is how python comes, for example. Something that behaves like a
 console application is what cc on MinGW seems to give you if you
 don’t give it any of the Windows-specific command line options when
 you compile a standard C program.
 
 What exactly do you mean by a console application?

I mean the kind of thing that Visual Studio creates if you select “Win32 
Console Application” when you create a new C++ project. I.e., a program with 
the standard C interface to the operating system, i.e., an entry point called 
main.

  There is a legacy console mode but it is very inconvenient to use.
  Cutting and pasting in particular are not at all intuitive.  Why exactly do 
 you want to use console mode?

I didn’t say that it was what I wanted: it is all I would have expected (as in 
“I always expect pain when I upgrade my operating system”). I agree that cut 
and paste are clunky in command prompt windows, so it is great to have 
something nicer.

  More generally, what exactly is it that you want to do that the present 
 version of Poly/ML will not let you do?

This isn’t much of a problem for me, but what you are offering is rather 
inconvenient for anyone who wants to write ML programs that present the kind of 
interface that Windows command line programs like “sort offer (with cmd.exe 
and the C runtime providing interactive input and output from a console window 
and redirection of standard input and output to files). Such things can be 
written portably using standard C or standard C++ and, it would be nice to be 
able to code similar things in ML without needing a wrapper to call them on 
Windows.

  If you have an ML program that you want to run as a process with a separate 
 GUI application that is easy.  Just create the input and output pipes and 
 pass them as arguments in the CreateProcess call.  The ML process will be 
 completely invisible and all the user will see is your GUI.  That's how I 
 normally run Poly/ML.
 

This is for the scenario where I write (in some other language) a GUI that is 
going to start my ML program and interact with it via files or pipes or 
suchlike. Is that right?

 The only circumstance where the present system may not work satisfactorily is 
 if you have written a GUI application in ML itself, for instance the mlEdit 
 example in mlsource/extra/Win/Examples.

How do you compile the code in that directory? It doesn’t seem to contain the 
source file for mlEdit that the documentation for the Windows interface refers 
to.

  When the user double-clicks on the application to run it there would be an 
 extra window because the RTS creates its own GUI.
 
 Cygwin does work for me, but unfortunately, having to install it is a
 stopper for some of my potential users. I tried compiling under MinGW
 with __CYGWIN__ set, but it doesn’t work. Would it be difficult to
 separate the choice between polystub.c being a standard C application
 and a Windows application from the __CYGWIN__ flag?
 
 Why does the user need to install Cygwin?  If you build an application under 
 Cygwin you just need to put the Cygwin DLL and perhaps a few library DLLs in 
 the same folder as your application.  Windows always searches for DLLs first 
 in the same folder as the executable.

That might be an option, but it seems like quite an overhead to have to include 
something that provides vast amounts of functionality to emulate UNIX that I 
just don’t need and is a potential source of problems. So I was trying to 
explore the options for having libpolyml use standard C++ libraries (and not 
the Windows GUI libraries) without emulating UNIX.

I am also thinking about the possibility of packaging an ML program as a 
Windows service (by providing my own libpolymain with entry points ServiceMain 
etc.) and thought that would be incompatible with the Windows GUI stuff, but 
maybe it will work with libpolyml compiled as it is presently or maybe it just 
doesn’t make sense. I will have to do some experiments.

Regards,

Rob.

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

Re: [polyml] Poly on MinGW

[Rob Arthan]

David,

On 19 May 2014, at 15:42, David Matthews david.matth...@prolingua.co.uk wrote:

 Rob,
 
 On 18/05/2014 17:36, Rob Arthan wrote:
 I am trying to understand my options for using Poly/ML on MinGW for
 building windows applications coded in Standard ML.
 
 There is a bug reported in http://sourceforge.net/p/mingw/bugs/2043/
 that you have to work around to build Poly/ML with the current MinGW.
 The work-around is to run configure with
 CXXFLAGS=-D_GLIBCXX_HAVE_FENV_H=1” in the environment. (I suspect I
 should also throw -O3 in there too, as I think that setting CXXFLAGS
 replaces its initial setting of -O3 inside the makefiles. Is that
 right?)
 
 I suspect it is.  I wasn't aware of the need for _GLIBCXX_HAVE_FENV_H=1 but 
 it's quite a while since I last used Mingw.  It isn't clear from the link 
 whether this is something the Poly/ML configure should do or not.

I agree that it wasn’t very clear whether this was thought to be a bug in the 
MinGW header files or not.

 
 Having got Poly/ML to compile, I found that polyc gives errors like
 the following when asked to compile a source file:
 
 gcc.exe: error: C:/DOCUME~1/rda/LOCALS~1/Temp/polyobj.2724.obj: No
 such file or directory
 
 Again, I haven't tried this with Mingw.  I'll take a look.
 

Thanks.

 If I create an object file from the Poly/ML GUI using PolyML.export,
 polyc will link it. If I understand what is going on correctly, the
 resulting program is a Windows application that brings up the Poly/ML
 GUI to provide the standard input, output and error channels,  unless
 it is run with standard input and output connected to pipes, in which
 case it works like a pipe. I think I may end up having to package the
 Standard ML parts of my application as a server, with the GUI
 provided by clients implemented in some other language. Are there any
 other options?
 
 I think there are three possible options for building Poly/ML on Windows: 
 Mingw, Visual C or Cygwin.  If you use Mingw or Visual C you are building the 
 native Windows version.  This version does put up the GUI, as you say, if the 
 standard input and output are missing.  This is actually done by the RTS 
 before the ML code is entered so applies equally to functions exported with 
 PolyML.export as to the usual Poly/ML read-eval-print loop.  Actually, it 
 occurs to me that it is now possible to write the GUI in ML and include it as 
 part of the top-level root function in Windows.  This would allow a 
 user-exported function to completely by-pass it.  I think a GUI is necessary 
 for Windows applications since that is what Windows users would expect.

I would actually have expected the “GUI” to be a command prompt window. I.e., I 
would have expected poly to be a console application. This is how python comes, 
for example. Something that behaves like a console application is what cc on 
MinGW seems to give you if you don’t give it any of the Windows-specific 
command line options when you compile a standard C program.

 
 Using Cygwin might be a possibility if you are thinking of providing a 
 separate GUI.  The package that Makarius has provided for running Isabelle on 
 Windows uses Poly/ML under Cygwin but all the user interaction is through 
 jEdit.  There might be issues, though, if you wanted the ML code to access 
 the Windows filing system because Cygwin imposes its own view of the filing 
 system.
 

Cygwin does work for me, but unfortunately, having to install it is a stopper 
for some of my potential users. I tried compiling under MinGW with __CYGWIN__ 
set, but it doesn’t work. Would it be difficult to separate the choice between 
polystub.c being a standard C application and a Windows application from the 
__CYGWIN__ flag?

Regards,

Rob.


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

[polyml] Poly on MinGW

[Rob Arthan]

I am trying to understand my options for using Poly/ML on MinGW for building 
windows applications coded in Standard ML.

There is a bug reported in http://sourceforge.net/p/mingw/bugs/2043/ that you 
have to work around to build Poly/ML with the current MinGW. The work-around is 
to run configure with CXXFLAGS=-D_GLIBCXX_HAVE_FENV_H=1” in the environment. 
(I suspect I should also throw -O3 in there too, as I think that setting 
CXXFLAGS replaces its initial setting of -O3 inside the makefiles. Is that 
right?)

Having got Poly/ML to compile, I found that polyc gives errors like the 
following when asked to compile a source file:

gcc.exe: error: C:/DOCUME~1/rda/LOCALS~1/Temp/polyobj.2724.obj: No such file or 
directory

If I create an object file from the Poly/ML GUI using PolyML.export, polyc will 
link it. If I understand what is going on correctly, the resulting program is a 
Windows application that brings up the Poly/ML GUI to provide the standard 
input, output and error channels,  unless it is run with standard input and 
output connected to pipes, in which case it works like a pipe. I think I may 
end up having to package the Standard ML parts of my application as a server, 
with the GUI provided by clients implemented in some other language. Are there 
any other options?

Regards,

Rob.






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

Re: [polyml] Poly/ML 5.5.2 Released

[Rob Arthan]

David,

On 12 May 2014, at 12:08, David Matthews david.matth...@prolingua.co.uk wrote:

 On 11/05/2014 17:21, Rob Arthan wrote:
 David,
 
 On 11 May 2014, at 12:23, David Matthews
 david.matth...@prolingua.co.uk wrote:
 
 On 10/05/2014 15:07, Rob Arthan wrote:
 The line that sets EXTRALDFLAGS for Mac OS X in polyc.in is
 missing a double quote character and this causes polyc to raise a
 syntax error.
 
 I've fixed that in SVN trunk and the fixes-5.2.2 branch.  I wonder
 whether it is worth exporting that and updating the tar.gz file on
 SourceForge.
 
 I think it might be worth fixing the 5.5.2 release tar.gz file as you
 have been encouraging people to use polyc and without the fix it just
 doesn’t work at all on Mac OS X.
 
 OK, I've just done that.  Can you check that it works?  In general I don't 
 like replacing public files in place once they've been released but I've made 
 an exception in this case.
 

Nothing seems to have changed - the line that sets EXTRALDFLAGS is still wrong.

Regards,

Rob.

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

Re: [polyml] Poly/ML 5.5.2 Released

[Rob Arthan]

David,

On 11 May 2014, at 12:23, David Matthews david.matth...@prolingua.co.uk wrote:

 On 10/05/2014 15:07, Rob Arthan wrote:
 The line that sets EXTRALDFLAGS for Mac OS X in polyc.in is missing a
 double quote character and this causes polyc to raise a syntax
 error.
 
 I've fixed that in SVN trunk and the fixes-5.2.2 branch.  I wonder whether it 
 is worth exporting that and updating the tar.gz file on SourceForge.

I think it might be worth fixing the 5.5.2 release tar.gz file as you have been 
encouraging people to use polyc and without the fix it just doesn’t work at all 
on Mac OS X.

Regards,

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

Re: [polyml] polyc

[Rob Arthan]

On 6 May 2014, at 12:56, David Matthews david.matth...@prolingua.co.uk wrote:

 Hi Rob,
 I've been away and I'm now just trying to catch up.
 
 On 23/04/2014 17:13, Rob Arthan wrote:
 I have a couple of comments and a query about polyc (which seemed 
 particularly attractive
 on Cygwin, where there seems to be quite a long list of libraries you need 
 to know
 about if you are going to call the linker directly).
 
 The comment is that the help text is a bit misleading as it has more 
 functionality
 than just compiling and linking a source file, e.g., you can pass it the 
 name of
 an object file and it will link it with libpolymain and libpolyml.
 
 I take it you mean the text that gets printed with polyc --help.  The man 
 page contains a bit more.  Any suggestions for a suitable, brief replacement?

Yes, that is what I meant. I had a go at this, but came to a halt when I 
realised that the implementation didn’t quite match the man page or my 
expectations. I expected polyc to use the file name extension to distinguish 
between source files and object files. The man page says it treats text files 
as source files and binary files as object files. The implementation checks the 
extension first and uses that to make the distinction if it recognises it. 
Otherwise it has a go at using the file program to see if the file is a text 
file. Was this actually what was intended? It seems odd not just to rely on the 
extensions (perhaps making them case insensitive, so you would recognise foo.ml 
and FOO.SML as well as foo.ML and foo.sml).

Here is the text I would propose for the implementation I expected:

Usage: polyc [OPTION]... [SOURCEFILE | OBJECTFILE]

Compile and/or link a file with Poly/ML.

A Standard ML source file has extension .ML or .sml and must define
a function 'main' of type 'unit - unit' that will be called when the
executable is run. An object file has a .o extension.

Options:

   -c   Compile but do not link, writing an object file with the
same base name as the source file
   -o fileWrite the executable file to file (default 'a.out')
Ignored if not linking
   --help   Write this help text and exit

Regards,

Rob.

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

Re: [polyml] Poly/ML 5.5.2 Released

[Rob Arthan]

On 9 May 2014, at 16:00, David Matthews david.matth...@prolingua.co.uk wrote:

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


The line that sets EXTRALDFLAGS for Mac OS X in polyc.in is missing a double 
quote character and this causes polyc to raise a syntax error.

When I fixed polyc, it gave the warning that was discussed in an earlier thread 
about version 5.5.1 
(http://lists.inf.ed.ac.uk/pipermail/polyml/2013-September/001353.html):

ld: warning: could not create compact unwind for _ffi_call_unix64: does not use 
RBP or RSP based frame

This doesn’t seem to have any adverse effects.

Regards,

Rob.




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

[polyml] printInAlphabeticalOrder

[Rob Arthan]

I am confused about what PolyML.Compiler.printInAlphabeticalOrder is intended 
to control.
If I enter the following:

signature S = sig val x : int val z : int val y : int end;
structure S = struct val x = 1 val z = 3 val y = 2 end;

the signature and the structure are both printed with the variables in reverse 
alphabetical
order. (I was rather hoping for an option to have them in the source code 
order.)

Regards,

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

[polyml] Pretty-printing infix constructors

[Rob Arthan]

When I executed the following

infix xxx;
datatype XXX = op xxx of int * string;
1 xxx banana;

I was rather hopping the expression at the end would print out with infix 
notation but it doesn't:

val it = xxx (1, banana): XXX

Is there an option in Poly/ML to have infix constructors print as infixes, or 
do I need to
write my own pretty-printer to get that.

Regards,

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

Re: [polyml] suppressing compiler output

[Rob Arthan]

On 29 Mar 2013, at 08:42, Gergely Buday gbu...@gmail.com wrote:

 
 Back to the original question: this is why I would like to suppress any 
 compiler message.
 
 

The function PolyML.compiler lets you write your own customised read-eval-print 
loop. In the code below, the fun my_read_eval_print_loop is a variant of the 
usual one that sends all compiler output to standard error and exits when 
standard input runs out. if you put it in my-revl.ML and run

poly  my-revl.ML 1a 2b

there will be a small predictable set of compiler messages at the head of file 
a followed by the standard output of the other code in my-revl.ML and all the 
rest of the compiler messages go in file b.  If you make an executable that 
runs my_read_eval_print_loop following Phil Clayton's post, then you will get a 
program that compiles and runs ML code and sends all compiler messages to 
standard error (so you can discard them using 2/dev/null on the command line).

Regards,

Rob.

=== beginning of my-revl.ML 
fun read_or_exit () = (
case TextIO.input1 TextIO.stdIn of
NONE = Posix.Process.exit 0wx0
|   some = some
);

fun my_read_eval_print_loop () = (
PolyML.compiler (read_or_exit,
[PolyML.Compiler.CPOutStream
(fn s = TextIO.output(TextIO.stdErr, s))]) ();
my_read_eval_print_loop ()
);

val _ = my_read_eval_print_loop();

(* could also do PolyML.export(my-revl, read_eval_print_loop) at this point *)

fun repeat f n = if n = 0 then () else (f (); repeat f (n-1));

fun say s () = TextIO.output(TextIO.stdOut, s ^ \n);

val hello = repeat (say Hello World!);

hello 10;

val goodbye = repeat (say Goodbye cruel World!);

goodbye 10;
=== end of my-revl.ML 

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

Re: [polyml] suppressing compiler output

[Rob Arthan]

David,

On 29 Mar 2013, at 11:50, David Matthews david.matth...@prolingua.co.uk wrote:

 On 29/03/2013 08:42, Gergely Buday wrote:
 Back to the original question: this is why I would like to suppress any
 compiler message.
 
 I did not find such a flag in the manual, would it be possible to add one,
 David?
 
 There have been a few suggestions for how to write your own top level and 
 that's definitely the best way if you really want control over the output.  
 I've just committed a change so that the -q option now sets 
 PolyML.print_depth to zero so that by default the output won't be printed.  
 To suppress the prompt you would be better off using the --use option to run 
 the file directly.  You will need to add
 OS.Process.exit OS.Process.success: unit;
 at the end if you don't want to enter the main read-eval-print-loop.

Quite a common thing to do in UN*X applications is not to prompt if the input 
isn't a terminal. Obviously, I can write my own read-eval-print loop that does 
that (indeed the read-eval-print loop in my earlier post on this topic doesn't 
prompt at all), but it might be a nice companion to the change you have just 
made to make the top level do that out of the box. That would give Gergely 
Buday exactly what he is asking for (i.e., the ability to have poly read code 
from the standard input and only output what the compiled code outputs).

Regards,

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

Re: [polyml] Poly/ML 5.5

[Rob Arthan]

David,

Many thanks for the new release. ProofPower builds and test fine on it. I don't 
have any specific feedback on performance yet - the build process itself is 
somewhat atypical.

On 15 Sep 2012, at 09:16, David Matthews wrote:

 ...
 Object files now use standard text and data areas when exporting. In 
 particular this means that it is no longer necessary to use --segprot on Mac 
 OS X to avoid a bus error.
 

I have make files that detect Mac OS X and insert the -segprot option 
automatically. Should I change these to be more specific about Poly/ML 
versions, or is it harmless to continue to give the -segprot option?

Regards,

Rob.___
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

[Rob Arthan]

Phil,

I don't think your test-1.sml is correct Standard ML. If you cut it right down 
to:

type ('a, 'b) t = 'b;
fun mkT n = (n : ('a, int) t);
val x = mkT 2;

You will find that Poly/ML says:

Warning-The type of (x) contains a free type variable. Setting it to a unique
   monotype.
val x = 2: (_a, int) t

and SML/NJ says:

Warning: type vars not generalized because of
   value restriction are instantiated to dummy types (X1,X2,...)
val x = 2 : (?.X1,int) t

What is happening here is that if x is given it most general type based on the 
right-hand side of the binding, then the binding is illegal so the compilers 
are generating a dummy monomorphic type to let it get through.

If you try it with an explicit type constraint as in:

val y : ('a, int) t = mkT 2;

both compilers will correctly raise an error.

The problem is the so-called value restriction (see 
http://users.cis.fiu.edu/~smithg/cop4555/valrestr.html). Since the right-hand 
side for your value binding for x involves a function call, and its type 
contains a free type variable, the value restriction disallows it. It seems 
when you wrap this up with the type constraints in signatures and the bindings 
in structures, the problem shows up at a different level and the error messages 
are a bit misleading, but the fundamental issue is that ML won't give x defined 
as you have defined it a polymorphic type.

Tip: with problems like this, it is often helps to see what happens with fewer 
signature constraints. Your example goes through with a warning if you remove 
the signature constraint on structure B - and it is that warning that explains 
why it can't work with the signature constraint.

Regards,

Rob.


(e.g., see http://users.cis.fiu.edu/~smithg/cop4555/valrestr.html)
On 21 Jul 2012, at 10:53, Phil Clayton wrote:

 Apparently the plain text attachments didn't work for everyone (and they're 
 not very readable via the list archive) so here they are again, this time as 
 a binary blob.
 
 Phil
 
 
 On 20/07/12 14:49, Phil Clayton wrote:
 I have been making use of phantom types (for encoding a
 single-inheritance class hierarchy) and have encountered a case where
 code accepted by MLton does not type check with Poly/ML.  After
 investigating, it appears that MLton, Poly/ML and SML/NJ all take
 different views on what is a valid program!
 
 Attached are two small examples with a slight difference where type
 checking accepts/rejects as follows:
 
 test-1.sml  test-2.sml
 
   MLton   20100608  accept  accept
   Poly/ML 5.4, latest   reject  accept
   SML/NJ  110.73reject  reject
 
 I don't know which of the above is consistent with the Definition yet.
 (I would be very glad if test-1 is a legal program though!)
 
 Phil
 
 
 ___
 polyml mailing list
 polyml@inf.ed.ac.uk
 http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
 
 
 
 tests.tar.gz___
 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] Poly/ML and SML/NJ warn inconsistently about using op for an infix constructor

[Rob Arthan]

On 4 Apr 2012, at 11:48, David Matthews wrote:

 On 03/04/2012 16:20, Rob Arthan wrote:
 On 30 Mar 2012, at 12:52, David Matthews wrote:
 
 Looking carefully at the syntax, though, op is not allowed in a
 datatype specification although in all other respects the syntax of
 a binding and a specification are the same.  I've added an error
 message if op is used in a specification.
 
 I didn't look at the syntax of modules. You are quite right. In fact,
 as far as I can see, op is not allowed anywhere in a signature.
 
 I've now reduced the error message to a warning since it seems Isabelle has 
 op in signatures.

Tut, tut :-). Somewhat to my surprise, the ProofPower source does comply with 
the standard syntax, even though I was completely unaware that op wasn't 
allowed in signatures.

 
 I hadn't actually realised that op was allowed on exception
 bindings and I've now fixed that.  I think a sensible approach is
 to produce a warning in the cases where a symbol could be used as
 an infix; in an expression, a fun binding or in a pattern (val
 binding) and to ignore it in other cases.
 
 I think it is wise to give the warning in those cases, because other
 compilers are not as liberal as Poly/ML, so I read the warning as a
 warning about a potential portability problem (and always act on
 it).
 
 Do any other compilers complain about missing op in those cases?

Yes, SML/NJ and MLton don't allow an infix vid without an op as an expression 
or a pattern.

 Phil's point was that SML/NJ was complaining about the presence of op 
 rather than its absence.

It is only a warning. I think Phil's point was that, as things stood, you 
couldn't write a datatype declaration with an infix constructor that would not 
give a warning on one of the two compilers: as was, Poly/ML warned when you 
didn't use op before an infix constructor in a datatype, while SML/NJ warned 
when you did.

  I tried an op in a datatype in a signature in MLton and it didn't say 
 anything although it's not correct.

Likewise SML/NJ appears to extend the standard syntax by allowing op in 
datatypes in signature (but giving a warning saying that they are unnecessary).

 
 Out of interest, are you still planning to allow things like (+)?
 
 Do you mean something like
val p = map (+)
 rather than
val p = map (op +)?
 I wasn't planning to since I don't think it's legal ML.  Did you mean 
 somewhere else?

No, that is what I meant: Poly/ML 5.4.1 doesn't share your view that it is 
illegal:

Poly/ML 5.4.1 Release
 (+);
Warning-(+) has infix status but was not preceded by op.
val it = fn: int * int - int
 map (+);
Warning-(+) has infix status but was not preceded by op.
val it = fn: (int * int) list - int list

This is why I said the warning is useful as it flags a potential portability 
problem: other compilers won't compile the above.

Regards,

Rob.


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

Re: [polyml] Building MS Windows applications

[Rob Arthan]

David,

Many thanks.  It's been a few years since I last used Visual Studio and I never 
progressed beyond beginner status, so I think MSYS and MinGW will minimise the 
culture shock for me for the time being!

On 17 Feb 2011, at 09:24, David Matthews wrote:

 I think I actually built that using Msys/Mingw.  If you install them you can 
 build from source exactly as you would on Unix or cygwin.

Done.  But when I do PolyML.export(hw, main)  and run the following in an 
MSYS shell:

gcc -o hw hw.obj -L/usr/lib -lpolymain -lpolyml

then I get a complaint that there is an undefined reference to 'WinMain@16'. I 
managed to devise a more complicated gcc command line that works by looking at 
how the Poly/ML installation creates poly.exe, but the result is a Windows 
application which just flashes up a window and executes immediately. Can I 
create a console application? I.e., an application with a C/C++ main() and 
C/C++ console I/O rather than a WinMain() and a GUI?

Aside: for the record, the more complicated command line that worked was:

gcc -o hw -mwindows -Wl,-u -Wl,_WinMain@16 hw.obj -L/usr/lib -lpolymain -lpolyml


  There are other possibilities.  There are project files for Visual C++ 6 
 which should work under newer versions of Visual C++.  I think it's now 
 possible to download Visual C++ Express free from Microsoft but you'll also 
 need a version of MASM if you want to build Poly/ML from source.
 

Regards,

Rob.

 Regards,
 David
 
 On 16/02/2011 16:56, Rob Arthan wrote:
 I have installed Poly/ML on MS Windows using the precompiled binary.
 Now I want to start building my own applications. What do I need for
 the equivalent in MS Windows of the following command line that I
 would use on UNIX?
 
 cc -o hello hello.o -lpolymain -lpolyml
 
 I.e., where do I find the polymain and polyml DLLs and what developer
 kits can I use? E.g., will MinGW work? And which developer kits are
 recommended?
 
 Regards,
 
 Rob.
 
 
 
 ___ 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] Building MS Windows applications

[Rob Arthan]

I have installed Poly/ML on MS Windows using the precompiled binary. Now I want 
to start building my own applications. What do I need for the equivalent in MS 
Windows of the following command line that I would use on UNIX?

cc -o hello hello.o -lpolymain -lpolyml

I.e., where do I find the polymain and polyml DLLs and what developer kits can 
I use? E.g., will MinGW work? And which developer kits are recommended?

Regards,

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

Re: [polyml] redirecting stdout elsewhere

[Rob Arthan]

On 19 Nov 2010, at 20:07, Makarius wrote:

 On Sun, 14 Nov 2010, Rob Arthan wrote:
 
 For the record, you can also achieve this kind of effect with Posix.IO.dup2. 
 See below for sample code.
 
 This looks like an interesting trick.  Can it also handle output produced by 
 the Poly/ML runtime system (exception_trace etc.)?
 

Yes, it can - who does that remind me of? :-)

Regards,

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

Re: [polyml] redirecting stdout elsewhere

[Rob Arthan]

Lucas,

For the record, you can also achieve this kind of effect with Posix.IO.dup2. 
See below for sample code.

Regards,

Rob.


(*

Redirecting standard output to a file using the Posix facilities
in the SML Basis Library.

Implements a stack of output files.

Rob Arthan. r...@lemma-one.com 12th November 2008.

*)
local
(*
Open Posix.IO then Posix.FileSys structures - order matters!
*)
open Posix.IO Posix.FileSys TextIO;
(*
Take a duplicate of current stdout.
*)
val duplicate_stdout : file_desc = dup stdout;
(*
Create an initially empty stack of file descriptors:
*)
val stack : file_desc list ref = ref [];
(*
File creation mode: read/write for user, group and others,
but bits set with umask(1) will be cleared as usual.
*)
val rw_rw_rw = S.flags[S.irusr, S.iwusr, S.irgrp,
S.iwgrp, S.iroth, S.iwoth];
in
(*
push_out_file: start a new output file, stacking the file descriptor.
*)
fun push_output_file {name: string, append : bool} : unit = (
let val flags = if append then O.append else O.trunc;
val fd = createf(name, O_WRONLY, flags, rw_rw_rw);
in  output(stdOut, *** Redirecting output to \ ^ name ^ \\n);
dup2{old = fd, new = stdout};
stack := fd :: !stack
end
);
(*
pop_output_file: close file descriptor at top of stack and
revert to previous; returns true if the output file stack
is not empty on exit, so you can close all open output files
and clear the stack with:

while pop_output_file() do ();

*)
fun pop_output_file (() : unit) : bool = (
(case !stack of
cur_fd :: rest = (
close cur_fd;
stack := rest
) | [] = ());
case !stack of
fd :: _ = (
dup2{old = fd, new = stdout};
true
) | [] = (
dup2{old = duplicate_stdout, new = stdout};
false
)
);
end;

On 13 Nov 2010, at 20:39, Lucas Dixon wrote:

 Thanks! that is exactly what I was looking for.
 
 lucas
 
 On 13/11/2010 01:06, Matthew Fluet wrote:
 I think you want the setOutstream function of the IMPERATIVE_IO
 signature (matched by TextIO), probably in conjunction with the
 getOutstream function.
 See 
 http://www.standardml.org/Basis/imperative-io.html#SIG:IMPERATIVE_IO.setOutstream:VAL
 
 -Matthew
 
 On Fri, Nov 12, 2010 at 7:16 PM, Lucas Dixonldi...@inf.ed.ac.uk  wrote:
 Hi,
 
 I was recently wondering if it is possible to redirect std-out to go to a
 different output stream in ML. Has anyone done anything similar? I was
 having trouble seeing how to do this with the Standard-ML basis...
 
 any suggestions on directions to look at? I can see how to effectively to it
 by hacking the compiler... but was wondering if there is a better way...
 (surely!?) ?
 
 cheers,
 lucas
 
 --
 The University of Edinburgh is a charitable body, registered in
 Scotland, with registration number SC005336.
 
 ___
 polyml mailing list
 polyml@inf.ed.ac.uk
 http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
 
 
 
 
 -- 
 The University of Edinburgh is a charitable body, registered in
 Scotland, with registration number SC005336.
 
 ___
 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] Poly/ML 5.4

[Rob Arthan]

David,

On 19 Aug 2010, at 18:59, David Matthews wrote:

 Matthew,
 That looks suspiciously like the execute bit problem.  Did you include
 -segprot POLY rwx rwx
 to the linker? See the last line of (the updated) 
 http://www.polyml.org/FAQ.html#standalone

On that point, I recall having some problems caused by using cc rather than 
c++. Was that an illusion?

Regards,

Rob.

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

Re: [polyml] Detecting unreferenced identifiers

[Rob Arthan]

David,

On 31 Aug 2009, at 18:26, you wrote:


Rob Arthan wrote:
 I have a problem building ProofPower with the latest Poly/ML. The  
build
 goes into a loop at a point where it opens a certain structure.  
This
 will be the first time Poly/ML has had to pretty-print a value of  
the
 type THM that represents theorems. This type has a circularity  
passing
 through a ref and a certain dictionary data type. I have attached  
a very

 cutdown version of the failing code. The cutdown version behaves
 slightly differently in that I see some never-ending output,  
while the

 ProofPower build just goes into a silent busy hang.

 The dictionary type OE_DICT that causes the problem is an amalgam  
of two

 simpler dictionary data types S_DICT (simple dictionaries using an
 association list) and E_DICT (efficient dictionaries using a hash  
key

 and a binary tree). Somewhat oddly the problem doesn't happen if I
 replace OE_DICT with either S_DICT or E_DICT even though the
 representation type for OE_DICT is just S_DICT * E_DICT.

I'm not sure what's happening in detail in your example but there has
been a significant change in the way printing works in the latest
version.  A printing function (and an equality function, if  
appropriate)

is now compiled for each type as it is created.  This means that
printing and type-specific equality functions are available in a  
wider

range of cases than they used to be, particularly in functors.

Previously, the code checked whether there was circularity and just
printed ... when it detected it.  That's not really possible with  
the

current code so it relies on the print depth (PolyML.print_depth) to
stop infinite looping.  Setting print_depth to 10 in your example
produces much more sensible output.



That works. Even better for me, if I change the order of compilation  
so that my user-defined pretty-printer for the circular type is  
installed first, that works too.



The only simple solution I can suggest is to set the default for the
printer depth to something much smaller, perhaps 10.  There's  
probably

no reason for the current, essentially unconstrained, print depth.

 I also noted in passing that types declared as abstypes are now  
equality
 types. Was this a conscious attempt to implement one of the  
Successor ML

 proposals?

No, it was something I noticed while working on the printing and
equality code.  An early draft of Standard ML explicitly said that
abstypes were not equality types outside the with...end block and
that's what Poly/ML implemented.  When I looked again recently I
couldn't actually see that anywhere in either the ML90 or ML97
definitions and it seems to conflict with the way equality is  
handled in
the semantics.  For that reason I took out the code which switched  
off

equality.



Section 4.9 of the ML97 definitions describes something called Abs(TE,  
VE) that I think is changing the types declared between abstype and  
with into non-equality types and getting rid of their constructors.  
I think the conflict you mention is why there is a Successor ML  
proposal to do what you have done.


Regards,

Rob.


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

[polyml] Performance problems with saving and loading state

[Rob Arthan]

We have performance problems with ProofPower when compiled with Poly/ML using 
the latest sources as compared with version 5.2.1. The main problem is with 
loading a large state. In some of QinetiQ's tests, it now takes nearly 40 
minutes to load a state (occupying about 150Mb on disc) that previously took 
about 20 seconds.

Unfortunately, my attempts to create simple examples of this type problem do 
not exhibit much difference between 5.2.1 and the latest sources. I wondered 
if anyone else has had similar problems or has any suggestions about how to 
isolate the problem.

I believe the problem is quite old. It apparently predates the move from CVS 
to SVN.

Regards,

Rob.

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