Poly/ML

polyml@lists.polyml.org

2 participants
711 discussions

polyml install to Alpine Linux
by dtopham＠gmail.com 20 Oct '20

20 Oct '20

I noticed same error seemed to have occurred from user installing to gentoo Linux. I can't tell from this if it was resolved or not (I'm relatively inexperienced) https://bugs.gentoo.org/713178 One thing in common between Alpine and this environment is they are using musl libc Could that be an issue?

4 7

polyml install to Alpine Linux
by dtopham＠gmail.com 18 Oct '20

18 Oct '20

Thanks Stefan! Brilliant! It is so nice to have a supportive community to build software with! That did it: no-pie On Sat, Oct 17, 2020 at 2:41 PM <polyml-request at inf.ed.ac.uk> wrote: > Send polyml mailing list submissions to > polyml at inf.ed.ac.uk > > To subscribe or unsubscribe via the World Wide Web, visit > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > or, via email, send a message with subject or body 'help' to > polyml-request at inf.ed.ac.uk > > You can reach the person managing the list at > polyml-owner at inf.ed.ac.uk > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of polyml digest..." > > > Today's Topics: > > 1. Re: polyml Digest, Vol 168, Issue 4 (David Topham) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sat, 17 Oct 2020 14:39:11 -0700 > From: David Topham <dtopham at gmail.com> > To: polyml at inf.ed.ac.uk > Subject: Re: [polyml] polyml Digest, Vol 168, Issue 4 > Message-ID: > <CAD034BFJRPsZzodxyX3iE5O+V-_E81p=+ > sbPr9PJxowMS6hZ+g at mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Thank you for the quick response. That is useful to know. Perhaps my > original download of source was corrupt. I tried again this time use the > polyml-master.zip *from github" and that made it much further. > > I think it may be almost complete, but got a segment fault at the last > minute. > > make all-recursive > make[1]: Entering directory '/root/polyml-master' > Making all in libpolyml > make[2]: Entering directory '/root/polyml-master/libpolyml' > Making all in libffi > make[3]: Entering directory '/root/polyml-master/libpolyml/libffi' > make 'AR_FLAGS=' 'CC_FOR_BUILD=' 'CFLAGS=-O3 -fomit-frame-pointer > -fstrict-aliasing -ffast-math -march=pentium -Wall -fexceptions' > 'CXXFLAGS=-g -O2' 'CFLAGS_FOR_BUILD=' 'CFLAGS_FOR_TARGET=' > 'INSTALL=/usr/bin/install -c' 'INSTALL_DATA=/usr/bin/install -c -m 644' > 'INSTALL_PROGRAM=/usr/bin/install -c' 'INSTALL_SCRIPT=/usr/bin/install -c' > 'JC1FLAGS=' 'LDFLAGS=' 'LIBCFLAGS=' 'LIBCFLAGS_FOR_TARGET=' 'MAKE=make' > 'MAKEINFO=/bin/sh /root/polyml-master/libpolyml/libffi/missing makeinfo ' > 'PICFLAG=' 'PICFLAG_FOR_TARGET=' 'RUNTESTFLAGS=' 'SHELL=/bin/sh' > 'exec_prefix=/usr/local' 'infodir=/usr/local/share/info' > 'libdir=/usr/local/lib' 'mandir=/usr/local/share/man' 'prefix=/usr/local' > 'AR=ar' 'AS=as' 'CC=gcc' 'CXX=g++' 'LD=/usr/i586-alpine-linux-musl/bin/ld' > 'NM=/usr/bin/nm -B' 'RANLIB=ranlib' 'DESTDIR=' all-recursive > make[4]: Entering directory '/root/polyml-master/libpolyml/libffi' > Making all in include > make[5]: Entering directory '/root/polyml-master/libpolyml/libffi/include' > make[5]: Nothing to be done for 'all'. > make[5]: Leaving directory '/root/polyml-master/libpolyml/libffi/include' > Making all in testsuite > make[5]: Entering directory > '/root/polyml-master/libpolyml/libffi/testsuite' > make[5]: Nothing to be done for 'all'. > make[5]: Leaving directory '/root/polyml-master/libpolyml/libffi/testsuite' > Making all in man > make[5]: Entering directory '/root/polyml-master/libpolyml/libffi/man' > make[5]: Nothing to be done for 'all'. > make[5]: Leaving directory '/root/polyml-master/libpolyml/libffi/man' > make[5]: Entering directory '/root/polyml-master/libpolyml/libffi' > make[5]: Leaving directory '/root/polyml-master/libpolyml/libffi' > make[4]: Leaving directory '/root/polyml-master/libpolyml/libffi' > make[3]: Leaving directory '/root/polyml-master/libpolyml/libffi' > make[3]: Entering directory '/root/polyml-master/libpolyml' > make[3]: Nothing to be done for 'all-am'. > make[3]: Leaving directory '/root/polyml-master/libpolyml' > make[2]: Leaving directory '/root/polyml-master/libpolyml' > Making all in libpolymain > make[2]: Entering directory '/root/polyml-master/libpolymain' > make[2]: Nothing to be done for 'all'. > make[2]: Leaving directory '/root/polyml-master/libpolymain' > Making all in . > make[2]: Entering directory '/root/polyml-master' > make[2]: Leaving directory '/root/polyml-master' > Making all in modules > make[2]: Entering directory '/root/polyml-master/modules' > Making all in IntInfAsInt > make[3]: Entering directory '/root/polyml-master/modules/IntInfAsInt' > echo "use \"./ROOT.sml\";" | ../../poly -q -error-exit > Segmentation fault > make[3]: *** [Makefile:479: IntInfAsInt] Error 139 > make[3]: Leaving directory '/root/polyml-master/modules/IntInfAsInt' > make[2]: *** [Makefile:377: all-recursive] Error 1 > make[2]: Leaving directory '/root/polyml-master/modules' > make[1]: *** [Makefile:729: all-recursive] Error 1 > make[1]: Leaving directory '/root/polyml-master' > make: *** [Makefile:488: all] Error 2 > > On Sat, Oct 17, 2020 at 4:00 AM <polyml-request at inf.ed.ac.uk> wrote: > > > Send polyml mailing list submissions to > > polyml at inf.ed.ac.uk > > > > To subscribe or unsubscribe via the World Wide Web, visit > > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > > or, via email, send a message with subject or body 'help' to > > polyml-request at inf.ed.ac.uk > > > > You can reach the person managing the list at > > polyml-owner at inf.ed.ac.uk > > > > When replying, please edit your Subject line so it is more specific > > than "Re: Contents of polyml digest..." > > > > > > Today's Topics: > > > > 1. building polyml on Alpine Linux (David Topham) > > 2. Re: PolyML REPL (Anton Lobach) > > 3. Re: building polyml on Alpine Linux (David Matthews) > > > > > > ---------------------------------------------------------------------- > > > > Message: 1 > > Date: Fri, 16 Oct 2020 15:17:37 -0700 > > From: David Topham <dtopham at gmail.com> > > To: polyml at inf.ed.ac.uk > > Subject: [polyml] building polyml on Alpine Linux > > Message-ID: > > < > > CAD034BH36eK--zKkho2iYUi4x6Ar+7qjg28Le3T-NfS+Js-pTQ at mail.gmail.com> > > Content-Type: text/plain; charset="utf-8" > > > > I have been trying to get polyml working on Alpine Linux 32-bit > > > > Since there is't yet a package to install it, I tried getting the source > > from github > > > > When doing make, I first got error about missing libffi directory. > > > > I thought I may bypass that by configuring with option to use system > libffi > > i.e. > > apk add libffi-dev > > ./configure --with-system-libffi --with-x > > > > Here is result: > > > > ---------------- > > make all-recursive > > make[1]: Entering directory '/root/vfpub/polyml-master' > > Making all in libpolyml > > make[2]: Entering directory '/root/vfpub/polyml-master/libpolyml' > > make[3]: Entering directory '/root/vfpub/polyml-master/libpolyml' > > /bin/sh ../libtool --tag=CXX --mode=compile g++ -DHAVE_CONFIG_H -I. > > -I.. -O3 -Wall -DMODULEDIR=\"/usr/local/lib/polyml/modules\" -O3 -MT > > arb.lo -MD -MP -MF .deps/arb.Tpo -c -o arb.lo arb.cpp > > libtool: compile: g++ -DHAVE_CONFIG_H -I. -I.. -O3 -Wall > > "-DMODULEDIR=\"/usr/local/lib/polyml/modules\"" -O3 -MT arb.lo -MD -MP > -MF > > .deps/arb.Tpo -c arb.cpp -fPIC -DPIC -o .libs/arb.o > > arb.cpp:87:10: fatal error: globals.h: No such file or directory > > 87 | #include "globals.h" > > | ^~~~~~~~~~~ > > compilation terminated. > > make[3]: *** [Makefile:800: arb.lo] Error 1 > > make[3]: Leaving directory '/root/vfpub/polyml-master/libpolyml' > > make[2]: *** [Makefile:840: all-recursive] Error 1 > > make[2]: Leaving directory '/root/vfpub/polyml-master/libpolyml' > > make[1]: *** [Makefile:729: all-recursive] Error 1 > > make[1]: Leaving directory '/root/vfpub/polyml-master' > > make: *** [Makefile:488: all] Error 2 > > --------------------------- > > > > Has anyone had luck building on Alpine? > >

