Re: [polyml] Size of stand-alone executables

t; > 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 call

[polyml] Problem linking .o file

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:

Re: [polyml] Problem with compact32bit

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, &g

Re: [polyml] Problem with compact32bit

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 &

Re: [polyml] Problem with compact32bit

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

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

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

Re: [polyml] Testing Poly/ML 5.8

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

Re: [polyml] Testing Poly/ML 5.8

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

Re: [polyml] Testing Poly/ML 5.8

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

Re: [polyml] Approaching release of 5.7.1

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

Re: [polyml] Approaching release of 5.7.1

gt; 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

Re: [polyml] Approaching release of 5.7.1

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

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

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

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

> 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 var

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

> 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

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

mpare 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

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

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 1

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

tended 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.cp

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

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 <

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

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

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

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 a

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

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

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

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:

Re: [polyml] Equality Type Parameter in Datatype Declaration

> 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

Re: [polyml] Equality Type Parameter in Datatype Declaration

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

Re: [polyml] not printed exception when executed file

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" )

[polyml] Poly/ML changes history

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

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

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

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

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) =

Re: [polyml] Poly/ML Changes History

> 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 change

[polyml] Poly/ML Changes History

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.

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

> 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

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

> 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

Re: [polyml] Fixed precision int

> 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: >

Re: [polyml] Towards Poly/ML 5.6

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 e

[polyml] addPrettyPrinter type security

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

Re: [polyml] Towards Poly/ML 5.6

egards, 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...

Re: [polyml] Towards Poly/ML 5.6

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

[polyml] Lexical analyser bug?

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

[polyml] C Interface documentation

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

Re: [polyml] regarding problem with PolyML debugging prompt

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

Re: [polyml] can't quit sessions

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

Re: [polyml] .polyml and poly-stats

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

Re: [polyml] .polyml and poly-stats

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

Re: [polyml] .polyml and poly-stats

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

Re: [polyml] Poly on MinGW

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

Re: [polyml] Poly on MinGW

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

[polyml] Poly on MinGW

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

Re: [polyml] Poly/ML 5.5.2 Released

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

Re: [polyml] Poly/ML 5.5.2 Released

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

Re: [polyml] polyc

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

Re: [polyml] Poly/ML 5.5.2 Released

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

[polyml] printInAlphabeticalOrder

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

[polyml] Pretty-printing infix constructors

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

Re: [polyml] suppressing compiler output

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

Re: [polyml] suppressing compiler output

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

Re: [polyml] Poly/ML 5.5

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

Re: [polyml] Type inference issue with phantom types

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:

Re: [polyml] Poly/ML and SML/NJ warn inconsistently about using op for an infix constructor

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

Re: [polyml] Building MS Windows applications

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

[polyml] Building MS Windows applications

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

Re: [polyml] redirecting stdout elsewhere

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

Re: [polyml] redirecting stdout elsewhere

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

Re: [polyml] Poly/ML 5.4

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

Re: [polyml] Detecting unreferenced identifiers

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

[polyml] Performance problems with saving and loading state

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