On 02/08/2013 16:47, Rob Arthan wrote:

I tried building ProofPower with it on a VirtualBox guest running Kubuntu 12.10.. The build runs the following command just after a run of poly that created pp-ml.o using PolyML.export.

LD_RUN_PATH=/opt/PolyML/latest/lib c++ -o slrp-ml pp-ml.o -L/opt/PolyML/latest/lib -lpolymain -lpolyml

LD_LIBRARY_PATH has been set in the shell script that calls this to /opt/PolyML/latest/lib

I get numerous undefined reference errors: /opt/PolyML/latest/lib/libpolyml.a(processes.o): In function `Processes::Init()': processes.cpp:(.text+0x166): undefined reference to `pthread_key_create ... /opt/PolyML/latest/lib/libpolyml.a(foreign.o): In function `load_sym(TaskData*, SaveVecEntry*)': foreign.cpp:(.text+0x27f9): undefined reference to `dlsym' ... /opt/PolyML/latest/lib/libpolyml.a(locking.o): In function `PLock::Trylock()': locking.cpp:(.text+0x257): undefined reference to `sem_init' ... collect2: error: ld returned 1 exit status

This seems to be a consequence of changing the default in configure to --disable-shared. It seems to require all the libraries (pthread, etc) at link time. It should be possible to get the old behaviour by building with --enable-shared. However, a better solution would be to change the linking line to use "polyc". e.g. /opt/PolyML/latest/bin/polyc -o slrp-ml pp-ml.o You then won't need any LD_RUN_PATH or LD_LIBRARY_PATH when you run slrp-ml because libpolyml will have been statically bound.

David

On 03/08/2013 11:06, Rob Arthan wrote:

/bin/sh on ubuntu-flavoured Linux is dash, which is very pernickety about POSIX compliance. polyc needs a couple of changes to work with it (see attached diffs file).

Thanks. I've applied those changes to buildpolyc which is the script that actually produces polyc as part of the build process.

However, I don't think polyc as it stands is going to work for me because it expects the poly binaries and libraries to be installed in /usr/local.

It should take the installation directories from the configure script so they are wherever make install will put them. This certainly works for me if I specify either --path or --bindir/libdir/mandir on the configure line. How are you installing Poly/ML?

David

On 05/08/2013 06:47, David Greenaway wrote:

Hi David,

We internally have some large Isabelle proofs. In different two cases (which both have heavy multi-threading and large heap sizes) I saw the following assertion fail:

poly: scanaddrs.cpp:324: static void ScanAddress::SetConstantValue(byte*, PolyWord, ScanRelocationKind): Assertion `newDisp < 0x80000000 && newDisp >= -(POLYSIGNED)0x80000000' failed.

This is on Linux x86_64, SVN revision 1827.

Is there any information I can provide to help you track this down?

Cheers, David

Hi David, Thanks for letting me know about this. I might have a better idea of what is happening if you could get a core dump and produce a trace back. Are you familiar with gdb? You will need to build poly with --enable-debug or at least with the -g option to gcc to get symbols in the executable. What memory size are you running in? Regards, David

On 31/08/2013 19:59, Phil Clayton wrote:

I'm trying the latest revision in SVN (1838) and have found that after

open PolyML;

entering either of the following causes a seg fault:

stackTrace (); PolyML.stackTrace ();

The previous version that I tried - 1738 - didn't do this.

The code was clearly wrong and it looks like it always had the potential to seg fault. I've committed a fix (1840). Thanks for the report.

David

01/09/13 13:56, Rob Arthan wrote:

On 2 Aug 2013, at 13:21, David Matthews <David.Matthews at prolingua.co.uk> wrote:

...

?. Please try out the SVN version and let me know how it goes. ?

I am grateful to Phil Clayton for pointing out a surprising performance issue that he noticed while building ProofPower. He found that the elapsed time for the build was over 3 minutes with the latest development version and less than 1.5 minutes with version 5.5, even though the user and system times were about the same. I repeated the experiments and got similar results.

The problem is easy to reproduce. E.g., construct a source file perftest.ML containing the following:

structure PerfTest = struct fun f x = x; end;

Then run

time echo 'use"perftest.ML"' | poly

WIth 5.5, I get:

real 0m0.016s user 0m0.003s sys 0m0.010s

With the latest version (SVN rev 1838), I get:

real 0m0.416s user 0m0.003s sys 0m0.010s

The ProofPower build runs Poly/ML about 180 times. The results I am seeing are compatible with an overhead of about 400ms on each of these runs.

I think this delay is actually when exiting Poly/ML. I have just this moment hit Ctrl+D to exit poly in a terminal but, as nothing happened immediately, I hit it again. In fact, both key strokes registered and I zapped the terminal. (It seems I really am that impatient!)

The delay can still be seen with just

time echo | poly

Phil

On 02/09/2013 06:47, Florian Weimer wrote:

• Phil Clayton:

...

I think this delay is actually when exiting Poly/ML. I have just this moment hit Ctrl+D to exit poly in a terminal but, as nothing happened immediately, I hit it again. In fact, both key strokes registered and I zapped the terminal. (It seems I really am that impatient!)

I pressed ^D quickly followed by ^C in GDB, and ended up with this on the call stack:

     // Now release schedLock and wait for a thread
     // to wake us up.  Use a timed wait to avoid the race with
     // setting exitRequest.
     initialThreadWait.WaitFor(&schedLock, 400);

I guess that's where those 400 milliseconds come from. :-/

Surely there's a better way to do this.

I'm fairly sure the problem is in commit 1835. There's a race condition there associated with initialThreadWait.Signal() and setting the threadExited flag. I'll try and deal with this and the other problems over the next few days.

David