1 0

polyml Digest, Vol 168, Issue 4
by dtopham＠gmail.com 17 Oct '20

17 Oct '20

Thank you for the quick response. That is useful to know. Perhaps my original download of source was corrupt. I tried again this time use the polyml-master.zip *from github" and that made it much further. I think it may be almost complete, but got a segment fault at the last minute. make all-recursive make[1]: Entering directory '/root/polyml-master' Making all in libpolyml make[2]: Entering directory '/root/polyml-master/libpolyml' Making all in libffi make[3]: Entering directory '/root/polyml-master/libpolyml/libffi' make 'AR_FLAGS=' 'CC_FOR_BUILD=' 'CFLAGS=-O3 -fomit-frame-pointer -fstrict-aliasing -ffast-math -march=pentium -Wall -fexceptions' 'CXXFLAGS=-g -O2' 'CFLAGS_FOR_BUILD=' 'CFLAGS_FOR_TARGET=' 'INSTALL=/usr/bin/install -c' 'INSTALL_DATA=/usr/bin/install -c -m 644' 'INSTALL_PROGRAM=/usr/bin/install -c' 'INSTALL_SCRIPT=/usr/bin/install -c' 'JC1FLAGS=' 'LDFLAGS=' 'LIBCFLAGS=' 'LIBCFLAGS_FOR_TARGET=' 'MAKE=make' 'MAKEINFO=/bin/sh /root/polyml-master/libpolyml/libffi/missing makeinfo ' 'PICFLAG=' 'PICFLAG_FOR_TARGET=' 'RUNTESTFLAGS=' 'SHELL=/bin/sh' 'exec_prefix=/usr/local' 'infodir=/usr/local/share/info' 'libdir=/usr/local/lib' 'mandir=/usr/local/share/man' 'prefix=/usr/local' 'AR=ar' 'AS=as' 'CC=gcc' 'CXX=g++' 'LD=/usr/i586-alpine-linux-musl/bin/ld' 'NM=/usr/bin/nm -B' 'RANLIB=ranlib' 'DESTDIR=' all-recursive make[4]: Entering directory '/root/polyml-master/libpolyml/libffi' Making all in include make[5]: Entering directory '/root/polyml-master/libpolyml/libffi/include' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/root/polyml-master/libpolyml/libffi/include' Making all in testsuite make[5]: Entering directory '/root/polyml-master/libpolyml/libffi/testsuite' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/root/polyml-master/libpolyml/libffi/testsuite' Making all in man make[5]: Entering directory '/root/polyml-master/libpolyml/libffi/man' make[5]: Nothing to be done for 'all'. make[5]: Leaving directory '/root/polyml-master/libpolyml/libffi/man' make[5]: Entering directory '/root/polyml-master/libpolyml/libffi' make[5]: Leaving directory '/root/polyml-master/libpolyml/libffi' make[4]: Leaving directory '/root/polyml-master/libpolyml/libffi' make[3]: Leaving directory '/root/polyml-master/libpolyml/libffi' make[3]: Entering directory '/root/polyml-master/libpolyml' make[3]: Nothing to be done for 'all-am'. make[3]: Leaving directory '/root/polyml-master/libpolyml' make[2]: Leaving directory '/root/polyml-master/libpolyml' Making all in libpolymain make[2]: Entering directory '/root/polyml-master/libpolymain' make[2]: Nothing to be done for 'all'. make[2]: Leaving directory '/root/polyml-master/libpolymain' Making all in . make[2]: Entering directory '/root/polyml-master' make[2]: Leaving directory '/root/polyml-master' Making all in modules make[2]: Entering directory '/root/polyml-master/modules' Making all in IntInfAsInt make[3]: Entering directory '/root/polyml-master/modules/IntInfAsInt' echo "use \"./ROOT.sml\";" | ../../poly -q -error-exit Segmentation fault make[3]: *** [Makefile:479: IntInfAsInt] Error 139 make[3]: Leaving directory '/root/polyml-master/modules/IntInfAsInt' make[2]: *** [Makefile:377: all-recursive] Error 1 make[2]: Leaving directory '/root/polyml-master/modules' make[1]: *** [Makefile:729: all-recursive] Error 1 make[1]: Leaving directory '/root/polyml-master' make: *** [Makefile:488: all] Error 2 On Sat, Oct 17, 2020 at 4:00 AM <polyml-request at inf.ed.ac.uk> wrote: > Send polyml mailing list submissions to > polyml at inf.ed.ac.uk > > To subscribe or unsubscribe via the World Wide Web, visit > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > or, via email, send a message with subject or body 'help' to > polyml-request at inf.ed.ac.uk > > You can reach the person managing the list at > polyml-owner at inf.ed.ac.uk > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of polyml digest..." > > > Today's Topics: > > 1. building polyml on Alpine Linux (David Topham) > 2. Re: PolyML REPL (Anton Lobach) > 3. Re: building polyml on Alpine Linux (David Matthews) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 16 Oct 2020 15:17:37 -0700 > From: David Topham <dtopham at gmail.com> > To: polyml at inf.ed.ac.uk > Subject: [polyml] building polyml on Alpine Linux > Message-ID: > < > CAD034BH36eK--zKkho2iYUi4x6Ar+7qjg28Le3T-NfS+Js-pTQ at mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > I have been trying to get polyml working on Alpine Linux 32-bit > > Since there is't yet a package to install it, I tried getting the source > from github > > When doing make, I first got error about missing libffi directory. > > I thought I may bypass that by configuring with option to use system libffi > i.e. > apk add libffi-dev > ./configure --with-system-libffi --with-x > > Here is result: > > ---------------- > make all-recursive > make[1]: Entering directory '/root/vfpub/polyml-master' > Making all in libpolyml > make[2]: Entering directory '/root/vfpub/polyml-master/libpolyml' > make[3]: Entering directory '/root/vfpub/polyml-master/libpolyml' > /bin/sh ../libtool --tag=CXX --mode=compile g++ -DHAVE_CONFIG_H -I. > -I.. -O3 -Wall -DMODULEDIR=\"/usr/local/lib/polyml/modules\" -O3 -MT > arb.lo -MD -MP -MF .deps/arb.Tpo -c -o arb.lo arb.cpp > libtool: compile: g++ -DHAVE_CONFIG_H -I. -I.. -O3 -Wall > "-DMODULEDIR=\"/usr/local/lib/polyml/modules\"" -O3 -MT arb.lo -MD -MP -MF > .deps/arb.Tpo -c arb.cpp -fPIC -DPIC -o .libs/arb.o > arb.cpp:87:10: fatal error: globals.h: No such file or directory > 87 | #include "globals.h" > | ^~~~~~~~~~~ > compilation terminated. > make[3]: *** [Makefile:800: arb.lo] Error 1 > make[3]: Leaving directory '/root/vfpub/polyml-master/libpolyml' > make[2]: *** [Makefile:840: all-recursive] Error 1 > make[2]: Leaving directory '/root/vfpub/polyml-master/libpolyml' > make[1]: *** [Makefile:729: all-recursive] Error 1 > make[1]: Leaving directory '/root/vfpub/polyml-master' > make: *** [Makefile:488: all] Error 2 > --------------------------- > > Has anyone had luck building on Alpine? >

