Re: [polyml] 5.7 Release

[David Matthews]

On 11/11/2017 10:41, Ramana Kumar wrote:

OK, thanks.

My impression of Git master is that there is often work-in-progress that
should not be expected to work.
Is it useful to report bugs while development is still in progress?
For example, trying it now I saw this:
Fail "Exception- InternalError: codeToPRegRev raised while compiling"


That is often true but at this point I'm trying to get the bugs out of 
it in order to prepare the release.  So any bug reports are welcome.


Michael Norrish reported this exception on the mailing list a few days 
ago and I've haven't had time to look into it.  If you have a piece of 
code that exhibits it then I would like to see it especially if you can 
cut it down to something manageable.  Please send anything to me 
directly rather than through the mailing list.


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

Re: [polyml] 5.7 Release

[David Matthews]

Hi Ramana,
The fixes branches are useful in the early phase of the development 
cycle if bugs are found soon after a release.  At some point it is no 
longer viable to keep back-porting especially if there is a risk that 
the fix itself may introduce bugs.  This particular change was one of a 
number to make the thread system more resilient.  At this point I'd 
suggest switching to Git master.


Regards,
David

On 11/11/2017 07:15, Ramana Kumar wrote:

Hi David,

Are you still updating the fixes-5.7 branch?
It seems to me that this commit might be a bug fix worth including, though
I'm not sure if it depends on new developments.
https://github.com/polyml/polyml/commit/5ba42e588373bd3cd63b8cadb8c4cb8a349c7fff#diff-27af5828c397c28b2fdeacab709ccf57

Cheers,
Ramana

On 17 May 2017 at 00:49, David Matthews 
wrote:



On 16/05/2017 04:47, Jerry James wrote:


I attempted to build this version for Fedora.  It succeeded on all
architectures except aarch64:

https://koji.fedoraproject.org/koji/taskinfo?taskID=19526061

I don't understand the failure, though.  We run "make check" after the
build to gain some confidence that the build is good.  Here is an
extract from the build log
(https://kojipkgs.fedoraproject.org//work/tasks/6133/19526133/build.log):
Test044.ML => Passed
make[2]: Leaving directory '/builddir/build/BUILD/polyml-5.7'
make[2]: *** [Makefile:1175: check-local] Error 1
make[1]: Leaving directory '/builddir/build/BUILD/polyml-5.7'
make[1]: *** [Makefile:997: check-am] Error 2
make: *** [Makefile:706: check-recursive] Error 1

It looks like every individual test passed, but the test suite as a
whole failed.  Do you have any idea what might cause this?  Thank you,



The only thing that occurs to me is that one or other of the tests messed
up the internal state so that when the poly process came to exit it
crashed.  I don't have access to any machine running aarch64 (that's 64-bit
ARM isn't it?) so there's no way I can test any of this.

Regards,
David


___
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] 5.7 Release

[David Matthews]

On 16/05/2017 04:47, Jerry James wrote:

I attempted to build this version for Fedora.  It succeeded on all
architectures except aarch64:

https://koji.fedoraproject.org/koji/taskinfo?taskID=19526061

I don't understand the failure, though.  We run "make check" after the
build to gain some confidence that the build is good.  Here is an
extract from the build log
(https://kojipkgs.fedoraproject.org//work/tasks/6133/19526133/build.log):
Test044.ML => Passed
make[2]: Leaving directory '/builddir/build/BUILD/polyml-5.7'
make[2]: *** [Makefile:1175: check-local] Error 1
make[1]: Leaving directory '/builddir/build/BUILD/polyml-5.7'
make[1]: *** [Makefile:997: check-am] Error 2
make: *** [Makefile:706: check-recursive] Error 1

It looks like every individual test passed, but the test suite as a
whole failed.  Do you have any idea what might cause this?  Thank you,


The only thing that occurs to me is that one or other of the tests 
messed up the internal state so that when the poly process came to exit 
it crashed.  I don't have access to any machine running aarch64 (that's 
64-bit ARM isn't it?) so there's no way I can test any of this.


Regards,
David

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

Re: [polyml] 5.7 Release

[David Matthews]

Hi Ramana,
I was going to do that at some stage, perhaps when there was something 
to include, but I've done it now.

Regards,
David

On 16/05/2017 04:33, Ramana Kumar wrote:

Hi David,

Is there going to be a fixes-5.7 branch as with previous releases?

Cheers,
Ramana

On 13 May 2017 at 00:50, David Matthews 
wrote:


I've finally got round to releasing version 5.7.  The source code was
actually tagged as 5.7 on Github a while ago and Github considered that a
release.  There are Windows installers for 32-bit and 64-bit as well as the
normal source code for everything else.

I'm aware that there are still some unresolved issues with this version
but it seems to be stable enough for release.

David
___
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] 5.7 Release

[Ramana Kumar]

Hi David,

Is there going to be a fixes-5.7 branch as with previous releases?

Cheers,
Ramana

On 13 May 2017 at 00:50, David Matthews 
wrote:

> I've finally got round to releasing version 5.7.  The source code was
> actually tagged as 5.7 on Github a while ago and Github considered that a
> release.  There are Windows installers for 32-bit and 64-bit as well as the
> normal source code for everything else.
>
> I'm aware that there are still some unresolved issues with this version
> but it seems to be stable enough for release.
>
> David
> ___
> 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] 5.7 Release

[James Clarke]

