Re: [polyml] Approaching release of 5.7.1

Phil, I've released 5.7.1 now using 44b7b88. That means the 400ms delay remains in that version but everything else should work. The crow-bar thread has been removed in current master (01482bf) so that should no longer show the 40s delay. The problem was that the 400ms delay was masking a

Re: [polyml] Approaching release of 5.7.1

David, As Rob says, I am using Linux (4.13.12-100.fc25.x86_64 from Fedora 25 updates). I have tried the updated version (ga24f39a) and this fixes the issue. ProofPower builds in the expected time. However, I have tried a few more tests and find that some compiled applications are very

Re: [polyml] Approaching release of 5.7.1

David, > On 26 Nov 2017, at 09:14, David Matthews > wrote: > > I don't see that myself but it's certainly possible. A delay followed by > Error 1 suggests that it is relying on the crow-bar thread to stop. The fact > that this only happens on some platforms

Re: [polyml] Approaching release of 5.7.1

I tried it on Ubuntu 16.04 and indeed it showed the problem. I had been testing on Debian stable. It seems to be a race condition which only showed up because this latest change removed the delay which was "fixing" the race. I don't know why it only showed up in Ubuntu but the answer seems

Re: [polyml] Approaching release of 5.7.1

On 25/11/17 22:45, Makarius wrote: > On 25/11/17 18:44, David Matthews wrote: > >> I've had a better look and I found that I was seeing this as well.  I've >> pushed a fix and it no longer seems to be doing it.  It's a very small >> change so I would be very surprised if it has broken anything

Re: [polyml] Approaching release of 5.7.1

On 26/11/17 10:14, David Matthews wrote: > > In view of this I'm inclined to release the version without this change > (44b7b88) as 5.7.1 and investigate the problem later.  Are you certain > the problem you've identified doesn't happen in that version? Yes, 44b7b88 works on these Ubuntu 12.04

Re: [polyml] Approaching release of 5.7.1

I don't see that myself but it's certainly possible. A delay followed by Error 1 suggests that it is relying on the crow-bar thread to stop. The fact that this only happens on some platforms suggests a race condition. In view of this I'm inclined to release the version without this change

Re: [polyml] Approaching release of 5.7.1

On 25/11/17 18:44, David Matthews wrote: > I've had a better look and I found that I was seeing this as well.  I've > pushed a fix and it no longer seems to be doing it.  It's a very small > change so I would be very surprised if it has broken anything but I'll > give it a couple of days and then

Re: [polyml] Approaching release of 5.7.1

Rob, I've had a better look and I found that I was seeing this as well. I've pushed a fix and it no longer seems to be doing it. It's a very small change so I would be very surprised if it has broken anything but I'll give it a couple of days and then release 5.7.1. Regards, David On

Re: [polyml] Approaching release of 5.7.1

David, Knowing Phil he will be using some version of Linux, but I see similar results on Mac OS: E.g., on Mac OS High Sierra 10.13.1: rda]- echo | time /usr/local/poly/5.7-inf/bin/poly Poly/ML 5.7 Release 0.00 real 0.00 user 0.00 sys rda]- echo | time

Re: [polyml] Approaching release of 5.7.1

I have just realized what is probably accounting for the delay below. I have noticed recently that there is a slight delay when exiting the poly session. echo | time poly gives 0.49 s elapsed time on my machine. After a build of ProofPower there are 262 SML files and most are processed

Re: [polyml] Approaching release of 5.7.1

David, That also fixed the issue for me. I have been using the latest commit (g44b7b88) without issue. My only observation is that there is a significant increase in the ProofPower build times: Poly/ML 5.7 real1m37.832s user1m33.262s sys 0m15.108s Poly/ML 5.7.1g44b7b88 real

Re: [polyml] Approaching release of 5.7.1

This actually looks like a weakness that libffi doesn't explicitly support Clang [0]. Swimming further upstream, this support is missing in the Autoconf Archive [1]. Whether this is worth fixing is debatable as even the GCC options in this script don't seem particularly well chosen for a modern

Re: [polyml] Approaching release of 5.7.1

On 15/11/17 09:58, David Matthews wrote: On 15/11/2017 17:10, Rob Arthan wrote: 1) On Mac OS (and presumably any system with clang as the C compiler), the configure script gives a warning. (I just let this go by and nothing seems to have gone wrong.) checking for C compiler vendor... clang

Re: [polyml] Approaching release of 5.7.1

Rob, On 15/11/2017 17:10, Rob Arthan wrote: 1) On Mac OS (and presumably any system with clang as the C compiler), the configure script gives a warning. (I just let this go by and nothing seems to have gone wrong.) checking for C compiler vendor... clang

Re: [polyml] Approaching release of 5.7.1

David, I've done my other tests and it's working fine. I have just a couple of observations. 1) On Mac OS (and presumably any system with clang as the C compiler), the configure script gives a warning. (I just let this go by and nothing seems to have gone wrong.) checking for C compiler

Re: [polyml] Approaching release of 5.7.1

Hi David, I just wanted to add that the latest git master (26c678b6) still fails to build HOL4 with the following: Fail "Exception- InternalError: codeToPRegRev raised while compiling" similar to as we have discussed on other threads. Cheers, Ramana On 14 November 2017 at 09:32, Rob Arthan

Re: [polyml] Approaching release of 5.7.1

> I'll try bumping the memory. Although the "months of not working" is not > quite correct, because it worked fine with 10 GB in 5.6. After a strange crash yesterday that didn't even print an error message [0,1] it seems we're back to normal now. I still don't quite understand why the memory

Re: [polyml] Approaching release of 5.7.1

On 08/11/17 15:49, Lars Hupel wrote: >> I've been using --minheap 3000 --maxheap 3 for that recently and it >> performs quite well (after months of not working at all). > > I'll try bumping the memory. Although the "months of not working" is not > quite correct, because it worked fine with 10

Re: [polyml] Approaching release of 5.7.1

> I've been using --minheap 3000 --maxheap 3 for that recently and it > performs quite well (after months of not working at all). I'll try bumping the memory. Although the "months of not working" is not quite correct, because it worked fine with 10 GB in 5.6.

Re: [polyml] Approaching release of 5.7.1

On 08/11/17 15:23, Lars Hupel wrote: > > since Isabelle/8905114fd23b, I'm seeing intermittent problems in the > session "Iptables_Semantics_Examples_Big": > > The relevant environment settings are: > > ML_PLATFORM="x86_64-linux" > ML_OPTIONS="-H 4000 --maxheap 10G" I've been using --minheap