1 0

building polyml on Alpine Linux
by dtopham＠gmail.com 17 Oct '20

17 Oct '20

I have been trying to get polyml working on Alpine Linux 32-bit Since there is't yet a package to install it, I tried getting the source from github When doing make, I first got error about missing libffi directory. I thought I may bypass that by configuring with option to use system libffi i.e. apk add libffi-dev ./configure --with-system-libffi --with-x Here is result: ---------------- make all-recursive make[1]: Entering directory '/root/vfpub/polyml-master' Making all in libpolyml make[2]: Entering directory '/root/vfpub/polyml-master/libpolyml' make[3]: Entering directory '/root/vfpub/polyml-master/libpolyml' /bin/sh ../libtool --tag=CXX --mode=compile g++ -DHAVE_CONFIG_H -I. -I.. -O3 -Wall -DMODULEDIR=\"/usr/local/lib/polyml/modules\" -O3 -MT arb.lo -MD -MP -MF .deps/arb.Tpo -c -o arb.lo arb.cpp libtool: compile: g++ -DHAVE_CONFIG_H -I. -I.. -O3 -Wall "-DMODULEDIR=\"/usr/local/lib/polyml/modules\"" -O3 -MT arb.lo -MD -MP -MF .deps/arb.Tpo -c arb.cpp -fPIC -DPIC -o .libs/arb.o arb.cpp:87:10: fatal error: globals.h: No such file or directory 87 | #include "globals.h" | ^~~~~~~~~~~ compilation terminated. make[3]: *** [Makefile:800: arb.lo] Error 1 make[3]: Leaving directory '/root/vfpub/polyml-master/libpolyml' make[2]: *** [Makefile:840: all-recursive] Error 1 make[2]: Leaving directory '/root/vfpub/polyml-master/libpolyml' make[1]: *** [Makefile:729: all-recursive] Error 1 make[1]: Leaving directory '/root/vfpub/polyml-master' make: *** [Makefile:488: all] Error 2 --------------------------- Has anyone had luck building on Alpine?