Hi David,
I can reproduce this (or at least a very similar issue) seemingly every time on 
32-bit PowerPC. All three of my uploads to Debian failed to build on it (across 
different machines) and I can reproduce it on another box. It happens with both 
jessie and unstable; below is the state of all the threads when I built it on 
unstable with two calls to "make compiler" followed by a "make check" (though 
./poly --script Tests/Succeed/Test166.ML also hangs, so the test harness and 
running other tests first is irrelevant). Do you have access to a PowerPC 
machine you can put Debian on? If not I can probably arrange getting you remote 
access to one.

Regards,
James

> (gdb) thread apply all bt
> 
> Thread 16 (Thread 0xee2ff450 (LWP 1795)):
> #0  0x1fdefb98 in pthread_cond_wait@@GLIBC_2.3.2 () from 
> /lib/powerpc-linux-gnu/libpthread.so.0
> #1  0x1ff45718 in pthread_cond_wait () from /lib/powerpc-linux-gnu/libc.so.6
> #2  0x20024eb4 in PCondVar::Wait (this=this@entry=0xf2a172b8, 
> pLock=pLock@entry=0x200911ec ) at locking.cpp:169
> #3  0x20036880 in Processes::WaitInfinite (this=this@entry=0x200911d8 
> , taskData=taskData@entry=0xf2a17280, hMutex=0xf2a6a4c0) at 
> processes.cpp:576
> #4  0x2003694c in PolyThreadCondVarWait (threadId=, arg=...) 
> at processes.cpp:509
> #5  0x2004ca2c in IntTaskData::SwitchToPoly (this=this@entry=0xf2a17280) at 
> interpret.cpp:855
> #6  0x2004f374 in IntTaskData::EnterPolyCode (this=0xf2a17280) at 
> interpret.cpp:1936
> #7  0x20037074 in NewThreadFunction (parameter=0xf2a17280) at 
> processes.cpp:1361
> #8  0x1fde7500 in start_thread () from /lib/powerpc-linux-gnu/libpthread.so.0
> #9  0x1ff339ac in clone () from /lib/powerpc-linux-gnu/libc.so.6
> 
> Thread 15 (Thread 0xeeaff450 (LWP 1794)):
> #0  0x1fdefb98 in pthread_cond_wait@@GLIBC_2.3.2 () from 
> /lib/powerpc-linux-gnu/libpthread.so.0
> #1  0x1ff45718 in pthread_cond_wait () from /lib/powerpc-linux-gnu/libc.so.6
> #2  0x20024eb4 in PCondVar::Wait (this=this@entry=0xf2a17088, 
> pLock=pLock@entry=0x200911ec ) at locking.cpp:169
> #3  0x20036880 in Processes::WaitInfinite (this=this@entry=0x200911d8 
> , taskData=taskData@entry=0xf2a17050, hMutex=0xf2a69510) at 
> processes.cpp:576
> #4  0x2003694c in PolyThreadCondVarWait (threadId=, arg=...) 
> at processes.cpp:509
> #5  0x2004ca2c in IntTaskData::SwitchToPoly (this=this@entry=0xf2a17050) at 
> interpret.cpp:855
> #6  0x2004f374 in IntTaskData::EnterPolyCode (this=0xf2a17050) at 
> interpret.cpp:1936
> #7  0x20037074 in NewThreadFunction (parameter=0xf2a17050) at 
> processes.cpp:1361
> #8  0x1fde7500 in start_thread () from /lib/powerpc-linux-gnu/libpthread.so.0
> #9  0x1ff339ac in clone () from /lib/powerpc-linux-gnu/libc.so.6
> 
> Thread 14 (Thread 0xef2ff450 (LWP 1793)):
> #0  0x1fdefb98 in pthread_cond_wait@@GLIBC_2.3.2 () from 
> /lib/powerpc-linux-gnu/libpthread.so.0
> #1  0x1ff45718 in pthread_cond_wait () from /lib/powerpc-linux-gnu/libc.so.6
> #2  0x20024eb4 in PCondVar::Wait (this=this@entry=0xf2a16f48, 
> pLock=pLock@entry=0x200911ec ) at locking.cpp:169
> #3  0x20036880 in Processes::WaitInfinite (this=this@entry=0x200911d8 
> , taskData=taskData@entry=0xf2a16f10, hMutex=0xf2a68560) at 
> processes.cpp:576
> #4  0x2003694c in PolyThreadCondVarWait (threadId=, arg=...) 
> at processes.cpp:509
> #5  0x2004ca2c in IntTaskData::SwitchToPoly (this=this@entry=0xf2a16f10) at 
> interpret.cpp:855
> #6  0x2004f374 in IntTaskData::EnterPolyCode (this=0xf2a16f10) at 
> interpret.cpp:1936
> #7  0x20037074 in NewThreadFunction (parameter=0xf2a16f10) at 
> processes.cpp:1361
> #8  0x1fde7500 in start_thread () from /lib/powerpc-linux-gnu/libpthread.so.0
> #9  0x1ff339ac in clone () from /lib/powerpc-linux-gnu/libc.so.6
> 
> Thread 13 (Thread 0xf1fff450 (LWP 1792)):
> #0  0x1fdefb98 in pthread_cond_wait@@GLIBC_2.3.2 () from 
> /lib/powerpc-linux-gnu/libpthread.so.0
> #1  0x1ff45718 in pthread_cond_wait () from /lib/powerpc-linux-gnu/libc.so.6
> #2  0x20024eb4 in PCondVar::Wait (this=this@entry=0xf2a19078, 
> pLock=pLock@entry=0x200911ec ) at locking.cpp:169
> #3  0x20036540 in Processes::MutexBlock (this=this@entry=0x200911d8 
> , taskData=taskData@entry=0xf2a19040, hMutex=0xf2a190e0) at 
> processes.cpp:465
> #4  0x2003661c in PolyThreadMutexBlock (threadId=, arg=...) at 
> processes.cpp:395
> #5  0x2004ca2c in IntTaskData::SwitchToPoly (this=this@entry=0xf2a19040) at 
> interpret.cpp:855
> #6  0x2004f374 in IntTaskData::EnterPolyCode (this=0xf2a19040) at 
> interpret.cpp:1936
> #7  0x20037074 in NewThreadFunction (parameter=0xf2a19040) at 
> processes.cpp:1361
> #8  0x1fde7500 in start_thread () from /lib/powerpc-linux-gnu/libpthread.so.0
> #9  0x1ff339ac in clone () from /lib/powerpc-linux-gnu/libc.so.6
> 
> Thread 12 (Thread 0xf29ff450 (LWP 1757)):
> #0  0x1fdefb98 in pthread_cond_wait@@GLIBC_2.3.2 () from 
> /lib/powerpc-linux-gnu/libpthread.so.0
> #1  0x1ff45718 in 

