Poly/ML

polyml@lists.polyml.org

698 discussions

More portable poly compilation
by makarius＠sketis.net 24 Dec '17

24 Dec '17

Dear experts on building and linking C++ applications, according to the blog "Creating portable Linux binaries" http://insanecoding.blogspot.de/2012/07/creating-portable-linux-binaries.ht… the following options could make the poly executable more portable accross different Linux versions: CFLAGS="-static-libgcc -static-libstdc++ -Wl,-Bstatic -lgmp -Wl,-Bdynamic" On the surface this works fine on x86_64-linux (Ubuntu 16.04 LTS), but there is a remaining dependency on libpolyml.so, which itself depends on dynamic gcc and stdc++ libraries. Including "-lpolyml" next to "-lgmp" above does not work, probably because these options also apply to the build process of libpolyml itself. How can I make libpolyml a static part of poly? Alternatively, how can I make libgcc and libstdc++ a static part of libpolyml? Makarius

3 2

C++ standard in use
by matthew.fernandez＠gmail.com 23 Dec '17

23 Dec '17

Hi David et al, While experimenting with some of the recent PolyML commits, I realised the build system doesn?t seem to set any particular C++ standard. I guess this results in the compiler default (e.g. GNU++14 in the latest GCC [0]). Is this intentional? Relatedly, coming up on 2018 it seems like it would be reasonable to require a compiler with C++11 support. I?m not sure how backwards compatible PolyML needs to be these days, but e.g. support for Windows 95/98 has been dropped. I notice some comments in interpreter.cpp that imply whatever is in Debian stable is a lower bound. Moving to C++11 would allow some parts of the code base to be replaced with their C++11 equivalents, reducing the maintenance burden. Some candidates: - Bitmap -> std::vector<bool> - NORETURNFN -> [[noreturn]] - PCondVar -> std::condition_variable - PLock -> std::mutex - PLocker -> std::lock_guard Perhaps this will provide a performance boost as well, but I wouldn?t necessarily count on it. I?d be curious to hear if anyone has strong feelings about this or if any PolyML devs out there are living with a pre-C++11 compiler. Thanks, Matt [0]: https://gcc.gnu.org/onlinedocs/gcc/Standards.html#C_002b_002b-Language

3 6

FFI conversions that are portable across Poly/ML versions
by phil.clayton＠veonix.com 22 Dec '17

22 Dec '17

I am trying to define LargeInt.int conversions for C integer types in terms of those supplied in Foreign in a way that will work with both Poly/ML 5.6 or 5.7. This requires that e.g. - Foreign.cUint64 is used for Poly/ML = 5.6 but - Foreign.cUint64Large is used for Poly/ML >= 5.7 I am thinking of achieving this by having separate SML files for different Poly/ML versions and using the right one as follows: let val version = PolyML.rtsVersion () in PolyML.use ( if version >= 570 then "src-5.7.sml" else if version = 560 then "src-5.6.sml" else raise Fail "unsupported Poly/ML version" ) end Is this a future-proof way to choose based on Poly/ML version? Another option might be to copy the implementation of these conversions from Foreign.sml but that may not be possible - for example I couldn't see how to get the flag bigEndian in an application. Is there a better way altogether with some compiler trickery? Phil

2 1

Retiring CInterface?
by David.Matthews＠prolingua.co.uk 18 Dec '17

18 Dec '17

Now that the Foreign structure has been around for a while I was wondering whether it was time to remove CInterface and the related structures. Is there any specific need to keep it? David

3 3

More robust shell script: allow spaces in directory names.
by Makarius 15 Dec '17

15 Dec '17