2 1

PolyML REPL
by antonlobach＠uri.edu 17 Oct '20

17 Oct '20

Hi, Does PolyML REPL produce native code or does it work as an interpreter? Regards, Anton Lobach

2 2

polyml sometimes runs out of memory with plenty available
by sorear＠fastmail.com 05 Oct '20

05 Oct '20

Attempting to run the CakeML CI test sequence (a 2-3 day process) on any Poly/ML version newer than 5.7 frequently results in out of memory errors. The probability of any given test failing is low and seems very sensitive to environmental factors, and I am still trying to reliably reproduce the failure in any setting, but I have managed to generate --debug gc --debug heapsize logs from failures (attached). The log file is from v5.8.1 but I have seen the issue on several different HEAD revisions over the past month. The "Run out of store - interrupting threads" message in the middle of a block of GC output makes me suspect a race condition but otherwise I have little to go on here. Any advice would be appreciated. I'll update if I find anything. The machine has 256GB installed and I generally run tests with --maxheap 75000, so a failure with a heap size of only 2GB is quite odd. -s

2 3

Non-blocking sockets
by vijay.the.lisper＠gmail.com 07 Sep '20

07 Sep '20

To use the non-blocking functions like acceptNB and sendVecNB, do I need to explicitly set the socket to non-blocking mode? If that is the case, how can I do it? Are there any documents/examples on how to generally do non-blocking IO in PolyML? Thank you, Vijay