Re: [polyml] 5.7 Release

[David Matthews]

On 01/03/2017 13:31, Makarius wrote:

On 01/03/17 13:55, David Matthews wrote:

On 24/02/17 13:26, Makarius wrote:
My current guess is that it is a problem of compiled ML code that is no
longer garbage-collected.


The current version does garbage collect code; it's just that it only
happens at a major GC.  Previously when code was part of the general
heap a short-lived code cell would be garbage-collected by a minor GC.
It could be that this is problem or it could be that there is a bug
which is resulting in code not being properly collected.



I'm inclined to release the current version of git master as 5.7 and
then look into this and other issues.


OK, it merely means that we need to skip this version for official
Isabelle use. I will continue testing Poly/ML repository versions privately.



That's understandable.  Adding support for interpretation is going to be 
a bit of work and until it's done and tested there's no way of being 
sure it will solve this problem.  I'd prefer not to delay the release.


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

Re: [polyml] 5.7 Release

[James Clarke]

This is on Debian unstable (the soon-to-be-released Stretch should be close 
enough), but also amd64 in VirtualBox. Perhaps there have been some glibc 
changes? I couldn't reproduce it under my macOS host, which would be consistent 
with that.

James

> On 1 Mar 2017, at 15:48, David Matthews  
> wrote:
> 
> Hi James,
> I've tried this with Debian stable 64-bit in a VirtualBox and haven't had any 
> problems.  Of course that's a different set-up but I would have expected to 
> see something if there was a problem.  It makes it rather difficult to track 
> this down.
> 
> David
> 
> On 23/02/2017 20:44, James Clarke wrote:
>> Hi David,
>> It seems Test166 (the new condition variable one) sometimes deadlocks. I'm 
>> able to reliably reproduce with the following:
>> 
>>> ./configure
>>> make -j2 compiler
>>> make -j2 compiler
>>> while true; do make -j2 check; done
>> 
>> (The -j2's are probably irrelevant, but I'm including them for completeness)
>> 
>> On the 40th iteration of the loop it got stuck for me:
>> 
>>> val runTests = fn: string -> bool
>>> Test028.ML => Passed
>>> Test166.ML =>
>> 
>> Threads:
>> 
>>> Thread 9 (Thread 0x7faf066fc700 (LWP 29448)):
>>> #0  pthread_cond_wait@@GLIBC_2.3.2 () at 
>>> ../sysdeps/unix/sysv/linux/x86_64/pthread_cond_wait.S:185
>>> #1  0x55ff143b7e30 in Processes::WaitInfinite(TaskData*, SaveVecEntry*) 
>>> ()
>>> #2  0x55ff143b7f4f in PolyThreadCondVarWait ()
>>> #3  0x55ff1426496d in area1 ()
>>> #4  0x7faf0ce71c00 in ?? ()
>>> #5  0x7faf066fbe08 in ?? ()
>>> #6  0x7faf0fb79040 in ?? () from /lib64/ld-linux-x86-64.so.2
>>> #7  0x7faf0e6f0e48 in __GI___libc_malloc (bytes=140389730295024) at 
>>> malloc.c:2925
>>> #8  0x55ff143c5477 in initThreadSignals(TaskData*) ()
>>> #9  0x55ff143b8990 in NewThreadFunction(void*) ()
>>> #10 0x7faf0f73f424 in start_thread (arg=0x7faf066fc700) at 
>>> pthread_create.c:333
>>> #11 0x7faf0e75e9bf in clone () at 
>>> ../sysdeps/unix/sysv/linux/x86_64/clone.S:105
>>> 
>>> Thread 8 (Thread 0x7faf06efd700 (LWP 29447)):
>>> #0  pthread_cond_wait@@GLIBC_2.3.2 () at 
>>> ../sysdeps/unix/sysv/linux/x86_64/pthread_cond_wait.S:185
>>> #1  0x55ff143b7e30 in Processes::WaitInfinite(TaskData*, SaveVecEntry*) 
>>> ()
>>> #2  0x55ff143b7f4f in PolyThreadCondVarWait ()
>>> #3  0x55ff1426496d in area1 ()
>>> #4  0x7faf0ce71c00 in ?? ()
>>> #5  0x7faf06efce08 in ?? ()
>>> #6  0x7faf0fb79040 in ?? () from /lib64/ld-linux-x86-64.so.2
>>> #7  0x7faf0e6f0e48 in __GI___libc_malloc (bytes=140389730294192) at 
>>> malloc.c:2925
>>> #8  0x55ff143c5477 in initThreadSignals(TaskData*) ()
>>> #9  0x55ff143b8990 in NewThreadFunction(void*) ()
>>> #10 0x7faf0f73f424 in start_thread (arg=0x7faf06efd700) at 
>>> pthread_create.c:333
>>> #11 0x7faf0e75e9bf in clone () at 
>>> ../sysdeps/unix/sysv/linux/x86_64/clone.S:105
>>> 
>>> Thread 7 (Thread 0x7faf076fe700 (LWP 29446)):
>>> #0  pthread_cond_wait@@GLIBC_2.3.2 () at 
>>> ../sysdeps/unix/sysv/linux/x86_64/pthread_cond_wait.S:185
>>> #1  0x55ff143b7e30 in Processes::WaitInfinite(TaskData*, SaveVecEntry*) 
>>> ()
>>> #2  0x55ff143b7f4f in PolyThreadCondVarWait ()
>>> #3  0x55ff1426496d in area1 ()
>>> #4  0x7faf0ce71c00 in ?? ()
>>> #5  0x7faf076fde08 in ?? ()
>>> #6  0x7faf0fb79040 in ?? () from /lib64/ld-linux-x86-64.so.2
>>> #7  0x7faf0e6f0e48 in __GI___libc_malloc (bytes=140389730242944) at 
>>> malloc.c:2925
>>> #8  0x55ff143c5477 in initThreadSignals(TaskData*) ()
>>> #9  0x55ff143b8990 in NewThreadFunction(void*) ()
>>> #10 0x7faf0f73f424 in start_thread (arg=0x7faf076fe700) at 
>>> pthread_create.c:333
>>> #11 0x7faf0e75e9bf in clone () at 
>>> ../sysdeps/unix/sysv/linux/x86_64/clone.S:105
>>> 
>>> Thread 6 (Thread 0x7faf07fff700 (LWP 29445)):
>>> #0  pthread_cond_wait@@GLIBC_2.3.2 () at 
>>> ../sysdeps/unix/sysv/linux/x86_64/pthread_cond_wait.S:185
>>> #1  0x55ff143b7237 in Processes::WaitForSignal(TaskData*, PLock*) ()
>>> #2  0x55ff143c4f8f in PolyWaitForSignal ()
>>> #3  0x55ff13f1b8ba in area1 ()
>>> #4  0x7faf0ce71c00 in ?? ()
>>> #5  0x7faf07ffee08 in ?? ()
>>> #6  0x7faf0fb79040 in ?? () from /lib64/ld-linux-x86-64.so.2
>>> #7  0x7faf0e6f0e48 in __GI___libc_malloc (bytes=140389730232720) at 
>>> malloc.c:2925
>>> #8  0x55ff143c5477 in initThreadSignals(TaskData*) ()
>>> #9  0x55ff143b8990 in NewThreadFunction(void*) ()
>>> #10 0x7faf0f73f424 in start_thread (arg=0x7faf07fff700) at 
>>> pthread_create.c:333
>>> #11 0x7faf0e75e9bf in clone () at 
>>> ../sysdeps/unix/sysv/linux/x86_64/clone.S:105
>>> 
>>> Thread 5 (Thread 0x7faf0ce72700 (LWP 29444)):
>>> #0  pthread_cond_wait@@GLIBC_2.3.2 () at 
>>> ../sysdeps/unix/sysv/linux/x86_64/pthread_cond_wait.S:185
>>> #1  0x55ff143b7e30 in Processes::WaitInfinite(TaskData*, SaveVecEntry*) 
>>> ()
>>> #2  0x55ff143b7f4f in PolyThreadCondVarWait ()
>>> 