diff --git a/polyc.in b/polyc.in index adaa586..e460305 100755 --- a/polyc.in +++ b/polyc.in @@ -1,14 +1,14 @@ #! /bin/sh -prefix=@prefix@ -exec_prefix=@exec_prefix@ -BINDIR=@bindir@ -LINK=@CXX@ -LIBDIR=@libdir@ +prefix="@prefix@" +exec_prefix="@exec_prefix@" +BINDIR="@bindir@" +LINK="@CXX@" +LIBDIR="@libdir@" LIBS="@dependentlibs@" CFLAGS="@polyc_CFLAGS@" DEFAULT_COMPILER="${BINDIR}/poly" -COMPILER=${DEFAULT_COMPILER} +COMPILER="${DEFAULT_COMPILER}" # Extra options for Windows. config.status sets these conditionals to either "" or "#". @@ -25,27 +25,27 @@ COMPILER=${DEFAULT_COMPILER} # Msys passes the Windows TEMP in temp (lower case) # On other systems allow TMPDIR to override /tmp. - at NATIVE_WINDOWS_TRUE@TEMPORARYDIR=${temp:-/tmp} - at NATIVE_WINDOWS_FALSE@TEMPORARYDIR=${TMPDIR:-/tmp} + at NATIVE_WINDOWS_TRUE@TEMPORARYDIR="${temp:-/tmp}" + at NATIVE_WINDOWS_FALSE@TEMPORARYDIR="${TMPDIR:-/tmp}" # Extra options for Mac OS X @MACOSLDOPTS_TRUE at EXTRALDFLAGS="-Wl,-no_pie" -TMPOBJFILE=${TEMPORARYDIR}/polyobj.$$.$SUFFIX +TMPOBJFILE="${TEMPORARYDIR}/polyobj.$$.$SUFFIX" trap 'rm -f "$TMPOBJFILE"' 0 compile() { - echo "val () = use (List.nth(CommandLine.arguments(), 2)); val () = PolyML.export(List.nth(CommandLine.arguments(), 3), main);" | ${COMPILER} -q --error-exit "$1" "$2" + echo "val () = use (List.nth(CommandLine.arguments(), 2)); val () = PolyML.export(List.nth(CommandLine.arguments(), 3), main);" | "${COMPILER}" -q --error-exit "$1" "$2" } link() { if [ X"$2" = "X" ] then - ${LINK} ${EXTRALDFLAGS} ${CFLAGS} "$1" -L${LIBDIR} -Wl,-rpath,${LIBDIR} -lpolymain -lpolyml ${LIBS} + "${LINK}" ${EXTRALDFLAGS} ${CFLAGS} "$1" "-L${LIBDIR}" "-Wl,-rpath,${LIBDIR}" -lpolymain -lpolyml ${LIBS} else - ${LINK} ${EXTRALDFLAGS} ${CFLAGS} "$1" -o "$2" -L${LIBDIR} -Wl,-rpath,${LIBDIR} -lpolymain -lpolyml ${LIBS} + "${LINK}" ${EXTRALDFLAGS} ${CFLAGS} "$1" -o "$2" "-L${LIBDIR}" "-Wl,-rpath,${LIBDIR}" -lpolymain -lpolyml ${LIBS} fi } @@ -112,8 +112,8 @@ done case "$compileonly" in yes) if [ "x$outputfile" = "x" ]; then - basename=${sourcefile##*/} - outputfile=${basename%.*}.o + basename="${sourcefile##*/}" + outputfile="${basename%.*}.o" fi compile "$sourcefile" "$outputfile" ;;

1 0

Build error: Exception- InternalError: Too many passes raised while compiling
by kostirya＠gmail.com 15 Dec '17

15 Dec '17

Hello. Poly/ML broken on FreeBSD i386 (clang version 3.8.0). ./polyimport polytemp.txt -I . < ./exportPoly.sml Use: basis/build.sml ... Use: basis/FinalPolyML.sml Exception- InternalError: Too many passes raised while compiling The error appeared due to commit 3886935542311d70fec94a3bc5da8b302792a79b (Tue Nov 28 17:45:49 2017) Turn byte moves of four or eight bytes (on X86/64) into moves of single words provided the alignment is correct. This is primarily to handle moves between SysWord.word and volatileRef. Nick.

2 1

PolyML sources [InternalError: asGenReg raised while compiling]
by David.Matthews＠prolingua.co.uk 01 Dec '17

01 Dec '17

Hi Bernard, Thanks for sending me that. I've committed a fix to Git master (6af4a34) which seems to fix it. This is a fix to the compiler so will need make compiler to rebuild the compiler. It's very simple so may be a candidate for the fixes branch once it's been tested a bit more widely. Regards, David On 30/11/2017 14:11, Bernard Berthomieu wrote: > Hello David, > > Many thanks for you help. > > I could isolate the part of my code in which the failure is raised. > To reproduce the problem, unpack the archive attached then type: > > ??? cd src_bb > ??? poly < build.ML > > > With release aa3b02654b38ad3faadc60c5960702cba6be87df or older, > all files in build.ML are loaded successfully. > > With current 5.7.1, compiling the last file fails and it prints: > > ??? Exception- InternalError: asGenReg raised while compiling > > ??? Exception- Fail "Exception- InternalError: asGenReg raised while > compiling" > ??? ?? raised > > > The last file simply applies two functors defined in the previous files. > > Regards, > ? Bernard. >

2 1

Approaching release of 5.7.1
by David.Matthews＠prolingua.co.uk 30 Nov '17

30 Nov '17

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

9 37

5.7.1 release candidate
by binghe.lisp＠gmail.com 21 Nov '17

21 Nov '17

