On Thu, Feb 21, 2019 at 5:48 AM David Matthews
wrote:
> This is a last chance to test the current git master before release.
Sorry to be late. When running configure, I see this:
checking whether as supports .note.GNU-stack... yes
./configure: line 18046: dependentlibs: command not found
That
Thanks, everyone for the testing and feedback. I've now updated the
remaining prebuilt compilers and officially released 5.8 on GitHub.
There is a fixes-5.8 branch but that currently just reflects master.
I'm pleased that the 32-bit under 64-bit version has proved so
successful. It has invol
On 10/03/2019 20:28, Rob Arthan wrote:
>
> After the "git pull", I've rebuilt Poly/ML and ProofPower and had no problems
> with any
> combination of --enable-intinf-asint, --enable-compact32bit and MacOS v.
> Fedora.
>
> Poly/ML compiled with --enable-compact32bit gives me 5-8% improvement in
David,
After the "git pull", I've rebuilt Poly/ML and ProofPower and had no problems
with any
combination of --enable-intinf-asint, --enable-compact32bit and MacOS v. Fedora.
Poly/ML compiled with --enable-compact32bit gives me 5-8% improvement in
execution times
and 30-40% improvement in the
On 09/03/2019 21:10, Rob Arthan wrote:
OK. Is there a way of telling whether poly has been built with
--enable-compact32bit? (So you can check whether
you got what you wanted.)
> PolyML.architecture();
val it = "X86_64_32": string
> Word.wordSize;
val it = 31: int
> LargeWord.wordSize;
val it
Rob, Phil and everyone else,
I'm in the process of putting together the 5.8 release and as part of
that I've pushed an updated pre-built compiler for X64/32 for Linux, Mac
OS etc. That means that for that platform only, for the moment, it is
no longer necessary to run "make compiler", althoug
Rob,
On 09/03/19 21:10, Rob Arthan wrote:
On 9 Mar 2019, at 16:59, David Matthews wrote:
3) On MacOS with —disable-intinf-asint and —enable-compact32bit,
the ProofPower build fails like this:
Assertion failed: (space != 0), function ScanObjectAddress, file quick_gc.cpp,
line 414.
4) On Fedor
David,
Thanks. I've interleaved my replies below.
> On 9 Mar 2019, at 16:59, David Matthews
> wrote:
>
> Rob,
> Thanks for testing this and your comments. I'm replying to your individual
> comments below.
>
> On 09/03/2019 16:11, Rob Arthan wrote:
>> 1) The configure script doesn’t validate
Rob,
Thanks for testing this and your comments. I'm replying to your
individual comments below.
On 09/03/2019 16:11, Rob Arthan wrote:
1) The configure script doesn’t validate an option beginning "—enable-“.
So I didn’t notice that I’d mistyped —enable-compact32bit until I realised that
I wa
David,
I’ve been trying building and testing ProofPower on the various combinations of
MacOS Mojave v. Linux Fedora 24, —enable-compact32bit v. —disable-compact32bit
and —enable-intinf-asint and —disable-intinf-asint and have a few observations.
1) The configure script doesn’t validate an option
Hi,
Thank you for testing this but could I ask you to re-read the second
paragraph of my message. It may seem surprising but slight differences
in timing can affect exactly when the garbage-collection happens and
allow the compilation to work.
David
On 22/02/2019 11:51, Chun Tian (binghe) w
Hi David,
I'm on Mac OS X 10.11 with Xcode 8.2 (Apple LLVM 8.0) [1]. When I build
latest Poly/ML sources with "--enable-compact32bit" (no others), when I
execute "make compiler" (after "make"), with large chances I get the
following error:
...
Created functor TYPECHECK_PARSETREE
Making MATCH_COMP
The current version of Poly/ML is approaching the point of creating a
new release, 5.8. Makarius has run a lot of tests with Isabelle and
various bugs have been fixed. This has mainly affected the 32-bit
object ID version for 64-bits but some of the fixes will also have
affected the native-ad
13 matches
Mail list logo