Re: [polyml] 5.7 Release

[Makarius]

On 01/03/17 13:55, David Matthews wrote:
>> On 24/02/17 13:26, Makarius wrote:
>> My current guess is that it is a problem of compiled ML code that is no
>> longer garbage-collected.
> 
> The current version does garbage collect code; it's just that it only
> happens at a major GC.  Previously when code was part of the general
> heap a short-lived code cell would be garbage-collected by a minor GC.
> It could be that this is problem or it could be that there is a bug
> which is resulting in code not being properly collected.

> I'm inclined to release the current version of git master as 5.7 and
> then look into this and other issues.

OK, it merely means that we need to skip this version for official
Isabelle use. I will continue testing Poly/ML repository versions privately.


Makarius


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

Re: [polyml] 5.7 Release

[David Matthews]

On 27/02/2017 22:55, Makarius wrote:

On 24/02/17 13:26, Makarius wrote:

We have strange memory management problems with Isabelle.

(1) Poly/ML pre-5.7 requires a bit more heap space (tested for HOL,
HOL-Library, HOL-Analysis), especially when running in parallel. This
might explain the failure building main HOL on the small macOS machine:
it probably runs into a situation where heap compaction no longer works
and the ML process interrupts all threads.

To address that, I have fine-tuned the defaults for parallel proofs,
leading up to Isabelle/05f1b5342298, with some hope that it might
improve the situation in general: less waste of CPU and memory on small
machines.