Thanks, now I see something useful: $ echo foo | ./munge.exe The exported object file has version 5.71 but this library supports 5.70 (then it hangs) I have Poly/ML 5.7 installed in /usr/local (by Homebrew on Mac OS X 10.11), and the new 5.7.1 manually installed into $HOME. So I guess, when building `munge.exe` it must have been linked with libpolyml.a (or libpolymain.a) in /usr/local/lib because I didn?t put $HOME/lib into DYLD_LIBRARY_PATH (LD_LIBRARY_PATH on Linux). After completely removing Poly/ML 5.7 and rebuilding and installing 5.7.1 into /usr/local, the problem is resolved. Now munge.exe works correctly on my side. P. S. but multiple copies of Poly/ML actually worked well in all other cases, I normally use Poly/ML 5.6 (installed into a dedicated directory) to build HOL4 K11 release but never needed to build and run munge.exe from that version. Any way, sorry for disturbing. Regards, Chun > Il giorno 21 nov 2017, alle ore 12:18, Michael.Norrish at data61.csiro.au ha scritto: > > Those that passed are not tests of the munger per se: they are building the necessary background theories, and the munger executables. Those tests that you are trying to run are actually trying to execute the mungers. > > If you test a munger interactively with > > $ echo foo | ./munge.exe > > what do you see? > > Michael > > On 21/11/17, 19:52, "Chun Tian" <binghe.lisp at gmail.com> wrote: > > Hi, > > I rebuilt again with -t option. By default Holmake have 4 parallel threads, now all are blocked by munge tests: > > 501 60326 60299 0 9:48am ttys000 0:00.00 /bin/sh -c ./tymunge.exe < tyabb_input > tyabb_output > 501 60327 60326 0 9:48am ttys000 0:00.00 ./tymunge.exe > 501 60330 60299 0 9:48am ttys000 0:00.00 /bin/sh -c ./munge.exe < input > output > 501 60331 60330 0 9:48am ttys000 0:00.00 ./munge.exe > 501 60332 60299 0 9:48am ttys000 0:00.00 /bin/sh -c ./utymunge.exe < tyabb_input > utyabb_output > 501 60333 60332 0 9:48am ttys000 0:00.00 ./utymunge.exe > 501 60334 60299 0 9:48am ttys000 0:00.00 /bin/sh -c ./munge.exe < gh242_input > gh242_output > 501 60335 60334 0 9:48am ttys000 0:00.00 ./munge.exe > > However some munge tests indeed passed: > > Building directory src/TeX/theory_tests [21 Nov, 09:48:01] > Recursively calling Holmake in /Users/binghe/ML/HOL.stdknl/tools/cmp > Finished recursive invocation in /Users/binghe/ML/HOL.stdknl/tools/cmp > tyabbrevTheory OK > foo248Theory OK > bag248Theory OK > mdtTheory OK > untyabbrevTheory OK > pp248Theory OK > tymunge.exe OK > munge.exe OK > utymunge.exe OK > munge248.exe OK > > Regards, > > Chun Tian > >> Il giorno 21 nov 2017, alle ore 03:57, Michael.Norrish at data61.csiro.au ha scritto: >> >> Does HOL build with the -t option? >> >> This does some testing of the munging technology. >> >> Michael >> >> On 21/11/17, 10:03, "polyml on behalf of Chun Tian" <polyml-bounces at inf.ed.ac.uk on behalf of binghe.lisp at gmail.com> wrote: >> >> Hi Ramana, >> >> I found that ?munge.exe? (generated from theories) doesn?t work with this new Poly release: it simply hangs when converting *.htex to *.tex files ? and when I switched back to poly 5.6, it worked again. >> >> Can you confirm this on your side? >> >> ?Chun >> >>> Il giorno 20 nov 2017, alle ore 22:58, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> ha scritto: >>> >>> The 5.7.1 candidate appears to work for HOL4 and CakeML - I haven't done extensive tests, but normal builds seem fine. >>> >>> On 21 November 2017 at 08:41, Makarius <makarius at sketis.net> wrote: >>> On 20/11/17 14:23, David Matthews wrote: >>>> Thanks to everyone who sent in bug reports. We're almost ready to >>>> release 5.7.1. I've updated Git master ( 44b7b88 ) with pre-built >>>> compilers for 5.7.1. This is the last chance check it before the >>>> release which will probably happen at the end of the week. >>> >>> I have successfully built this version on Linux, Windows, mac OS, and >>> ran vorious manual tests of Isabelle + AFP. It all looks fine. >>> >>> Note that I will be on travel on Wed--Fri this week, so if there are any >>> last-minute issues, I cannot do any tests during these days. >>> >>> >>> Makarius >>> >>> _______________________________________________ >>> polyml mailing list >>> polyml at inf.ed.ac.uk >>> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml >>> >>> _______________________________________________ >>> polyml mailing list >>> polyml at inf.ed.ac.uk >>> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml >> >> >> > > >

1 0

5.7.1 release candidate
by David.Matthews＠prolingua.co.uk 20 Nov '17

20 Nov '17

Thanks to everyone who sent in bug reports. We're almost ready to release 5.7.1. I've updated Git master ( 44b7b88 ) with pre-built compilers for 5.7.1. This is the last chance check it before the release which will probably happen at the end of the week. David

5 4

← Newer
1
...
9
10
11
12
13
14
15
...
70
Older →

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