[polyml] C++ standard in use

2017-12-15 Thread Matthew Fernandez
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
 - 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
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] polyc and libraries

2017-12-15 Thread David Matthews

On 15/12/2017 18:41, Makarius wrote:

On 15/12/17 17:46, David Matthews wrote:

On 15/12/2017 16:15, Makarius wrote:


    * The polyc script cannot handle directory names with spaces, e.g. the
main "prefix".


I guess it would need some extra quotation.  Do you want to propose a fix?


See the included change: my very first commit produced with git (with
VSCode and gitk).


Thanks.  I'll have a look at that.


    * Instead of insisting in hardwired directory locations it should be
possible to refer to the relative location of the polyc itself.  In GNU
bash I am using THIS="$(cd "$(dirname "$0")"; pwd)" -- it is unclear to
me how to do it in /bin/sh.


The paths are set from the installation directories in configure i.e.
where the binaries and libraries are to be installed.  It's possible to
set the library and binary directories independently so there's no
necessary relationship between them.


The above change might already be sufficient for that: isabelle
build_polyml merely needs to change /bin/sh into bash and make the
prefix relative. This will allow users of Isabelle to use the bundled
Poly/ML polyc, even though it is not directly relevant for Isabelle --
see also
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-February/msg00144.html


I don't think you can give configure anything but absolute paths but 
when I'm testing I usually set --libdir, --bindir and --mandir to the 
same directory so everything ends up in the same place.  The only case 
where I've had a problem is with shared libraries in Msys/Mingw where 
libtool insists on putting the DLL in "libdir/../bin".



I see further references to the install dir in:

   pkgconfig/polyml.pc
   libpolymain.la
   libpolyml.la

Are these relevant for polyc?


No.  polyml.pc is only used if you have pkg_config.  The other two are 
only used by libtool as far as I'm aware.


David


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

Re: [polyml] polyc and libraries

2017-12-15 Thread David Matthews

On 15/12/2017 16:15, Makarius wrote:

On 12/12/17 14:14, David Matthews wrote:

The polyc script has been developed mainly to simplify the linking of an
exported ML function and in particular to try to capture the libraries
that need to be included.  I've been having another look at this because
of an issue that was reported a while back.


Here are some further observations and open problems from the past:

   * The polyc script cannot handle directory names with spaces, e.g. the
main "prefix".


I guess it would need some extra quotation.  Do you want to propose a fix?


   * Instead of insisting in hardwired directory locations it should be
possible to refer to the relative location of the polyc itself.  In GNU
bash I am using THIS="$(cd "$(dirname "$0")"; pwd)" -- it is unclear to
me how to do it in /bin/sh.


The paths are set from the installation directories in configure i.e. 
where the binaries and libraries are to be installed.  It's possible to 
set the library and binary directories independently so there's no 
necessary relationship between them.



   * Use of libgmp on Mac OS X is generally unclear to me. Is there a
robust way to build poly with gmp on an old OS version (e.g. Mac OS X
10.10) and use it on a newer one? Is there any chance to do this with
x86 instead of x86_64?


There have been problems with linking libgmp and Poly/ML on Mac OS X in 
the past.  Is there someone who uses Mac OS who could answer this?


David



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

Re: [polyml] polyc and libraries

2017-12-15 Thread David Matthews
There seems to be a problem with building it as a shared library in 
FreeBSD.  It seems to work fine with

./configure --disable-shared

David

On 15/12/2017 12:58, Kostirya wrote:

It is broken. I think this is because of the inconsistency of the
options: -nostdlib and -lstdc++.

libtool: link: c++  -fPIC -DPIC -shared -nostdlib /usr/lib/crti.o
/usr/lib/crtbeginS.o  .libs/arb.o .libs/basicio.o .libs/bitmap.o
.libs/check_objects.o .libs/diagnostics.o .libs/errors.o
.libs/exporter.o .libs/foreign.o .libs/gc.o .libs/gc_check_weak_ref.o
.libs/gc_copy_phase.o .libs/gc_mark_phase.o .libs/gc_share_phase.o
.libs/gc_update_phase.o .libs/gctaskfarm.o .libs/heapsizing.o
.libs/locking.o .libs/memmgr.o .libs/mpoly.o .libs/network.o
.libs/objsize.o .libs/osmem.o .libs/pexport.o .libs/poly_specific.o
.libs/polyffi.o .libs/polystring.o .libs/process_env.o
.libs/processes.o .libs/profiling.o .libs/quick_gc.o .libs/realconv.o
.libs/reals.o .libs/rts_module.o .libs/rtsentry.o .libs/run_time.o
.libs/save_vec.o .libs/savestate.o .libs/scanaddrs.o .libs/sharedata.o
.libs/sighandler.o .libs/statistics.o .libs/timing.o .libs/xwindows.o
.libs/x86_dep.o .libs/x86assembly_gas32.o .libs/elfexport.o
.libs/unix_specific.o  -Wl,--whole-archive
libffi/.libs/libffi_convenience.a -Wl,--no-whole-archive
-L/usr/local/lib -lpthread -lgmp -lstdc++ -L/usr/lib -lc++ -lm -lc
-lgcc -lgcc_s /usr/lib/crtendS.o /usr/lib/crtn.o  -O3   -Wl,-soname
-Wl,libpolyml.so.9 -o .libs/libpolyml.so.9.0.0
/usr/bin/ld: cannot find -lstdc++
c++: error: linker command failed with exit code 1 (use -v to see invocation)
*** Error code 1

Stop.
make[1]: stopped in /scr/polyml_git/libpolyml
*** Error code 1


I delete
AC_CHECK_LIB(stdc++, main)
line from configure.ac and do successfully built polyml on FreeBSD and
DragonFlyBSD. But stdc++ is need for linux...
___
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] polyc and libraries

2017-12-15 Thread Makarius
On 12/12/17 14:14, David Matthews wrote:
> The polyc script has been developed mainly to simplify the linking of an
> exported ML function and in particular to try to capture the libraries
> that need to be included.  I've been having another look at this because
> of an issue that was reported a while back.

Here are some further observations and open problems from the past:

  * The polyc script cannot handle directory names with spaces, e.g. the
main "prefix".

  * Instead of insisting in hardwired directory locations it should be
possible to refer to the relative location of the polyc itself.  In GNU
bash I am using THIS="$(cd "$(dirname "$0")"; pwd)" -- it is unclear to
me how to do it in /bin/sh.

  * Use of libgmp on Mac OS X is generally unclear to me. Is there a
robust way to build poly with gmp on an old OS version (e.g. Mac OS X
10.10) and use it on a newer one? Is there any chance to do this with
x86 instead of x86_64?


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

Re: [polyml] Build error: Exception- InternalError: Too many passes raised while compiling

2017-12-15 Thread David Matthews
Thanks.  It was a code-generator problem that only showed up because of 
a change elsewhere.  It should now be fixed.


David

On 14/12/2017 13:17, Kostirya wrote:

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