(2) The big problem is AFP/Iptables_Semantics_Examples. Here is the
timing with Poly/ML 5.6 on lxbroy10, an old AMD machine that is
relatively slow:

Finished Iptables_Semantics_Examples (4:35:13 elapsed time, 23:35:08 cpu
time, factor 5.14)

With Poly/ML 5.7 it quickly runs into memory problems. See the included
PNG images for comparison.

That session is definitely quite ambitious, not to say insane. It
contains lots of invocations of the "eval" proof method, which means
dynamic compilation of ML from HOL specifications, and throwing away the
result.


My current guess is that it is a problem of compiled ML code that is no
longer garbage-collected.

Is there a way to measure the size of this persistent ML code?

Is there a way to invoke the Poly/ML compiler in interpreted mode via
some flag?


The current version does garbage collect code; it's just that it only 
happens at a major GC.  Previously when code was part of the general 
heap a short-lived code cell would be garbage-collected by a minor GC. 
It could be that this is problem or it could be that there is a bug 
which is resulting in code not being properly collected.


It isn't possible to use the current byte-code interpreter with the 
machine-code version.  The idea I had for interpretation was to 
interpret at the level of the code-tree, essentially one step on from 
the parse-tree.  Each instruction of top-level code without a loop is 
executed only once and so it's a complete waste of resources to optimise 
it and generate machine code, but that's what happens at the moment.  It 
should be fairly easy to add an interpretation step since something like 
that already happens for expressions involving constants.


I'm inclined to release the current version of git master as 5.7 and 
then look into this and other issues.


David

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

Re: [polyml] 5.7 Release

[Makarius]