3 2

Updates in master - statistics and support for secure OSs
by David.Matthews＠prolingua.co.uk 11 Aug '20

11 Aug '20

There have been a number of updates in the pipeline that were held off until 5.8.1 was released. I've merged a few into master and there are some more that will come in in due course. Statistics: The statistics have been revisited, particularly the shared statistics. The statistics now include information about garbage-collections and other operations that cause the ML environment to be suspended. Obviously this is only useful if the statistics are being read by another process but the idea is that it would be possible to provide information to a user about why the ML environment is not responding. On Unix Poly/ML only creates the shared memory file for the statistics if --exportstats is given. The file is now created in the directory given in the $POLYSTATSDIR environment variable if that is present, falling back to $HOME/.polyml otherwise. When looking for remote statistics $POLYSTATSDIR is checked first followed by $HOME/.polyml. Secure OSs: There is now support for OpenBSD and SELinux in enforcing mode. There was a problem with these operating systems because they forbid the creation of memory areas with both execute and write permissions. In order to create and garbage collect ML code the RTS needs to be able to write to the code areas and it also needs to be executed. The work-around is to use memory mapped files and create two separate regions mapped to the same file. This is only done if the usual memory allocation with read-write-execute permission fails. I wanted to get this working because I was concerned that at some point more main-stream operating systems, such as Mac OS, might introduce a similar restriction. Note that there is still an issue with text-relocations but this can be got round using either "chcon -t textrel_shlib_t poly" on SELinux or LDFLAGS='-Wl,-z,notext' on OpenBSD. David

