Poly/ML

polyml@lists.polyml.org

3 participants
698 discussions

hitherto unobserved error while building HOL on ARM Mac
by michael.norrish＠anu.edu.au 18 Jul '22

18 Jul '22

I see signal 11 (seg fault) periodically, but I just also saw > Assertion failed: (space->partialGCScan+length+1 <= space->lowerAllocPtr), function ScanOwnedAreas, file quick_gc.cpp, line 499. This is running SHA bafe319b. -- Michael Norrish School of Computing, Australian National University Canberra, AUSTRALIA E: michael.norrish at anu.edu.au W: cecs.anu.edu.au/people/michael-norrish

1 0

Update to ARM code-generator
by David.Matthews＠prolingua.co.uk 25 Jan '22

25 Jan '22

The long-promised update to the ARM code-generator is now in Git master. This builds on the old version by adding the register allocation strategy borrowed from the X86 version as well as low-level peephole optimisation. On my Apple M1 processor it now seems to be faster than X86 code with Rosetta. There are still some improvements to be made, particularly with floating point, but no major changes are anticipated. It includes one optimisation that isn't present on the X86 at the moment: small tuples are returned in registers rather than on the stack. Please try it and let me know how it goes. David

3 3

Poly/ML package in Debian and Ubuntu
by David.Matthews＠prolingua.co.uk 17 Jan '22

17 Jan '22

Does anyone know anything about the polyml package in Debian and Ubuntu? It seems that the currently packaged version is still 5.7.1. I've seen a couple of bug reports that have turned out to be issues that have long since been fixed. I'm quite happy to have Poly/ML packaged for distributions but if they get out of date then they become a problem. David

2 2

Start poly in an augmented environment
by technical+polymlmailinglist＠zacque.tk 08 Dec '21

08 Dec '21

Hi, I find the Basis Library to be inadequate for many of my use cases. E.g. I'm used to having built-in Set and Map/Dict abstract datatypes (ADTs); and built-in sort function for all the common ADTs. Then, I realise I can start poly by loading all the code with "--use FILE" from command line. So, my question is how to suppress "poly --use ROOT.sml" loaded definition message to STDOUT? E.g. $ poly --use ROOT.sml Poly/ML 5.8.2 Release val testme = "Test me!": string <---- suppress this line val it = (): unit <---- and this line > 1; val it = 1: int <---- while keep printing of results I have tried "poly --use 'FILE' -q" with the "-q" option. But it turns off printing of results as well (which is undesired). I hope there is an easy way (probably a switch/flag?) to achieve what I want, and avoid writing another REPL. Thanks! -- Cheers, zacque

2 2

5.9 released
by David.Matthews＠prolingua.co.uk 07 Dec '21

07 Dec '21

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

4 3

Polyml installation
by d_parkinson＠gmx.com 05 Dec '21

05 Dec '21

An HTML attachment was scrubbed... URL: <http://lists.inf.ed.ac.uk/pipermail/polyml/attachments/20211205/e300306b/at…>

2 1

Size of stand-alone executables
by rda＠lemma-one.com 27 Nov '21

27 Nov '21

David, Thanks for your reply to my post about linking errors. You were quite right. I have now rebuilt everything on 5.8.2 and have reproduced the problem I was trying to investigate. My user was trying to create an executable to run a specific function in an extension of ProofPower as a stand-alone program rather than via the ProofPower read-eval-print loop. He was surprised that executable is much bigger than the saved state that the read-eval-print loop loads. Here are the sizes I got. -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.) Regards, Rob.

3 3

Problem linking .o file
by rda＠lemma-one.com 25 Nov '21

25 Nov '21

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.

2 1

Detect Current Running OS in Poly/ML
by technical+polymlmailinglist＠zacque.tk 13 Nov '21

13 Nov '21

Hi, How to detect the current running OS in Poly/ML? I'm looking for something like: datatype Platform = Linux | Windows | macOS | BSD | ... val getPlatform : unit -> Platform If not, how can I implement something like this, if possible? I'm asking because it's useful for writing OS specific library, e.g. path library to print Unix/Windows-style path. I've tried searching around the web and looking into the Basis Library manual, but still couldn't find anything useful. Any pointer will be much appreciated. Thanks! -- Cheers, zacque

2 2

Updates to master for 5.9 release
by David.Matthews＠prolingua.co.uk 13 Nov '21

13 Nov '21

There have been a number of updates to master since the initial announcement. Thank you for all the feedback. Most of the issues have been about the ARM64 code-generator. Some could be fixed easily but one has required more work. The symptom was an InternalError exception that indicated that the code was too large for the offset in an instruction. This has now been fixed by using a pair of instructions in that case but it has required changes to the run-time system to handle the different relocations that are needed. That had to be done for each of the major operating systems since Linux/BSD, Windows and Mac OS each have their own object code format. It's possible, though unlikely, that these changes have broken something on platforms other than ARM so I will hold off the final release for a week or in case there are any problems. David

1 0

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

Poly/ML