On 24/02/17 13:26, Makarius wrote:
> We have strange memory management problems with Isabelle.
> 
> I've been using repository versions of Poly/ML privately during the past
> few months, without seeing such problems. Only the official switch in
> http://isabelle.in.tum.de/repos/isabelle/rev/42b92fa72a51 exposed that,
> ranging from main HOL not building on an underpowered macOS machine to
> some big AFP entry not building on an overpowered Linux box.
> 
> For the moment, I have switched the Isabelle setup back to stable
> Poly/ML 5.6 (see http://isabelle.in.tum.de/repos/isabelle/rev/18f3d341f8c0).
> 
> I will come back on that when I've investigated the situation further.

I've now spent some time with it. Here are some preliminary observations
for Isabelle/002b4c8c366e and AFP/d0bd0f0fe3b2 and Poly/ML 5.6 vs.
Poly/ML pre-5.7 (6307085deb18):

(1) Poly/ML pre-5.7 requires a bit more heap space (tested for HOL,
HOL-Library, HOL-Analysis), especially when running in parallel. This
might explain the failure building main HOL on the small macOS machine:
it probably runs into a situation where heap compaction no longer works
and the ML process interrupts all threads.

To address that, I have fine-tuned the defaults for parallel proofs,
leading up to Isabelle/05f1b5342298, with some hope that it might
improve the situation in general: less waste of CPU and memory on small
machines.


(2) The big problem is AFP/Iptables_Semantics_Examples. Here is the
timing with Poly/ML 5.6 on lxbroy10, an old AMD machine that is
relatively slow:

Finished Iptables_Semantics_Examples (4:35:13 elapsed time, 23:35:08 cpu
time, factor 5.14)

With Poly/ML 5.7 it quickly runs into memory problems. See the included
PNG images for comparison.

That session is definitely quite ambitious, not to say insane. It
contains lots of invocations of the "eval" proof method, which means
dynamic compilation of ML from HOL specifications, and throwing away the
result.


My current guess is that it is a problem of compiled ML code that is no
longer garbage-collected.

Is there a way to measure the size of this persistent ML code?

Is there a way to invoke the Poly/ML compiler in interpreted mode via
some flag?


See also
http://isabelle.in.tum.de/repos/isabelle/file/1803a9787eca/src/Pure/ML/ml_compiler.ML#l270
where Poly/ML is invoked in Isabelle/ML.


Makarius

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

Re: [polyml] 5.7 Release

[Makarius]

On 21/02/17 13:48, David Matthews wrote:
> The latest version, provisionally called 5.6.1, has had very little
> change for several months.  I'm not aware of any show-stoppers so I
> think it would be a good time to make a release.  Because there have
> been some major changes I was planning to call it 5.7.  This is the last
> chance to do any last tests before the release.

We have strange memory management problems with Isabelle.

I've been using repository versions of Poly/ML privately during the past
few months, without seeing such problems. Only the official switch in
http://isabelle.in.tum.de/repos/isabelle/rev/42b92fa72a51 exposed that,
ranging from main HOL not building on an underpowered macOS machine to
some big AFP entry not building on an overpowered Linux box.

For the moment, I have switched the Isabelle setup back to stable
Poly/ML 5.6 (see http://isabelle.in.tum.de/repos/isabelle/rev/18f3d341f8c0).

I will come back on that when I've investigated the situation further.


Makarius


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

Re: [polyml] 5.7 Release

[James Clarke]

Hi David,
It seems Test166 (the new condition variable one) sometimes deadlocks. I'm able 
to reliably reproduce with the following:

> ./configure
> make -j2 compiler
> make -j2 compiler
> while true; do make -j2 check; done

(The -j2's are probably irrelevant, but I'm including them for completeness)

On the 40th iteration of the loop it got stuck for me:

> val runTests = fn: string -> bool
> Test028.ML => Passed
> Test166.ML =>

Threads:

> Thread 9 (Thread 0x7faf066fc700 (LWP 29448)):
> #0  pthread_cond_wait@@GLIBC_2.3.2 () at 
> ../sysdeps/unix/sysv/linux/x86_64/pthread_cond_wait.S:185
> #1  0x55ff143b7e30 in Processes::WaitInfinite(TaskData*, SaveVecEntry*) 
> ()  
> #2  0x55ff143b7f4f in PolyThreadCondVarWait ()
> #3  0x55ff1426496d in area1 ()
> #4  0x7faf0ce71c00 in ?? ()
> #5  0x7faf066fbe08 in ?? ()
> #6  0x7faf0fb79040 in ?? () from /lib64/ld-linux-x86-64.so.2
> #7  0x7faf0e6f0e48 in __GI___libc_malloc (bytes=140389730295024) at 
> malloc.c:2925
> #8  0x55ff143c5477 in initThreadSignals(TaskData*) () 
>  
> #9  0x55ff143b8990 in NewThreadFunction(void*) () 
>  
> #10 0x7faf0f73f424 in start_thread (arg=0x7faf066fc700) at 
> pthread_create.c:333
> #11 0x7faf0e75e9bf in clone () at 
> ../sysdeps/unix/sysv/linux/x86_64/clone.S:105
>   
>   
>
> Thread 8 (Thread 0x7faf06efd700 (LWP 29447)): 
>
> #0  pthread_cond_wait@@GLIBC_2.3.2 () at 
> ../sysdeps/unix/sysv/linux/x86_64/pthread_cond_wait.S:185 
> #1  0x55ff143b7e30 in Processes::WaitInfinite(TaskData*, SaveVecEntry*) ()
> #2  0x55ff143b7f4f in PolyThreadCondVarWait ()   
> #3  0x55ff1426496d in area1 ()  
> #4  0x7faf0ce71c00 in ?? ()   
>  
> #5  0x7faf06efce08 in ?? ()   
>  
> #6  0x7faf0fb79040 in ?? () from /lib64/ld-linux-x86-64.so.2
> #7  0x7faf0e6f0e48 in __GI___libc_malloc (bytes=140389730294192) at 
> malloc.c:2925
> #8  0x55ff143c5477 in initThreadSignals(TaskData*) () 
>   
>
> #9  0x55ff143b8990 in NewThreadFunction(void*) () 
>
> #10 0x7faf0f73f424 in start_thread (arg=0x7faf06efd700) at 
> pthread_create.c:333
> #11 0x7faf0e75e9bf in clone () at 
> ../sysdeps/unix/sysv/linux/x86_64/clone.S:105
>  
> Thread 7 (Thread 0x7faf076fe700 (LWP 29446)):   
> #0  pthread_cond_wait@@GLIBC_2.3.2 () at 
> ../sysdeps/unix/sysv/linux/x86_64/pthread_cond_wait.S:185
> #1  0x55ff143b7e30 in Processes::WaitInfinite(TaskData*, SaveVecEntry*) 
> () 
> #2  0x55ff143b7f4f in PolyThreadCondVarWait ()
> #3  0x55ff1426496d in area1 ()   
> #4  0x7faf0ce71c00 in ?? ()   
>   
>   
> #5  0x7faf076fde08 in ?? ()   
>
> #6  0x7faf0fb79040 in ?? () from /lib64/ld-linux-x86-64.so.2  
>  
> #7  0x7faf0e6f0e48 in __GI___libc_malloc (bytes=140389730242944) at 
> malloc.c:2925
> #8  0x55ff143c5477 in initThreadSignals(TaskData*) ()
> #9  0x55ff143b8990 in NewThreadFunction(void*) () 
>  
> #10 0x7faf0f73f424 in start_thread (arg=0x7faf076fe700) at 
> pthread_create.c:333
> #11 0x7faf0e75e9bf in clone () at 
> ../sysdeps/unix/sysv/linux/x86_64/clone.S:105
>  
> Thread 6 (Thread 0x7faf07fff700 (LWP 29445)): 
>   
> #0  pthread_cond_wait@@GLIBC_2.3.2 () at 
> ../sysdeps/unix/sysv/linux/x86_64/pthread_cond_wait.S:185
> #1  0x55ff143b7237 in Processes::WaitForSignal(TaskData*, PLock*) ()
> #2  0x55ff143c4f8f in PolyWaitForSignal ()
> #3  0x55ff13f1b8ba in area1 ()
>   
>  
> #4  0x7faf0ce71c00 in ?? ()
> #5  0x7faf07ffee08 in ?? ()
> #6  0x7faf0fb79040 in ?? () from /lib64/ld-linux-x86-64.so.2
> #7  0x7faf0e6f0e48 in __GI___libc_malloc (bytes=140389730232720) at 
> 

Re: [polyml] 5.7 Release

[David Matthews]

Thanks.  I've added BICArbitrary to the case and it seems to be fine now.

David

On 21/02/2017 19:19, James Clarke wrote:

Seems I forgot to include the mailing list; adding it back in.

James


On 21 Feb 2017, at 19:14, James Clarke  wrote:

Hi David,
I just uploaded the latest version to Debian's experimental suite[1], and it seems all 
the interpreted versions are failing when running "make compiler". The error 
itself is:


./polyimport  polytemp.txt -I . < ./exportPoly.sml
Use: basis/build.sml
Use: basis/RuntimeCalls.ML
Use: basis/InitialBasis.ML
Exception- Match unexpectedly raised while compiling


Further up in the build logs there is:


Making INTGCODE
mlsource/MLCompiler/CodeTree/ByteCode/INTGCODE.ML:167: warning: Matches are not 
exhaustive.
Found near
 case pt of
BICEval evl => genEval (evl, tailKind) |
BICExtract ext => if whereto = NoResult then () else locaddr ext |
BICField {...} => (... ...; ...) |
... ... => ... ... |
... => ... |
...



Looking at the source, BICArbitrary is not handled (though there may be others).

Regards,
James

[1] Logs at 
https://buildd.debian.org/status/package.php?p=polyml=experimental


On 21 Feb 2017, at 12:48, David Matthews  wrote:

The latest version, provisionally called 5.6.1, has had very little change for 
several months.  I'm not aware of any show-stoppers so I think it would be a 
good time to make a release.  Because there have been some major changes I was 
planning to call it 5.7.  This is the last chance to do any last tests before 
the release.

David
___
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] 5.7 Release

[James Clarke]

Seems I forgot to include the mailing list; adding it back in.

James

> On 21 Feb 2017, at 19:14, James Clarke  wrote:
> 
> Hi David,
> I just uploaded the latest version to Debian's experimental suite[1], and it 
> seems all the interpreted versions are failing when running "make compiler". 
> The error itself is:
> 
>> ./polyimport  polytemp.txt -I . < ./exportPoly.sml
>> Use: basis/build.sml
>> Use: basis/RuntimeCalls.ML
>> Use: basis/InitialBasis.ML
>> Exception- Match unexpectedly raised while compiling
> 
> Further up in the build logs there is:
> 
>> Making INTGCODE
>> mlsource/MLCompiler/CodeTree/ByteCode/INTGCODE.ML:167: warning: Matches are 
>> not exhaustive.
>> Found near
>>  case pt of
>> BICEval evl => genEval (evl, tailKind) |
>> BICExtract ext => if whereto = NoResult then () else locaddr ext |
>> BICField {...} => (... ...; ...) |
>> ... ... => ... ... |
>> ... => ... |
>> ...
> 
> 
> Looking at the source, BICArbitrary is not handled (though there may be 
> others).
> 
> Regards,
> James
> 
> [1] Logs at 
> https://buildd.debian.org/status/package.php?p=polyml=experimental
> 
>> On 21 Feb 2017, at 12:48, David Matthews  
>> wrote:
>> 
>> The latest version, provisionally called 5.6.1, has had very little change 
>> for several months.  I'm not aware of any show-stoppers so I think it would 
>> be a good time to make a release.  Because there have been some major 
>> changes I was planning to call it 5.7.  This is the last chance to do any 
>> last tests before the release.
>> 
>> David
>> ___
>> 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] 5.7 Release