2 2

Version 5.8.1 Release
by David.Matthews＠prolingua.co.uk 22 Jul '20

22 Jul '20

After the recent bug fixes I thought it was time to produce a new release. There are very few new features; it's almost all bug fixes. Thanks to everyone for the patches and bug reports. David

3 4

Compiler (0ad5aa87) raises Option
by Michael.Norrish＠data61.csiro.au 10 Jul '20

10 Jul '20

I don't expect this in isolation will help, but the following HOL function causes the compiler to emit a Fail "Exception- Option unexpectedly raised while compiling" message. ?- - - fun EXISTS_SEP_REWRITE_RULE rw th = let (* possibly fragile *) val (p,q) = dest_eq (concl (SPEC_ALL rw)) val frame = genvar(type_of p) val vs = list_dest dest_sep_exists p val lhs = mk_star(last vs,frame) val vs = butlast vs fun find_exists_match lhs tm = let val (v,t) = dest_sep_exists tm val vs = list_dest dest_sep_exists tm in (butlast vs,last vs,generic_star_match [] lhs (last vs)) end fun find_term_and_apply f tm = f (find_term (can f) tm) fun foo th = let val (ws,tm,s) = find_term_and_apply (find_exists_match lhs) (concl th) val (t,t2) = (dest_eq (concl (SPEC_ALL rw))) val zs = list_dest dest_sep_exists t val (zs,z) = (butlast zs,list_dest dest_star (last zs)) val xs = list_dest dest_star tm val ys = filter (fn y => not (tmem y (map (subst s) z))) xs val t3 = foldr mk_sep_exists (subst s (list_mk_star z (type_of frame))) (map (subst s) zs) val goal = foldr mk_sep_exists (list_mk_star (t3::ys) (type_of frame)) ws val goal = mk_eq(foldr mk_sep_exists tm ws,goal) val lemma = auto_prove "EXISTS_SEP_REWRITE_RULE" (goal, SIMP_TAC std_ss [GSYM rw] THEN SIMP_TAC (std_ss++sep_cond_ss) [SEP_CLAUSES] THEN CONV_TAC (BINOP_CONV SEP_EXISTS_AC_CONV) THEN SIMP_TAC (std_ss++star_ss) [AC CONJ_ASSOC CONJ_COMM]) val lemma = CONV_RULE (RAND_CONV (ONCE_REWRITE_CONV [rw] THENC SIMP_CONV std_ss [SEP_CLAUSES])) lemma in foo (RW1 [lemma] th) end handle HOL_ERR _ => th in foo th end; - - - This comes from HOL4's examples/machine-code/hoare-triple/helperLib.sml (line 667 onwards). I will try to reduce it to a smaller instance. Michael

4 8

← Newer
1
...
4
5
6
7
8
9
10
...
72
Older →

Jump to page:

2026

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