[David Matthews]

I've not seen anything like that.  I did a search to see if anyone else 
had had a crash in similar circumstances in other programs and 
interestingly the closest match was also in FreeBSD.  It's difficult to 
know where the problem is.


David

On 21/02/2017 15:32, Kostirya wrote:

it's also when i compile sml code:


polyc gc_bench.sml

Segmentation fault (core dumped)


gdb -c poly.core /home/nick/polyml/bin/poly

...
(gdb) bt
#0  0x000800fea618 in _rtld_is_dlopened () from /libexec/ld-elf.so.1
#1  0x000800fe9e3a in _rtld_is_dlopened () from /libexec/ld-elf.so.1
#2  0x000800fe6ea0 in dlopen () from /libexec/ld-elf.so.1
#3  0x000801213a48 in pthread_exit () from /lib/libthr.so.3
#4  0x00080121396b in pthread_exit () from /lib/libthr.so.3
#5  0x00080120885d in pthread_create () from /lib/libthr.so.3
#6  0x in ?? ()
(gdb)

2017-02-21 16:57 GMT+02:00 Kostirya :

I sometimes get Segmentation fault on pure SML code (without FFI).
Feels it's after main function finished.



gdb -c a.out.core a.out

GNU gdb 6.1.1 [FreeBSD]
Copyright 2004 Free Software Foundation, Inc.
GDB is free software, covered by the GNU General Public License, and you are
welcome to change it and/or distribute copies of it under certain conditions.
Type "show copying" to see the conditions.
There is absolutely no warranty for GDB.  Type "show warranty" for details.
This GDB was configured as "amd64-marcel-freebsd"...
Core was generated by `a.out'.
Program terminated with signal 11, Segmentation fault.
Reading symbols from /lib/libthr.so.3...done.
Loaded symbols for /lib/libthr.so.3
Reading symbols from /lib/libm.so.5...done.
Loaded symbols for /lib/libm.so.5
Reading symbols from /usr/lib/libc++.so.1...done.
Loaded symbols for /usr/lib/libc++.so.1
Reading symbols from /lib/libcxxrt.so.1...done.
Loaded symbols for /lib/libcxxrt.so.1
Reading symbols from /lib/libgcc_s.so.1...done.
Loaded symbols for /lib/libgcc_s.so.1
Reading symbols from /lib/libc.so.7...done.
Loaded symbols for /lib/libc.so.7
Reading symbols from /libexec/ld-elf.so.1...done.
Loaded symbols for /libexec/ld-elf.so.1
#0  0x00080067e618 in _rtld_is_dlopened () from /libexec/ld-elf.so.1
[New Thread 802023800 (LWP 100475/)]
[New Thread 802023400 (LWP 100474/)]
[New Thread 801c07400 (LWP 100473/)]
[New Thread 801c07000 (LWP 100472/)]
[New Thread 801c06c00 (LWP 100471/)]
[New Thread 801c06800 (LWP 100470/)]
[New Thread 801c06400 (LWP 100112/)]
(gdb) bt
#0  0x00080067e618 in _rtld_is_dlopened () from /libexec/ld-elf.so.1
#1  0x00080067de3a in _rtld_is_dlopened () from /libexec/ld-elf.so.1
#2  0x00080067aea0 in dlopen () from /libexec/ld-elf.so.1
#3  0x0008008a7a48 in pthread_exit () from /lib/libthr.so.3
#4  0x0008008a796b in pthread_exit () from /lib/libthr.so.3
#5  0x00080089c85d in pthread_create () from /lib/libthr.so.3
#6  0x in ?? ()
(gdb)

2017-02-21 14:48 GMT+02:00 David Matthews :

The latest version, provisionally called 5.6.1, has had very little change
for several months.  I'm not aware of any show-stoppers so I think it would
be a good time to make a release.  Because there have been some major
changes I was planning to call it 5.7.  This is the last chance to do any
last tests before the release.

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


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

Re: [polyml] 5.7 Release

[Kostirya]

I sometimes get Segmentation fault on pure SML code (without FFI).
Feels it's after main function finished.


> gdb -c a.out.core a.out
GNU gdb 6.1.1 [FreeBSD]
Copyright 2004 Free Software Foundation, Inc.
GDB is free software, covered by the GNU General Public License, and you are
welcome to change it and/or distribute copies of it under certain conditions.
Type "show copying" to see the conditions.
There is absolutely no warranty for GDB.  Type "show warranty" for details.
This GDB was configured as "amd64-marcel-freebsd"...
Core was generated by `a.out'.
Program terminated with signal 11, Segmentation fault.
Reading symbols from /lib/libthr.so.3...done.
Loaded symbols for /lib/libthr.so.3
Reading symbols from /lib/libm.so.5...done.
Loaded symbols for /lib/libm.so.5
Reading symbols from /usr/lib/libc++.so.1...done.
Loaded symbols for /usr/lib/libc++.so.1
Reading symbols from /lib/libcxxrt.so.1...done.
Loaded symbols for /lib/libcxxrt.so.1
Reading symbols from /lib/libgcc_s.so.1...done.
Loaded symbols for /lib/libgcc_s.so.1
Reading symbols from /lib/libc.so.7...done.
Loaded symbols for /lib/libc.so.7
Reading symbols from /libexec/ld-elf.so.1...done.
Loaded symbols for /libexec/ld-elf.so.1
#0  0x00080067e618 in _rtld_is_dlopened () from /libexec/ld-elf.so.1
[New Thread 802023800 (LWP 100475/)]
[New Thread 802023400 (LWP 100474/)]
[New Thread 801c07400 (LWP 100473/)]
[New Thread 801c07000 (LWP 100472/)]
[New Thread 801c06c00 (LWP 100471/)]
[New Thread 801c06800 (LWP 100470/)]
[New Thread 801c06400 (LWP 100112/)]
(gdb) bt
#0  0x00080067e618 in _rtld_is_dlopened () from /libexec/ld-elf.so.1
#1  0x00080067de3a in _rtld_is_dlopened () from /libexec/ld-elf.so.1
#2  0x00080067aea0 in dlopen () from /libexec/ld-elf.so.1
#3  0x0008008a7a48 in pthread_exit () from /lib/libthr.so.3
#4  0x0008008a796b in pthread_exit () from /lib/libthr.so.3
#5  0x00080089c85d in pthread_create () from /lib/libthr.so.3
#6  0x in ?? ()
(gdb)

2017-02-21 14:48 GMT+02:00 David Matthews :
> The latest version, provisionally called 5.6.1, has had very little change
> for several months.  I'm not aware of any show-stoppers so I think it would
> be a good time to make a release.  Because there have been some major
> changes I was planning to call it 5.7.  This is the last chance to do any
> last tests before the release.
>
> David
> ___
> 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] 5.7 Release

[David Matthews]

Thanks.  That's now been done.  David

On 21/02/2017 14:30, James Clarke wrote:

The configure script needs to be regenerated from configure.ac.

James


On 21 Feb 2017, at 14:17, Kostirya  wrote:

I think polyc is little broken.
"polyc_CFLAGS" macro do not replaced on "-O3":


git pull && ./configure && make && make compiler && make install

...

grep polyc_CFLAGS ./polyc

CFLAGS="@polyc_CFLAGS@"

2017-02-21 14:48 GMT+02:00 David Matthews :

The latest version, provisionally called 5.6.1, has had very little change
for several months.  I'm not aware of any show-stoppers so I think it would
be a good time to make a release.  Because there have been some major
changes I was planning to call it 5.7.  This is the last chance to do any
last tests before the release.

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


___
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